Formal deduction in first order logic How do you show that a deduction exist in the Hilbert Proof System, as used in Herbert Enderton, A Mathematical Introduction to Logic.
L is a FOL (First Order Language) which contains R, where R is a single binary predicate symbol.
a1, a2, a3 are defined as:
a1 = $∀x∀y∀z(Rxy → (Ryz → Rxz))$
a2 = $∀x(¬Rxx)$
a3 = $∀x∀y(x \ne y→Rxy∨Ryx)$
We have the theory, Γ = {a1, a2, a3} and for :
$Γ ⊢ ∀x∀y(Rxy → (¬Ryx))$
How does one going about showing that a proof exists?
 A: Well, there are two options.
Option 1: You could write out a proof using the Hilbert Proof System. The details of this proof are going to depend on the details of the proof system. Since I don't have a copy of Enderton on hand, I can't help you here.
Option 2: If you know the completeness theorem for first-order logic, you can argue semantically instead of syntactically. The completeness theorem says that all models for $\Gamma$ satisfy a sentence $\phi$ if and only if there is a proof of $\phi$ from $\Gamma$. This frees us from the formal rules of the system and allows us to argue on a higher level.
So take a model $M\models \Gamma$. Why must the sentence $\forall x \forall y (Rxy \rightarrow \lnot Ryx)$ hold in $M$? Hint: What are the axioms a1, a2, a3 saying about $R$?
A: I'll complete the answer above with a proof using the axioms and rules of Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001).
The axioms are [see page 112] :

The logical axioms are all generalizations of wffs of the following forms, where $x$ and $у$ are variables and $\alpha$ and $\beta$ are wffs: 
  
  
*
  
*Tautologies; 
  
*$\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$;
  
*$\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$; 
  
*$\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

If the language includes equality, the usual axiom for it are added. 
Modus ponens is the sole rule of inference.
From a1) : $∀x∀y∀z(Rxy → (Ryz → Rxz))$, applying Ax.2 we get :
(1) $Rxy → (Ryx → Rxx)$
(2) $Rxy$ --- assumed
(3) $Ryx → Rxx$ --- from (1) and (2) by mp
(4) $\lnot Rxx \rightarrow \lnot Ryx$ --- from (3) and Ax.1 by mp 
(5) $¬Rxx$ --- from a2) : $∀x(¬Rxx)$, applying Ax.2
(6) $\lnot Ryx$ --- from (4) and (5) by mp
(7) $Rxy \rightarrow \lnot Ryx$ --- form (2) and (6) by Deduction Theorem (page 118)
Now we can apply the Generalization Theorem [page 117] twice to get :
(8) $\forall x \forall y (Rxy \rightarrow \lnot Ryx)$ --- $x$ does not occur free in any 
formula in $\Gamma = \{ ∀x∀y∀z(Rxy → (Ryz → Rxz)), ∀x(¬Rxx) \}$.
In conclusion, we have proved that :


$\Gamma = \{ ∀x∀y∀z(Rxy → (Ryz → Rxz)), ∀x(¬Rxx) \} \vdash \forall x \forall y (Rxy \rightarrow \lnot Ryx)$.


