bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. __=__ = __<=>__
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maedervars p, q: Logical
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. p /\ q = p res q
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. (p => q) = ((\ . p) =e= \ . p /\ q)
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. (p <=> q) = ((p => q) /\ (q => p))
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maedervars t : Type; pr : Pred t
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. (forall y : t . pr y) = ((\ y : t . pr y) =e= \ y : t . true)
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. false = forall a : Logical . a()
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. not p <=> p => false
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. p \/ q <=> forall a : Logical . (p => a()) /\ (q => a()) => a()
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. (exists y : t . pr y) = forall a : Logical
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder . (forall y : t . pr y => a()) => a()
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. a = b <=> (def a => a =e= b) /\ (def b => def a)
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maederop choose : Pred t ->? t
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. choose pr = a <=> forall y : t . pr y <=> a = y
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maederop epsilon : Pred t -> t
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. (exists x : t . pr x) => pr(epsilon pr)
bb5f80fa01a1783a3e84ced6fa4c4c1a74da211dChristian Maeder. p \/ not p %implied