The Logic Book, M.Bergmann, J.Moor, J.Nelson, McGraw Hill, 4th edition, problem 10.6E 3b

We are asked to show that the following is a theorem in PDE, the extended predicate derivation system.

(x)(y)(x = x ∨y = y)



I proceed by assuming the negation of the formula, marking the scope of the assumption as I go along. Lines 7 and 8 show contradictions, so the assumption is discharged and shown not to be true (double negation), which reduces to the theorem we were seeking to prove.

1. * ¬ (x)(y)(x = x ∨y = y) / AIP
2. * (∃x) ¬ (y)(x = x ∨y = y) / 1, CQ
3. * (∃x)(∃y) ¬ (x = x ∨y = y) / 2, CQ
4. * (∃y) ¬ (a = a ∨y = y) / 3, EI x/a
5. * ¬ (a = a ∨b = b) / 4, EI y/b
6. * ¬ (a = a) • ¬ (b = b) / 5, DeM
7. * ¬ (a = a) / 6, Simp.
8. * ¬ (b = b) / 7, Simp.
9. ¬ ¬ (x)(y)(x = x ∨y = y) / 1- 7(8) IP
10. (x)(y)(x = x ∨y = y) / 9, DN