You are here
HomeHilbert system
Primary tabs
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:

(intuitionistic propositional logic)

axiom schemes:
i. $A\to(B\to A)$
ii. $(A\to(B\to C))\to((A\to B)\to(A\to C))$
iii. $A\to A\vee B$
iv. $B\to A\vee B$
v. $(A\to C)\to((B\to C)\to(A\vee B\to C))$
vi. $A\wedge B\to A$
vii. $A\wedge B\to B$
viii. $A\to(B\to(A\wedge B))$
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:
i. all of the axiom schemes above, and
ii. law of double negation: $\neg(\neg A)\to A$
iii. $\forall xA\to A[x/y]$
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:
i. modus ponens, and
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:
i. all of the axiom schemes in intuitionistic propositional logic, as well as the law of double negation, and
ii. Axiom K, or the normality axiom: $\square(A\to B)\to(\square A\to\square B)$
iii. Axiom T: $\square A\to A$
iv. Axiom 4: $\square A\to\square(\square A)$

rules of inference:
i. modus ponens, and
ii. necessitation: from $A$, we may infer $\square A$

where $A,B,C$ above are wellformed 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

Hilbert systems need not be unique for a given logical system. For example, see this link.

For a given logical system, every Hilbert system is deductively equivalent to a Gentzen system: for any axiom $A$ in a Hilbert system $H$, convert it to the sequent $\Rightarrow A$, and for any rule: from $A_{1},\ldots,A_{n}$ we may deduce $B$, convert it to the rule: from $\Delta\Rightarrow A_{1},\ldots,A_{n}$, we may infer $\Delta\Rightarrow B$.

Since axioms are semantically valid statements, the use of Hilbert systems is more about deriving other semantically valid statements, or theorems, and less about the syntactical analysis of deductions themselves. Outside of structural proof theory, deductive systems a la Hilbert style are used almost exclusively everywhere in mathematics.
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)
Mathematics Subject Classification
03F03 no label found03B99 no label found03B22 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections