Formal proof of a very simple fact.

Question

Let $L$ be a first-order language with the predicate symbol $R$, and let $x,y$ be variables in $L$.

I want to show that

$\forall x \forall y R(x,y) \vdash R(y,x)$

Where $\vdash$ means formally prove.

I am using Enderton's A Mathematical Introduction to Logic, so I am using his deductive system. I am allowed to use any theorem to show that there is a formal derivation, except for the completeness theorem.

The best I can do is $\forall x \forall y R(x,y) \vdash R(z,y)$

where $z$ is a variable distinct from $x$ and $y$. I have been trying for hours, please help. Note that I am not actually looking for a formal proof, I just need to show that one exists.

Answer 1

Ref to :

• Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 112.

The first step is :

$∀x∀yR(x,y) ⊢ ∀yR(z,y)$, using Axiom.2 with $z$ as $t$ (and Modus Ponens rule, of course).

The second step is :

$∀yR(z,y) ⊢ R(z,x)$, using again Axiom.2 with $x$ as $t$.

Then we use Generalization Theorem [page 117] to get :

$R(z,x) ⊢ ∀zR(z,x)$

and finally we apply again Axiom.2 to have :

$∀zR(z,x) ⊢ R(y,x)$.

---

Axiom.2 is :

$\forall x \alpha \to \alpha^x_t$, where $t$ is a term is substitutable for $x$ in $\alpha$.