\decl "logical false" False: *Prop
- \decl "logical conjunction" And: *Prop => *Prop -> *Prop
+ \decl "logical conjunction" And: { [*Prop] [*Prop] } *Prop
- \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
+ \decl "logical disjunction" Or: { [*Prop] [*Prop] } *Prop
\* implication and non-dependent abstraction are isomorphic *\
\def "logical implication"
- Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
+ Imp = { [p:*Prop] [q:*Prop] } [p]^1 q : { [*Prop] [*Prop] } *Prop
\* comprehension and dependent abstraction are isomorphic *\
\def "unrestricted logical comprehension"
- All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
+ All = [q:[*Obj]^1 *Prop] [x:*Obj]^1 q(x) : [[*Obj]^1 *Prop] *Prop
- \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
+ \decl "unrestricted logical existence" Ex: [[*Obj]^1 *Prop] *Prop
- \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
+ \decl "syntactical identity" Id: { [*Obj] [*Obj] } *Prop
\close
\open abbreviations \* [1] 2.3. *\
\def "logical negation"
- Not = [p:*Prop] p -> False : *Prop -> *Prop
+ Not = [p:*Prop] Imp(p, False) : [*Prop] *Prop
\def "logical equivalence"
- Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
+ Iff = { [p:*Prop] [q:*Prop] } And(Imp(p, q), Imp(q, p)) : { [*Prop] [*Prop] } *Prop
\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
+ EX = [p:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(p(x), All([y:*Obj]^2 Imp(p(y), Id(x, y)))))
+ : [[*Obj]^1 *Prop] *Prop
\def "negated syntactical identity"
- NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop
+ NId = { [x:*Obj] [y:*Obj] } Not(Id(x, y)) : { [*Obj] [*Obj] } *Prop
\close