# How to proof this this sentence with natural deduction?

I need to prove this sentence:

$\forall x~\Big[\exists y~\big[L(y,x)\land\forall z~[L(z,x)\to (y=z)]\big]\Big]\land\exists x~[L(x,x)]\vdash\exists x~\big[\lnot\exists y~[L(y,x)\land\lnot (x=y)]\big]$

My proof:

$\begin{array}{r|l:l}1. & ∀x [∃y[L(y,x)∧∀z [L(z,x)→(y=z)]]] ∧ ∃x [L(x,x)]& \textsf{Premise }{1} \\ 2.&∀x [∃y[L(y,x)∧ ∀z [L(z,x)→(y=z)]]]&\wedge\textsf{-elimination }{1} \\ 3.&∃x [L(x,x)]&\wedge\textsf{-elimination }{1} \\ 4.&\quad ∃y[L(y,a)∧ ∀z [L(z,a)→(y=z)]]&\textsf{∀-elimination }{2} \\ 5.&\qquad L(b,a)∧ ∀z [L(z,a)→(b=z)]&\textsf{Assumption }{5} \\ 6.&\qquad\quad ∃y [L(y,a)∧¬(a=y)]&\textsf{Assumption }{6} \\ 7.&\qquad\quad L(b,a)&\wedge\textsf{-elimination }{5} \\ 8.&\qquad\quad ∀z [L(z,a)→(b=z)]&\wedge\textsf{-elimination }{5} \\ 9.&\qquad\qquad L(c,a)→(b=c)&∀\textsf{-elimination }{8} \\ 10&\qquad\qquad..... \end{array}$

I know that I need to find a contradiction in order to negate Assumption{6} and then do existential introduction, but I have no idea how to do it.

I note that you started making some assumptions/subproofs without indicating what those assumptions are for, and how those subproofs are going to be used. That is a good way to get lost and stuck, and thus a really bad habit you should try to break!

Instead, whenever you make an assumption, skip a few lines, indicate what you are looking for at the end of the subproof, close the subproof, apply whatever rule you intended to use that subproof for, and finally go back to try and fill in the missing lines. For example, if you are making an assumption with the idea of doing a proof by contradiction, then skip a few lines, write a contradiction, close the subproof, and infer the negation of the assumption. That way, you retain oversight of the proof, keep it organized, and off-load your working memory to paper. In fact, this strategy coincides with the all-important 'proof plans' any mathematician uses to tackle complicated proofs.

Another tip: whenever you have both universals and existentials to work with, you typically want to eliminate the existentials first, because you can always instantiate the universals with whatever constant you used to instantiate the existential, but you can not do that the other way around.

A tricky enough proof to be instructive to do.

Let's have some motivation. (It is always a good plan to think through informally how the argument ought to go!)

Reading "L" as loves, the two-part premiss says: (1) take anyone you like, one and only one person loves them; and also (2) there is someone who loves themselves.

Given (2), let's suppose the self-loving person is Alex. Since by (1) there is someone (dub them Brown) who is the sole person who loves Alex, Brown has to be Alex! And by (1) again, no one other than this Alex/Brown loves Alex. So there is someone (Alex/Brown!!) such that it isn't the case that there exists some other person who loves them. Which is what the conclusion says.

Here's a formal proof, Fitch-style, that follows that line of reasoning tolerably closely. Think strategically (following Bram28's good advice!). You should be able to see straight away you are going to need to use two key steps of Existential Quantifier Elimination (using the existentials buried in the two halves of the premiss). Fill in the justifications for each line to make sure you understand the proof.

$\forall x[\exists y[L(y,x) \land \forall z[L(z,x)→(y=z)]]] \land \exists xL(x,x)\\ \forall x[\exists y[L(y,x) \land \forall z[L(z,x)→(y=z)]]]\\ \exists xL(x,x)\\ \quad|\quad L(a, a)\\ \quad|\quad \exists y[L(y,a) \land \forall z[L(z,a)→(y= z)]]\\ \quad|\quad\quad|\quad [L(b,a) \land \forall z[L(z,a)→(b = z)]]\\ \quad|\quad\quad|\quad \forall z[L(z,a)→(b = z)]\\ \quad|\quad\quad|\quad [L(a,a)→(b = a)]\\ \quad|\quad\quad|\quad (b = a)\\ \quad|\quad\quad|\quad\quad|\quad [L(c,a) \land \neg(a = c)]]\\ \quad|\quad\quad|\quad\quad|\quad L(c,a)\\ \quad|\quad\quad|\quad\quad|\quad \neg(a = c)\\ \quad|\quad\quad|\quad\quad|\quad [L(c,a)→(b = c)]\\ \quad|\quad\quad|\quad\quad|\quad (b = c)\\ \quad|\quad\quad|\quad\quad|\quad (a = c)\\ \quad|\quad\quad|\quad\quad|\quad \bot\\ \quad|\quad\quad|\quad \neg[L(c,a) \land \neg(a = c)] \\ \quad|\quad\quad|\quad \forall y\neg[L(y,a) \land \neg(a = y)] \\ \quad|\quad\quad|\quad \neg\exists y[L(y,a) \land \neg(a = y)] \\ \quad|\quad\quad|\quad \exists x[\neg\exists y[L(y,x) \land \neg(x = y)]] \\ \quad|\quad \exists x[\neg\exists y[L(y,x) \land \neg(x = y)]] \\ \exists x[\neg\exists y[L(y,x) \land \neg(x = y)]] \\$

• Please, could you tell how you got from L(c,a) -> (b=c) – Buscemi Nov 29 '17 at 20:15
• From the universal quantification at line 7. – Peter Smith Nov 29 '17 at 20:17
• Thanks! Also @Bram28 suggested to eliminate existentials first before universal quantifiers. Can I use this strategy when existential quantifier is inside universial quantifier? For example like ∀y[∃x[.....]]? – Buscemi Nov 29 '17 at 20:20
• Careful: you always have to tackle the "main operator" of a wff first ... – Peter Smith Nov 29 '17 at 20:21
• Also, how do you proof from 18th to 19 th lines? Its obvious that they the same, but can you just plug it in? – Buscemi Nov 29 '17 at 23:19