3.3 Hilbert Systems

Hilbert systems provide a very compact and minimalistic approach to formal proofs, where almost all logical reasoning is encoded in a fixed collection of axiom schemes, and only a small number of inference rules are used to derive new formulas.

In contrast with natural deduction and the sequent calculus, where many rules correspond directly to logical connectives, Hilbert systems concentrate the logical content in axioms and rely heavily on repeated applications of a single inference rule.

Structure of the System

A Hilbert system consists of:

a collection of axiom schemes, which are formulas that are taken as universally valid patterns,

a small number of inference rules, usually just one rule, called modus ponens.

A derivation in a Hilbert system is a finite sequence of formulas:

A_1, A_2, \dots, A_n

where each formula $A_i$ is either an instance of an axiom scheme, an assumption from a given set $\Gamma$ , or follows from earlier formulas by applying an inference rule.

If there exists such a derivation of a formula $A$ from assumptions $\Gamma$ , we write:

\Gamma \vdash A

Modus Ponens

The main inference rule is modus ponens:

\frac{A \qquad A \to B}{B}

This rule allows one to derive $B$ whenever both $A$ and $A \to B$ have already been derived.

Because this is usually the only rule, all reasoning in a Hilbert system is ultimately carried out by chaining implications together.

Axiom Schemes

A typical Hilbert system for propositional logic includes axiom schemes such as the following.

First axiom scheme:

A \to (B \to A)

Second axiom scheme:

(A \to (B \to C)) \to ((A \to B) \to (A \to C))

Third axiom scheme:

(¬A \to ¬B) \to (B \to A)

Each of these is not a single formula but a pattern that represents infinitely many formulas, obtained by substituting arbitrary formulas for the variables $A$ , $B$ , and $C$ .

These axioms are chosen so that they are valid under all valuations and sufficient to derive all valid formulas.

Example 3.7

We show that:

\vdash A \to A

The proof proceeds by constructing a sequence of formulas using only the axiom schemes and modus ponens.

First consider the instance of the first axiom:

A \to (A \to A)

Next consider the instance of the second axiom:

(A \to ((A \to A) \to A)) \to ((A \to (A \to A)) \to (A \to A))

Using the first axiom again, we have:

A \to ((A \to A) \to A)

Applying modus ponens to these formulas step by step, we eventually derive:

A \to A

This example illustrates that even simple statements may require several steps in a Hilbert system, because the system has very few rules.

Lemma 3.8 (Deduction Theorem)

If:

\Gamma, A \vdash B

then:

\Gamma \vdash A \to B

Proof

The proof is carried out by transforming a derivation of $B$ from $\Gamma$ together with $A$ into a derivation of $A \to B$ from $\Gamma$ alone, by systematically inserting implications into each step of the derivation.

Each step of the original derivation is replaced by a formula that expresses that step under the assumption $A$ , and the axiom schemes are used to ensure that the transformation is valid.

This process is somewhat technical, but it is possible because the axioms are designed to simulate the effect of conditional reasoning.

Lemma 3.9 (Reflexivity of Implication)

For every formula $A$ :

\vdash A \to A

Proof

This follows from the example above, where a derivation was explicitly constructed using the axiom schemes and modus ponens.

Expressiveness

Despite having only one inference rule, Hilbert systems are as expressive as other proof systems such as natural deduction and the sequent calculus, and they can derive exactly the same set of valid formulas.

However, proofs in Hilbert systems are often longer and less intuitive, because many steps are needed to simulate reasoning that is more direct in other systems.

Soundness

Hilbert systems are sound, meaning that every formula that can be derived in the system is valid under every valuation.

This follows from the fact that all axiom schemes are valid and that modus ponens preserves truth, so that every step in a derivation maintains validity.

Completeness

Hilbert systems are also complete, meaning that every valid formula can be derived using the axioms and inference rules.

This shows that the system is powerful enough to capture all semantic truths of propositional logic.

Role of Hilbert Systems

Hilbert systems are important because they provide a very simple and uniform framework for formal proofs, and they are especially useful in theoretical investigations where minimal assumptions and simplicity of rules are important.

They also serve as a foundation for many developments in proof theory and logic, where the focus is on the formal properties of derivations rather than on intuitive reasoning steps.