# Definition:Hilbert Proof System

## 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.

## Examples in Propositional Logic

### 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: $\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:

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

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.