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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.