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 |