# Prove $\exists x (\exists yA(y) \to A(x))$ is a theorem.

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 5):

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\}$$ $$\fitch{}{ \fitch{\color{blue} 1.\, \neg (\exists y A(y) \to A(c))}{ \fitch{\color{blue} 2.\, A(c)}{ \fitch{\color{blue} 3.\, \exists yA(y)}{ \color{blue} 4.\, A(c) \R{2} }\\ \color{blue} 5.\, \exists yA(y) \to A(c) \ii{3-4} \color{blue} 6.\, \bot \ne{1,5} }\\ \ldots\\ \color{blue} k.\, \bot }\\ \color{blue}{k+1}.\, \exists y A(y) \to A(c)\\ \color{blue}{k+2}.\, \exists x(\exists y A(y) \to A(x)) \\ }$$

Is this a good skeleton for this proof ? How can I derive last contradiction ?

• Also, you need to include justification for each step in your proof, or it becomes hard to glean what your reasoning is. We spoke about this yesterday. Mar 24 '20 at 14:43
• If you want to start by using the negation of what you are to prove, then you need to start with $\lnot \exists x( \exists y A(y) \to A(x))$. In your first line, x is a free variable. So we cannot say $\exists y(A(y)) \to A(c)$ contradicts $\lnot \exists y(A(y)\to A(x))$, because we don't know that $c = x$. Mar 24 '20 at 14:52
• @amWhy, just edited the question. Still, cannot think a way of using your suggestion. Mar 24 '20 at 19:01

Exploring your route gets you in a tangle where you need to quantify in an illegitimate way halfway through the proof.

Better, assume the negation of the desired conclusion and proceed ...

First let's just (in effect) use brute forcce! A standard proof strategy when you have a supposition of the form $$\neg(\alpha \to \beta)$$, is to suppose $$\neg \alpha$$, get a contradiction, proving $$P$$. OK, here there is an existential quantifier in the way between the negation and the conditional, but let's still try the same dodge, of assuming the negation of the antecedent of the internal conditional. Then let's do the pretty obvious thing at each stage.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{} {\fitch{\neg\exists x(\exists yAy \to Ax)} {\fitch{\neg\exists yAy}{\fitch{\exists yAy}{\bot\\ Ac}\\ (\exists yAy \to Ac)\\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \neg\neg\exists yAy\\ \exists yAy\\ \fitch{Ac}{ \fitch{\exists yAy}{Ac}\\ (\exists yAy \to Ac)\\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \bot }\\ \neg\neg\exists x(\exists yAy \to Ax)\\ \exists x(\exists yAy \to Ax) }$$

Looking at that proof, though, and seeing the proof ideas involved, we can spot [as noted by the OP] that we can speed things up a bit by doing some things in the opposite order:

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{} {\fitch{\neg\exists x(\exists yAy \to Ax)} {\fitch{\exists yAy} {\fitch{Ac} {\fitch{\exists y Ay}{Ac}\\ (\exists yAy \to Ac)\\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \bot\\ Ac }\\ (\exists yAy \to Ac) \\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \neg\neg\exists x(\exists yAy \to Ax)\\ \exists x(\exists yAy \to Ax) }$$

• Nicely done, @Peter! Mar 24 '20 at 21:28
• Thank you very much, @PeterSmith ! Would be possible to shorten the proof a little, like this ? Mar 24 '20 at 21:53
• $\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{{}\, }{ \fitch{{1}.\, \neg\exists x(\exists yA(y) \to A(c))}{ \fitch{{2}.\, \exists yA(y)}{ \fitch{{3}.\, A(c)}{ \fitch{{4}.\, \exists yA(y)}{ {5}.\, A(c) }\\ {6}.\, \exists yA(y) \to A(c)\\ {7}.\, \exists x(\exists yA(y) \to A(c)))\\ {8}.\, \bot }\\ {9}.\, \bot\\ {10}.\, A(c) }\\ {11}.\, \exists yA(y) \to A(c)\\ {12}.\, \exists x(\exists yA(y) \to A(c)))\\ {13}.\, \bot }\\ {14}.\, \exists yA(y) \to A(c)) }$ Mar 24 '20 at 21:53
• No. You can't apply $\exists$E using the supposition (3) because $c$ already appears in a previous undischarged supposition. This is the sort of problem I was alluding to in my preliminary comment. Mar 24 '20 at 21:57
• @F.Zer But c already appears in your line (1)as given which is a supposition which is still live at (3). However, on a closer look I see you have probably mistyped at lines (1), (7), and also both mistyped and failed to discharge properly at line (14). Mar 25 '20 at 7:06