helm/software/helena/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]^1 *Prop] All([x:*Obj]^2 Imp(Cl(x), q(x)))
  26            : [[*Obj]^1 *Prop] *Prop
  27
  28    \def "logical existence restricted to classifications"
  29       CEx = [q:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(Cl(x), q(x)))
  30           : [[*Obj]^1 *Prop] *Prop
  31
  32    \def "logical comprehension restricted to a classification"
  33       EAll = { [a:*Obj] [q:[*Obj]^1 *Prop] } All([x:*Obj]^2 Imp(Eta(x, a), q(x)))
  34            : { [*Obj] [[*Obj]^1 *Prop] } *Prop
  35
  36    \def "logical existence restricted to a classification"
  37       EEx = { [a:*Obj] [q:[*Obj]^1 *Prop] } Ex([x:*Obj]^2 And(Eta(x, a), q(x)))
  38           : { [*Obj] [[*Obj]^1 *Prop] } *Prop
  39
  40 \close
  41
  42 \open non_logical_abbreviations \* [1] 2.4. 2.7 *\
  43
  44    \def "object application"
  45       OAt = { [f:*Obj] [x:*Obj] } At(T(f), T(x)) : { [*Obj] [*Obj] } *Term
  46
  47    \def "convergence of a term to an object"
  48       Conv = [t:*Term] EX([y:*Obj]^2 E(t, y)) : [*Term] *Prop
  49
  50    \def "term-term equivalence"
  51       Eq = { [t1:*Term] [t2:*Term] } All([y:*Obj]^2 Iff(E(t1, y), E(t2, y)))
  52          : { [*Term] [*Term] } *Prop
  53
  54    \def "classification membership of a term"
  55       TEta = { [t:*Term] [a:*Obj] } EEx(a, [y:*Obj]^2 E(t, y))
  56            : { [*Term] [*Obj] } *Prop
  57
  58    \def "operation (rule with inhabited domain)"
  59       Op = [f:*Obj] Ex([x:*Obj]^2 Conv(OAt(f, x))) : [*Obj] *Prop
  60
  61    \def "classification inclusion"
  62       ESub = { [a1:*Obj] [a2:*Obj] } EAll(a1, [x:*Obj]^2 Eta(x, a2))
  63            : { [*Obj] [*Obj] } *Prop
  64
  65     \def "classification morphism"
  66       ETo = { [f:*Obj] [a:*Obj] [ b:*Obj] } EAll(a, [x:*Obj]^2 TEta(OAt(f, x), b))
  67           : { [*Obj] [*Obj] [*Obj] } *Prop
  68
  69 \close
  70
  71 \open non_logical_axioms \* [1] 2.4. 3.2 *\
  72
  73 \* we axiomatize E because *Term is not inductively generated *\
  74    \ax e_refl: [y:*Obj] E(T(y), y)
  75
  76    \ax e_at_in: [t1:*Term][t2:*Term][f:*Obj][x:*Obj][y:*Obj]
  77                 [E(t1, f)] [E(t2, x)] [App(f, x, y)] E(At(t1, t2), y)
  78 \*
  79    \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] [E(At(T(f), T(x)), y)] App(f, x, y)
  80 *\
  81    \ax "I (i)" id_dec: [x:*Obj][y:*Obj] Or(Id(x, y), NId(x, y))
  82
  83    \ax "I (ii)" at_mono: [f:*Obj][x:*Obj][y1:*Obj][y2:*Obj]
  84                          [E(OAt(f, x), y1)] [E(OAt(f, x), y2)] Id(y1, y2)
  85
  86    \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] [Eta(x, a)] Cl(a)
  87
  88 \close