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