Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
I'm supposed to prove, using only primitive rules (the introduction and elimination rules for AND, OR, NOT, conditional, biconditional, existential, universal, and equality) the following:
$$\exists x~\forall y~(x=y) \to \forall x~\forall y~(x=y)$$
I checked this in a tree proof generator and the argument is indeed valid, but I can't figure out how to approach a natural deduction proof using only primitive rules here. What should my starting point be?
Your starting point should be to think about this informally: what are the statements saying that would make this valid? Well, the first statement says that there is something that is identical to everything. But if everything is identical to this one thing, then that means that there is really only that one thing, and nothing else. And so yes, the second statement would therefore also be true: everything (which is just one thing) is identical to everything (still just that one thing)
Now, as far as formally proving this using a natural deduction system goes, that all depends on the specific rules your specific deduction system has: there are many slightly different natural deduction systems, so a proof in one system may not constitute a proof in another. Why don't you post some of your own efforts in trying to make this into a proof, so you can show us some of your own effort, and at the same time it'll give us an idea exactly what system you are working with.
Does it help to use some alpha-replacement as a reminder that the bound variables for different quantifiers need not refer to the same entities? $$\exists x~\forall y~(x=y)~\to~\forall x~\forall y~(x=y)\\\Updownarrow\\\exists x~\forall y~(x=y)~\to~\forall u~\forall v~(u=v)$$
So this proof should involve: an assumption of the antecedant, existential elimination, universal eliminations, an argument of some kind, two universal introductions, and a conditional introduction to discharge the assumption.
But wait, we need to make two universal eliminations--to two different arbitrary entities-- to set things up for those two universal introductions later. Also the argument needs to discard the witness so that an existential introduction is unrequired.
What kind of argument do you need to make? Well the only thing left to discuss is that equality relationship. Use its properties.
As a contrast to Bram28's answer, instead of understanding anything, you can think like a machine. The outermost connective is $\to$, so (ignoring cut) we need $\to$-introduction, then we have $\forall$ twice, so use $\forall$-introduction. We now have $$x_0, y_0; \exists x.\forall y.x = y\vdash x_0 = y_0$$ Now the only option is $\exists$-elimination, giving $$x_0, y_0, x_1; \forall y.x_1 = y\vdash x_0 = y_0$$ Now the only thing we can do is use $\forall$-elimination which only gives us two additional facts: $$x_0, y_0, x_1; x_1 = y_0, x_1 = x_0\vdash x_0 = y_0$$ Now we can apply $=$-elimination producing: $$x_0, y_0; x_0 = y_0\vdash x_0 = y_0$$ And we're done.
If we ignore cut, then at each step in the proof there are relatively few options, often only one. Actually writing this out in typical natural deduction style is a bit awkward because natural deduction proofs proceed from the top and bottom simultaneously to the middle. The sequent calculus avoids this by being strictly bottom-up. In particular, doing the $\forall$-eliminations will produce two floating branches that will be connected to the "trunk" of the proof with the $=$-elimination. Anyway, to reiterate, regardless of the exact rules of your system, for many proofs of simple logical facts there will be only a few (or possibly only one) way of continuing the proof making even brute-force search often quite effective. Obviously, adding a bit of intuition to guide the search when there is more than one option can avoid wasting time on dead-ends.
The OP has the following question:
I checked this in a tree proof generator and the argument is indeed valid, but I can't figure out how to approach a natural deduction proof using only primitive rules here. What should my starting point be?
Here is a proof using a Fitch-style proof checker:
To attempt existential elimination, I start a subproof (line 2) replacing the variable $x$ with the name $a$ as an assumption. In order to close this subproof and discharge the assumption, I need to derive a line that no longer uses that name $a$.
On line 3 I use universal elimination replacing the variable $y$ with the name $b$ and referencing line 2. One line 4, I do the same thing but with a new name $c$. The reason to do this twice is to eventually derive a line that does not have the name $a$ in it so I can close the subproof. That is done by substituting the name $a$ from line 4 with the name $b$ from line 3 and placing the result on line 5. I justify this with equality elimination (=E).
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
