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 : [p:*Prop, q:*Prop] *Prop
  10
  11    \decl "logical disjunction" Or : [p:*Prop, q:*Prop] *Prop
  12
  13    \decl "logical implication" Imp : [p:*Prop, q:*Prop] *Prop
  14
  15    \decl "logical comprehension" All : [p:[x:*Set]*Prop] *Prop
  16
  17    \decl "logical existence" Ex : [p:[x:*Set]*Prop] *Prop
  18
  19    \decl "syntactical identity" Id : [x:*Set, y:*Set] *Prop
  20
  21    \decl "rule application" App : [f:*Set, x:*Set, y:*Set] *Prop
  22
  23    \decl "classification predicate" Cl : [a:*Set] *Prop
  24
  25    \decl "classification membership" Eta : [x:*Set, a:*Set] *Prop
  26
  27    \decl "object-to-term-coercion" T : [x:*Set] *Term
  28
  29    \decl "term application" At : [t:*Term, u:*Term] *Term
  30
  31    \decl "term-object equivalence" E : [t:*Term, x:*Set] *Prop
  32
  33 \close
  34
  35 \open non_logical_axioms
  36
  37    \decl "E: reflexivity" e_refl : [x:*Set] E(T(x), x)
  38
  39 \close