= Solution
Let $N$ abbreviate the given negated existential statement, and choose a fresh variable $u$ that is not free in the undischarged premise. Work from an assumed $P(u)$ to $Q(u)$:
``
1 ¬∃x (Q(x) → P(x)) premise N
2 | P(u) assume
3 | | Q(u) assume
4 | | P(u) available from 2
5 | Q(u) → P(u) →-intro, discharge 3–4
6 | ∃x (Q(x) → P(x)) ∃-intro, witness u in 5
7 | ⊥ ¬-elim, 6 and 1
8 | Q(u) ⊥-elim, 7
9 P(u) → Q(u) →-intro, discharge 2–8
10 ∀x (P(x) → Q(x)) ∀-intro, 9, u fresh
``
The occurrence of $u$ in the <temporary assumption> at line 2 is harmless because that assumption is discharged before <universal quantifier introduction rule>. No unproved implication-creation rule or quantifier-negation equivalence is needed.
Back to article page
