Why is this set {CqCpq, CCpCqrCCpqCpr, CCNpNqCqp} the most common set of axioms for propositional calculus?

Question

If you look, you can find many "equivalent", sufficient axiom sets for classical propositional calculus. The set {CqCpq, CCpCqrCCpqCpr, CCNpNqCqp} seems like the axiom set most commonly used. There do exist systems with only one axiom, and systems with no axioms, so why is {CqCpq-1, CCpCqrCCpqCpr-2, CCNpNqCqp-3} more common than other axiom sets? Does there exist a rational ground as to why one would select this axiom set over any other given axiom set? I can see why one might select it over axiom sets with just one axiom, as those axiom sets at least very often involve a long axiom which also doesn't seem very intuitive, or at least I believe that most people would not find those single-axiom systems as all that intuitive. But, this in no way guarantees this particular axiom set as more intuitive than any other sufficient axiom set, given that one grounds the the selection of this axiom set over any other via "intuitive" considerations. Also, that the axiom set above comes as all that intuitive in comparison to at least one other axiom set seems doubtful (see final paragraph).

What follows indicates what actually prompted this question in my mind. Say we compare the axiom set {CCpqCCqrCpr-4, CCNppp-5, CNpCpq-6} with the above. Why prefer the first set over the second in light of that 1. Jan Lukasiewicz, the logician responsible for both axiom sets as sets (not the axioms, the sets as sufficient and non-redundant for classical propositional calculus), at least appears to have preferred the second axiom set to the first (as evidenced by his book on Aristotle's Syllogistic, and his textbook Elements of Mathematical Logic which uses the second axiom set, but not the first) and 2. the second axiom set is simpler than the first axiom set in the sense that the total number of letters is smaller for the second set than for the first set? The only answer I've come up with so far, other than historical accident, comes as that if you have the rules of conditional proof along with substitution and conditional elimination, the first set works out as simpler in that it that 2 of its axioms can get eliminated because of the rules of conditional proof, while the second axiom set comes as more complicated in that only 1 of its axioms can get eliminated.

The question "Why is this set {CqCpq, CCpCqrCCpqCpr, CCNpNqCqp} preferred over any other sufficient axiom set?" seems a generalization of "why prefer the first axiom set over the second?", which I think indicates why the particular question of "why prefer the first axiom set over the second axiom set" seems relevant to the general question here.

As a possible pre-emption:

If one tries to argue that the first set involves more intuitive axioms, I simply don't see that. It seems at least plausible to argue that "most" people with experience with logical reasoning before learning formal logic would probably not find 1 intuitive (since it's a "paradox" of material implication), 2 does not seem intuitive either, and 3 seems at best somewhat intuitive (it doesn't even directly correspond to the rule of modus tollens as commonly presented, since you have CNpNq as the antecedent, instead of where you have Cpq as a premise for modus tollens, and a negation Nq as the other premise. This at least seems to imply that if you interpret it in the light of modus tollens you'll have to assume that NNp==p to understand the axiom, making it not all that intuitive). On the other hand, I would expect that 4 comes as one of the most intuitive, if not the most intuitive formulas of formal logic. So, even if 5 (which I don't find intuitive) is not intuitive, and 6 is not intuitive, the second set as a whole works out as more intuitive than the first set.

Edit: related question at math.stackexchange.

Answer 1

I think the answer are largely historical. However, there are some nice mathematical properties about the system in question, which suggest they are intuitive:

• [K] p → q → p
• [S] (p → q → r) → (p → q) → p → r
• [contraposition] (~p → ~q) → p → q

Modus Ponens: p → q , p / q

A related (complete) system replaces contraposition with double negation: ((p → ⊥) → ⊥) → p . This is due to Alonzo Church, Alan Turing's PhD supervisor and father of the λ-calculus. As far as I can tell, this system is also rather popular. On the other hand, it can be argued that its less intuitive, as I write below.

Axioms 1 and 2 are quite old: they appear in Frege's Begriffsschrift (1879), §14. Forms of double negation appear in §17 and §18; Frege does not mention contraposition in his text.

Outside of philosophical logic, axioms K and S play an important rôle in combinatory logic, as part of the Curry-Howard Correspondence. This connects a fragment of propositional logic to computer programs. To demonstrate, here's how you'd write S and K in the programming language Haskell, along with their type declarations:

k :: p -> q -> p
k x y = x    

s :: (p -> q -> r) -> (p -> q) -> p -> r
s f g x = (f x) (g x)

Under the Curry-Howard reading of S and K, modus ponens corresponds to function application.

One can express all of the simply typed λ-calculus, using a very old embedding algorithm due to Schoenfinkle from his On The Building Blocks of Mathematical Logic (1924). Schoenfinkle appears to have developed S and K independent of Frege, which indicates they have some mathematical naturality.

Using the combinatory logic and the Schoenfinkle embedding of the simply typed λ-calculus, one can quickly prove theorems by constructing little programs to specification. A classic example is s k k :: p -> p; the program s k k is the identify function given my above definition. It can also be thought of as a proof of "p → p" via the Curry-Howard correspondence.

S, K, and modus ponens are also complete for the implicational fragment of intuitionistic logic.

Finally, axioms regarding negation are natural to mathematicians and have a long traditional in philosophy. For one thing, contraposition dates back Aristotle's Organon; virtually no philosopher disputed its validity until intuitionists in the 20th century.

Double Negation is not as intuitive as contraposition - this might be why its not as popular. In rhetoric, litotes makes use of double negatives to change the meaning of sentences in order to make understatements. It also has a rocky history. It was embraced as early in the 3rd century by the Stoic Alexander of Aphrodisias, however by the middle ages logicians argued over its validity. In particular, Peter of Abelard in the 12th century rejected double negation. The subsequent rise of consequentialist interpretations of logic would ultimately settle this dispute. By the time of the 17th century, Arnauld and Nicole's Port Royale Logic (1662) presents double negation elimination in Chapter III, Rule III. Double negation elimination was later embraced by almost every western philosopher after the 17th century, including Leibniz, Kant, and in Boole's Laws of Thought (1854).

Answer 2

The reason is partly historical (see Matt's answer, tracing back to Frege) and partly "technical".

The first two axioms are the "minimum" needed in an axiom system with "conditional" as primitive to prove the Deduction Theorem, which is a fundamental tool in Hilbert-style proof systems to manage derivations.

The third one is one of many possibilities to introduce "negation" and licence the derivation of all tautologies in classical logic.

We have many ways to do this :

• Mendelson : (¬C→¬B)→((¬C→B)→C) (Reductio ad absurdum)

• Church : ¬¬A→A (Double negation), with ⊥ (falsum) as primitive and ¬A defined as A→⊥

• other possibilities are with (¬A→¬B)→(B→A) or (¬A→B)→(¬B→A) as third axiom

• finally : ⊥→A (Ex falso quodlibet) and ((A→B)→A)→A (Peirce's law).

Of course, if we introduce ∨ as usual, we can use also : ¬A ∨ A (Excluded middle).

They also give us an easy connection with intuitionistic propositional calculus.

If we start with Hilbert-Bernays' axioms (the first two axioms for → plus the six axiom expressing introduction- and elimination-rules for ∨ and ∧) we can obtain classical logic adding Excluded middle or one of the above equivalents, while intuitionistic logic is obtained adding instead Ex falso quodlibet.

Answer 3

I agree fully with Mitch's answer above. Although he didn't cover part of the question...

On the question of a single axiom, the answer is yes... many are known as you were pointed at above. But more generally, Tarski announced in 1930 that any system with substitution and modus ponens and that has as theorems either of the sets: {CpCqp, CpCqCCpCqrr} or {CpCqp, CpCqCCpCqrCsr} has a single axiom basis. (Adrian Rezus published a proof in 1982 of the first basis, Dolph Ulrich presented a proof of the second some years ago) John Halleck recently showed that (Cpp, CpCqCCpCqrCsr} and {CpCqp, CCpCqrCqCpr} were also suffice show that there is a single axiom basis for a system.

As to a zero axiom basis... Rules have to operate on something, so you need at least one axiom, unless you are admitting zero premiss rules... which are effectively axioms.

As an aside, Jean Porte in the 1960's, and Lloyd Humberstone recently, show that you can have a system with exactly the same theorems as standard PC WITHOUT having the rule of Modus Ponens, and without being able to prove that rule. Both systems have the single axiom "Cpp" and a large number (138 in Jean Porte's case) of single premise rules.

Answer 4

I don't think there's a strict technical answer. Because there are many possible -equivalent- systems (axiomatizations plus rules of inference), equivalent in the sense that they all prove exactly the same propositions, the choice among them boils down to other properties, some technical and some simply style.

From the automated deduction direction, anecdotally, it seems that the more rules of inference you have (and fewer axioms), the longer it takes to find a proof.

As to style, the three rules you gave are understandable, meaningful, and fairly short. I bet there is a single axiom, but then I expect it would be long, unfathomable, and hard to remember. With a single rule of inference (like modus ponens) you need a few more axioms, but then the longer list, even though with simple axioms, is itself too long to remember.

One could define 'simplest' as fewest axioms, or fewest rules of inference, r even shortest number of symbols to represent (axioms/rules of inference together), but the resulting system may not be psychologically satisfying.

Short answer, it boils down to human preference.

Answer 5

The following feels rather conjectural. Hence, I asked this question in the first place.

Pure natural deduction systems with no axioms don't come as common, because you if you weight rules of inference and axioms equally, natural deduction systems often have a greater number of things in the background (the sum of the number of rules of inference and the number of axioms equals "the number of things in the background") than this axiom set. So, pure natural deduction systems with no axioms in someway come as more "complicated".

Systems with fewer axioms, more axioms, or and equivalent number of axioms also generally come as more complicated. This seems readily apparent for systems with more axioms. Systems with fewer axioms, or an equivalent number of axioms I think also come as more complicated in the following sense. Suppose we have rules of hypothesis introduction, and conditional introduction, in addition to detachment and substitution. Then, {CqCpq, CCpCqrCCpqCpr, CCNpNqCqp} becomes very simple in the following sense. CqCpq is not needed as axiom, nor is CCpCqrCCpqCpr, since you can derive both of those using the rules of conditional proof (hypothesis introduction and conditional introduction) and detachment only. You only need CCNpNqCqp as an axiom (or a rule of inference "CNpNq, q|-p"). Do all other sufficient axioms in this context (with the rules involving conditional proof) of propositional calculus come as longer? If so, it would seem to follow that {CqCpq, CCpCqrCCpqCpr, CCNpNqCqp} is the simplest system for propositional calculus in that any other system augmented by the rules of conditional proof (with detachment and substitution taken for granted) either requires more axioms, or requires a longer axiom than CCNpNqCqp.