# Hilbert system

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Hilbert_system
> Markdown URL: https://mediated.wiki/source/Hilbert_system.md
> Source: https://en.wikipedia.org/wiki/Hilbert_system
> Source revision: 1355538887
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

System of formal deduction in logic

In [logic](/source/Logic), more specifically [proof theory](/source/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](/source/Formal_proof) [system](/source/Proof_calculus) attributed to [Gottlob Frege](/source/Gottlob_Frege)[1] and [David Hilbert](/source/David_Hilbert).[2] These [deductive systems](/source/Deductive_system) are most often studied for [first-order logic](/source/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 postulated inference rule is [modus ponens](/source/Modus_ponens).[6][7] Every Hilbert system is an [axiomatic system](/source/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](/source/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](/source/Anne_Sjerp_Troelstra) defines a "Hilbert system" as a system with axioms *and* with → E {\displaystyle {\rightarrow }E} and ∀ I {\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](#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](/source/Wilhelm_Ackermann)'s *[Principles of Mathematical Logic](/source/Principles_of_Mathematical_Logic)* (1928).[2]

Most variants of Hilbert systems take a characteristic tack in the way they balance a [trade-off](/source/Trade-off) between [logical axioms](/source/Logical_axiom) and [rules of inference](/source/Rule_of_inference).[1][6][15][11] Hilbert systems can be characterised by the choice of a large number of [schemas](/source/Axiom_schema) of logical axioms and a small set of [rules of inference](/source/Rule_of_inference). Systems of [natural deduction](/source/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](/source/Modus_ponens), for [propositional logics](/source/Propositional_logic) – or two – with [generalisation](/source/Universal_generalization), to handle [predicate logics](/source/Predicate_logic), as well – and several infinite axiom schemas. Hilbert systems for alethic [modal logics](/source/Modal_logic), sometimes called [Hilbert-Lewis systems](https://en.wikipedia.org/w/index.php?title=Hilbert-Lewis_system&action=edit&redlink=1), additionally require the [necessitation rule](https://en.wikipedia.org/w/index.php?title=Necessitation_rule&action=edit&redlink=1). 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](https://en.wikipedia.org/w/index.php?title=Uniform_substitution&action=edit&redlink=1) rule is required.[14]

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](/source/Natural_deduction) and [sequent calculus](/source/Sequent_calculus) contain some context-changing rules.[16] Thus, if one is interested only in the derivability of [tautologies](/source/Tautology_(logic)), no hypothetical judgments, then one can formalize the Hilbert system in such a way that its rules of inference contain only [judgments](/source/Judgment_(mathematical_logic)) of a rather simple form. The same cannot be done with the other two deductions systems:[*[citation needed](https://en.wikipedia.org/wiki/Wikipedia: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.

## Formal deductions

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (August 2024) (Learn how and when to remove this message)

A graphic representation of the deduction system

In a Hilbert system, a **formal deduction** (or **[proof](/source/Formal_proof)**) is a finite sequence of formulas in which each formula is either an axiom or is obtained from previous formulas by a rule of inference.[17] These formal deductions are meant to mirror natural-language proofs, although they are far more detailed.[18]

Suppose Γ {\displaystyle \Gamma } is a set of formulas, considered as **hypotheses**. For example, Γ {\displaystyle \Gamma } could be a set of axioms for [group theory](/source/Group_theory) or [set theory](/source/Set_theory). The notation Γ ⊢ ϕ {\displaystyle \Gamma \vdash \phi } means that there is a deduction that ends with ϕ {\displaystyle \phi } using as axioms only **logical axioms** and elements of Γ {\displaystyle \Gamma } .[19] Thus, informally, Γ ⊢ ϕ {\displaystyle \Gamma \vdash \phi } means that ϕ {\displaystyle \phi } is provable assuming all the formulas in Γ {\displaystyle \Gamma } .

Hilbert systems are characterized by the use of numerous schemas of **logical axioms**. An [axiom schema](/source/Axiom_schema) is an infinite set of axioms obtained by substituting all formulas of some form into a specific pattern.[20] The set of logical axioms includes not only those axioms generated from this pattern, but also any generalization of one of those axioms.[21] A generalization of a formula is obtained by prefixing zero or more universal quantifiers on the formula; for example ∀ y ( ∀ x P x y → P t y ) {\displaystyle \forall y(\forall xPxy\to Pty)} is a generalization of ∀ x P x y → P t y {\displaystyle \forall xPxy\to Pty} .

## Propositional logic

The following are some Hilbert systems that have been used in [propositional logic](/source/Propositional_logic). One of them, the [§ Schematic form of P2](#Schematic_form_of_P2), is also considered a [Frege system](/source/Frege_system).

### Frege's *Begriffsschrift*

Axiomatic proofs have been used in mathematics since the famous [Ancient Greek](/source/Ancient_Greek) textbook, [Euclid](/source/Euclid)'s *[Elements of Geometry](/source/Euclid's_Elements)*, c. 300 BC. But the first known [fully formalized](/source/Formal_system) proof system that thereby qualifies as a Hilbert system dates back to [Gottlob Frege](/source/Gottlob_Frege)'s [1879](/source/1879) *[Begriffsschrift](/source/Begriffsschrift)*.[9][22] Frege's system used only [implication](/source/Material_conditional) and [negation](/source/Negation) as connectives,[23] and it had six axioms,[22] which were these ones:[24][25]

- Proposition 1: a ⊃ ( b ⊃ a ) {\displaystyle a\supset (b\supset a)}

- Proposition 2: ( c ⊃ ( b ⊃ a ) ) ⊃ ( ( c ⊃ b ) ⊃ ( c ⊃ a ) ) {\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}

- Proposition 8: ( d ⊃ ( b ⊃ a ) ) ⊃ ( b ⊃ ( d ⊃ a ) ) {\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}

- Proposition 28: ( b ⊃ a ) ⊃ ( ¬ a ⊃ ¬ b ) {\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}

- Proposition 31: ¬ ¬ a ⊃ a {\displaystyle \neg \neg a\supset a}

- Proposition 41: a ⊃ ¬ ¬ a {\displaystyle a\supset \neg \neg a}

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.[24]

### Łukasiewicz's P2

[Jan Łukasiewicz](/source/Jan_%C5%81ukasiewicz) showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence C C N p N q C q p {\displaystyle CCNpNqCqp} ".[25] Which, taken out of Łukasiewicz's [Polish notation](/source/Polish_notation) into modern notation, means ( ¬ p → ¬ q ) → ( q → p ) {\displaystyle (\neg p\rightarrow \neg q)\rightarrow (q\rightarrow p)} . Hence, Łukasiewicz is credited[22] with this system of three axioms:

- p → ( q → p ) {\displaystyle p\to (q\to p)}

- ( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) ) {\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}

- ( ¬ p → ¬ q ) → ( q → p ) {\displaystyle (\neg p\to \neg q)\to (q\to p)}

Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule.[22] The exact same system was given (with an explicit substitution rule) by [Alonzo Church](/source/Alonzo_Church),[26] who referred to it as the system P2,[26][27] and helped popularize it.[27]

### Schematic form of P2

One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemas (metalogical variables that may stand for any [well-formed formulas](/source/Well-formed_formula)), the axioms are given as:[9][27]

- φ → ( ψ → φ ) {\displaystyle \varphi \to (\psi \to \varphi )}

- ( φ → ( ψ → χ ) ) → ( ( φ → ψ ) → ( φ → χ ) ) {\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}

- ( ¬ φ → ¬ ψ ) → ( ψ → φ ) {\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}

The schematic version of P2 is attributed to [John von Neumann](/source/John_von_Neumann),[22] and is used in the [Metamath](/source/Metamath) "set.mm" formal proof database.[27] In fact, the very idea of using axiom schemas to replace the rule of substitution is attributed to von Neumann.[28] The schematic version of P2 has also been attributed to [Hilbert](/source/David_Hilbert), and named H {\displaystyle {\mathcal {H}}} in this context.[29]

Systems for propositional logic whose inference rules are schematic are also called [Frege systems](/source/Frege_system); as the authors that originally defined the term "Frege system"[30] note, this actually excludes Frege's own system, given above, since it had axioms instead of axiom schemas.[28]

#### Proof example in P2

As an example, a proof of A → A {\displaystyle A\to A} in P2 is given below. First, the axioms are given names:

- (A1) ( p → ( q → p ) ) {\displaystyle (p\to (q\to p))}

- (A2) ( ( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) ) ) {\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}

- (A3) ( ( ¬ p → ¬ q ) → ( q → p ) ) {\displaystyle ((\neg p\to \neg q)\to (q\to p))}

And the proof is as follows:

1. A → ( ( B → A ) → A ) {\displaystyle A\to ((B\to A)\to A)} (instance of (A1))

1. ( A → ( ( B → A ) → A ) ) → ( ( A → ( B → A ) ) → ( A → A ) ) {\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))} (instance of (A2))

1. ( A → ( B → A ) ) → ( A → A ) {\displaystyle (A\to (B\to A))\to (A\to A)} (from (1) and (2) by [modus ponens](/source/Modus_ponens))

1. A → ( B → A ) {\displaystyle A\to (B\to A)} (instance of (A1))

1. A → A {\displaystyle A\to A} (from (4) and (3) by modus ponens)

## Predicate logic (example system)

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (August 2024) (Learn how and when to remove this message)

There is an unlimited amount of axiomatisations of predicate logic, since for any logic there is freedom in choosing axioms and rules that characterise that logic. 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 ¬ {\displaystyle \lnot } and → {\displaystyle \to } and only the quantifier ∀ {\displaystyle \forall } . Later we show how the system can be extended to include additional logical connectives, such as ∧ {\displaystyle \land } and ∨ {\displaystyle \lor } , without enlarging the class of deducible formulas.

The first four logical axiom schemas allow (together with modus ponens) for the manipulation of logical connectives.

- P1. ϕ → ϕ {\displaystyle \phi \to \phi }

- P2. ϕ → ( ψ → ϕ ) {\displaystyle \phi \to \left(\psi \to \phi \right)}

- P3. ( ϕ → ( ψ → ξ ) ) → ( ( ϕ → ψ ) → ( ϕ → ξ ) ) {\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}

- P4. ( ¬ ϕ → ¬ ψ ) → ( ψ → ϕ ) {\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}

The axiom P1 is redundant, as it follows from P3, P2 and modus ponens (see [proof](#Proof_example_in_P2)). These axioms describe [classical propositional logic](/source/Classical_propositional_logic); without axiom P4 we get [positive implicational logic](/source/Implicational_propositional_calculus). [Minimal logic](/source/Minimal_logic) is achieved either by adding instead the axiom P4m, or by defining ¬ ϕ {\displaystyle \lnot \phi } as ϕ → ⊥ {\displaystyle \phi \to \bot } .

- P4m. ( ϕ → ψ ) → ( ( ϕ → ¬ ψ ) → ¬ ϕ ) {\displaystyle \left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)}

[Intuitionistic logic](/source/Intuitionistic_logic) is achieved by adding axioms P4i and P5i to positive implicational logic, or by adding axiom P5i to minimal logic. Both P4i and P5i are theorems of classical propositional logic.

- P4i. ( ϕ → ¬ ϕ ) → ¬ ϕ {\displaystyle \left(\phi \to \lnot \phi \right)\to \lnot \phi }

- P5i. ¬ ϕ → ( ϕ → ψ ) {\displaystyle \lnot \phi \to \left(\phi \to \psi \right)}

Note that these are axiom schemas, which represent infinitely many specific instances of axioms. For example, P1 might represent the particular axiom instance p → p {\displaystyle p\to p} , or it might represent ( p → q ) → ( p → q ) {\displaystyle \left(p\to q\right)\to \left(p\to q\right)} : the ϕ {\displaystyle \phi } is a place where any formula can be placed. A variable such as this that ranges over formulae is called a 'schematic variable'.

With a second rule of [uniform substitution](https://en.wikipedia.org/w/index.php?title=Uniform_substitution&action=edit&redlink=1) (US), we can change each of these axiom schemas into a single axiom, replacing each schematic variable by some propositional variable that isn't mentioned in any axiom to get what we call the substitutional axiomatisation. Both formalisations have variables, but where the one-rule axiomatisation has schematic variables that are outside the logic's language, the substitutional axiomatisation uses propositional variables that do the same work by expressing the idea of a variable ranging over formulae with a rule that uses substitution.

- US. Let ϕ ( p ) {\displaystyle \phi (p)} be a formula with one or more instances of the propositional variable p {\displaystyle p} , and let ψ {\displaystyle \psi } be another formula. Then from ϕ ( p ) {\displaystyle \phi (p)} , infer ϕ ( ψ ) {\displaystyle \phi (\psi )} .

The next three logical axiom schemas provide ways to add, manipulate, and remove universal quantifiers.

- Q5. ∀ x ( ϕ ) → ϕ [ x := t ] {\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]} where *t* may be substituted for *x* in ϕ {\displaystyle \,\!\phi }

- Q6. ∀ x ( ϕ → ψ ) → ( ∀ x ( ϕ ) → ∀ x ( ψ ) ) {\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}

- Q7. ϕ → ∀ x ( ϕ ) {\displaystyle \phi \to \forall x\left(\phi \right)} where *x* is not free in ϕ {\displaystyle \phi } .

These three additional rules extend the propositional system to axiomatise [classical predicate logic](/source/Classical_predicate_logic). Likewise, these three rules extend system for intuitionistic propositional logic (with P1-3 and P4i and P5i) to [intuitionistic predicate logic](https://en.wikipedia.org/w/index.php?title=Intuitionistic_predicate_logic&action=edit&redlink=1).

Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation, in which case the rules Q6 and Q7 are redundant.

- [Generalization](/source/Universal_generalization): If Γ ⊢ ϕ {\displaystyle \Gamma \vdash \phi } and *x* does not occur free in any formula of Γ {\displaystyle \Gamma } then Γ ⊢ ∀ x ϕ {\displaystyle \Gamma \vdash \forall x\phi } .

The final axiom schemas are required to work with formulas involving the equality symbol.

- I8. x = x {\displaystyle x=x} for every variable *x*.

- I9. ( x = y ) → ( ϕ [ z := x ] → ϕ [ z := y ] ) {\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}

## Conservative extensions

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (March 2024) (Learn how and when to remove this message)

It is common to include in a Hilbert system only axioms for the logical operators implication and negation towards [functional completeness](/source/Functional_completeness). Given these axioms, it is possible to form [conservative extensions](/source/Conservative_extension) of the [deduction theorem](/source/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](/source/Logical_equivalence) 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. When fully extended, a Hilbert system will resemble more closely a system of [natural deduction](/source/Natural_deduction).

### Existential quantification

- Introduction

- ∀ x ( ϕ → ∃ y ( ϕ [ x := y ] ) ) {\displaystyle \forall x(\phi \to \exists y(\phi [x:=y]))}

- Elimination

- ∀ x ( ϕ → ψ ) → ( ∃ x ( ϕ ) → ψ ) {\displaystyle \forall x(\phi \to \psi )\to (\exists x(\phi )\to \psi )} where x {\displaystyle x} is not a [free variable](/source/Free_variable) of ψ {\displaystyle \psi } .

### Conjunction and disjunction

- Conjunction introduction and elimination

- introduction: α → ( β → α ∧ β ) {\displaystyle \alpha \to (\beta \to \alpha \land \beta )}

- elimination left: α ∧ β → α {\displaystyle \alpha \wedge \beta \to \alpha }

- elimination right: α ∧ β → β {\displaystyle \alpha \wedge \beta \to \beta }

- Disjunction introduction and elimination

- introduction left: α → α ∨ β {\displaystyle \alpha \to \alpha \vee \beta }

- introduction right: β → α ∨ β {\displaystyle \beta \to \alpha \vee \beta }

- elimination: ( α → γ ) → ( ( β → γ ) → α ∨ β → γ ) {\displaystyle (\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )}

## See also

- [List of Hilbert systems](/source/List_of_Hilbert_systems)

- [Natural deduction](/source/Natural_deduction)

- [Sequent calculus](/source/Sequent_calculus)

## Notes

1. ^ [***a***](#cite_ref-Máté_&_Ruzsa_1997_1-0) [***b***](#cite_ref-Máté_&_Ruzsa_1997_1-1) Máté & Ruzsa 1997:129

1. ^ [***a***](#cite_ref-:1_2-0) [***b***](#cite_ref-:1_2-1) [***c***](#cite_ref-:1_2-2) Smith, Peter (2013-02-21). [*An Introduction to Gödel's Theorems*](https://books.google.com/books?id=-SBpYKebkJMC). Cambridge University Press. p. 10. [ISBN](/source/ISBN_(identifier)) [978-1-107-02284-3](https://en.wikipedia.org/wiki/Special:BookSources/978-1-107-02284-3).

1. ^ [***a***](#cite_ref-:2_3-0) [***b***](#cite_ref-:2_3-1) [***c***](#cite_ref-:2_3-2) Restall, Greg (2002-09-11). [*An Introduction to Substructural Logics*](https://books.google.com/books?id=Z3AsBgAAQBAJ). Routledge. pp. 73–74. [ISBN](/source/ISBN_(identifier)) [978-1-135-11131-1](https://en.wikipedia.org/wiki/Special:BookSources/978-1-135-11131-1).

1. **[^](#cite_ref-4)** Gaifman, Haim (2002). ["A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness"](https://www.columbia.edu/~hg17/ViewMathLogic/view1-deductive-system.pdf) (PDF). *Columbia*. Retrieved 2024-08-19.

1. **[^](#cite_ref-5)** Benthem, Johan van; Gupta, Amitabha; [Parikh, Rohit](/source/Rohit_Parikh) (2011-04-02). [*Proof, Computation and Agency: Logic at the Crossroads*](https://books.google.com/books?id=OnIeiWWAfpkC). Springer Science & Business Media. p. 41. [ISBN](/source/ISBN_(identifier)) [978-94-007-0080-2](https://en.wikipedia.org/wiki/Special:BookSources/978-94-007-0080-2).

1. ^ [***a***](#cite_ref-Bacon_424_6-0) [***b***](#cite_ref-Bacon_424_6-1) Bacon, Andrew (2023-09-29). [*A Philosophical Introduction to Higher-order Logics*](https://books.google.com/books?id=qa3WEAAAQBAJ). Taylor & Francis. p. 424. [ISBN](/source/ISBN_(identifier)) [978-1-000-92575-3](https://en.wikipedia.org/wiki/Special:BookSources/978-1-000-92575-3).

1. **[^](#cite_ref-7)** Eijck, Jan van (1991-02-26). [*Logics in AI: European Workshop JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990. Proceedings*](https://books.google.com/books?id=ejgMbaqLfNsC). Springer Science & Business Media. p. 113. [ISBN](/source/ISBN_(identifier)) [978-3-540-53686-4](https://en.wikipedia.org/wiki/Special:BookSources/978-3-540-53686-4).

1. **[^](#cite_ref-8)** Haack, Susan (1978-07-27). [*Philosophy of Logics*](https://books.google.com/books?id=0GsZ8SBQrUcC). Cambridge University Press. p. 19. [ISBN](/source/ISBN_(identifier)) [978-0-521-29329-7](https://en.wikipedia.org/wiki/Special:BookSources/978-0-521-29329-7).

1. ^ [***a***](#cite_ref-BostockIntermediate_9-0) [***b***](#cite_ref-BostockIntermediate_9-1) [***c***](#cite_ref-BostockIntermediate_9-2) Bostock, David (1997). *Intermediate logic*. Oxford : New York: Clarendon Press; Oxford University Press. pp. 4–5, 8–13, 18–19, 22, 27, 29, 191, 194. [ISBN](/source/ISBN_(identifier)) [978-0-19-875141-0](https://en.wikipedia.org/wiki/Special:BookSources/978-0-19-875141-0).

1. **[^](#cite_ref-10)** Lucas, J. R. (2018-10-10). [*A Treatise on Time and Space*](https://books.google.com/books?id=ymsPEAAAQBAJ). Routledge. p. 152. [ISBN](/source/ISBN_(identifier)) [978-0-429-68517-0](https://en.wikipedia.org/wiki/Special:BookSources/978-0-429-68517-0).

1. ^ [***a***](#cite_ref-Basic_Proof_Theory_11-0) [***b***](#cite_ref-Basic_Proof_Theory_11-1) Troelstra, A. S.; Schwichtenberg, H. (2000). [*Basic Proof Theory*](https://www.cambridge.org/core/books/basic-proof-theory/928508F797214A017D245A1FB67CCCD9). Cambridge Tracts in Theoretical Computer Science (2 ed.). Cambridge: Cambridge University Press. p. 51. [doi](/source/Doi_(identifier)):[10.1017/cbo9781139168717](https://doi.org/10.1017%2Fcbo9781139168717). [ISBN](/source/ISBN_(identifier)) [978-0-521-77911-1](https://en.wikipedia.org/wiki/Special:BookSources/978-0-521-77911-1).

1. **[^](#cite_ref-12)** ["Introduction to Logic - Chapter 4"](http://intrologic.stanford.edu/chapters/chapter_04.html). *intrologic.stanford.edu*. Retrieved 2024-08-16.

1. **[^](#cite_ref-13)** Buss, S. R. (1998-07-09). [*Handbook of Proof Theory*](https://books.google.com/books?id=MfTMDeCq7ukC). Elsevier. pp. 552–553. [ISBN](/source/ISBN_(identifier)) [978-0-08-053318-6](https://en.wikipedia.org/wiki/Special:BookSources/978-0-08-053318-6).

1. ^ [***a***](#cite_ref-Ono_5_14-0) [***b***](#cite_ref-Ono_5_14-1) Ono, Hiroakira (2019-08-02). [*Proof Theory and Algebra in Logic*](https://books.google.com/books?id=SR2nDwAAQBAJ). Springer. p. 5. [ISBN](/source/ISBN_(identifier)) [978-981-13-7997-0](https://en.wikipedia.org/wiki/Special:BookSources/978-981-13-7997-0).

1. **[^](#cite_ref-15)** Eijck, Jan van (1991-02-26). [*Logics in AI: European Workshop JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990. Proceedings*](https://books.google.com/books?id=ejgMbaqLfNsC). Springer Science & Business Media. p. 113. [ISBN](/source/ISBN_(identifier)) [978-3-540-53686-4](https://en.wikipedia.org/wiki/Special:BookSources/978-3-540-53686-4).

1. **[^](#cite_ref-16)** Gabbay, Dov M.; Guenthner, Franz (2013-03-14). [*Handbook of Philosophical Logic*](https://books.google.com/books?id=54LrCAAAQBAJ). Springer Science & Business Media. p. 201. [ISBN](/source/ISBN_(identifier)) [978-94-017-0458-8](https://en.wikipedia.org/wiki/Special:BookSources/978-94-017-0458-8).

1. **[^](#cite_ref-17)** Kute, Tushar B. ["Hilbert Systems"](https://www3.cs.stonybrook.edu/~cse371/chapter8.pdf) (PDF). *Stony Brook University*. Retrieved 21 November 2025.

1. **[^](#cite_ref-18)** Stonybrook. ["Chapter 8: Hilbert Systems"](https://www3.cs.stonybrook.edu/~cse371/chapter8.pdf) (PDF). *Stony Brook University*. Retrieved 21 November 2025.

1. **[^](#cite_ref-19)** Kute, Tushar B. ["Hilbert Systems"](https://www3.cs.stonybrook.edu/~cse371/chapter8.pdf) (PDF). *Stony Brook University*. Retrieved 21 November 2025.

1. **[^](#cite_ref-20)** Goertzel, Ben. ["Deduction in First-Order Logic"](https://www.goertzel.org/RWR.pdf) (PDF). *Goertzel.org*. Retrieved 21 November 2025.

1. **[^](#cite_ref-21)** Kute, Tushar B. ["Hilbert Systems"](https://www3.cs.stonybrook.edu/~cse371/chapter8.pdf) (PDF). *Stony Brook University*. Retrieved 21 November 2025.

1. ^ [***a***](#cite_ref-:44_22-0) [***b***](#cite_ref-:44_22-1) [***c***](#cite_ref-:44_22-2) [***d***](#cite_ref-:44_22-3) [***e***](#cite_ref-:44_22-4) Smullyan, Raymond M. (2014-07-23). [*A Beginner's Guide to Mathematical Logic*](https://books.google.com/books?id=n6S-AwAAQBAJ). Courier Corporation. pp. 102–103. [ISBN](/source/ISBN_(identifier)) [978-0-486-49237-7](https://en.wikipedia.org/wiki/Special:BookSources/978-0-486-49237-7).

1. **[^](#cite_ref-SEP_PropositionalLogic_23-0)** Franks, Curtis (2023), ["Propositional Logic"](https://plato.stanford.edu/archives/fall2023/entries/logic-propositional/), in Zalta, Edward N.; Nodelman, Uri (eds.), *The Stanford Encyclopedia of Philosophy* (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 2024-03-22

1. ^ [***a***](#cite_ref-:45_24-0) [***b***](#cite_ref-:45_24-1) Mendelsohn, Richard L. (2005-01-10). [*The Philosophy of Gottlob Frege*](https://books.google.com/books?id=G6_90xFwUbUC). Cambridge University Press. p. 185. [ISBN](/source/ISBN_(identifier)) [978-1-139-44403-3](https://en.wikipedia.org/wiki/Special:BookSources/978-1-139-44403-3).

1. ^ [***a***](#cite_ref-:46_25-0) [***b***](#cite_ref-:46_25-1) Łukasiewicz, Jan (1970). [*Jan Lukasiewicz: Selected Works*](https://books.google.com/books?id=Jb_zOwAACAAJ). North-Holland. p. 136.

1. ^ [***a***](#cite_ref-:47_26-0) [***b***](#cite_ref-:47_26-1) Church, Alonzo (1996). [*Introduction to Mathematical Logic*](https://books.google.com/books?id=JDLQOMKbdScC). Princeton University Press. p. 119. [ISBN](/source/ISBN_(identifier)) [978-0-691-02906-1](https://en.wikipedia.org/wiki/Special:BookSources/978-0-691-02906-1).

1. ^ [***a***](#cite_ref-:48_27-0) [***b***](#cite_ref-:48_27-1) [***c***](#cite_ref-:48_27-2) [***d***](#cite_ref-:48_27-3) ["Proof Explorer - Home Page - Metamath"](https://us.metamath.org/mpegif/mmset.html#scaxioms). *us.metamath.org*. Retrieved 2024-07-02.

1. ^ [***a***](#cite_ref-:12_28-0) [***b***](#cite_ref-:12_28-1) Cook, Stephen A.; Reckhow, Robert A. (1979). ["The relative efficiency of propositional proof systems"](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/relative-efficiency-of-propositional-proof-systems/218048250981F835B4B2A4080205A0BA). *The Journal of Symbolic Logic*. **44** (1): 39. [doi](/source/Doi_(identifier)):[10.2307/2273702](https://doi.org/10.2307%2F2273702). [ISSN](/source/ISSN_(identifier)) [0022-4812](https://search.worldcat.org/issn/0022-4812). [JSTOR](/source/JSTOR_(identifier)) [2273702](https://www.jstor.org/stable/2273702).

1. **[^](#cite_ref-:49_29-0)** Walicki, Michał (2017). *Introduction to mathematical logic* (Extended ed.). New Jersey: World Scientific. p. 126. [ISBN](/source/ISBN_(identifier)) [978-981-4719-95-7](https://en.wikipedia.org/wiki/Special:BookSources/978-981-4719-95-7).

1. **[^](#cite_ref-:0_30-0)** Pudlák, Pavel; Buss, Samuel R. (1995). ["How to lie without being (easily) convicted and the lengths of proofs in propositional calculus"](https://link.springer.com/chapter/10.1007/BFb0022253). In Pacholski, Leszek; Tiuryn, Jerzy (eds.). *Computer Science Logic*. Lecture Notes in Computer Science. Vol. 933. Berlin, Heidelberg: Springer. p. 152. [doi](/source/Doi_(identifier)):[10.1007/BFb0022253](https://doi.org/10.1007%2FBFb0022253). [ISBN](/source/ISBN_(identifier)) [978-3-540-49404-1](https://en.wikipedia.org/wiki/Special:BookSources/978-3-540-49404-1).

## References

- Curry, Haskell B.; Robert Feys (1958). *Combinatory Logic Vol. I*. Vol. 1. Amsterdam: North Holland.

- Monk, J. Donald (1976). [*Mathematical Logic*](https://archive.org/details/mathematicallogi00jdon). Graduate Texts in Mathematics. Berlin, New York: [Springer-Verlag](/source/Springer-Verlag). [ISBN](/source/ISBN_(identifier)) [978-0-387-90170-1](https://en.wikipedia.org/wiki/Special:BookSources/978-0-387-90170-1).

- Ruzsa, Imre; Máté, András (1997). *Bevezetés a modern logikába* (in Hungarian). Budapest: Osiris Kiadó.

- Tarski, Alfred (1990). *Bizonyítás és igazság* (in Hungarian). Budapest: Gondolat. It is a Hungarian translation of [Alfred Tarski](/source/Alfred_Tarski)'s selected papers on [semantic theory of truth](/source/Semantic_theory_of_truth).

- David Hilbert (1927) "The foundations of mathematics", translated by Stephan Bauer-Menglerberg and Dagfinn Føllesdal (pp. 464–479). in: - van Heijenoort, Jean (1967). [*From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931*](https://archive.org/details/fromfregetogodel0000vanh) (3rd printing 1976 ed.). Cambridge MA: Harvard University Press. [ISBN](/source/ISBN_(identifier)) [0-674-32449-8](https://en.wikipedia.org/wiki/Special:BookSources/0-674-32449-8). - Hilbert's 1927, Based on an earlier 1925 "foundations" lecture (pp. 367–392), presents his 17 axioms—axioms of implication #1-4, axioms about & and V #5-10, axioms of negation #11-12, his logical ε-axiom #13, axioms of equality #14-15, and axioms of number #16-17—along with the other necessary elements of his Formalist "proof theory"—e.g. induction axioms, recursion axioms, etc.; he also offers up a spirited defense against L.E.J. Brouwer's Intuitionism. Also see Hermann Weyl's (1927) comments and rebuttal (pp. 480–484), Paul Bernay's (1927) appendix to Hilbert's lecture (pp. 485–489) and Luitzen Egbertus Jan Brouwer's (1927) response (pp. 490–495)

- Kleene, Stephen Cole (1952). *Introduction to Metamathematics* (10th impression with 1971 corrections ed.). Amsterdam NY: North Holland Publishing Company. [ISBN](/source/ISBN_(identifier)) [0-7204-2103-9](https://en.wikipedia.org/wiki/Special:BookSources/0-7204-2103-9). {{[cite book](https://en.wikipedia.org/wiki/Template:Cite_book)}}: ISBN / Date incompatibility ([help](https://en.wikipedia.org/wiki/Help:CS1_errors#invalid_isbn_date)) - See in particular Chapter IV Formal System (pp. 69–85) wherein Kleene presents subchapters §16 Formal symbols, §17 Formation rules, §18 Free and bound variables (including substitution), §19 Transformation rules (e.g. modus ponens) -- and from these he presents 21 "postulates"—18 axioms and 3 "immediate-consequence" relations divided as follows: Postulates for the propostional calculus #1-8, Additional postulates for the predicate calculus #9-12, and Additional postulates for number theory #13-21.

## External links

- Gaifman, Haim. ["A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness"](https://www.columbia.edu/~hg17/ViewMathLogic/view1-deductive-system.pdf) (PDF).

- Farmer, W. M. ["Propositional logic"](http://imps.mcmaster.ca/courses/SE-2F03-05/slides/02-prop-logic.pdf) (PDF). It describes (among others) a specific Hilbert-style proof system (that is restricted to [propositional calculus](/source/Propositional_calculus)).

v t e Mathematical logic General Axiom list Cardinality First-order logic Formal proof Formal semantics Foundations of mathematics Information theory Lemma Logical consequence Model Theorem Theory Type theory Theorems (list), paradoxes Gödel's completeness – incompleteness theorems Tarski's undefinability Banach–Tarski paradox Cantor's theorem – paradox – diagonal argument Compactness Halting problem Lindström's Löwenheim–Skolem Russell's paradox Logics Traditional Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram Propositional Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞ Predicate First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus Set theory Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities Types of sets Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann Maps, cardinality Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary Theories Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive Formal systems (list), language, syntax Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list Example axiomatic systems (list) of true arithmetic Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry Euclidean Elements Hilbert's Tarski's non-Euclidean Principia Mathematica Proof theory Formal proof Natural deduction Logical consequence Rule of inference Sequent calculus Theorem Systems axiomatic deductive Hilbert list Complete theory Independence (from ZFC) Proof of impossibility Ordinal analysis Reverse mathematics Self-verifying theories Model theory Interpretation function of models Model atomic equivalence finite prime saturated spectrum submodel Non-standard model of non-standard arithmetic Diagram elementary Categorical theory Model complete theory Satisfiability Semantics of logic Strength Theories of truth semantic Tarski's Kripke's T-schema Transfer principle Truth predicate Truth value Type Ultraproduct Validity Computability theory Church encoding Church–Turing thesis Computably enumerable Computable function Computable set Decision problem decidable undecidable P NP P versus NP problem Kolmogorov complexity Lambda calculus Primitive recursive function Recursion Recursive set Turing machine Type theory Related Abstract logic Algebraic logic Automated theorem proving Category theory Concrete/Abstract category Category of sets History of logic History of mathematical logic timeline Logicism Mathematical object Philosophy of mathematics Supertask Mathematics portal

v t e Major topics in Foundations of Mathematics Mathematical logic Peano axioms Mathematical induction Formal system Axiomatic system Hilbert system Natural deduction Mathematical proof Model theory Mathematical constructivism Modal logic List of mathematical logic topics Set theory Set Naive set theory Axiomatic set theory Zermelo set theory Zermelo–Fraenkel set theory Constructive set theory Descriptive set theory Determinacy Russell's paradox List of set theory topics Type theory Axiom of reducibility Simple type theory Dependent type theory Intuitionistic type theory Homotopy type theory Univalent foundations Girard's paradox Category theory Category Topos theory Category of sets Higher category theory ∞-groupoid ∞-topos theory Mathematical structuralism Glossary of category theory List of category theory topics

---
Adapted from the Wikipedia article [Hilbert system](https://en.wikipedia.org/wiki/Hilbert_system) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Hilbert_system?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.