I'm new to first-order logic and need a little bit of help with proving the following:
∀x∃yA(x,y) ⊢ ¬∃x∀y¬A(x,y)
It seemed straightforward but I have been stuck at it for hours. This is what I have come up with so far:
Any help is greatly appreciated!!
$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}$
Here's the Fitch style layout for this proof.
$$\fitch{~~1.~\forall x~\exists y~A(x,y)}{\fitch{~~2.~\exists x~\forall y~\lnot A(x,y)}{\fitch{~~3.~[b]~\forall y~\lnot A(b,y)}{~~4.~\exists y~A(b,y)\hspace{8ex}{\forall}\mathsf E~1\\\fitch{~~5.~[c] A(b,c)}{~~6.~\lnot A(b,c)\hspace{8ex}{\forall}\mathsf E~4\\~~7.~\bot\hspace{14ex}{\lnot}\mathsf E~5,6}\\~~8.~\bot\hspace{16ex}\exists\mathsf E~4,5{-}7}\\~~9.~\bot\hspace{18ex}\exists\mathsf E~2,3{-}8}\\10.~\lnot\exists x~\forall y~\lnot A(x,y)\hspace{6ex}{\lnot}\mathsf I~2{-}9}$$
As you can see, there are three assumptions raised - one for the negation introduction, and two for the existential eliminations. The two universal eliminations are made to the free variables raised in the assumption for the existential eliminations (called the witness variables).
Note: Some systems simply reuse the variable bound to the existential statement but, when allowed, you should use a local variable for clarity.
Now for your tree system: An existential elimination takes the following form: $$\dfrac{\lower{1.5ex}{\exists z~P(z)}~~{\small[a]}\dfrac{\begin{array}{c}[P(a)]^n\\[-1ex]\vdots\end{array}}{Q}{\tiny\textsf{somehow}}}{Q}{\small\exists\mathsf E^n}$$
Remember, the witness variable must not occur free within the derived consequent ($Q$). However, it may occur free in other statements within that derivation--such as for example, generated by a universal elimination.
Relevantly here we have the proof for $\forall w~\lnot P(w), \exists z~P(z)\vdash\bot$
$$\dfrac{\lower{1.5ex}{\exists z~P(z)}~~{\small[a]}\dfrac{\lower{1.5ex}{[P(a)]^n}\dfrac{\forall w~\lnot P(w)}{\lnot P(a)}{\small\forall\mathsf E}}{\bot}{\small\lnot\mathsf E}}{\bot}{\small\exists\mathsf E^n}$$
Well, the proof you seek is a little more complicated, but that is the basis.
$$\phantom{\dfrac{\dfrac{\lower{1ex}{[\exists x~\forall y~\lnot A(x,y)]^1}~~{\small[b]}\dfrac{\dfrac{\forall x~\exists y~A(x,y)}{\exists y~A(b,y)}{\small\forall\mathsf E}~~{\small[c]}\dfrac{\dfrac{[\forall y~\lnot A(b,y)]^2}{\lnot A(b,c)}{\small\forall\mathsf E}~\lower{1.5ex}{[A(b,c)]^3}}{\bot}{\small\lnot\mathsf E}}{\bot}{\small\exists\mathsf E^3}}{\bot}{\small\exists\mathsf E^2}}{\lnot\exists x~\forall y~\lnot A(x,y)}{\small\lnot\mathsf I^1}}$$