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 sequence 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 |