Math 2.0

Mathematical logic and foundations Definition

Hilbert system

Builds on Propositional logicImplicationNegation

Definition

Consider formulas of propositional logic built from variables with negation ¬\neg and implication →\to. The standard Hilbert system for this language has the following axioms, for all formulas φ\varphi, ψ\psi, χ\chi:

  1. φ→(ψ→φ)\varphi \to (\psi \to \varphi);
  2. (φ→(ψ→χ))→((φ→ψ)→(φ→χ))(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi));
  3. (¬φ→¬ψ)→(ψ→φ)(\neg \varphi \to \neg \psi) \to (\psi \to \varphi).

Its only rule of inference is modus ponens: from φ\varphi and φ→ψ\varphi \to \psi, infer ψ\psi. Let Γ\Gamma be a set of formulas. A derivation of φ\varphi from Γ\Gamma is a finite sequence of formulas that ends with φ\varphi. Each formula in it is an axiom, a member of Γ\Gamma, or follows from two earlier formulas by modus ponens. One writes Γ⊢φ\Gamma \vdash \varphi when such a derivation exists.

Remarks

Here is a derivation of φ→φ\varphi \to \varphi from no hypotheses.

  1. (φ→((φ→φ)→φ))→((φ→(φ→φ))→(φ→φ))(\varphi \to ((\varphi \to \varphi) \to \varphi)) \to ((\varphi \to (\varphi \to \varphi)) \to (\varphi \to \varphi)), axiom 2.
  2. φ→((φ→φ)→φ)\varphi \to ((\varphi \to \varphi) \to \varphi), axiom 1.
  3. (φ→(φ→φ))→(φ→φ)(\varphi \to (\varphi \to \varphi)) \to (\varphi \to \varphi), modus ponens from lines 2 and 1.
  4. φ→(φ→φ)\varphi \to (\varphi \to \varphi), axiom 1.
  5. φ→φ\varphi \to \varphi, modus ponens from lines 4 and 3.

The sequence φ,  φ→ψ\varphi, \; \varphi \to \psi is not a derivation of φ→ψ\varphi \to \psi from no hypotheses: its first line is neither an axiom nor obtained by a rule. More generally, a Hilbert system is any proof system of this shape: axiom schemas, few rules, and proofs as lists. For predicate logic one adds axioms for the quantifiers and the rule of generalization.

Reading path

To understand this page from the ground up, read these 10 pages in order. The foundations come first.

Show the path as a graph
Implication, concept, no evidence levelImplicationconceptNegation, concept, no evidence levelNegationconceptProposition, concept, no evidence levelPropositionconceptConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionPropositional logic, concept, no evidence levelPropositional logicconceptHilbert system, definition, no evidence levelHilbert systemdefinition
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Implication concept
  2. Negation concept
  3. Proposition concept
  4. Conjunction definition
  5. Disjunction definition
  6. Implication definition
  7. Negation definition
  8. Biconditional definition
  9. Propositional logic concept
  10. Hilbert system definition

Further reading

  1. Web https://en.wikipedia.org/wiki/Hilbert_system
About this page
TagET1HPME8VV
URIm2://ET1HPME8VV
Kinddefinition
WritingW0 stub
MSC03B05, 03F03
DefinesHilbert system
UsesPropositional logic, Implication, Negation
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.