Definition:Hilbert Proof System/Instance 1

From ProofWiki
Jump to navigation Jump to search


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:


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

Source of Name

This entry was named for David Hilbert.