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 |