There is an axiom system that I found in Elliot Mendelson's, "Introduction to Mathematical Logic", p.27, and Theodore Sider's, "Logic for Philosophy", p.59:
(A1) $P \to (Q \to P)$
(A2) $(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$
(A3) $(\neg Q \to \neg P) \to ((\neg Q \to P) \to Q)$
It is said that these three axiom schemata are sufficient for classical propositional logic. And yet there are others (said to be) equally sufficient axiom systems for classical propositional logic, such as Hilbert-Bernays axioms which consists in 10 axiom schemata (cf. Jan von Plato, "Elements of Logical Reasoning", p.250). In Hilbert-Bernays axiom system, I noticed several features:
It includes both double negation rules, i.e. $\neg \neg P \to P$ and $P \to \neg \neg P$.
It includes some forms of Introduction Rules and Elimination Rules that usually found in Gentzen-style Natural Deduction system.
Does it means that Hilbert-Bernays axiom system is less economical than Mendelson's? I understand the reason to include as axiom schema such tautologies as double negation and contraposition; it is for the ease of use in proof. But isn't that the whole point of axiomatic system is to be sufficiently defined by a minimal number of tautologies not derivable from others (such that it constitutes some sort of minimal foundation for all other tautologies)? After all, we cannot include all tautologies as axioms. If that is so, then is Hilbert-Bernays axiom system superfluous?
Lastly, why do we not found the basic concept of classical logic, i.e. Law of Non-Contradiction ($\neg (P \wedge \neg P)$) and Law of Excluded Middle ($P \lor \neg P$), as two axiom schemata? Does it mean that these two Laws is derivable from three axioms of Mendelson's and Hilbert-Bernays'? If it's just another two of many tautologies of classical propositional logic, then why call those two "Law"? This is puzzling because I often found description of intuitionistic logic as classical logic minus Law of Excluded Middle and paraconsistent logic as classical logic minus Law of Non-Contradiction. If so, then which axioms should I subtract from the axiom system of classical logic to produce intuitionistic logic or paraconsistent logic?