# Definition:Hilbert Proof System/Instance 2

## Contents

## Definition

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

## Also see

- Hilbert Proof System Instance 2 is Consistent
- Hilbert Proof System Instance 2 Independence Results
- Results about
**Hilbert Proof System Instance 2**can be found here.

## Source of Name

This entry was named for David Hilbert.

## Sources

- 1959: A.H. Basson and D.J. O'Connor:
*Introduction to Symbolic Logic*(3rd ed.) ... (previous) ... (next): $\S 4.2$: The Construction of an Axiom System: Transformation Rules, Definitions, Axioms