Description
This module includes first proofs of predicate calculus theorems.
Uses the following modules:
First we prove a simple implication:
Proposition 1
($ x (R(x)) Þ Ø" x (ØR(x))) (theo1)
1 | (" x (R(x)) Þ R(y)) | add axiom axiom5 |
2 | (" x (ØR(x)) Þ ØR(y)) | replace predicate variable R(@1) by ØR(@1) in 1 |
3 | (Ø" x (ØR(x)) Ú ØR(y)) | use abbreviation impl in 2 at occurence 1 |
4 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
5 | ((Ø" x (ØR(x)) Ú Q) Þ (Q Ú Ø" x (ØR(x)))) | replace proposition variable P by Ø" x (ØR(x)) in 4 |
6 | ((Ø" x (ØR(x)) Ú ØR(y)) Þ (ØR(y) Ú Ø" x (ØR(x)))) | replace proposition variable Q by ØR(y) in 5 |
7 | (ØR(y) Ú Ø" x (ØR(x))) | modus ponens with 3, 6 |
8 | (R(y) Þ Ø" x (ØR(x))) | reverse abbreviation impl in 7 at occurence 1 |
9 | ($ y (R(y)) Þ Ø" x (ØR(x))) | particularization by y in 8 |
10 | ($ x (R(x)) Þ Ø" x (ØR(x))) | rename bound variable y into x in 9 at occurence 1 |
qed |