Definition:Hilbert Proof System/Instance 2
Definition
This instance of a Hilbert proof system is used in:
Let $\LL$ be the language of propositional logic.
$\HH$ 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$:
| \((\text A 1)\) | $:$ | Rule of Idempotence | \(\ds (p \lor p) \implies p \) | ||||||
| \((\text A 2)\) | $:$ | Rule of Addition | \(\ds q \implies (p \lor q) \) | ||||||
| \((\text A 3)\) | $:$ | Rule of Commutation | \(\ds (p \lor q) \implies (q \lor p) \) | ||||||
| \((\text A 4)\) | $:$ | Factor Principle | \(\ds (q \implies r) \implies \left({ (p \lor q) \implies (p \lor r)}\right) \) |
Rules of Inference
$\text {RST} 1$: Rule of Uniform Substitution
 | This page has been identified as a candidate for refactoring of medium complexity. In particular: 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}$.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code. |
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.
$\text {RST} 2$: Rule of Substitution by Definition
The following expressions are regarded definitional abbreviations:
| \((1)\) | $:$ | Conjunction | \(\ds \mathbf A \land \mathbf B \) | \(\ds =_{\text{def} } \) | \(\ds \neg \left({ \neg \mathbf A \lor \neg \mathbf B }\right) \) | ||||
| \((2)\) | $:$ | Conditional | \(\ds \mathbf A \implies \mathbf B \) | \(\ds =_{\text{def} } \) | \(\ds \neg \mathbf A \lor \mathbf B \) | ||||
| \((3)\) | $:$ | Biconditional | \(\ds \mathbf A \iff \mathbf B \) | \(\ds =_{\text{def} } \) | \(\ds (\mathbf A \implies \mathbf B) \land (\mathbf B \implies \mathbf A) \) |
$\text {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.
$\text {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.)
Also see
- Results about Hilbert Proof System Instance 2 can be found here.
Source of Name
This entry was named for David Hilbert.
Sources
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.2$: The Construction of an Axiom System: Transformation Rules, Definitions, Axioms