Why are there several axiom systems for propositional logic?

Question

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:

1. It includes both double negation rules, i.e. $\neg \neg P \to P$ and $P \to \neg \neg P$.

2. 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?

Answer 1

There are indeed many presentations of classical propositional logic¹.

If complexity was measured purely in terms of number of axioms, then yes, Mendelson's axiom system would be more "economical". We could be even more "economical" with Meredith's system: $$((((A\to B)\to(\neg C\to\neg D))\to C)\to E)\to((E\to A)\to(D\to A))$$ Just rolls right off the tongue. While minimality is often a driver, people do still need to discover more minimal systems. (Indeed, the above is not the most minimal system if we include the complexity of the axiom and not just the number.) There's also the question of accepting the axioms. Ideally, we want the axioms to be "self-evident" or at least easy to understand intuitively. Maybe it's just me, but Meredith's axiom does not leap out at me as something that should obviously be true, let alone sufficient to prove all other classical tautologies.

Minimality is, however, not the "whole point" of axiomatic systems. You mention another reason: sometimes you actually do want to prove things at which point it is better to have a richer and more intuitive axiomatic system. You may argue that we can just derive any theorems we want to use from some minimal basis, and then forget about that basis. This is true but unnecessary complexity if we have no other reason for considering this minimal basis. When we compare different styles of proof system (e.g. Hilbert v. Sequent Calculus v. Natural Deduction), translations between them (especially into Hilbert-style systems) can involve a lot of mechanical complexity. That complexity can sometimes be significantly reduced by a careful choice of axioms.

For the Laws of the Excluded Middle (LEM) and Non-contradiction, the first thing you'd need to do is define the connectives. You can't prove $\neg(P\land\neg P)$ in a system that doesn't have $\land$. Given $\neg$ and $\to$ as primitives, standard definitions of $\land$ and $\lor$ are $P\land Q:\equiv \neg(P\to\neg Q)$ and $P\lor Q:\equiv\neg P\to Q$. With these definitions (or others), then yes, the LEM and Non-contradiction can both be proven in the systems you mention and any other proof system for classical propositional logic. Your concern here is an illustration that we often care about which axioms we have and not just that they're short and effective.

This also leads to another reason why we might want a certain presentation. We may want that presentation to line up with other, related logics. As you're starting to realize, it is ill-defined to say something like "intuitionistic propositional logic (IPL) is classical propositional logic (CPL) minus the LEM". When people say things like this, they are being sloppy. However, "CPL is IPL plus LEM" is unambiguous. Any presentation of IPL to which we add LEM is a presentation of CPL. For that presentation, it makes sense to talk about removing LEM. It doesn't make sense to talk about removing an axiom without a presentation of axioms that contains that axiom. It is also quite possible to have a presentation of CPL containing LEM that becomes much weaker than IPL when LEM is removed. In fact, you'd expect this because a presentation of IPL with LEM added is likely to be redundant because things which are intuitionistically distinct become identifiable when LEM is added. The story is the same for paraconsistent logics.

While it isn't as much of a driver for Hilbert-style proof systems, for natural deduction and sequent calculi the concerns of structural proof theory often push for more axioms (or rules of inference, rather). For example, many axioms in a Hilbert-style proof system mix together connectives, e.g. as Meredith's does above. This means we can't understand a connective on its own terms, but only by how it interacts with other connectives. A driving force in typical structural presentations is to characterize connectives by rules that don't reference any other connectives. This better reveals the "true" nature of the connectives, and it makes the system more modular. It becomes meaningful to talk about adding or removing a single connective allowing you to build a logic à la carte. In fact, structural proof theory motivates many constraints on what a proof system should look like such as logical harmony.

¹ And that link only considers Hilbert-style proof systems.