Definition:Hilbert Proof System

Definition

Hilbert proof systems are a class of proof systems for propositional and predicate logic.

Their characteristics include:

• The presence of many axioms;
• Typically only Modus Ponendo Ponens as a rule of inference.

Specific instances may deviate from this general scheme at some points.

Examples in Predicate Logic

• 2009: Kenneth Kunen: The Foundations of Mathematics: Instance 1

Although this article appears correct, it's inelegant. There has to be a better way of doing it. In particular: Transclusion is going to be unfeasible in this detail. But how to change it? // Above is another attempt. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Improve}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Examples in Propositional Logic

Instance 1

This instance of a Hilbert proof system is used in:

• 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.)

Let $\LL$ be the language of propositional logic.

$\mathscr H$ has the following axioms and rules of inference:

Axioms

Let $\mathbf A, \mathbf B, \mathbf C$ be WFFs.

The following three WFFs are axioms of $\mathscr H$:

			Axiom 1:		\(\ds \mathbf A \implies \paren {\mathbf B \implies \mathbf A} \)
			Axiom 2:		\(\ds \paren {\mathbf A \implies \paren {\mathbf B \implies \mathbf C} } \implies \paren {\paren {\mathbf A \implies \mathbf B} \implies \paren {\mathbf A \implies \mathbf C} } \)
			Axiom 3:		\(\ds \paren {\neg \mathbf B \implies \neg \mathbf A} \implies \paren {\mathbf A \implies \mathbf B} \)

Rules of Inference

The sole rule of inference is Modus Ponendo Ponens:

From $\mathbf A$ and $\mathbf A \implies \mathbf B$, one may infer $\mathbf B$.

Instance 2

This instance of a Hilbert proof system is used in:

• 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.)

Let $\LL$ be the language of propositional logic.

$\HH$ has the following axioms and rules of inference:

Axioms

Let $p, q, r$ be propositional variables.

Then the following WFFs are axioms of $\mathscr H$:

\((\text A 1)\)	$:$		Rule of Idempotence		\(\ds (p \lor p) \implies p \)
\((\text A 2)\)	$:$		Rule of Addition		\(\ds q \implies (p \lor q) \)
\((\text A 3)\)	$:$		Rule of Commutation		\(\ds (p \lor q) \implies (q \lor p) \)
\((\text A 4)\)	$:$		Factor Principle		\(\ds (q \implies r) \implies \left({ (p \lor q) \implies (p \lor r)}\right) \)

Rules of Inference

$\text {RST} 1$: Rule of Uniform Substitution

This page has been identified as a candidate for refactoring of medium complexity. In particular: This rule should have its own dedicated page like the others. But separate from the Rule of Substitution, which is too vague at this point (might be a subpage though). Also review source flow afterwards Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Any WFF $\mathbf A$ may be substituted for any propositional variable $p$ in a $\mathscr H_2$-theorem $\mathbf B$.

The resulting theorem can be denoted $\mathbf B \paren {\mathbf A \mathbin{//} p}$.

See the Rule of Substitution.

$\text {RST} 2$: Rule of Substitution by Definition

The following expressions are regarded definitional abbreviations:

\((1)\)	$:$		Conjunction			\(\ds \mathbf A \land \mathbf B \)	\(\ds =_{\text{def} } \)	\(\ds \neg \left({ \neg \mathbf A \lor \neg \mathbf B }\right) \)
\((2)\)	$:$		Conditional			\(\ds \mathbf A \implies \mathbf B \)	\(\ds =_{\text{def} } \)	\(\ds \neg \mathbf A \lor \mathbf B \)
\((3)\)	$:$		Biconditional			\(\ds \mathbf A \iff \mathbf B \)	\(\ds =_{\text{def} } \)	\(\ds (\mathbf A \implies \mathbf B) \land (\mathbf B \implies \mathbf A) \)

$\text {RST} 3$: Rule of Detachment

If $\mathbf A \implies \mathbf B$ and $\mathbf A$ are theorems of $\mathscr H$, then so is $\mathbf B$.

That is, Modus Ponendo Ponens.

$\text {RST} 4$: Rule of Adjunction

If $\mathbf A$ and $\mathbf B$ are theorems of $\mathscr H$, then so is $\mathbf A \land \mathbf B$.

That is, the Rule of Conjunction.

(This rule can be proved from the other three and so is only a convenience.)

Source of Name

This entry was named for David Hilbert.