Axiomatic logic: Hilbert's system

Propositional Logic: Hilbert's deductive system

Axiomatic logic: Hilbert's system

Hilbert's proof system, or Hilbert's system for short, is an example of the axiomatic proof system in which a number of axioms are taken as a starting points and new formulas are derived from those axioms by means of derivation rules. Hilbert's deductive scheme is a relatively simple system: there are only three axioms and one derivation rule (Modus Ponens) in it.

Hilbert's system Logical formulas of the following forms are the axioms of Hilbert's system: \[\begin{array}{ll} \varphi\rightarrow(\psi\rightarrow \chi) & \text{Axiom a} \\[0.2cm] \bigl(\varphi\rightarrow(\psi\rightarrow \chi)\bigr)\rightarrow \bigl(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow \chi)\bigr) & \text{Axiom b} \\[0.2cm] (\neg\,\varphi\rightarrow \neg\,\psi)\rightarrow (\psi\rightarrow \varphi)& \text{Axiom c}\end{array}\] Nothing else is an axiom.

Hilbert's system has only one derivation rule, namely Modus Ponens (\(\mathrm{MP}\)):

If \(\varphi\) is derived and \(\varphi\rightarrow \psi\) is derived, then \(\psi\) is also derived.

Examples of axioms There are infinitely many axioms, for example for proposition variables \(p\), \(q\), and \(r\) the following formulas are new axioms: \[\begin{aligned} p\rightarrow(p\rightarrow p) & \quad\text{Axiom a with }\varphi=\psi=\chi=p\\ (p\rightarrow q) \rightarrow (p\rightarrow (q\rightarrow p) & \quad\text{Axiom b with }\varphi=\chi=p, \psi=q\\ \bigl (\neg\neg\,p\rightarrow \neg(q\rightarrow r)\bigr)\rightarrow \bigl((q\rightarrow r)\rightarrow \neg\,p\bigr)&\quad \text{Axiom c with }\varphi=\neg\,p, \psi=q\rightarrow r\end{aligned}\]

Derivation in a deductive system A derivation from a formula set \(\Sigma\) is a finite numbered sequence of formulas, where we have: each formula in the sequence is an axiom, or a formula from \(\Sigma\), or a formula derived from previous formulas in the sequence using a derivation rule. A derivation within a deductive system in which no additional premises are used is called a theorem.

We denote derivations in a similar way to natural deduction, except that we now have axioms and only one derivation rule available. Furthermore, we only allow the connectives \(\neg\) and \(\rightarrow\) because this allows us to introduce conjunction ( \(\land\) ) and disjunction (\(\lor\)), respectively, as abbreviations via the definitions \(\varphi\land\psi = \neg(\varphi\rightarrow \neg\,\psi\) ) and \(\varphi\lor\psi = \neg\,\varphi\rightarrow \neg\, \psi\). The negation \(\neg\,\varphi\) can also be introduced as \(\varphi\vdash\bot\). A few examples illustrate how derivations work in Hilbert's system.

Example 1 Show that \(p\rightarrow q, q\rightarrow r, q\vdash r\).

Worked-out solution: \[\begin{array}{l|ll} 1 & p\rightarrow q & (\mathrm{P)}\\ 2 & q\rightarrow r & (\mathrm{P}) \\ 3 & p & (\mathrm{P}) \\ 4 & q & \mathrm{MP}, 1, 3\\ 5 & r & \mathrm{MP}, 2, 4\end{array}\]

Example 2 Show \(\neg\, p\rightarrow \neg\,q, q\vdash p\).

Worked-out solution: \[\begin{array}{l|ll} 1 & \neg\, p\rightarrow \neg\,q & (\mathrm{P)}\\ 2 & q & (\mathrm{P})\\ 3 & (\neg\,p\rightarrow \neg\, q)\rightarrow (q\rightarrow p) & \mathrm{Ax\;c} \\ 4 & q\rightarrow p & \mathrm{MP}, 1, 3 \\ 5 & p & \mathrm{MP}, 2, 4\end{array}\]

Example 3 Show that for each formula \(\varphi\) the following holds: \(\vdash \varphi\rightarrow \varphi\).

Worked-out solution: \[\begin{array}{l|ll} 1 & \varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr) & \mathrm{Ax\;a}\text{ met }(\varphi\rightarrow \varphi)\text{ voor }\psi\\ 2 & \Bigl(\varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr)\Bigr)\rightarrow \Bigl(\bigl(\varphi\rightarrow(\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow\varphi)\Bigr) & \mathrm{Ax\;b}\text{ met }(\varphi\rightarrow \varphi)\text{ voor }\psi\\ 3 & \bigl(\varphi\rightarrow (\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow \varphi) & \mathrm{MP}, 1, 2\\ 4 & \varphi\rightarrow (\varphi\rightarrow\varphi) & \mathrm{Ax\;a}\text{ met }\varphi\text{ voor }\psi\\ 5 & \varphi\rightarrow \varphi & \mathrm{MP}, 3, 4\end{array}\] Although the proof is written from front to back, you construct it in the opposite direction. The formula \(\varphi\rightarrow \varphi\) is not an axiom, but \(\varphi\rightarrow (\varphi\rightarrow\varphi)\) is. So you are done if you can prove \(\bigl(\varphi\rightarrow (\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow \varphi)\). But that follows from the axiom \(\Bigl(\varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr)\Bigr)\rightarrow \Bigl(\bigl(\varphi\rightarrow(\varphi\rightarrow \varphi)\bigr)\rightarrow (\varphi\rightarrow\varphi)\Bigr) \) plus the axiom \(\varphi\rightarrow \bigl((\varphi\rightarrow\varphi)\rightarrow\varphi\bigr) \) and that's it!

Hilbert's system uses a minimum of axioms and rules of reasoning. Giving such an economical system has the advantage that reasoning about the system is easy. The disadvantage is that providing derivations within the system is initially a bit more difficult than with a system such as that of natural deduction with multiple derivation rules. You must now first fabricate extra reasoning aids: every theorem you have proved may from that moment be used as if it were an axiom. Example 3 is such a statement that may be used in further derivations.

The following statement is also useful for derivations.

Deduction theorem In Hilbert's system, for a set of well-formed formulas \(\Sigma\) (premises, axioms and derivative formulas) and for the formulas \(\varphi\) and \(\psi\), the following holds: if \(\Sigma,\varphi\vdash \psi\) if and only if \(\Sigma\vdash \varphi\rightarrow \psi\).

We first prove that \(\Sigma,\varphi\vdash \psi\) follows from \(\Sigma\vdash \varphi\rightarrow \psi\). If \(\Sigma\vdash \varphi\rightarrow \psi\), then also \(\Sigma, \varphi \vdash \varphi\rightarrow \psi\). Because \(\Sigma, \varphi\vdash \varphi\) we also get \(\Sigma,\varphi\vdash \psi\) via Modus Ponens.

The proof that \(\Sigma\vdash \varphi\rightarrow \psi\) follows from \(\Sigma,\varphi\vdash \psi\) goes by induction to the length of the derivation of \(\psi\) from \(\Sigma,\varphi\). We distinguish 3 cases:

\(\psi\in\Sigma\cup\{\varphi\}\). This splits into two subcases: if \(\psi\in\Sigma\), then \(\Sigma \vdash \psi\), and if \(\psi=\varphi\), then also (according to example 3) \(\Sigma, \varphi\vdash \varphi\) and therefore \(\Sigma, \varphi\vdash \psi\).
\(\psi\) is an axiom. Then: \(\Sigma\vdash \psi\). We also have \(\psi\rightarrow (\varphi\rightarrow \psi)\) as an instance of Axiom a. With Modus Ponens we get \(\Sigma\vdash \varphi\rightarrow \psi\).
\(\Sigma,\varphi\vdash \psi\) comes via Modus Ponens from an earlier formula \(\chi\) via \(\Sigma,\varphi\vdash \chi\) and \(\Sigma,\varphi\vdash \chi\rightarrow \psi\). The induction hypothesis applies to this. So we have: \(\Sigma\vdash \varphi\rightarrow \chi\) and \(\Sigma\vdash \varphi\rightarrow (\chi\rightarrow \psi)\). The derivation for \(\Sigma\vdash \varphi\rightarrow \psi\) now goes as follows: \[\begin{array}{r|ll} \vdots & \vdots & \\ \vdots & \Sigma & \\ \vdots & \vdots & \\ k & \varphi\rightarrow \chi & \\ \vdots & \vdots & \\ l &\varphi\rightarrow (\chi\rightarrow \psi) & \\ l+1 & \bigl( \varphi\rightarrow (\chi\rightarrow \psi)\bigr)\rightarrow \bigl((\varphi\rightarrow \chi)\rightarrow (\varphi\rightarrow\psi)\bigr) & \mathrm{Ax\;b}\text{ with }\varphi\text{ and }\psi\text{ verwisseld}\\ l+2 & (\varphi\rightarrow \chi)\rightarrow (\varphi\rightarrow\psi) & \mathrm{MP}, l, l+1\\ l+2 & \varphi\rightarrow \psi & \mathrm{MP}, k, l+1\end{array}\]

The motivation to briefly discuss Hilbert's system in this treatise on propositional logic has its origin in the following theorem.

The derivation \(\Sigma\vdash \varphi\) is possible in Hilbert's system if and only if the derivation by natural deduction is possible.

Outline of the proof Suppose that \(\Sigma\vdash \varphi\) can be demonstrated in Hilbert's system. With induction on the length of a derivation it can then be proven that the derivation can also be done by natural deduction because all axioms can be deduced by natural deduction and the implication elimination rule can be used to apply the Modus Ponens rule.

Conversely, if \(\Sigma\vdash \varphi\) can be proven, then by induction on the length of a derivation it can be proven that the statement can also be proven in Hilbert's system. You use the Deduction theorem and the fact that the axioms other than Axiom a and Axiom b are essentially the same as rules of reasoning in natural deduction.