Editing Propositional calculus (section)

=== 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" />