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.
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.
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}$.
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}$
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 particularly knowledgeable in this area, then you can help ProofWiki by resolving the issues.
To discuss this page in more detail, feel free to use the talk page.
If you are able to do so, then when you have finished you can 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 (see the proofread template for usage).
Sources
Move the included into a ProofWiki list. Wikipedia links have absolutely no place on this site.
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}$.