3 \* Intuitionistic Predicate Logic with Equality *\
5 \open elements \* [1] 2.1. 2.2. 3.1 *\
7 \decl "logical false" False: *Prop
9 \decl "logical conjunction" And: *Prop => *Prop -> *Prop
11 \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
13 \* implication and non-dependent abstraction are isomorphic *\
14 \def "logical implication"
15 Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
17 \* comprehension and dependent abstraction are isomorphic *\
18 \def "unrestricted logical comprehension"
19 All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
21 \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
23 \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
27 \open abbreviations \* [1] 2.3. *\
29 \def "logical negation"
30 Not = [p:*Prop] p -> False : *Prop -> *Prop
32 \def "logical equivalence"
33 Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
35 \def "unrestricted strict logical existence"
36 EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
37 : (*Obj -> *Prop) -> *Prop
39 \def "negated syntactical identity"
40 NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop