Definition:Classical Propositional Logic

Definition

Classical propositional logic is the branch of propositional logic based upon Aristotelian logic, whose philosophical tenets state that:

$(1): \quad$ A statement must be either true or false, and there can be no middle value.

$(2): \quad$ A statement cannot be both true and not true at the same time, that is, it may not contradict itself.

Thus, we proceed by recalling the formal language of propositional logic $\LL_0$.

To make $\LL_0$ into a formal system, we need to endow it with a deductive apparatus.

That is, with axioms and rules of inference.

This page or section has statements made on it that ought to be extracted and proved in a Theorem page. In particular: Put the following into its own section. In particular, the Łukasiewicz system needs its own suite of pages. Also, the technique of stating the fact that there are several methods, and picking one as an example, is too vague for ProofWiki. We need to establish a page from which each one is linked. Also note that this has already been documented in Definition:Hilbert Proof System/Instance 1. 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. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by creating any appropriate Theorem pages that may be needed. To discuss this page in more detail, feel free to use the talk page.

There are several (equivalent) methods of defining such a deductive apparatus.

One popular and particularly elegant set of axioms for classical logic was devised by Jan Łukasiewicz. It consists of three axioms and an inference rule: modus ponens. The axioms are as follows:

$\vdash \phi \implies \paren {\psi \implies \phi}$

$\vdash \paren {\phi \implies \paren {\psi \implies \chi} } \implies \paren {\paren {\phi \implies \psi} \implies \paren {\phi \implies \chi} }$

$\vdash \paren {\not \psi \implies \not \phi} \implies \paren {\phi \implies \psi}$

Lord_Farin suggests: This page needs the help of a knowledgeable authority. In particular: formalise the deductive apparatuses devised for CPC, like natural deduction and various systems based on less or different axioms and inference rules If you are knowledgeable in this area, then you can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues. 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 {{Help}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Sources

Although this article appears correct, it's inelegant. There has to be a better way of doing it. In particular: Move the included into a $\mathsf{Pr} \infty \mathsf{fWiki}$ list. Wikipedia links have absolutely no place on this site. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it. 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 {{Improve}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

A Nice List of Hilbert-style Deductive Systems