Definition:Hilbert Proof System

From ProofWiki
Jump to navigation Jump to search

Definition

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

Their characteristics include:

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


Instance 1

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 $\mathbf A, \mathbf B, \mathbf C$ be WFFs.

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

Axiom 1:    \(\displaystyle \mathbf A \implies \left({\mathbf B \implies \mathbf A}\right) \)             
Axiom 2:    \(\displaystyle \left({\mathbf A \implies \left({\mathbf B \implies \mathbf C}\right)}\right) \implies \left({\left({\mathbf A \implies \mathbf B}\right) \implies \left({\mathbf A \implies \mathbf C}\right)}\right) \)             
Axiom 3:    \(\displaystyle \left({\neg \mathbf B \implies \neg \mathbf A}\right) \implies \left({\mathbf A \implies \mathbf B}\right) \)             


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.