# Hilbert system

A Hilbert system is a style (formulation) of deductive system that emphasizes the role played by the axioms in the system. Typically, a Hilbert system has many axiom schemes, but only a few, sometimes one, rules of inference  . As such, a Hilbert system is also called an axiom system. Below we list three examples of axiom systems in mathematical logic:

• axiom schemes:

1. i.

$A\to(B\to A)$

2. ii.

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

3. iii.

$A\to A\vee B$

4. iv.

$B\to A\vee B$

5. v.

$(A\to C)\to((B\to C)\to(A\vee B\to C))$

6. vi.

$A\wedge B\to A$

7. vii.

$A\wedge B\to B$

8. viii.

$A\to(B\to(A\wedge B))$

9. ix.

$\perp\to A$

• rule of inference: (modus ponens  ): from $A\to B$ and $A$, we may infer $B$

• (classical predicate logic without equality)

• axiom schemes:

1. i.

all of the axiom schemes above, and

2. ii.

law of double negation: $\neg(\neg A)\to A$

3. iii.

$\forall xA\to A[x/y]$

4. iv.

$\forall x(A\to B)\to(A\to\forall yB[x/y])$

In the last two axiom schemes, we require that $y$ is free for $x$ in $A$, and in the last axiom scheme, we also require that $x$ does not occur free in $A$.

• rules of inference:

1. i.

modus ponens, and

2. ii.

generalization: from $A$, we may infer $\forall yA[x/y]$, where $y$ is free for $x$ in $A$

• (S4 modal propositional logic)

• axiom schemes:

1. i.

all of the axiom schemes in intuitionistic propositional logic, as well as the law of double negation, and

2. ii.

Axiom K, or the normality axiom: $\square(A\to B)\to(\square A\to\square B)$

3. iii.

Axiom T: $\square A\to A$

4. iv.

Axiom 4: $\square A\to\square(\square A)$

• rules of inference:

1. i.

modus ponens, and

2. ii.

necessitation: from $A$, we may infer $\square A$

where $A,B,C$ above are well-formed formulas, $x,y$ are individual variables, and $\to,\vee,\wedge$ are binary, $\square$ unary, and $\perp$ nullary logical connectives in the respective logical systems. The connective $\neg$ may be defined as $\neg A:=A\to\perp$ for any formula   $A$.

Remarks

## References

• 1 H. Enderton: A Mathematical Introduction to Logic, Academic Press, San Diego (1972).
• 2 A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press (2000)
• 3 B. F. Chellas, Modal Logic, An Introduction, Cambridge University Press (1980)
 Title Hilbert system Canonical name HilbertSystem Date of creation 2013-03-22 19:13:14 Last modified on 2013-03-22 19:13:14 Owner CWoo (3771) Last modified by CWoo (3771) Numerical id 15 Author CWoo (3771) Entry type Definition Classification msc 03F03 Classification msc 03B99 Classification msc 03B22 Synonym axiom system Related topic GentzenSystem Defines generalization Defines necessitation Defines double negation