Hilbert system

In logic and proof theory, a Hilbert system, Hilbert calculus, or Hilbert-style proof system is a type of formal proof system in which logical principles are expressed primarily by axiom schemata or axioms, and proofs use a comparatively small number of rules of inference. The terminology is not completely uniform: some authors use Hilbert system for a narrower class of calculi, while others use axiomatic system or axiomatic calculus for essentially the same style of presentation.

Hilbert systems are commonly contrasted with natural deduction and sequent calculus. A typical Hilbert presentation has many logical axiom schemata and only one or two primitive inference rules, whereas natural-deduction and sequent systems place more of the logical structure in their inference rules. Modus ponens is the characteristic rule of many propositional Hilbert calculi; first-order systems often add generalization, although it is also possible to formulate first-order logic with modus ponens as the only primitive rule.

The style is historically associated with Gottlob Frege, whose 1879 Begriffsschrift contained a highly formal axiomatic logical calculus, and with David Hilbert and his school. Hilbert and Wilhelm Ackermann's Principles of Mathematical Logic (1928) was especially influential in establishing axiomatic presentations of propositional and predicate logic.

General form

Formal deductions

Let $H$ be a Hilbert system with a collection of logical axioms or axiom schemata and a collection of inference rules. A proof in $H$ is a finite sequence of formulas

$\varphi _{1},\ldots ,\varphi _{n}$

such that every $\varphi _{i}$ is either a logical axiom (or an instance of an axiom schema), or follows from earlier formulas in the sequence by one of the inference rules. The last formula, $\varphi _{n}$, is the formula proved.

More generally, if $\Gamma$ is a set of formulas regarded as assumptions or as the non-logical axioms of a theory, a derivation from $\Gamma$ may also use members of $\Gamma$ as lines of the derivation. The notation

$\Gamma \vdash _{H}\varphi$

means that there is such a derivation whose final formula is $\varphi$. When $\Gamma$ is empty, one writes

$\vdash _{H}\varphi$,

and $\varphi$ is called a theorem of the system.

The distinction between logical axioms and proper or non-logical axioms is important in applications. The logical axioms belong to the underlying calculus, while proper axioms specify a particular mathematical theory, such as group theory, Peano arithmetic, or Zermelo–Fraenkel set theory.

Axiom schemata and substitution

Modern Hilbert systems are often presented using axiom schemata. For example,

$\varphi \to (\psi \to \varphi )$

does not denote one formula of the object language if $\varphi$ and $\psi$ are being used as metavariables. It represents every formula obtained by replacing them with well-formed formulas of the language.

An alternative is to use a finite collection of particular formulas containing propositional variables and add a primitive rule of uniform substitution. For propositional logic this rule has the form

${\frac {\varphi }{\sigma (\varphi )}}$,

where $\sigma$ uniformly replaces propositional variables by arbitrary formulas. The schematic and substitutional presentations are closely related, and both occur under the description Hilbert-style.

Historically, this distinction matters because Frege's formulas in the Begriffsschrift were not axiom schemata in the modern sense; his Roman letters functioned within Frege's own quantificational notation, and Frege separately employed a substitution procedure.

Assumptions and the deduction theorem

In a standard Hilbert derivation from assumptions, the set of assumptions is fixed while the primitive inference rules are applied. In particular, there is normally no primitive rule corresponding directly to the natural-deduction operation of assuming a formula temporarily and then discharging it.

For many Hilbert systems, the corresponding operation is supplied by the deduction theorem. In a familiar propositional Hilbert calculus,

$\Gamma \cup \{\varphi \}\vdash \psi$

if and only if

$\Gamma \vdash \varphi \to \psi$. The deduction theorem is a metatheorem about transformations of derivations, rather than a primitive inference rule. In first-order calculi containing a generalization rule, its formulation requires additional restrictions concerning variables that occur free in assumptions.

This is one important difference between Hilbert systems and natural deduction. Natural deduction typically represents the analogous move directly by implication introduction:

${\frac {\Gamma ,\varphi \vdash \psi }{\Gamma \vdash \varphi \to \psi }}$,

with the occurrence of $\varphi$ being discharged.

Propositional logic

Many different Hilbert axiomatizations of classical propositional logic are known. They can use different primitive connectives and distribute the work differently between axioms, axiom schemata, and inference rules.

A three-schema calculus

A widely used system with primitive connectives $\to$ and $\neg$ has the following axiom schemata:

(A1) $\varphi \to (\psi \to \varphi )$

(A2) $(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$

(A3) $(\neg \varphi \to \neg \psi )\to (\psi \to \varphi )$

together with the single inference rule

Modus ponens (MP): from $\varphi$ and $\varphi \to \psi$, infer $\psi$.

The same basis may instead be presented using three particular formulas with propositional variables, together with uniform substitution. Church presented such a calculus as the system $P_{2}$. Closely related three-axiom reductions of Frege's propositional calculus are due to Jan Łukasiewicz.

Example proof

As a simple example, $A\to A$ can be proved without using (A3):

1. $A\to ((B\to A)\to A)$   (instance of A1)
2. $(A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$   (instance of A2)
3. $(A\to (B\to A))\to (A\to A)$   (1, 2 by MP)
4. $A\to (B\to A)$   (instance of A1)
5. $A\to A$   (4, 3 by MP)

Such derivations illustrate a characteristic feature of Hilbert calculi: even elementary results may require several applications of axiom schemata and modus ponens. In practice, once metatheorems such as the deduction theorem and derived rules have been established, they are commonly used to abbreviate later arguments.

First-order logic

There is no unique Hilbert axiomatization of first-order logic. Equivalent calculi may employ different primitive connectives, treat equality differently, or move principles between the axiom set and the rules of inference. Two common styles are illustrated below.

A formulation with modus ponens only

Enderton gives a first-order deductive calculus in which modus ponens is the only primitive inference rule. In a language whose primitive propositional connectives are $\neg$ and $\to$ and whose primitive quantifier is $\forall$, the logical axioms are all universal generalizations of formulas belonging to the following groups:

1. Propositional tautologies. Any substitution instance of a tautology of classical propositional logic.
2. Universal instantiation:

   $\forall x\,\varphi \to \varphi [x:=t]$,

   where the term $t$ is substitutable for $x$ in $\varphi$.

3. Distribution of universal quantification over implication:

   $\forall x(\varphi \to \psi )\to (\forall x\varphi \to \forall x\psi )$.

4. Vacuous universal quantification:

   $\varphi \to \forall x\varphi$,

   where $x$ does not occur free in $\varphi$.

Here a generalization of $\theta$ means a formula

$\forall x_{1}\cdots \forall x_{n}\theta$

for some $n\geq 0$. Taking generalizations of the logical axioms makes a separate primitive generalization rule unnecessary.

If equality is included as a logical symbol, Enderton adds axiom groups for reflexivity and substitution of identicals:

1. $x=x$.
2. $x=y\to (\varphi \to \varphi ')$, where $\varphi$ is atomic and $\varphi '$ results from replacing zero or more appropriate occurrences of $x$ in $\varphi$ by $y$.

Other equivalent sets of equality axioms are common.

A formulation with generalization

Another standard presentation, used for example by Mendelson, takes the following propositional axiom schemata:

(A1) $\varphi \to (\psi \to \varphi )$

(A2) $(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$

(A3) $(\neg \psi \to \neg \varphi )\to ((\neg \psi \to \varphi )\to \psi )$

and adds the quantifier axiom schemata

(A4) $\forall x\,\varphi \to \varphi [x:=t]$, where $t$ is free for $x$ in $\varphi$;

(A5) $\forall x(\varphi \to \psi )\to (\varphi \to \forall x\psi )$, where $x$ does not occur free in $\varphi$.

The inference rules are

Modus ponens: from $\varphi$ and $\varphi \to \psi$, infer $\psi$;

Generalization: from $\varphi$, infer $\forall x\varphi$.

The restrictions in (A4) and (A5) are essential. The first prevents variable capture during substitution, while the second prevents an illicit dependency on a variable that is being quantified.

These two first-order examples illustrate the flexibility characteristic of Hilbert systems: a principle such as generalization can be represented by a primitive inference rule in one calculus and absorbed into the logical axioms of another.

Derived and defined connectives

A Hilbert calculus need not take every familiar connective as primitive. For classical propositional logic, the pair $\{\neg ,\to \}$ is functionally complete: every truth function can be expressed using only negation and implication. Thus one may define, for example,

$\varphi \lor \psi \;:=\;\neg \varphi \to \psi$,

$\varphi \land \psi \;:=\;\neg (\varphi \to \neg \psi )$.

Similarly, if $\forall$ and negation are primitive in classical first-order logic, existential quantification can be introduced by

$\exists x\,\varphi \;:=\;\neg \forall x\,\neg \varphi$.

When new notation is introduced purely by such explicit definitions, formulas containing the new symbols can be translated back into the original language. In this sense the enlarged language is a conservative extension: it does not make any new sentence of the old language provable merely by introducing the abbreviations.

Instead of treating $\land$ and $\lor$ as abbreviations, one can make them primitive and add suitable Hilbert axiom schemata. A common set includes

Conjunction

$\varphi \to (\psi \to \varphi \land \psi )$

$\varphi \land \psi \to \varphi$

$\varphi \land \psi \to \psi$

Disjunction

$\varphi \to \varphi \lor \psi$

$\psi \to \varphi \lor \psi$

$(\varphi \to \chi )\to ((\psi \to \chi )\to ((\varphi \lor \psi )\to \chi ))$.

With an appropriate proof of equivalence to their definitions, these give another conservative presentation of the same classical logic. The exact collection of schemata is conventional rather than unique.

Other logics

Hilbert systems are not restricted to classical propositional and first-order logic. They are widely used for modal logic, intuitionistic logic, relevance logic, many-valued logics, and other non-classical systems.

For example, the basic normal modal logic K has a standard Hilbert axiomatization consisting of the theorems or axioms of classical propositional logic, the modal axiom schema

$\Box (\varphi \to \psi )\to (\Box \varphi \to \Box \psi )$

and the rules modus ponens and necessitation

${\frac {\varphi }{\Box \varphi }}$.

Stronger normal modal logics are often obtained by adding further modal axiom schemata.

The balance between axioms and rules can differ considerably among non-classical Hilbert calculi. Consequently, possessing a particular number of axioms or having modus ponens as the sole rule is characteristic of many important examples, but is not a definition applying to every system described as Hilbert-style.

Historical development

Frege's Begriffsschrift

Frege's 1879 Begriffsschrift is one of the foundational works of modern formal logic and is often credited with introducing modern quantificational logic. Its logical system officially contains nine axioms. Six of them form what, in modern terminology, can be regarded as its propositional portion; the remaining axioms concern identity and generality.

In a modernized notation, the six propositional formulas are analogous to

1. $A\to (B\to A)$
2. $(C\to (B\to A))\to ((C\to B)\to (C\to A))$
3. $(D\to (B\to A))\to (B\to (D\to A))$
4. $(B\to A)\to (\neg A\to \neg B)$
5. $\neg \neg A\to A$
6. $A\to \neg \neg A$.

Frege described a form of modus ponens as his principal mode of inference, but also used operations corresponding to substitution and the introduction or movement of universal generality. His notation and conception of variables differ significantly from modern schematic presentations, so the displayed formulas are modern analogues rather than literal transcriptions of Frege's formalism.

Łukasiewicz later showed, using a modern treatment of the propositional part of Frege's system, that one of the six formulas is redundant and that the negational portion can be substantially compressed.

Hilbert and Ackermann

During the early twentieth century, Hilbert and his collaborators developed axiomatic logical calculi as part of the broader program of formalizing mathematics and studying formal proofs mathematically. The first edition of Hilbert and Ackermann's Grundzüge der theoretischen Logik appeared in 1928 and became an influential systematic presentation of propositional and predicate logic. Modern uses of terms such as Hilbert calculus and Hilbert-style system reflect this tradition, although historically related calculi also predate Hilbert in Frege's work.

Łukasiewicz and compact axiom bases

The search for small and independent axiom bases became an important part of twentieth-century investigations of propositional logic. Łukasiewicz and other members of the Lwów–Warsaw school studied numerous bases using implication, negation, equivalence, and other primitive connectives, as well as problems of independence and completeness.

Such minimality is mathematically interesting but does not determine which Hilbert calculus is most convenient in practice. Adding redundant axiom schemata or derived rules may make ordinary deductions much shorter while leaving the set of theorems unchanged.

Relation to other proof systems

Natural deduction and sequent calculus

Hilbert systems, natural deduction, and sequent calculus can often be constructed so that they prove exactly the same formulas, but they represent deductive structure differently.

In a typical Hilbert system, a line of a derivation is simply a formula, and the assumptions available to a derivation remain fixed while primitive rules are applied. Operations such as the introduction and discharge of an assumption are handled indirectly through metatheorems such as the deduction theorem.

In natural deduction, by contrast, rules are designed around the introduction and elimination behavior of logical constants. Assumptions may be introduced temporarily and subsequently discharged. Sequent calculus makes contexts explicit in sequents such as

$\Gamma \Rightarrow \Delta$,

and its logical and structural rules directly manipulate those contexts.

Consequently, Hilbert systems often have particularly compact definitions but relatively long fully expanded proofs. Natural-deduction systems are generally closer to the organization of ordinary mathematical arguments, while sequent calculi are especially useful for structural results such as cut elimination.

Frege systems in proof complexity

In proof complexity, the term Frege system has a more specific technical meaning introduced by Stephen Cook and Robert Reckhow. A Frege system is a propositional proof system based on a finite collection of sound, implicationally complete schematic inference rules.

The name honors Frege, but Frege's own Begriffsschrift calculus is not literally a Frege system in this modern technical sense, because its axioms were not given as modern substitution schemata. Standard schematic Hilbert calculi for classical propositional logic do qualify.

Cook and Reckhow's theory abstracts away from the particular choice of ordinary propositional axioms: different Frege systems are polynomially equivalent in proof strength, in the sense relevant to proof complexity.

See also

• Axiomatic system
• List of Hilbert systems
• Frege system
• Natural deduction
• Sequent calculus
• Deduction theorem
• Axiom schema
• Modus ponens
• Proof theory

Further reading

• Church, Alonzo (1956). Introduction to Mathematical Logic. Vol. 1. Princeton University Press.
• Enderton, Herbert B. (2001). A Mathematical Introduction to Logic (2nd ed.). Academic Press.
• Mendelson, Elliott (2015). Introduction to Mathematical Logic (6th ed.). CRC Press. ISBN 978-1-4822-3772-6.
• Ono, Hiroakira (2019). Proof Theory and Algebra in Logic. Springer. doi:10.1007/978-981-13-7997-0.
• Troelstra, A. S.; Schwichtenberg, H. (2000). Basic Proof Theory (2nd ed.). Cambridge University Press. ISBN 978-0-521-77911-1.