Definition:Hilbert Proof System
Definition
Hilbert proof systems are a class of proof systems for propositional and predicate logic.
Their characteristics include:
- The presence of many axioms;
- Typically only Modus Ponendo Ponens as a rule of inference.
Specific instances may deviate from this general scheme at some points.
Transclusion is going to be unfeasible in this detail. But how to change it?
You can help Proof Wiki by redesigning it.
To discuss this proof in more detail, feel free to use the talk page.
If you are able to fix this proof, then when you have done so you can remove this instance of {{Improve}} from the code.
If you would welcome a second opinion as to whether your improvement is correct, add an invitation to {{Proofread}} the page (see the proofread template for usage).
Instance 1
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$.
Instance 2
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 $p, q, r$ be propositional variables.
Then the following WFFs are axioms of $\mathscr H$:
| \((A1)\) | $:$ | Rule of Idempotence | \(\displaystyle (p \lor p) \implies p \) | |||||
| \((A2)\) | $:$ | Rule of Addition | \(\displaystyle q \implies (p \lor q) \) | |||||
| \((A3)\) | $:$ | Rule of Commutation | \(\displaystyle (p \lor q) \implies (q \lor p) \) | |||||
| \((A4)\) | $:$ | Factor Principle | \(\displaystyle (q \implies r) \implies \left({ (p \lor q) \implies (p \lor r)}\right) \) |
Rules of Inference
$RST \, 1$: Rule of Uniform Substitution
This rule should have its own dedicated page like the others. But separate from the Rule of Substitution, which is too vague at this point (might be a subpage though). Also review source flow afterwards
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
Any WFF $\mathbf A$ may be substituted for any propositional variable $p$ in a $\mathscr H_2$-theorem $\mathbf B$.
The resulting theorem can be denoted $\mathbf B \paren{ \mathbf A \mathbin{//} p }$.
See the Rule of Substitution.
$RST \, 2$: Rule of Substitution by Definition
The following expressions are regarded definitional abbreviations:
| \((1)\) | $:$ | Conjunction | \(\displaystyle \mathbf A \land \mathbf B \) | \(\displaystyle =_{\text{def} } \) | \(\displaystyle \neg \left({ \neg \mathbf A \lor \neg \mathbf B }\right) \) | |||
| \((2)\) | $:$ | Conditional | \(\displaystyle \mathbf A \implies \mathbf B \) | \(\displaystyle =_{\text{def} } \) | \(\displaystyle \neg \mathbf A \lor \mathbf B \) | |||
| \((3)\) | $:$ | Biconditional | \(\displaystyle \mathbf A \iff \mathbf B \) | \(\displaystyle =_{\text{def} } \) | \(\displaystyle (\mathbf A \implies \mathbf B) \land (\mathbf B \implies \mathbf A) \) |
$RST \, 3$: Rule of Detachment
If $\mathbf A \implies \mathbf B$ and $\mathbf A$ are theorems of $\mathscr H$, then so is $\mathbf B$.
That is, Modus Ponendo Ponens.
$RST \, 4$: Rule of Adjunction
If $\mathbf A$ and $\mathbf B$ are theorems of $\mathscr H$, then so is $\mathbf A \land \mathbf B$.
That is, the Rule of Conjunction.
(This rule can be proved from the other three and so is only a convenience.)
Source of Name
This entry was named for David Hilbert.
