-\graph Z3
+\require preamble
-\sorts Prop, Set, Term
+\* Intuitionistic Predicate Logic with Equality *\
-\open syntax \* [1] 2.1. *\
+\open elements \* [1] 2.1. 2.2. 3.1 *\
- \decl "logical false" False : *Prop
+ \decl "logical false" False: *Prop
- \decl "logical conjunction" And : [p:*Prop, q:*Prop] *Prop
+ \decl "logical conjunction" And: *Prop => *Prop -> *Prop
- \decl "logical disjunction" Or : [p:*Prop, q:*Prop] *Prop
+ \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
- \decl "logical implication" Imp : [p:*Prop, q:*Prop] *Prop
+\* implication and non-dependent abstraction are isomorphic *\
+ \def "logical implication"
+ Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
- \decl "logical comprehension" All : [p:[x:*Set]*Prop] *Prop
+\* comprehension and dependent abstraction are isomorphic *\
+ \def "unrestricted logical comprehension"
+ All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
- \decl "logical existence" Ex : [p:[x:*Set]*Prop] *Prop
+ \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
- \decl "syntactical identity" Id : [x:*Set, y:*Set] *Prop
+ \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
- \decl "rule application" App : [f:*Set, x:*Set, y:*Set] *Prop
-
- \decl "classification predicate" Cl : [a:*Set] *Prop
-
- \decl "classification membership" Eta : [x:*Set, a:*Set] *Prop
-
- \decl "object-to-term-coercion" T : [x:*Set] *Term
+\close
- \decl "term application" At : [t:*Term, u:*Term] *Term
+\open abbreviations \* [1] 2.3. *\
- \decl "term-object equivalence" E : [t:*Term, x:*Set] *Prop
+ \def "logical negation"
+ Not = [p:*Prop] p -> False : *Prop -> *Prop
-\close
+ \def "logical equivalence"
+ Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
-\open non_logical_axioms
+ \def "unrestricted strict logical existence"
+ EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
+ : (*Obj -> *Prop) -> *Prop
- \decl "E: reflexivity" e_refl : [x:*Set] E(T(x), x)
+ \def "negated syntactical identity"
+ NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop
\close