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.

  • That is an interesting notation, one that I'm not family with. Is that polish notation, with 'C' for implication or '->'? – Mitch Sep 26 '11 at 12:46
  • @Mitch Yes, it's Polish notation. C stand for the material conditional, and N stands for negation If you wish to see what the wffs above look like in another notation, I'll point out that the formation rules for "N" and "C" go "If x is a wff, then Nx is a wff." "If x and y are wffs, then Cxy is a wff." – Doug Spoonwood Sep 26 '11 at 13:26
  • 1
    Do you have a reference for this notation? Even though it should be straightforward to understand, I'm having troubles doing the translation. – Mitch Sep 26 '11 at 14:10
  • Do you have a source for alternative axiomatizations to compare? – Mitch Sep 26 '11 at 14:11
  • 1
    For the notation, the wikipedia en.wikipedia.org/wiki/Polish_notation should do. Just remember that "+", "-", etc. work like C since they're both binary. – Doug Spoonwood Sep 26 '11 at 15:44

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).


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.


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.

  • 1
    I don't quite understand this. Axioms happen in the object language, while rules happen in the metalanguage. So, how are rules effectively axioms? What do you mean by effectively? – Doug Spoonwood Aug 25 '12 at 0:28
  • In addition to the axiom sets you have there you can replace simplification 2 CpCqp with 1 CCCqprCpr. 1 CCCqprCpr is more general than simplification in that you can derive 2 CpCqp using just 1 CCCqprCpr in one step using condensed detachment, but the converse fails. – Doug Spoonwood Jun 14 '13 at 4:59
  • So wait... there can get found single axioms for the positive implicational conjunctive calculus... for the system {CpCqp, CCpCqrCCpqCpr, CKpqp, CKpqq, CpCqKpq}? The positive implicational disjunctive calculus... {CpCqp, CCpCqrCCpqCpr, CpApq, CpAqp, CCpqCCrqCAprq}? The positive equivalential calculus... {{CpCqp, CCpCqrCCpqCpr, CEpqCpq, CEpqCqp, CCpqCCqpEpq}? There also exist single axioms for combinations of those systems? There exists a single axiom for the system {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp, CpCqKpq, CKpqp, CKpqq, CpApq, CpAqp, CCpqCCrqCAprq, CEpqCpq, CEpqCqp, CCpqCCqpEpq}? – Doug Spoonwood Apr 29 '14 at 16:10
  • Or does your statement about single axioms only apply to calculi where implication is the only connective? – Doug Spoonwood Apr 29 '14 at 16:10
  • In response to your question, If the system has at least the required theorems, and is defined axiomatically, Tarski's claim applies. The axioms are [as Rezus puts it] a trick that allows them to pack up arbitrary theorems up as one theorem, and the final pack up (the single axiom) just unpacks them all. So it doesn't matter at all what other axioms/theorems may exist in addition to the required ones. – john Jun 6 '18 at 1:46

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.

  • You can find in the literature single axioms for propositional calculus just having the rule of detachment (along with substitution if you count substitution as another rule of inference). A. N. Prior lists some of these in the appendix of his Formal Logic. You can find one online here, us.metamath.org/mpegif/meredith.html. With a slightly different rule of detachment, there's also Nicod's axiom and what others uncovered after him fitelson.org/ar.html – Doug Spoonwood Oct 16 '11 at 22:55

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.

  • Did you mean "Cpq, p|-q" instead of "CNpNq, p|-q" for modus ponens? (I'm not sure I get the notation) – Mitch Sep 26 '11 at 14:09
  • No, I wasn't talking about modus ponens. Though I didn't mean to write "CNpNq, p|-q". I meant modus tollens "CNpNq, q|-p". And I'll edit this, along with the axiom. Thanks! – Doug Spoonwood Sep 26 '11 at 15:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.