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

   1 \require preamble
   2
   3 \* Intuitionistic Predicate Logic with Equality *\
   4
   5 \open elements \* [1] 2.1. 2.2. *\
   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 \* implication and non-dependent abstraction are isomorphic *\
  14    \def "logical implication"
  15       Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
  16
  17    \decl "logical comprehension" All: (*Obj -> *Prop) -> *Prop
  18
  19    \decl "logical existence" Ex: (*Obj -> *Prop) -> *Prop
  20
  21    \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
  22
  23 \close
  24
  25 \open abbreviations \* [1] 2.3. *\
  26
  27    \def "logical negation"
  28       Not = [p:*Prop] p -> False : *Prop -> *Prop
  29
  30    \def "logical equivalence"
  31       Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
  32
  33    \def "logical strict existence"
  34       EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
  35          : (*Obj -> *Prop) -> *Prop
  36
  37    \def "negated syntactical identity"
  38       NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop
  39
  40 \close