# 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?

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$?

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:

1. Tautologies;

2. $\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$;

3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$;

4. $\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)$.