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 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
4 | ((B Þ Q) Þ ((A Þ B) Þ (A Þ Q))) | replace proposition variable P by B in 3 |
5 | ((B Þ C) Þ ((A Þ B) Þ (A Þ C))) | replace proposition variable Q by C in 4 |
6 | ((B Þ C) Þ ((D Þ B) Þ (D Þ C))) | replace proposition variable A by D in 5 |
7 | ((R(y) Þ C) Þ ((D Þ R(y)) Þ (D Þ C))) | replace proposition variable B by R(y) in 6 |
8 | ((R(y) Þ $ x (R(x))) Þ ((D Þ R(y)) Þ (D Þ $ x (R(x))))) | replace proposition variable C by $ x (R(x)) in 7 |
9 | ((R(y) Þ $ x (R(x))) Þ ((" x (R(x)) Þ R(y)) Þ (" x (R(x)) Þ $ x (R(x))))) | replace proposition variable D by " x (R(x)) in 8 |
10 | ((" x (R(x)) Þ R(y)) Þ (" x (R(x)) Þ $ x (R(x)))) | modus ponens with 2, 9 |
11 | (" x (R(x)) Þ $ x (R(x))) | modus ponens with 1, 10 |
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 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
3 | ((A Þ Q) Þ (ØQ Þ ØA)) | replace proposition variable P by A in 2 |
4 | ((A Þ B) Þ (ØB Þ ØA)) | replace proposition variable Q by B in 3 |
5 | ((R(y) Þ B) Þ (ØB Þ ØR(y))) | replace proposition variable A by R(y) in 4 |
6 | ((R(y) Þ $ x (R(x))) Þ (Ø$ x (R(x)) Þ ØR(y))) | replace proposition variable B by $ x (R(x)) in 5 |
7 | (Ø$ x (R(x)) Þ ØR(y)) | modus ponens with 1, 6 |
8 | (Ø$ x (R(x)) Þ " y (ØR(y))) | generalization by y in 7 |
9 | ((Ø$ x (R(x)) Þ B) Þ (ØB Þ ØØ$ x (R(x)))) | replace proposition variable A by Ø$ x (R(x)) in 4 |
10 | ((Ø$ x (R(x)) Þ " y (ØR(y))) Þ (Ø" y (ØR(y)) Þ ØØ$ x (R(x)))) | replace proposition variable B by " y (ØR(y)) in 9 |
11 | (Ø" y (ØR(y)) Þ ØØ$ x (R(x))) | modus ponens with 8, 10 |
12 | (ØØP Þ P) | add proposition hilb6 |
13 | (ØØQ Þ Q) | replace proposition variable P by Q in 12 |
14 | (ØØ$ x (R(x)) Þ $ x (R(x))) | replace proposition variable Q by $ x (R(x)) in 13 |
15 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
16 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
17 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
18 | ((B Þ Q) Þ ((A Ú B) Þ (A Ú Q))) | replace proposition variable P by B in 17 |
19 | ((B Þ C) Þ ((A Ú B) Þ (A Ú C))) | replace proposition variable Q by C in 18 |
20 | ((B Þ C) Þ ((D Ú B) Þ (D Ú C))) | replace proposition variable A by D in 19 |
21 | ((ØØ$ x (R(x)) Þ C) Þ ((D Ú ØØ$ x (R(x))) Þ (D Ú C))) | replace proposition variable B by ØØ$ x (R(x)) in 20 |
22 | ((ØØ$ x (R(x)) Þ $ x (R(x))) Þ ((D Ú ØØ$ x (R(x))) Þ (D Ú $ x (R(x))))) | replace proposition variable C by $ x (R(x)) in 21 |
23 | ((ØØ$ x (R(x)) Þ $ x (R(x))) Þ ((ØØ" y (ØR(y)) Ú ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x))))) | replace proposition variable D by ØØ" y (ØR(y)) in 22 |
24 | ((ØØ" y (ØR(y)) Ú ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) | modus ponens with 14, 23 |
25 | ((A Þ Q) Þ (ØA Ú Q)) | replace proposition variable P by A in 15 |
26 | ((A Þ B) Þ (ØA Ú B)) | replace proposition variable Q by B in 25 |
27 | ((Ø" y (ØR(y)) Þ B) Þ (ØØ" y (ØR(y)) Ú B)) | replace proposition variable A by Ø" y (ØR(y)) in 26 |
28 | ((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú ØØ$ x (R(x)))) | replace proposition variable B by ØØ$ x (R(x)) in 27 |
29 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
30 | ((B Þ Q) Þ ((A Þ B) Þ (A Þ Q))) | replace proposition variable P by B in 29 |
31 | ((B Þ C) Þ ((A Þ B) Þ (A Þ C))) | replace proposition variable Q by C in 30 |
32 | ((B Þ C) Þ ((D Þ B) Þ (D Þ C))) | replace proposition variable A by D in 31 |
33 | (((ØØ" y (ØR(y)) Ú ØØ$ x (R(x))) Þ C) Þ ((D Þ (ØØ" y (ØR(y)) Ú ØØ$ x (R(x)))) Þ (D Þ C))) | replace proposition variable B by (ØØ" y (ØR(y)) Ú ØØ$ x (R(x))) in 32 |
34 | (((ØØ" y (ØR(y)) Ú ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) Þ ((D Þ (ØØ" y (ØR(y)) Ú ØØ$ x (R(x)))) Þ (D Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))))) | replace proposition variable C by (ØØ" y (ØR(y)) Ú $ x (R(x))) in 33 |
35 | (((ØØ" y (ØR(y)) Ú ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) Þ (((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú ØØ$ x (R(x)))) Þ ((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))))) | replace proposition variable D by (Ø" y (ØR(y)) Þ ØØ$ x (R(x))) in 34 |
36 | (((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú ØØ$ x (R(x)))) Þ ((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x))))) | modus ponens with 24, 35 |
37 | ((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) | modus ponens with 28, 36 |
38 | ((ØA Ú Q) Þ (A Þ Q)) | replace proposition variable P by A in 16 |
39 | ((ØA Ú B) Þ (A Þ B)) | replace proposition variable Q by B in 38 |
40 | ((ØØ" y (ØR(y)) Ú B) Þ (Ø" y (ØR(y)) Þ B)) | replace proposition variable A by Ø" y (ØR(y)) in 39 |
41 | ((ØØ" y (ØR(y)) Ú $ x (R(x))) Þ (Ø" y (ØR(y)) Þ $ x (R(x)))) | replace proposition variable B by $ x (R(x)) in 40 |
42 | (((ØØ" y (ØR(y)) Ú $ x (R(x))) Þ C) Þ ((D Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) Þ (D Þ C))) | replace proposition variable B by (ØØ" y (ØR(y)) Ú $ x (R(x))) in 32 |
43 | (((ØØ" y (ØR(y)) Ú $ x (R(x))) Þ (Ø" y (ØR(y)) Þ $ x (R(x)))) Þ ((D Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) Þ (D Þ (Ø" y (ØR(y)) Þ $ x (R(x)))))) | replace proposition variable C by (Ø" y (ØR(y)) Þ $ x (R(x))) in 42 |
44 | (((ØØ" y (ØR(y)) Ú $ x (R(x))) Þ (Ø" y (ØR(y)) Þ $ x (R(x)))) Þ (((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) Þ ((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (Ø" y (ØR(y)) Þ $ x (R(x)))))) | replace proposition variable D by (Ø" y (ØR(y)) Þ ØØ$ x (R(x))) in 43 |
45 | (((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (ØØ" y (ØR(y)) Ú $ x (R(x)))) Þ ((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (Ø" y (ØR(y)) Þ $ x (R(x))))) | modus ponens with 41, 44 |
46 | ((Ø" y (ØR(y)) Þ ØØ$ x (R(x))) Þ (Ø" y (ØR(y)) Þ $ x (R(x)))) | modus ponens with 37, 45 |
47 | (Ø" y (ØR(y)) Þ $ x (R(x))) | modus ponens with 11, 46 |
48 | (Ø" x (ØR(x)) Þ $ x (R(x))) | rename bound variable y into x in 47 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 | (" x (R(x)) Þ R(w)) | rename free variable y into w in 1 |
3 | (" r (R(r)) Þ R(w)) | rename bound variable x into r in 2 at occurence 1 |
4 | (" r (R(r)) Þ R(u)) | rename free variable w into u in 3 |
5 | (" y (R(y)) Þ R(u)) | rename bound variable r into y in 4 at occurence 1 |
6 | (" y (R(z, y)) Þ R(z, u)) | replace predicate variable R(@S1) by R(z, @S1) in 5 |
7 | (" x (R(x)) Þ R(r)) | rename free variable y into r in 1 |
8 | (" s (R(s)) Þ R(r)) | rename bound variable x into s in 7 at occurence 1 |
9 | (" s (R(s)) Þ R(z)) | rename free variable r into z in 8 |
10 | (" v (R(v)) Þ R(z)) | rename bound variable s into v in 9 at occurence 1 |
11 | (" v (" w (R(v, w))) Þ " w (R(z, w))) | replace predicate variable R(@S1) by " w (R(@S1, w)) in 10 |
12 | (" c (" w (R(c, w))) Þ " w (R(z, w))) | rename bound variable v into c in 11 at occurence 1 |
13 | (" c (" d (R(c, d))) Þ " w (R(z, w))) | rename bound variable w into d in 12 at occurence 1 |
14 | (" c (" d (R(c, d))) Þ " x14 (R(z, x14))) | rename bound variable w into x14 in 13 at occurence 1 |
15 | (" x (" d (R(x, d))) Þ " x14 (R(z, x14))) | rename bound variable c into x in 14 at occurence 1 |
16 | (" x (" y (R(x, y))) Þ " x14 (R(z, x14))) | rename bound variable d into y in 15 at occurence 1 |
17 | (" x (" y (R(x, y))) Þ " y (R(z, y))) | rename bound variable x14 into y in 16 at occurence 1 |
18 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
19 | ((C Þ Q) Þ ((A Þ C) Þ (A Þ Q))) | replace proposition variable P by C in 18 |
20 | ((C Þ D) Þ ((A Þ C) Þ (A Þ D))) | replace proposition variable Q by D in 19 |
21 | ((C Þ D) Þ ((P7 Þ C) Þ (P7 Þ D))) | replace proposition variable A by P7 in 20 |
22 | ((" y (R(z, y)) Þ D) Þ ((P7 Þ " y (R(z, y))) Þ (P7 Þ D))) | replace proposition variable C by " y (R(z, y)) in 21 |
23 | ((" y (R(z, y)) Þ R(z, u)) Þ ((P7 Þ " y (R(z, y))) Þ (P7 Þ R(z, u)))) | replace proposition variable D by R(z, u) in 22 |
24 | ((" y (R(z, y)) Þ R(z, u)) Þ ((" x (" y (R(x, y))) Þ " y (R(z, y))) Þ (" x (" y (R(x, y))) Þ R(z, u)))) | replace proposition variable P7 by " x (" y (R(x, y))) in 23 |
25 | ((" x (" y (R(x, y))) Þ " y (R(z, y))) Þ (" x (" y (R(x, y))) Þ R(z, u))) | modus ponens with 6, 24 |
26 | (" x (" y (R(x, y))) Þ R(z, u)) | modus ponens with 17, 25 |
27 | (" x (" y (R(x, y))) Þ " z (R(z, u))) | generalization by z in 26 |
28 | (" x (" y (R(x, y))) Þ " u (" z (R(z, u)))) | generalization by u in 27 |
29 | (" x (" y (R(x, y))) Þ " y (" z (R(z, y)))) | rename bound variable u into y in 28 at occurence 1 |
30 | (" x (" y (R(x, y))) Þ " y (" x (R(x, y)))) | rename bound variable z into x in 29 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 | (" x (R(x)) Þ R(w)) | rename free variable y into w in 1 |
3 | (" r (R(r)) Þ R(w)) | rename bound variable x into r in 2 at occurence 1 |
4 | (" r (R(r)) Þ R(u)) | rename free variable w into u in 3 |
5 | (" y (R(y)) Þ R(u)) | rename bound variable r into y in 4 at occurence 1 |
6 | (" y (R(x, y)) Þ R(x, u)) | replace predicate variable R(@S1) by R(x, @S1) in 5 |
7 | (R(y) Þ $ x (R(x))) | add axiom axiom6 |
8 | (R(v) Þ $ x (R(x))) | rename free variable y into v in 7 |
9 | (R(v) Þ $ w (R(w))) | rename bound variable x into w in 8 at occurence 1 |
10 | (R(x) Þ $ w (R(w))) | rename free variable v into x in 9 |
11 | (R(x) Þ $ z (R(z))) | rename bound variable w into z in 10 at occurence 1 |
12 | (R(x, u) Þ $ z (R(z, u))) | replace predicate variable R(@S1) by R(@S1, u) in 11 |
13 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
14 | ((C Þ Q) Þ ((A Þ C) Þ (A Þ Q))) | replace proposition variable P by C in 13 |
15 | ((C Þ D) Þ ((A Þ C) Þ (A Þ D))) | replace proposition variable Q by D in 14 |
16 | ((C Þ D) Þ ((P7 Þ C) Þ (P7 Þ D))) | replace proposition variable A by P7 in 15 |
17 | ((R(x, u) Þ D) Þ ((P7 Þ R(x, u)) Þ (P7 Þ D))) | replace proposition variable C by R(x, u) in 16 |
18 | ((R(x, u) Þ $ z (R(z, u))) Þ ((P7 Þ R(x, u)) Þ (P7 Þ $ z (R(z, u))))) | replace proposition variable D by $ z (R(z, u)) in 17 |
19 | ((R(x, u) Þ $ z (R(z, u))) Þ ((" y (R(x, y)) Þ R(x, u)) Þ (" y (R(x, y)) Þ $ z (R(z, u))))) | replace proposition variable P7 by " y (R(x, y)) in 18 |
20 | ((" y (R(x, y)) Þ R(x, u)) Þ (" y (R(x, y)) Þ $ z (R(z, u)))) | modus ponens with 12, 19 |
21 | (" y (R(x, y)) Þ $ z (R(z, u))) | modus ponens with 6, 20 |
22 | ($ x (" y (R(x, y))) Þ $ z (R(z, u))) | particularization by x in 21 |
23 | ($ x (" y (R(x, y))) Þ " u ($ z (R(z, u)))) | generalization by u in 22 |
24 | ($ x (" y (R(x, y))) Þ " c ($ z (R(z, c)))) | rename bound variable u into c in 23 at occurence 1 |
25 | ($ x (" y (R(x, y))) Þ " c ($ d (R(d, c)))) | rename bound variable z into d in 24 at occurence 1 |
26 | ($ x (" y (R(x, y))) Þ " y ($ d (R(d, y)))) | rename bound variable c into y in 25 at occurence 1 |
27 | ($ x (" y (R(x, y))) Þ " y ($ x (R(x, y)))) | rename bound variable d into x in 26 at occurence 1 |
qed |