Hilbert style axiom system without generalisation

Question

I the book Computational Complexity by C. Papadimitriou he introduces for first order logic the following axioms:

AX0: Any expression whose Boolean form is a tautology.

AX1: Any expression of the following form:

AX1a: $t = t$.

AX1b: $(t_1 = t_1' \land \ldots \land t_k = t_k') \Rightarrow f(t_1, \ldots, t_k) = f(t_1', \ldots, t_k')$.

AX1c: $(t_1 = t_1' \land \ldots \land t_k = t_k') \Rightarrow (R(t_1,\ldots,t_k) \Rightarrow R(t_1', \ldots, t_k'))$.

AX2: Any expression of the form $\forall x \phi \Rightarrow \phi[x \leftarrow t]$

AX3: Any expression of the form $\phi \Rightarrow \forall \phi$, with $x$ not free in $\phi$.

AX4: Any expression of the form $(\forall x(\phi \Rightarrow \varphi)) \Rightarrow (\forall x \phi \Rightarrow \forall x \varphi)$.

Remerk: AX0 includes Modus Ponens. And $t$ denotes a term in the language of first order logic.

In the text there is a form of generalisation mentioned, to cite the text (the paragraph's where all these axioms are justified):

Proposition 5.7: If $\phi$ is valid, then so is $\forall x \phi$.

There is a stronger form of this. Suppose that $x$ does not occur free in $\phi$. Then we claim that $\phi \Rightarrow \forall x \phi$ is valid. The reason is that, any model that satisfies $\phi$ will also satisfy $\forall x\phi$, as the $x = u$ part of the definition of satisfaction becomes irrelevant. We summarize this as follows:

Proposition 5.8.: If $x$ does not appear free in $\phi$, then $\phi \Rightarrow \forall \phi$ is valid.

What makes me wonder is that Propostion 5.7 is entirely dropped from the axioms, so I thought it might be deducable from the the other. And indeed if $x$ does no appear free in $\phi$, then Modus ponus with AX3 gives it, but what if $x$ does appear free in $\phi$. Surely by definition, if then $\phi$ is valid it must be satisfied by every model, in particular whatever value the free variable has, which makes this rule evident. But in that case I do not see how to deduce it from the other axioms...

So, why is the rule of generalisation missing in the axioms? Is it somehow deducible from the others?

Answer 1

Yes, it is a quite common presentation of first-order logic.

See e.g.:

• Herbert Enderton, A Mathematical Introduction to Logic, Academic Press (2nd ed. 2001), page 109-on.

It has one rule of inference only : modus ponens, while Generalization is derivable in the form [see page 117]:

If $\Gamma \vdash \varphi$ and $x$ do not occur free in any formula in $\Gamma$, then $\Gamma \vdash ∀x \ \varphi$.

The proof is by induction on the lenght of the derivation of $\Gamma \vdash \varphi$ (and it needs axioms Ax3 and Ax4).

With $\Gamma = \emptyset$, we have : if $\vdash \varphi$, then $\vdash \forall x \ \varphi$.