= Solution
Use the already proved inference in (a) on the negated existential premise. Eliminate the remaining existential with a fresh witness $u$, which must not appear in the final conclusion or the other undischarged assumptions.
``
1 ∃x P(x) premise
2 ¬∃x (Q(x) → P(x)) premise
3 ∀x (P(x) → Q(x)) derivation in (a), from 2
4 | P(u) fresh-witness assumption for 1
5 | P(u) → Q(u) ∀-elim, 3
6 | Q(u) →-elim, 4 and 5
7 | P(u) ∧ Q(u) ∧-intro, 4 and 6
8 | ∃x (P(x) ∧ Q(x)) ∃-intro, witness u
9 ∃x (P(x) ∧ Q(x)) ∃-elim, 1, subproof 4–8
``
The result in (a) is a proved dependency, not an additional <axiom>. The witness introduced at line 4 does not escape its subproof.
Back to article page
