What would a formal Fitch proof for this look like?
I am given ¬∀x(P(x)→Q(x)), and need to derive ∃xP(x) from it.
I started with this, but I don't know if I am doing the right thing, and where to go from there:
EDIT: Did it (see answer)
1) ¬∀x(P(x) → Q(x)) --- premise
2) ¬∃xP(x) --- assumed [a]
3) P(x) --- assumed [b]
4) ∃xP(x) --- from 3) by ∃-intro
5) ⊥ --- contradiction : from 2) and 4)
6) Q(x) --- from 5) by ⊥-elim
7) P(x) → Q(x) --- from 3) and 6) by →-intro, discharging [b]
8) ∀x(P(x) → Q(x)) --- from 7) by ∀-intro
9) ⊥ --- contradiction : from 1) and 8)
10) ∃xP(x) --- from 2) by Double Negation (or ¬-elim), discharging [a].
The following proof is the same as Mauro ALLEGRANZA's but it uses Klement's Fitch-style proof checker. Descriptions of the rules are in forallx. Both are available online and listed below. They may help as supplementary material to what you are currently using.
You may be required in your proof checker to represent contradictions as conjunctions of contradictory statements. This proof checker only requires noting the contradiction as "⊥" and listing the contradictory lines such as I did on lines 5 and 9.
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
2.∃x~(P(x)->Q(x)) ~ Universal out Pr.
3.~(P(a)->Q(a)) Existential out (x/a) 2
4.P(a)&~Q(a) ~ conditional out 3
5.P(a) Conjunction out 4
6.∃xP(x) Existential In 5