\begin{definition}[Definition:Classical Propositional Logic]
'''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.
{{ExtractTheorem|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 {{BookReference|Logic for Mathematicians|1988|Alan G. Hamilton|ed = 2nd|edpage = Second Edition}}, which User:Prime.mover needs to get working on.}}
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 {{AuthorRef|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}$
{{Help|formalise the deductive apparatuses devised for CPC, like natural deduction and various systems based on less or different axioms and inference rules|user = Lord_Farin}}
\end{definition}