Help with a simple proof in predicate logic (with identity)

Question

it's been a while since I've done formal logic, and I was trying to help a friend with a proof. His logic course is using Lemmon's Beginning Logic. Here's what he's supposed to show, without using reductio ad absurdum: $$\exists x\,\forall y\,Ryx \vdash \exists y\,\forall x\quad x=y \implies \forall z\, Rzx.$$ Intuitively, the premise could be understood to say there's someone who is $R$'ed (e.g. respected) by everyone. And the conclusion could be understood to say there's someone such that anyone who turns out to be the very same individual is $R$'ed by everyone. So it seems like the conclusion is just a convoluted way of restating the premise. But I'll be damned if I know how to get started with the proof.

Answer 1

I'm not familiar with Lemmon's proof system, but I'll give you a Natural Deduction derivation.

The key step is the equality rule $(=\text E)$ [see Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 122]:

$$\dfrac{(s=t) \ \ \ \ \ \ \phi[s/x]}{\phi[t/x]}$$

Thus, from the premise :

1) $∃x∀yRyx$

we need the temporary assumption :

2) $∀yRya$ --- [a],

and then we apply a "standard" sub-derivation to rename the bound variable $x$, getting:

3) $∀zRza$.

Now we apply the rule $(=\text E)$ in the form : $(a=x), \ ∀zRza \vdash ∀zRzx$ [with $∀zRzw$ as $\phi(w)$] with 3) to derive :

4) $(a=x) \vdash ∀zRzx$.

With the "derived rule" $(=\text{symm})$ : $(s=t) \vdash (t=s)$ [see page 123] followed by $\to$-intro, we get :

5) $(x=a) \to ∀zRzx$.

Now we apply $\forall \text I$ :

6) $\forall x \ [(x=a) \to ∀zRzx]$

followed by $\exists \text I$ :

7) $\exists y \forall x \ [(x=y) \to ∀zRzx]$.

All the derivation is "subject" to the assumption [a]. But $a$ is not free in the conclusion 7) of the sub-derivation; thus, we can apply $\exists\text{E}$ :

$$\dfrac{∃x \phi(x) \ \ \ \ \ \ \phi[t/x] \vdash \psi}{\psi}$$

provided that the term $t$ does not occur in $\psi, \phi$ or any undischarged assumption except $\phi[t/x]$, to 1), 2) and 7) to discharge [a] and conclude with :

$∃x∀yRyx \vdash \exists y \forall x \ [(x=y) \to ∀zRzx]$.