Proving ∀x∃yRxy,∀x∀y(Rxy→∃zRzx), ∀x∀y(Ryx→∀zRxz) ∴∀x∀yRxy

Question

I have been trying the following prove but no success. Any help is appreciated. Thank you. ∀x∃yRxy ∀x∀y(Rxy→∃zRzx) ∀x∀y(Ryx→∀zRxz) ∴∀x∀yRxy

Answer 1

I'm assuming you want some flavour of natural deduction proof (as it would be simply evil to set this as an exercise for a Hilbert-style proof-system!).

This is then interesting enough to answer. For it vividly illustrates how thinking strategically helps you construct a natural deduction proof (and with luck makes the proof easy to find!). Break down the construction of proof into stages, but not necessarily stages that follow one after another -- rather, as here, you often need to construct the stages one inside another. To explain:

Stage A

You have three universal premisses and are aiming for a universal conclusion. So the obvious thing to do is take some arbitrary $a$. Your given premisses then yield the derived premisses

$\exists yRay\\ \forall y(Ray \to \exists zRza)\\ \forall y(Rya \to \forall zRaz)$

Suppose you can derive the initial conclusion

$\forall yRay$

Then, since $a$ is arbitrary, you can then derive the wanted final conclusion

$\forall x\forall yRxy$.

[You get the new premisses by three applications of UE, the final step will be UI, and the layout will depend on your preferred proof system!]

Stage B

So we now have a simpler exercise, to get from the derived premisses to the initial conclusion. Your proof here will have to use the existential premiss (and always a good policy to instantiate existentials before universals). So that tells us that the shape of the simpler proof should be like this:

$\exists yRay\\ \forall y(Ray \to \exists zRza)\\ \forall y(Rya \to \forall zRaz)\\ \quad\quad | \quad Rab\\ \quad\quad | \quad\quad\vdots\\ \quad\quad | \quad\forall yRay\\ \forall yRay$

where the final step invokes EE (roughly, given $\exists y\varphi(y)$ and a proof from $\varphi(b)$ to a conclusion $C$ not involving $b$, we can infer $C$). OK so far?

Stage C

At some point we are going to have to invoke the second derived premiss and get at that existential conclusion and then use it in another proof by EE. So that suggests that the proof will have to continue like this:

$\exists yRay\\ \forall y(Ray \to \exists zRza)\\ \forall y(Rya \to \forall zRaz)\\ \quad\quad | \quad Rab\\ \quad\quad | \quad (Rab \to \exists zRza)\\ \quad\quad | \quad \exists zRza\\ \quad\quad | \quad \quad | \quad Rca\\ \quad\quad | \quad\quad | \quad \vdots\\ \quad\quad | \quad\quad | \quad\forall yRay\\ \quad\quad | \quad\forall yRay\\ \forall yRay$

Again -- OK so far, see why the proof outline more or less writes itself?

Stage D

Obviously, we now have to make use of the third derived premiss. And there is only one sensible way of instantiating that universal quantification! Which gives us ...

$\exists yRay\\ \forall y(Ray \to \exists zRza)\\ \forall y(Rya \to \forall zRaz)\\ \quad\quad | \quad Rab\\ \quad\quad | \quad (Rab \to \exists zRza)\\ \quad\quad | \quad \exists zRza\\ \quad\quad | \quad \quad | \quad Rca\\ \quad\quad | \quad \quad | \quad (Rca \to \forall zRaz)\\ \quad\quad | \quad \quad | \quad\forall zRaz\\ \quad\quad | \quad\quad | \quad \vdots\\ \quad\quad | \quad\quad | \quad\forall yRay\\ \quad\quad | \quad\forall yRay\\ \forall yRay$

Drat! We haven't quite finished, as in the subsubproof we've derived $\forall zRaz$ and we want $\forall yRay$. But hopefully you can join up the dots and change the variable by a UE followed by a UI!

So we are done. Now it just remains to implement the proof idea into your favourite natural deduction system!

Answer 2

Here is a proof using the logic software program Fitch: