Hilbert system

In logic, more specifically proof theory, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style system, Hilbert-style proof system, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of formal proof system attributed to Gottlob Frege^[1] and David Hilbert.^[2] These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

It is defined as a deductive system that generates theorems from axioms and inference rules,^[3][4][5] especially if the only inference rule is modus ponens.^[6][7] Every Hilbert system is an axiomatic system, which is used by many authors as a sole less specific term to declare their Hilbert systems,^[8][9][10] without mentioning any more specific terms. In this context, "Hilbert systems" are contrasted with natural deduction systems,^[3] in which no axioms are used, only inference rules.

While all sources that refer to an "axiomatic" logical proof system characterize it simply as a logical proof system with axioms, sources that use variants of the term "Hilbert system" sometimes define it in different ways, which will not be used in this article. For instance, Troelstra defines a "Hilbert system" as a system with axioms and with ${\displaystyle {\rightarrow }E}$ and ${\displaystyle {\forall }I}$ as the only inference rules.^[11] A specific set of axioms is also sometimes called "the Hilbert system",^[12] or "the Hilbert-style calculus".^[13] Sometimes, "Hilbert-style" is used to convey the type of axiomatic system that has its axioms given in schematic form,^[2] as in the § Schematic form of P2 below—but other sources use the term "Hilbert-style" as encompassing both systems with schematic axioms and systems with a rule of substitution,^[14] as this article does. The use of "Hilbert-style" and similar terms to describe axiomatic proof systems in logic is due to the influence of Hilbert and Ackermann's Principles of Mathematical Logic (1928).^[2]

Most variants of Hilbert systems take a characteristic tack in the way they balance a trade-off between logical axioms and rules of inference.^{[1][15][16][17]} Hilbert systems can be characterised by the choice of a large number of schemas of logical axioms and a small set of rules of inference. Systems of natural deduction take the opposite tack, including many deduction rules but very few or no axiom schemas.^[3] The most commonly studied Hilbert systems have either just one rule of inference – modus ponens, for propositional logics – or two – with generalisation, to handle predicate logics, as well – and several infinite axiom schemas. Hilbert systems for alethic modal logics, sometimes called Hilbert-Lewis systems, additionally require the necessitation rule. Some systems use a finite list of concrete formulas as axioms instead of an infinite set of formulas via axiom schemas, in which case the uniform substitution rule is required.^[18]

A characteristic feature of the many variants of Hilbert systems is that the context is not changed in any of their rules of inference, while both natural deduction and sequent calculus contain some context-changing rules.^[19] Thus, if one is interested only in the derivability of tautologies, no hypothetical judgments, then one can formalize the Hilbert system in such a way that its rules of inference contain only judgments of a rather simple form. The same cannot be done with the other two deductions systems:^{[citation needed]} as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided – not even if we want to use them just for proving derivability of tautologies.