# Definition:Hilbert Proof System/Instance 1

Jump to navigation Jump to search
 It has been suggested that this page or section be renamed. One may discuss this suggestion on the talk page.

## Definition

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

## Source of Name

This entry was named for David Hilbert.