Every axiom set for classical propositional calculus (under uniform substitution and detachment) with a conditional and negation connective that I've seen has at least two negation symbols in it (and sometimes more). By uniform substitution I mean the rule that any variable can get substituted by any meaningful expression so long as it gets substituted for every instance of that variable in that formula. Detachment also gets called modus ponens.

Sometimes those negation symbols appear in a single meaningful expression (alternatively, a well-formed formula), such as with the axiom set:

{CpCqp, CCpCqrCCpqCpr, CCNpNqCCNpqp}.

Sometimes one negation symbol appears in two meaningful expressions, such as in the axiom set:

{CCpqCCqrCpr, CCNppp, CpCNpq}.

But, in either case there's at least two negation symbols in the whole axiom set.

Even in the single axioms I've seen there exist at least two instances of the negation symbol used.

This contrasts with systems where the meaningful expressions can contain falsum, where a single instance of a symbol for falsum can suffice, such as this axiom set:

{CCpqCCqrCpr, CpCqp, CCCpqpp, C0p}

If all axiom sets for "C-N" (conditional-negation) classical propositional calculus have at least two 'Ns', why is this? Is it a fluke or is there some connection to something like the laws of double negation CpNNp and CNNpp? How do '0' and 'N' differ such that only one instance of '0' is needed to axiomitize C-0 propositional calculus, but two instances of 'N' are needed to axiomitize C-N propositional calculus? Why, apparently, is there no axiom set with just one 'N' symbol possible? Has such an axiom set not gotten discovered or did it get missed? Or is there some semantical property of classical propositional calculus which implies the necessity of two negation symbols in a complete axiom set for classical propositional calculus?

I remember reading that Wajsberg noticed something about every tautology having two instances of the same variable and that there existed a reason for that (I might be misremembering that).

Why does apparently every axiom set have at least two negation symbols in the axiom set for classical propositional calculus? Does there exist a reason for this or is this a fluke/matter of coincidence?

I thought about this question a while ago, didn't know how to go about resolving it a while ago, and still don't know how to go about thinking about it or getting at an answer.

Edit: The two-negation minimum rule (if it's a rule) would also appear to hold for conditional-negation only natural deduction systems and sequent calculi also, since their formulations don't differ in the number of negation symbols used if I understand the relationships correctly.

  • $\begingroup$ In the axiom set that contains an explicit falsum 0, can you replace falsum with NCaa where a is a fresh variable? $\endgroup$ May 15, 2022 at 22:03
  • 1
    $\begingroup$ @GregNisbet I'm assuming that if we make such a replacement, the definition Np as Cp0 disappears, since 0 isn't a formula in the system, and negation becomes a primitive concept instead of a defined concept. CCpqCCqrCpr, CpCqp, CCCpqpp, CNCppq, makes CCNxNyCyx underivable according to a quick check using Mace4. The suggested model is the standard conditional: C00 = 1, C01 = 1, C10 = 0, C11 = 0, and negation N0 = 0, N1 = 0, with 1 as designated. The conditionals hold from checks with the classical conditional. CNCppq = C0q = 1. But, CCN0N1C10 = CC000 = C10 = 0. And thus Mace4 is correct. $\endgroup$ May 15, 2022 at 23:00
  • 1
    $\begingroup$ So the answer is no. $\endgroup$ May 15, 2022 at 23:01
  • 1
    $\begingroup$ this is a fun puzzle. I gotta say though, messing around with mace4 for a bit, I get the impression that without two occurrences of negation I can't seem to rule out a constant interpretation for negation. $\endgroup$ May 16, 2022 at 4:17

2 Answers 2


I think that you are correct and having negation appear twice is needed. My reasoning (not very rigorous, I will admit) would go as follows:

  • First, notice that from MP plus CpCqp and CCpCqrCCpqCpr you can prove the deduction theorem. And so far no negation was used.
  • Now, in order to be able to prove things about negation itself, we will need to have some way to add negation(s) to a conclusion and some way to remove negation(s), a bit like one does for natural deduction systems. This would be the reason for the minimum of 2 negations needed.
  • To take things a bit further, consider the axiom CCNpNqCqp and notice the positions where the negated variables appear. Let's rewrite the axiom with different names for each position as CCxyCzt, which would expand to $\lnot(\lnot x \lor y)\lor\lnot z \lor t$, so one negation in a positive position and the other in a negative position. On your second example with CCNppp, CpCNpq we have the same thing, one negation in a positive position and the other in a negative position. I suspect that this is related to my point above.
  • So what about the C-0 case? Well, then you will add C0p as a axiom, with 0 in a negative position, and then define negation as Np = Cp0, with 0 in a positive position. So in a way it is the same thing.

I think the third axiom set you provided has the answer to this question. Only one negation is needed.

{ C[Cpq][CCqrCpr], CpCqp, C[CCpqp][p], C0p }

Is equivalent to

{ C[Cpq][CCqrCpr], CpCqp, C[CCpqp][p], C[NCaa]p }

Let $v$ be a valuation assigning a $0$ or $1$ to every possible variable symbol.

If $a$ is mapped to $1$, then C[NCaa]p is equivalent to C[NC11]p and thus C0p.

If $a$ is mapped to $0$, then C[NCaa]p is equivalent to C[NC00]p and thus C0p.

  • $\begingroup$ This example for sure doesn't work given that negation becomes a primitive concept (which I'd argue it should, since it now appears explicitly in the axiom set), and the definition of negation accordingly as Cp0 disappears. So, no, it doesn't answer the question since it doesn't provide an axiom set with only one negation needed. Falsum isn't quite the same as the negation of an arbitrary tautology, nor is verum the same as an arbitrary tautology. $\endgroup$ May 15, 2022 at 23:03
  • $\begingroup$ So, this thing doesn't answer the question but only because "contrapositive elimination" C[CNpNq][Cqp] is not derivable, correct? It's not clear to me why negation being a primitive concept versus a syntactic abbrevation for Ca0 is important. $\endgroup$ May 15, 2022 at 23:07
  • 1
    $\begingroup$ Conrapositive elimination is not derivable, but that implies that many other formulas with negation won't be derivable also. In fact, if the calculus allows for an infinity of formulas, an infinity set of tautologies won't be derivable. CaCCNpNqCqp won't be derivable, CaCbCCNpNqCqp won't be derivable.. do you see the recursive pattern here? Using Mace4 it says that CxCNxy is not derivable. CCxCyzCyCxz is derivable from the first three axioms, so CNxCxy is not derivable. CxCCNyNxy is not derivable also. There are likely many more counterexamples of no particularly obvious pattern. $\endgroup$ May 15, 2022 at 23:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .