Definition:Hilbert Proof System/Instance 1
Jump to navigation
Jump to search
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.
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.3$: Definition $3.9$
- 1988: Alan G. Hamilton: Logic for Mathematicians (2nd ed.): $\S 2$: Formal statement calculus: $2.1$ The formal system $L$