Uses the following modules:
A simple implication:
1. Proposition
(" x (R(x)) Þ $ x (R(x))) (predtheo1)
1 | (" x (R(x)) Þ R(y)) | add axiom axiom5 |
2 | (R(y) Þ $ x (R(x))) | add axiom axiom6 |
3 | (" x (R(x)) Þ $ x (R(x))) | hypothetical syllogism with 1 and 2 |
qed |
A well known implication:
2. Proposition
($ x (R(x)) Þ Ø" x (ØR(x))) (predtheo2)
1 | (" x (R(x)) Þ R(y)) | add axiom axiom5 |
2 | (" x (ØR(x)) Þ ØR(y)) | replace predicate variable R(@S1) by ØR(@S1) 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 |
The reverse is also true:
3. Proposition
(Ø" x (ØR(x)) Þ $ x (R(x))) (predtheo3)
1 | (R(y) Þ $ x (R(x))) | add axiom axiom6 |
2 | (Ø$ x (R(x)) Þ ØR(y)) | apply proposition hilb7 in 1 |
3 | (Ø$ x (R(x)) Þ " y (ØR(y))) | generalization by y in 2 |
4 | (Ø" y (ØR(y)) Þ ØØ$ x (R(x))) | apply proposition hilb7 in 3 |
5 | (Ø" y (ØR(y)) Þ $ x (R(x))) | elementary equivalence in 4 at 1 of hilb6 with hilb5 |
6 | (Ø" x (ØR(x)) Þ $ x (R(x))) | rename bound variable y into x in 5 at occurence 1 |
qed |
Exchange of universal quantors:
4. Proposition
(" x (" y (R(x, y))) Þ " y (" x (R(x, y)))) (predtheo4)
1 | (" x (R(x)) Þ R(y)) | add axiom axiom5 |
2 | (" y (R(y)) Þ R(u)) | substitute variables in 1 |
3 | (" y (R(z, y)) Þ R(z, u)) | replace predicate variable R(@S1) by R(z, @S1) in 2 |
4 | (" v (R(v)) Þ R(z)) | substitute variables in 1 |
5 | (" v (" w (R(v, w))) Þ " w (R(z, w))) | replace predicate variable R(@S1) by " w (R(@S1, w)) in 4 |
6 | (" x (" y (R(x, y))) Þ " y (R(z, y))) | substitute variables in 5 |
7 | (" x (" y (R(x, y))) Þ R(z, u)) | hypothetical syllogism with 6 and 3 |
8 | (" x (" y (R(x, y))) Þ " z (R(z, u))) | generalization by z in 7 |
9 | (" x (" y (R(x, y))) Þ " u (" z (R(z, u)))) | generalization by u in 8 |
10 | (" x (" y (R(x, y))) Þ " y (" z (R(z, y)))) | rename bound variable u into y in 9 at occurence 1 |
11 | (" x (" y (R(x, y))) Þ " y (" x (R(x, y)))) | rename bound variable z into x in 10 at occurence 1 |
qed |
Implication of changing seqence of existence and universal quantor:
5. Proposition
($ x (" y (R(x, y))) Þ " y ($ x (R(x, y)))) (predtheo5)
1 | (" x (R(x)) Þ R(y)) | add axiom axiom5 |
2 | (" y (R(y)) Þ R(u)) | substitute variables in 1 |
3 | (" y (R(x, y)) Þ R(x, u)) | replace predicate variable R(@S1) by R(x, @S1) in 2 |
4 | (R(y) Þ $ x (R(x))) | add axiom axiom6 |
5 | (R(x) Þ $ z (R(z))) | substitute variables in 4 |
6 | (R(x, u) Þ $ z (R(z, u))) | replace predicate variable R(@S1) by R(@S1, u) in 5 |
7 | (" y (R(x, y)) Þ $ z (R(z, u))) | hypothetical syllogism with 3 and 6 |
8 | ($ x (" y (R(x, y))) Þ $ z (R(z, u))) | particularization by x in 7 |
9 | ($ x (" y (R(x, y))) Þ " u ($ z (R(z, u)))) | generalization by u in 8 |
10 | ($ x (" y (R(x, y))) Þ " y ($ x (R(x, y)))) | substitute variables in 9 |
qed |