Natural Deduction proof with identity: ∀x∃y(Rxy∧Py), ∀x¬Rxx==> ¬∀x∀y (Px→(Py→x=y))

Question

I have a small question about how to finish the proof in the title. The main idea seems to be make an assumption of ∀x∀y (Px→(Py→x=y)) and to derive a contradiction between Raa and ¬Raa from that, which then proves the conclusion:

So

1.∀x∀y (Px→(Py→x=y))

2. ∀y (Pa→(Py→a=y))

3.(Pa→(Pb→a=b))

4. Assume Pa, then by modus ponens

5.Pb→a=b

Pb can be derived from the premiss ∀x∃y(Rxy∧Py), which gives

6.∃y(Ray∧Py)

7. Existential elimination gives the assumption Rab∧Pb

8. Pb by conjunction elimination

9. Plugging Pb into 5. gives a=b by modus ponens

10. Use the assumption Rab∧Pb again

11. Use conjunction elimination to get Rab

12. Then combine 9. and 11. to get Raa

13. Then take the premiss ∀x¬Rxx

14. Use universal quantifier elimination to get ¬Raa

15. From the contradiction between 14. and 12. you can prove ¬Pa (Pa was the assumption in 4.)

    But where do I go from here? I need to get another contradiction in order to discharge my assumption ∀x∀y (Px→(Py→x=y)) and prove the conclusion...but anything I assume seems impossible to discharge again!

Thanks for your help and sorry for the long explanation!

Answer 1

You don't know that $Pa$, hence the difficulty you're having. I'll sketch the deduction:

1. Assume $\forall x \forall y\,(Px\to (Py\to x=y))$.
2. Let $a$ be any individual. By hypothesis, we get
3. $\exists y\,(Ray \land Py)$. (This is your 6.)
4. $Rab \land Pb$ (existential elimination, giving your 7.)
5. Similarly to 3., $\exists y\,(Rby \land Py)$, so
6. $Rbc \land Pc$ for some $c$ (existential elimination).
7. $Pb\to (Pc\to b=c)$, using the assumption.
8. From 4., $Pb$, and from 6., $Pc$.
9. From 8. and 7. by modus ponens, $b=c$.
10. From 6. and 9., $Rbb$.
11. $\neg Rbb$, by instantiating $\forall x\,\neg Rxx$ with $b$.
12. From 10. and 11., contradiction; so conclude that the assumption is false.

Answer 2

My first thought when approaching this type of problem is to read out the statements and come up with a natural language proof. For convenience I will replace $Rxy$ with $x\prec y$ and read it as "$y$ is bigger than $x$" simply because we have a lot of convenient adjectives for that relation. $\forall x\exists y(x\prec y\land Py)$ says that for every $x$ there is a $y$ bigger than $x$ which has property $P$, and $\forall x,x\not\prec x$ means that no element is bigger than itself, while $\lnot\forall x\forall y(Px\to(Py\to x=y))$ means that it is not the case that there is at most one element $x$ with property $P$, i.e. there are at least two distinct elements with property $P$.

From this, the answer is (hopefully) already clear: We assume there is at least one element $a$, and then there is an $b$ bigger than $a$ with property $P$, and there is also a $c$ bigger than $b$ with property $P$ (and $b\ne c$ because $c$ is bigger). If we knew that $\prec$ was transitive, we could even continue to get an infinite number of distinct elements with property $P$, but with only irreflexivity we can only get two.

Now to turn this into a rigorous proof.

• 1: Assume $\forall x\exists y(x\prec y\land Py)$
• 2: Assume $\forall x,x\not\prec x$
• 3: Assume $\forall x\forall y(Px\to(Py\to x=y))$

We're going to prove a contradiction from these three, thus proving the negation of (3).

• 4: $\exists y(a\prec y\land Py)$ by universal generalization $x:=a$ on (1)
• 5: Take $b$ from (4) with $a\prec b\land Pb$
• 6: $\exists y(b\prec y\land Py)$ by universal generalization $x:=b$ on (1)
• 7: Take $c$ from (6) with $b\prec c\land Pc$
• 8: $Pb$ from and elimination on (5)
• 9: $Pc$ from and elimination on (7)
• 10: $Pb\to(Pc\to b=c)$ from universal generalization $x:=b,y:=c$ on (3)
• 11: $Pc\to b=c$ from modus ponens on (8,10)
• 12: $b=c$ from modus ponens on (9,11)
• 13: $b\prec c$ from and elimination on (7)
• 14: $b\prec b$ from equality substitution on (12,13)
• 15: $b\not\prec b$ from universal generalization $x:=b$ on (2)
• 16: contradiction from (14,15)

This is nothing more than an explication of the same natural language proof: get $b$ and $c$, and note that they are distinct and both have property $P$.

Answer 3

For those who like a nice Gentzen-style proof:

Have ¬∀x∀y(Px→(Py→(x=y)) as your root.

Line1: ∃Elim. Have ∃y(Rcy∧Py) and ¬∀x∀y(Px→(Py→(x=y)) on the same line.

To prove ∃y(Rcy∧Py) it's just a simple ∀Elim from ∀x∃y(Rxy∧Py)

Line2: ¬Intro. Have Pa and ¬Pa on the same line.

To prove Pa it's just a simple ^Elim from (Rca ^ Pa) which is discharged at line1.

Line3 (above ¬Pa): ∃Elim. Have ∃y(Ray∧Py) and ¬Pa on the same line.

We can derive ∃y(Ray∧Py) from ∀x∃y(Rxy∧Py).

Line4 (above ¬Pa): ¬Intro. Have Raa and ¬Raa on the same line.

¬Raa can be derived from ∀x¬Rxx.

Line5 (above Raa): Have (a=b) and Rab on the same line.

Rab can be derived from (Rab^Pb), which is discharged at line3.

Line6 (above (a=b)): ->Elim. Have (Pb -> (a=b)) and Pb on the same line.

Pb can be derived from (Rab^Pb), which is discharged at line3.

Line7: ->Elim. Have (Pa -> (Pb -> (a=b))) and Pa on the same line.

Pa is discharged at line 4. Two more uses of ∀Elim and you get ∀x∀y(Px→(Py→x=y)) which is discharged at line2.

The proof is then complete. : )