Definition:Hilbert Proof System/Instance 1
Jump to navigation
Jump to search
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 $\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.
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.3$: Definition $3.9$