|
Theorems |
AND_DEF : (/\) = (\p q. (\f. f p q) = (\f. f T T))COND_DEF : COND = (\t t1 t2. @x. ((t <=> T) ==> x = t1) /\ ((t <=> F) ==> x = t2))EXISTS_DEF : (?) = (\p. !q. (!x. p x ==> q) ==> q)EXISTS_UNIQUE_DEF : (?!) = (\p. (?) p /\ (!x y. p x /\ p y ==> x = y))FORALL_DEF : (!) = (\p. p = (\x. T))F_DEF : F <=> (!p. p)IMP_DEF : (==>) = (\p q. p /\ q <=> p)NOT_DEF : (~) = (\p. p ==> F)OR_DEF : (\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r)T_DEF : T <=> (\p. p) = (\p. p) |
