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 $\LL$ 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:    \(\ds \mathbf A \implies \paren {\mathbf B \implies \mathbf A} \)      
Axiom 2:    \(\ds \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:    \(\ds \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.