helm/software/lambda-delta/examples/exp_math/T0.hln

   1 \require L
   2
   3 \* Feferman's system T0 *\
   4
   5 \open elements \* [1] 2.1. 2.2. 2.4. *\
   6
   7    \decl "rule application" App: *Obj => *Obj => *Obj -> *Prop
   8
   9    \decl "classification predicate" Cl: *Obj -> *Prop
  10
  11    \decl "classification membership" Eta: *Obj => *Obj -> *Prop
  12
  13 \* we must make an explicit coercion from *Obj to *Term *\
  14    \decl "object-to-term-coercion" T: *Obj -> *Term
  15
  16    \decl "term application" At: *Term => *Term -> *Term
  17
  18    \decl "term-object equivalence" E: *Term => *Obj -> *Prop
  19
  20 \close
  21
  22 \open logical_abbreviations \* [1] 2.3. 2.5. *\
  23
  24    \def "logical comprehension restricted to classifications"
  25       CAll = [q:*Obj->*Prop] [x:*Obj] Cl(x) -> q(x)
  26            : (*Obj -> *Prop) -> *Prop
  27
  28    \def "logical existence restricted to classifications"
  29       CEx = [q:*Obj->*Prop] Ex([x:*Obj] And(Cl(x), q(x)))
  30           : (*Obj -> *Prop) -> *Prop
  31
  32    \def "logical comprehension restricted to a classification"
  33       EAll = [a:*Obj, q:*Obj->*Prop] [x:*Obj] Eta(x, a) -> q(x)
  34            : *Obj => (*Obj -> *Prop) -> *Prop
  35
  36    \def "logical existence restricted to a classification"
  37       EEx = [a:*Obj, q:*Obj->*Prop] Ex([x:*Obj] And(Eta(x, a), q(x)))
  38           : *Obj => (*Obj -> *Prop) -> *Prop
  39
  40 \close
  41
  42 \open non_logical_abbreviations \* [1] 2.4. *\
  43
  44    \def "convergence of a term to an object"
  45       Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
  46
  47    \def "term-term equivalence"
  48       Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
  49          : *Term => *Term -> *Prop
  50
  51 \close
  52
  53 \open non_logical_axioms \* [1] 2.4. *\
  54
  55 \* we axiomatize E because *Term is not inductively generated *\
  56    \ax e_refl: [y:*Obj] E(T(y), y)
  57 \*
  58    \ax e_at_in: [f:*Obj][x:*Obj][y:*Obj] App(f,x,y) -> E(At(T(f), T(x)), y)
  59
  60    \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y)
  61 *\
  62 \close