First we prove a simple implication:
1. Proposition
∃x R(x) → ¬∀x ¬R(x) (theo1)
| 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 |