Editing Propositional calculus (section)

== Syntactic proof via axioms ==
{{Main article|Hilbert system}}
It is possible to perform proofs axiomatically, which means that certain [[Tautology (logic)|tautologies]] are taken as self-evident and various others are deduced from them using [[modus ponens]] as an [[Rule of inference|inference rule]], as well as a ''rule of [[Substitution (logic)|substitution]]'', which permits replacing any [[well-formed formula]] with any {{glossary link|substitution-instance|glossary=Glossary of logic}} of it.<ref name=":44" /> Alternatively, one uses axiom schemas instead of axioms, and no rule of substitution is used.<ref name=":44" />

This section gives the axioms of some historically notable axiomatic systems for propositional logic. For more examples, as well as metalogical theorems that are specific to such axiomatic systems (such as their completeness and consistency), see the article [[Axiomatic system (logic)]].

=== Frege's ''Begriffsschrift'' ===
Although axiomatic proof has been used since the famous [[Ancient Greek]] textbook, [[Euclid]]'s ''[[Euclid's Elements|Elements of Geometry]]'', in propositional logic it dates back to [[Gottlob Frege]]'s [[1879]] ''[[Begriffsschrift]]''.<ref name="BostockIntermediate" /><ref name=":44"/> Frege's system used only [[Material conditional|implication]] and [[negation]] as connectives.<ref name=":2" /> It had six axioms:<ref name=":44" /><ref name=":45"/><ref name=":46"/>

* Proposition 1: <math>a \to (b \to a)</math>
* Proposition 2: <math>(c \to (b \to a)) \to ((c \to b) \to (c \to a))</math>
* Proposition 8: <math>(d \to (b \to a)) \to (b \to (d \to a))</math>
* Proposition 28: <math>(b \to a) \to (\neg a \to \neg b)</math>
* Proposition 31: <math>\neg \neg a \to a</math>
* Proposition 41: <math>a \to \neg \neg a</math>

These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truth-functional propositional logic.<ref name=":45" />

=== Łukasiewicz's P<sub>2</sub> ===
[[Jan Łukasiewicz]] showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence <math>CCNpNqCpq</math>".<ref name=":46" /> Which, taken out of Łukasiewicz's [[Polish notation]] into modern notation, means <math>(\neg p \rightarrow \neg q) \rightarrow (p \rightarrow q)</math>. Hence, Łukasiewicz is credited<ref name=":44" /> with this system of three axioms:

* <math>p \to (q \to p)</math>
* <math>(p \to (q \to r)) \to ((p \to q) \to (p \to r))</math>
* <math>(\neg p \to \neg q) \to (q \to p)</math>

Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule.<ref name=":44" /> The exact same system was given (with an explicit substitution rule) by [[Alonzo Church]],<ref name=":47"/> who referred to it as the system P<sub>2</sub><ref name=":47" /><ref name=":48"/> and helped popularize it.<ref name=":48" />

==== Schematic form of P<sub>2</sub> ====
One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemata (metalogical variables that may stand for any [[well-formed formula]]s), the axioms are given as:<ref name="BostockIntermediate" /><ref name=":48" />

* <math>\varphi \to (\psi \to \varphi)</math>
* <math>(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))</math>
* <math>(\neg \varphi \to \neg \psi) \to (\psi \to \varphi)</math>

The schematic version of P<sub>2</sub> is attributed to [[John von Neumann]],<ref name=":44" /> and is used in the [[Metamath]] "set.mm" formal proof database.<ref name=":48" /> It has also been attributed to [[David Hilbert|Hilbert]],<ref name=":49"/> and named <math>\mathcal{H}</math> in this context.<ref name=":49" />

====Proof example in P<sub>2</sub>====
As an example, a proof of <math> A \to A </math> in P<sub>2</sub> is given below. First, the axioms are given names:
:(A1) <math>(p \to (q \to p))</math>
:(A2) <math>((p \to (q \to r)) \to ((p \to q) \to (p \to r)))</math>
:(A3) <math>((\neg p \to \neg q) \to (q \to p))</math>

And the proof is as follows:
# <math> A \to ((B \to A) \to A)</math> &nbsp; &nbsp; &nbsp; (instance of (A1))
# <math> (A \to ((B \to A) \to A)) \to ((A \to (B \to A)) \to (A \to A))</math> &nbsp; &nbsp; &nbsp; (instance of (A2))
# <math> (A \to (B \to A)) \to (A \to A)</math> &nbsp; &nbsp; &nbsp; (from (1) and (2) by [[modus ponens]])
# <math> A \to (B \to A)</math> &nbsp; &nbsp; &nbsp; (instance of (A1))
# <math> A \to A </math> &nbsp; &nbsp; &nbsp; (from (4) and (3) by modus ponens)