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

   1 \graph Z3
   2
   3 \sorts Prop, Set, Term
   4
   5 \open syntax \* [1] 2.1. *\
   6
   7    \decl "logical false" False: *Prop
   8
   9    \decl "logical conjunction" And: *Prop => *Prop -> *Prop
  10
  11    \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
  12
  13    \decl "logical implication" Imp: *Prop => *Prop -> *Prop
  14
  15    \decl "logical comprehension" All: [~:*Set->*Prop] *Prop
  16
  17    \decl "logical existence" Ex: [~:*Set->*Prop] *Prop
  18
  19    \decl "syntactical identity" Id: *Set => *Set -> *Prop
  20
  21    \decl "rule application" App: *Set => *Set => *Set -> *Prop
  22
  23    \decl "classification predicate" Cl: *Set -> *Prop
  24
  25    \decl "classification membership" Eta: *Set => *Set -> *Prop
  26
  27    \decl "object-to-term-coercion" T: *Set -> *Term
  28
  29    \decl "term application" At: *Term => *Term -> *Term
  30
  31    \decl "term-object equivalence" E: *Term => *Set -> *Prop
  32
  33 \close
  34
  35 \open non_logical_axioms
  36
  37    \ax e_refl: [x:*Set] E(T(x), x)
  38
  39    \ax e_at_in: [f:*Set][x:*Set][y:*Set] App(f,x,y) -> E(At(T(f), T(x)), y)
  40
  41    \ax e_at_out: [f:*Set][x:*Set][y:*Set] E(At(T(f), T(x)), y) -> App(f,x,y)
  42
  43 \close