A Model Proof in Logic A Model Proof in Logic E

This is a proof of
|- (p p) false
which is (3.15) where P is p. Typically, (3.1) and (3.1) are used transparently. In this proof, detail concerning their use is explictly given.
(p p) false
=


(3.8) and Leibniz where E is (p p) r
gives |- ((p p) false) ((p p) true).


(p p) true
=


(3.2) where P is p and Q is p and Leibniz where E is r true
gives |- ((p p) true) ((p p) true).


(p p) true
=

(3.1) where P is p, Q is p, and R is true.

p (p true )
=


(3.11) where P is p and Q is true and Leibniz where E is p r
gives |- (p (p true)) (p (p true)).


p (p true)
=


(3.12) where P is true and Leibniz where E is p (p r)
gives |- (p (p true)) ( p (p true)).


p (p true)
=

(3.1) where P is p, Q is p and R is true.

(p p) true
=


(3.3) where P is p and Leibniz where E is (p p ) r
gives |- ( (p p) true) ((p p)      (p p) ).


(p p)      (p p)  .
Transitivity applied four times gives
|- ((p p) false)         ((p p)      (p p)) .
But (3.5) where P is p p gives |- (p p)      (p p) . By Equanimity,
|- p p false  .
Note that the use of Transitivity four times and Equanimity once can be replaced by the use of Equanimity five times.
Note that (3.1) is the Axiom Scheme
|-  (P (Q R))      ((P Q) R)  .


File translated from TEX by TTH, version 2.60.
On 26 Sep 2000, 20:54.