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.
Instance 1
This instance of a Hilbert proof system is used in:
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: | \(\displaystyle \mathbf A \implies \paren {\mathbf B \implies \mathbf A} \) | |||||||
Axiom 2: | \(\displaystyle \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: | \(\displaystyle \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:
Let $\mathcal L$ be the language of propositional logic.
$\mathscr H$ 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$:
\((A1)\) | $:$ | Rule of Idempotence | \(\displaystyle (p \lor p) \implies p \) | |||||
\((A2)\) | $:$ | Rule of Addition | \(\displaystyle q \implies (p \lor q) \) | |||||
\((A3)\) | $:$ | Rule of Commutation | \(\displaystyle (p \lor q) \implies (q \lor p) \) | |||||
\((A4)\) | $:$ | Factor Principle | \(\displaystyle (q \implies r) \implies \left({ (p \lor q) \implies (p \lor r)}\right) \) |
Rules of Inference
$RST \, 1$: Rule of Uniform Substitution
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.
$RST \, 2$: Rule of Substitution by Definition
The following expressions are regarded definitional abbreviations:
\((1)\) | $:$ | Conjunction | \(\displaystyle \mathbf A \land \mathbf B \) | \(\displaystyle =_{\text{def} } \) | \(\displaystyle \neg \left({ \neg \mathbf A \lor \neg \mathbf B }\right) \) | |||
\((2)\) | $:$ | Conditional | \(\displaystyle \mathbf A \implies \mathbf B \) | \(\displaystyle =_{\text{def} } \) | \(\displaystyle \neg \mathbf A \lor \mathbf B \) | |||
\((3)\) | $:$ | Biconditional | \(\displaystyle \mathbf A \iff \mathbf B \) | \(\displaystyle =_{\text{def} } \) | \(\displaystyle (\mathbf A \implies \mathbf B) \land (\mathbf B \implies \mathbf A) \) |
$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.
$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.