Formal proof for first-order logic question using natural deduction

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:

attempt.jpg

Any help is greatly appreciated!!

• The proof is tricky: you have to work by contradiction, assuming $\exists x \forall y \lnot Axy$ and use two nested $(\exists \text E)$ – Mauro ALLEGRANZA Jan 20 at 16:19
• Hi, thank you for your comment! I realised I needed to assume ∃𝑥∀𝑦¬𝐴𝑥𝑦 and use one ∃E towards the end, but I am not sure where the other ∃E should come in... – tacosandburritos Jan 20 at 16:52
• It comes for a universal elimination on the premise. Universal Elimination may be invoked on either a fresh or extant variable. In this case the extant variable would be the witness to the assumed existential. – Graham Kemp Jan 21 at 1:44
• Thank you so much for the detailed and clear explanation! I really appreciate it! – tacosandburritos Jan 21 at 17:57

$$\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}}$$