Hilbert system
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.
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.
[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.
[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.
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.
These formal deductions are meant to mirror natural-language proofs, although they are far more detailed.
Hilbert systems are characterized by the use of numerous schemas of logical axioms.
One of them, the § Schematic form of P2, is also considered a Frege system.
Axiomatic proofs have been used in mathematics since the famous Ancient Greek textbook, Euclid's Elements of Geometry, c. 300 BC.
[9][20] Frege's system used only implication and negation as connectives,[21] and it had six axioms,[20] which were these ones:[22][23] These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truth-functional propositional logic.
Hence, using Greek letters to represent schemas (metalogical variables that may stand for any well-formed formulas), the axioms are given as:[9][25] The schematic version of P2 is attributed to John von Neumann,[20] and is used in the Metamath "set.mm" formal proof database.
[25] In fact, the very idea of using axiom schemas to replace the rule of substitution is attributed to von Neumann.
[26] The schematic version of P2 has also been attributed to Hilbert, and named
We describe here a Hilbert system with nine axioms and just the rule modus ponens, which we call the one-rule axiomatisation and which describes classical equational logic.
We deal with a minimal language for this logic, where formulas use only the connectives
Later we show how the system can be extended to include additional logical connectives, such as
Minimal logic is achieved either by adding instead the axiom P4m, or by defining
The next three logical axiom schemas provide ways to add, manipulate, and remove universal quantifiers.
These three additional rules extend the propositional system to axiomatise classical predicate logic.
The final axiom schemas are required to work with formulas involving the equality symbol.
It is common to include in a Hilbert system only axioms for the logical operators implication and negation towards functional completeness.
Given these axioms, it is possible to form conservative extensions of the deduction theorem that permit the use of additional connectives.
These extensions are called conservative because if a formula φ involving new connectives is rewritten as a logically equivalent formula θ involving only negation, implication, and universal quantification, then φ is derivable in the extended system if and only if θ is derivable in the original system.
