Definition:Hilbert Proof System/Instance 1

This page has been identified as a candidate for refactoring of advanced complexity.
In particular: Note that in Definition:Classical Propositional Logic (which needs refactoring) this system is attributed to Jan Łukasiewicz. This is also documented and explored in 1988: Alan G. Hamilton: Logic for Mathematicians (2nd ed.), which User:Prime.mover needs to get working on.
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.

It has been suggested that this page be renamed.
To discuss this page in more detail, feel free to use the talk page.

This article needs to be linked to other articles.
In particular: To dedicated pages for the axiomatic formulas
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
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 {{MissingLinks}} from the code.

Definition

This instance of a Hilbert proof system is used in:

2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.)

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:		$\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.

Sources

2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.3$: Definition $3.9$

This page may be the result of a refactoring operation.
As such, the following source works, along with any process flow, will need to be reviewed.
When this has been completed, the citation of that source work (if it is appropriate that it stay on this page) is to be placed above this message, into the usual chronological ordering.
In particular: This still needs to be inserted into the flow in the correct place. Work on Hamilton has not gone far yet. This is here so that we do not lose track of the fact that this is cited, as it is not named as such in Hamilton itself.
If you have access to any of these works, then you are invited to review this list, and make any necessary corrections.
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 {{SourceReview}} from the code.

1988: Alan G. Hamilton: Logic for Mathematicians (2nd ed.): $\S 2$: Formal statement calculus: $2.1$ The formal system $L$

			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} \)