Hilbert system

A graphic representation of the deduction system

In a Hilbert-style deduction system, a formal deduction 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. These formal deductions are meant to mirror natural-language proofs, although they are far more detailed.

Suppose ${\displaystyle \Gamma }$ is a set of formulas, considered as hypotheses. For example, ${\displaystyle \Gamma }$ could be a set of axioms for group theory or 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 }$. Thus, informally, ${\displaystyle \Gamma \vdash \phi }$ means that ${\displaystyle \phi }$ is provable assuming all the formulas in ${\displaystyle \Gamma }$.

Hilbert-style deduction systems are characterized by the use of numerous schemes of logical axioms. An axiom scheme is an infinite set of axioms obtained by substituting all formulas of some form into a specific pattern. The set of logical axioms includes not only those axioms generated from this pattern, but also any generalization of one of those axioms. A generalization of a formula is obtained by prefixing zero or more universal quantifiers on the formula; for example ${\displaystyle \forall y(\forall xPxy\to Pty)}$ is a generalization of ${\displaystyle \forall xPxy\to Pty}$.

It is common to include in a Hilbert-style deduction system only axioms for implication and negation. 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. When fully extended, a Hilbert-style system will resemble more closely a system of natural deduction.

Because Hilbert-style systems have very few deduction rules, it is common to prove metatheorems that show that additional deduction rules add no deductive power, in the sense that a deduction using the new deduction rules can be converted into a deduction using only the original deduction rules.

Some common metatheorems of this form are:

• The deduction theorem: ${\displaystyle \Gamma$ ;\phi \vdash \psi } if and only if ${\displaystyle \Gamma \vdash \phi \to \psi }$.
• ${\displaystyle \Gamma \vdash \phi \leftrightarrow \psi }$ if and only if ${\displaystyle \Gamma \vdash \phi \to \psi }$ and ${\displaystyle \Gamma \vdash \psi \to \phi }$.
• Contraposition: If ${\displaystyle \Gamma$ ;\phi \vdash \psi } then ${\displaystyle \Gamma$ ;\lnot \psi \vdash \lnot \phi } .
• Generalization: If ${\displaystyle \Gamma \vdash \phi }$ and x does not occur free in any formula of ${\displaystyle \Gamma }$ then ${\displaystyle \Gamma \vdash \forall x\phi }$.

Following are several theorems in propositional logic, along with their proofs (or links to these proofs in other articles). Note that since (P1) itself can be proved using the other axioms, in fact (P2), (P3) and (P4) suffice for proving all these theorems.

(HS1) ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$ - Hypothetical syllogism, see proof.

(L1) ${\displaystyle p\to ((p\to q)\to q)}$ - proof:

(1) ${\displaystyle ((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))}$       (instance of (P3))

(2) ${\displaystyle (p\to q)\to (p\to q)}$       (instance of (P1))

(3) ${\displaystyle ((p\to q)\to p)\to ((p\to q)\to q)}$       (from (2) and (1) by modus ponens)

(4) ${\displaystyle (((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))}$       (instance of (HS1))

(5) ${\displaystyle (p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))}$       (from (3) and (4) by modus ponens)

(6) ${\displaystyle p\to ((p\to q)\to p)}$       (instance of (P2))

(7) ${\displaystyle p\to ((p\to q)\to q)}$       (from (6) and (5) by modus ponens)

The following two theorems are known together as Double negation:

(DN1)${\displaystyle \neg \neg p\to p}$

(DN2) ${\displaystyle p\to \neg \neg p}$

See proofs.

(L2) ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$ - for this proof we use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps:

(1) ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$       (instance of (P3))

(2) ${\displaystyle ((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$       (instance of (HS1))

(3) ${\displaystyle (p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$       (from (1) and (2) using the hypothetical syllogism metatheorem)

(4) ${\displaystyle ((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))}$       (instance of (P3))

(5) ${\displaystyle ((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))}$       (from (3) and (4) using modus ponens)

(6) ${\displaystyle q\to (p\to q)}$       (instance of (P2))

(7) ${\displaystyle (q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))}$       (instance of (P2))

(8) ${\displaystyle (p\to (q\to r))\to (q\to (p\to q))}$       (from (6) and (7) using modus ponens)

(9) ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$       (from (8) and (5) using modus ponens)

(HS2) ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$ - an alternative form of the hypothetical syllogism. proof:

(1) ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$       (instance of (HS1))

(2) ${\displaystyle ((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))}$       (instance of (L2))

(3) ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$ (from (1) and (2) by modus ponens)

(TR1) ${\displaystyle (p\to q)\to (\neg q\to \neg p)}$ - Transposition, see proof (the other direction of transposition is (P4)).

(TR2) ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$ - another form of transposition; proof:

(1) ${\displaystyle (\neg p\to q)\to (\neg q\to \neg \neg p)}$       (instance of (TR1))

(2) ${\displaystyle \neg \neg p\to p}$       (instance of (DN1))

(3) ${\displaystyle (\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))}$       (instance of (HS1))

(4) ${\displaystyle (\neg q\to \neg \neg p)\to (\neg q\to p)}$       (from (2) and (3) by modus ponens)

(5) ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$       (from (1) and (4) using the hypothetical syllogism metatheorem)

(L3) ${\displaystyle (\neg p\to p)\to p}$ - proof:

(1) ${\displaystyle \neg p\to (\neg \neg (q\to q)\to \neg p)}$       (instance of (P2))

(2) ${\displaystyle (\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))}$       (instance of (P4))

(3) ${\displaystyle \neg p\to (p\to \neg (q\to q))}$       (from (1) and (2) using the hypothetical syllogism metatheorem)

(4) ${\displaystyle (\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))}$       (instance of (P3))

(5) ${\displaystyle (\neg p\to p)\to (\neg p\to \neg (q\to q))}$       (from (3) and (4) using modes ponens)

(6) ${\displaystyle (\neg p\to \neg (q\to q))\to ((q\to q)\to p)}$       (instance of (P4))

(7) ${\displaystyle (\neg p\to p)\to ((q\to q)\to p)}$       (from (5) and (6) using the hypothetical syllogism metatheorem)

(8) ${\displaystyle q\to q}$       (instance of (P1))

(9) ${\displaystyle (q\to q)\to (((q\to q)\to p)\to p)}$       (instance of (L1))

(10) ${\displaystyle ((q\to q)\to p)\to p}$       (from (8) and (9) using modes ponens)

(11) ${\displaystyle (\neg p\to p)\to p}$       (from (7) and (10) using the hypothetical syllogism metatheorem)

The axiom 3 above is credited to Łukasiewicz.[2] The original system by Frege had axioms P2 and P3 but four other axioms instead of axiom P4 (see Frege's propositional calculus). Russell and Whitehead also suggested a system with five propositional axioms.

Axioms P1, P2 and P3, with the deduction rule modus ponens (formalising intuitionistic propositional logic), correspond to combinatory logic base combinators I, K and S with the application operator. Proofs in the Hilbert system then correspond to combinator terms in combinatory logic. See also Curry–Howard correspondence.

• List of Hilbert systems
• Natural deduction

• Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. Vol. 1. Amsterdam: North Holland.
• Monk, J. Donald (1976). Mathematical Logic. Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. ISBN 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's selected papers on 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 (3rd printing 1976 ed.). Cambridge MA: Harvard University Press. ISBN 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 0-7204-2103-9.
  • 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.

• Gaifman, Haim. "A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness" (PDF).
• Farmer, W. M. "Propositional logic" (PDF). It describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).