Most (all?) logic books consider "p or not p" to be a tautology, hence always true, and this is usually stated without any further discussion. (I never gave it a second thought.)

In common language, "p or not p" means that one of the two possibilities must be true, and that sounds so obvious that only a fool would doubt it. So maybe I'm that fool, because it occurred to me recently that the status of this proposition is somewhat mysterious when applied to undecidable mathematical statements.

Specifically, I thought about the famous Continuum Hypothesis from Set Theory (CH). Neither CH nor its negation can be proved, so neither one can be said to be true, but if that's the case then what does it mean to say "CH or not CH" is true?

I can rephrase this as follows: how does someone who accepts the law of the excluded middle come to terms with the "truth" of the statement "CH or not CH"?


10 Answers 10


"P or not P" is a tautology of classical logic, but not of all logics. It is not a tautology of intuitionistic logic, for example. So, one approach would be to say that classical logic does not apply to unprovable propositions in mathematics. Indeed, intuitionists maintain that it does not apply to mathematics at all, since they hold that mathematics is all about proving things and hence it has no unprovable truths.

There are also other domains where its applicability has been challenged, for example with future contingents. If P is some proposition about an event that might happen tomorrow, then a fairly common approach is to say that P does not have a truth value until the event happens or does not. This approach was taken by Aristotle in a passage where he discusses a possible sea battle that might or might not happen. Assuming "P or not P" in such cases allows the construction of arguments that appear to prove some version of fatalism.

If you wish to stick with classical logic, one way to resolve this is to use a modal logic, in which the modal operator □ is interpreted as "it is provable that" or "it is a determined fact that". So, for some provable mathematical proposition P we could write □P, while for an unprovable one we would write ¬□P. This allows us to distinguish between:

  1. □P ∨ ¬□P which remains a tautology of classical logic, meaning that P is either provable or it isn't.

  2. □(P ∨ ¬P) which states that the tautology "P ∨ ¬P" is provable.

  3. □P ∨ □¬P which states that we can prove P or we can prove not P, which is false for unprovable P.

More generally, there is no guarantee that a particular logic will always apply. It always has to be assessed relative to a given semantics, or to a given set of metaphysical assumptions.

--- Updated answer.

Since you've updated your question, here is an update to the answer. You ask, how does someone who accepts the law of the excluded middle come to terms with the "truth" of the statement "CH or not CH"? The point is, you don't accept the truth of such a statement unless you are committed to a kind of realism with respect to the underlying domain: in this case mathematics. Accepting it amounts to the assumption that all mathematical propostions are either true or not true, independently of our ability to verify them. Platonists about mathematics believe such things, but others do not.

This leads to an important point that Michael Dummett wrote about extensively. Logic, via its semantics, is linked to underlying metaphysical assumptions about the domain or subject matter that it is applied to. Classical logic, with its law of excluded middle, corresponds to realism with respect to the domain. Intuitionism is a form of antirealism. It has a different semantics for negation, and it results in a distinct logic that lacks LEM. According to Dummett, being antirealist about some domain corresponds to being unwilling to accept as an assumption that propositions within that domain must always be either true or false independently of our ability to verify them.

Dummett's views can be found in his book, The Logical Basis of Metaphysics. As I noted in my comment, there is also a classic text on the logic of provability by George Boolos: The Logic of Provability. He develops a modal logic called K4W that models what it is for a proposition to be provable in a formal system. It is also possible to use the Gödel-McKinsey-Tarski translation to map intuitionistic logic into S4 modal logic.

  • That's quite an interesting perspective, I like that interpretation of the modal operator, is there a book that develops modal logic along that line?
    – Sam
    Jan 19 at 1:28
  • The classic text in this area is George Boolos, The Logic of Provability. He develops a modal logic called K4W that models what it is for a proposition to be provable in a formal system. It is also possible to use the Gödel-McKinsey-Tarski translation to map intuitionistic logic into S4 modal logic.
    – Bumble
    Jan 19 at 2:12
  • I think these are great ideas especially considering that all my life I (shamefully) sneered at intuitionists for their "misguided" view of mathematical truth, and now I find myself following a line of thought that lands squarely in their domain. It's going to be a nice trip. Thank you.
    – Sam
    Jan 19 at 3:05
  • So accepting the LEM is like accepting the existence of an independent mathematical universe where CH is either true or false, regardless of whether can prove it or not. I can't help drawing some parallels with Kant where the mathematical universe is the thing-in-itself and our theorems are what our senses and intuitions make of it.
    – Sam
    Jan 19 at 3:32
  • That's pretty much it. If you wish to be really precise, Dummett links realism to the Principle of Bivalence, rather than the LEM. They are distinct things, though the difference is subtle and not critical here.
    – Bumble
    Jan 19 at 4:18

The classical discussion is in Aristotle where he points out the LEM (Law of the Excluded Middle) doesn't appear to hold for future statements. Mathematically, this began as a new current in mathematics by Brouwers intuitionistic logic. You might find it intetesting to look at Heyting algebras which is the analogue of Boolean algebras in this context.

  • In the two cases you mention, there are ways to interpret "p or not p" that will make sense of the situation where p is undecidable. In the future case, one of the two statements will be true, but their truth cannot be asserted and in the intuitionistic case the disjunction is simply not tautological. But my question is about the status of this proposition for classical predicate logic. In that setting, what does the proposition "CH or not CH" says? In other words, what does it say to a person who fully accepts all the axioms of first order logic?
    – Sam
    Jan 18 at 19:16
  • A sea-fight must either take place tomorrow or not, but it is not necessary that it should take place tomorrow, neither is it necessary that it should not take place, yet it is necessary that it either should or should not take place tomorrow. (De Interpretatione, 9, 19 a 30.) emphasis mine
    – Dave
    Jan 18 at 19:39
  • Yes, but then one can say that at least one of the statements will be true, maybe not now but in the future. But in the case of CH, it's not a matter of time, the undecidability of CH will still be true a million years from now, so we're still left with the problem of explaining why we say that "CH or not CH" is true.
    – Sam
    Jan 19 at 1:39
  • @Sam: Actually future mathematicians in "a million years time" may actually decide that GCH and in particular CH is true and adopt it as an axiom. Thus it becomes trivially decidable. Jan 21 at 10:25
  • @MoziburUllah Undecidability is always relative to a theory. If you add axioms then you're changing the theory and also the question, even to the point of making it trivial, as you said. But as far as ZFC goes, CH will remain undecidable for all eternity.
    – Sam
    Jan 22 at 5:30

An interpretation applicable for classical logic is...

The system in which CH is (provably) undecidable is under specified with respect to statements involving the truth of CH.

If I set up a formal system:

Socrates is a man
All men are mortal
Cassius is a cat

Then the proposition "Cassius is mortal" is undecidable in this formalism. If we want a formalism where we can reason about cats and their mortality, then we'd need to construct a different formal system with additional or changed axioms. We free to set up a formal system where cats are mortal like men, or immortal like gods, or have 9 lives (and an appropriate definition of "mortal" that accomodates the possibility of multiple lives) and so on.

My recollection is that for a long time mathematicians wanted to be able to prove Euclid's 5th postulate from the other four, but no such proof was found. One can do geometry without the 5th postulate and a certain set of geometrical proofs can be constructed, or one use Euclid's version of the 5th postulate and do the proofs of Euclidean geometry, or one can use an alternative to the 5th postulate and do hyperbolic geometry and so on...

The final thing to keep in mind is that all consistent and sufficiently complex formal systems will have undecidable propositions (thanks Goedel), so this is the natural state of affairs. But it also points out the unlimited nature of mathematics: when you note one or more undecidable propositions in the system you're working in, you get to pick* which way to go through the infinitely branching tree of possible formal systems...

But what about tautologies in this picture? Tautologies are just logical expressions that involve variables that evaluate to true for any truth assignments to variables they involve. For "p is true" "p or not p" evaluates to True. For "p is false" "p or not p" evaluates to true. Therefore "p or not p" is a tautology. For any finite logical expression, whether or not it is a tautology can be determined by enumeration. Even though CH is unprovable, it is still the case that "CH or not CH" is true irrespective of whether you assign the value true or false to the proposition CH. In that sense the tautology is still true despite the (necessary) existence of undecidable propositions in your formalism.

If you're looking reify or highlight the importance of undecidable propositions along the lines of "p is undecidable so it doesn't have a truth value", and if you want to keep playing a formal game, then you'll need a new symbol, in addition to true and false, to mark the statements in the formalism which don't (or can't) take on only true/false values. Now you've gone down the route of paraconsistent logics. However, this too is selecting a different branch, much closer to the root, in the tree of possible formal systems...

[This idea of a tree of different formal systems, where the nodes correspond to different undecided propositions and thus forms a complex, in a sense fractal, structure comes from a book I read several years ago maybe about computability, and I can't be sure, but maybe it was An Introduction to Goedel's Theorems by Smith 2007 ]

‘*’ There can be a constraint on your “freedom” here: if picking one way or the other results in an internally inconsistent formal system, then your hand is forced as inconsistent systems aren’t that useful to work on.

  • An undecidable sentence, but its very nature, is neither true nor false, there's no need to branch into different logics to make that statement. That was precisely the point of Gödel's theorem, against Hilbert's idea that every sentence did in fact have a truth value.
    – Sam
    Jan 20 at 0:22
  • Your example with the three propositions is clear, but my question remains: What would it mean to say (in that world) that the proposition "Cassius is either mortal or immortal" is true when each of the alternatives will be forever undecidable?
    – Sam
    Jan 20 at 0:33
  • 1
    @sam in that world do the proof by enumeration: for all assignments of truth values to the proposition C=“Cassius is mortal”, the proposition “C or not C” is true. So you can prove the LEM as applied to that proposition despite not being able to prove either of the clauses in the disjunction. As many people have pointed out, I’m limiting this discussion to bivalent logics since that seems consistent with your comments. having picked that constraint, “p or not p” is provably true, even for undecidable p.
    – Dave
    Jan 20 at 2:41
  • @sam Goedel showed that there are undecidable true statements scientificamerican.com/article/what-is-goumldels-proof
    – Dave
    Jan 20 at 2:44
  • @sam the space here is more complicated. There can be undecidable but true statements (technically what “undecidable but true” means is: p is undecidable in F; the formal system that is F augmented with the proposition “not p” yields a contradiction, and the formal system F augmented with p does not yield contradiction. Then there are what you might call “free” cases where both F+p and F+notp are self consistent. Or there can be cases where F+x makes p provable (and is consistent) and so on.
    – Dave
    Jan 20 at 3:02

You are essentially stating the position of Intuionist mathematics. Intuitionism doesn't consider the Law of the Excluded Middle (p or not p) to be valid.

What Intuitionism amounts to is the claim that nothing in mathematics is either true or false, but merely derivable or not derivable from the axioms. This idea comes from the formalization and axiomatization of mathematics that followed the discovery of Russel's paradox and the subsequent invention of ZF set theory to resolve it. The problem with this position is that 2+3=5 is not merely derivable but true. If you have a collection of two objects and a collection of three objects, you have, in combination, five objects.

  • 1
    While I was vaguely aware of the intuitionists ideas, I now see the value of that perspective (from yours and other replies here). But my problem was to try to make sense of "CH or not CH" from a classical perspective (that is, accepting the LEM). I like Bumble's answer which "solves" the problem for me by identifying the classical perspective with the Platonist view of Mathematics.
    – Sam
    Jan 19 at 3:27
  • Other systems in which p = !p could be valid: (1) quantum particle prior to wave collapse (2) politics Jan 21 at 15:32
  • @Sam, it's not really related to platonism. Your rules of inference basically pick out which sentences you will accept as propositions. If you accept, for example, sentences with vague conditions like "roses are red", then some sentences may be neither true nor false. Logics that accept such sentences often add truth values (the above is an example from fuzzy logic). Once you add truth values, you typically drop LEM. The LEM is basically a filter that controls which declarative sentences you are dealing with. Jan 21 at 18:13
  • @DavidGudeman Your perspective is way more general and therefore harder to discuss. That's why I phrased the question in the specific case of mathematics, where things are more clearly defined.
    – Sam
    Jan 22 at 5:41

It is true that one or the other holds. Given a specific model of ZFC, it is true that either CH or not CH hold in it. It being undecidable merely means that you can't prove which one is true from inside the model. You just don't have enough information to be able to prove one or the other. Undecidability has more to do with provability than it has with "truth". In some models it is true, in all others it isn't, but in all of them, we can't know from just looking from inside the model. And in all cases, either it holds, or it does not.

  • If you believe that "given a specific model of ZFC then either CH or ¬CH holds in it" then you probably agree with the Platonic (or "realist") position where any model is assumed to exist independently of us in a separate universe where it abides there for eternity, and we mere mortals are only allowed to explore what little we can in that universe and "discover" its truths. Not that there's anything wrong with that.
    – Sam
    Jan 19 at 19:11
  • 1
    @Sam Wouldn't the Platonic position be about believing that there's some "true" model of ZFC - separately from the question of whether CH or ¬CH holds in any given model? Jan 20 at 2:18
  • @MishaLavrov It's a highly subjective matter, but I think that's the case. The Platonic position assumes the objective existence of a "mathematical universe", and once that's accepted is kind of contradictory to start talking about an alternative universe, so whatever it is that ZFC represents must be unique.
    – Sam
    Jan 20 at 15:57
  • In that sense I don't, I don't believe there is an objectively "right" model of ZFC. I do believe all models exist in some mathematical universe independent from us. Bear in mind those models exist in a higher, non-ZFC meta theory, so I wouldn't be so sure it's right to think of ZFC as "the mathematical universe". I don't doubt there is some abstract, complex and self-contained mathematical universe, but models of ZFCs are merely parts of it and they can be different. (cont.)
    – Uretki
    Jan 21 at 8:44
  • 1
    @Sam : The statement ‘given a specific model of ZFC then either CH or ¬CH holds in it’ is itself a theorem of ZFC. You don't have to be a Platonist to state it (although there are some things you can't be, like an intuitionist). Jan 21 at 19:11

In the example you give, exactly one of those things is true. Either CH is true or it isn't. The fact that we don't know and can't prove whether or not CH is true doesn't mean that it's neither true nor untrue, but rather just that we don't know and can't prove it. Something being unprovable or even unknowable does not change that it's either true or it isn't.

To move away from formal logic a bit to a more "real-world" example, consider a murder trial. The jury is presented evidence both in support of guilt (by the prosecution) and in support of innocence (by the defense.) The jury may not have sufficient evidence to completely prove either the guilt or innocence of the defendant. However, that doesn't change the fact that the defendant either committed the murder or they did not. The jury may never have any way to know for sure which of those things is true, but that doesn't change the fact that one of them certainly is.

  • You wrote: "In the example you give, exactly one of those things is true". How so? My point is precisely that we can't affirm the truth of CH or ¬CH. As for your second point, discussing "real-world" examples would take us to a whole new level of complexity, one where I don't think we could have a fruitful discussion. I prefer to stay in the simple world or formal logic and mathematics, where, as you can see from the answers/comments provided, there's plenty of interesting things to discuss. But that's just my preference, I don't mean to downplay the importance of applied logic.
    – Sam
    Jan 19 at 18:34
  • @Sam As mentioned in the answer, us knowing whether or not CH is true or even having a way of possibly knowing whether or not it's true doesn't affect at all whether or not it's actually true. The only way to change that is to redefine what "true" means, which, while perhaps leading to interesting discussions, wouldn't change that the Law of the Excluded Middle remains true under the definition of truth it was stated in reference to.
    – reirab
    Jan 19 at 19:29
  • I'd like to know what you mean by CH being "actually true" (or ¬CH, same thing). From Gödel and Cohen results we know there is a model of the standard set theory axioms (ZFC) where CH is true and there is another model where it is false. Problem is, as far as ZFC goes, those two models are identical, so talk about something being "actually true" sounds very mysterious to me.
    – Sam
    Jan 20 at 0:04
  • 2
    @Sam For LEM to not apply you need more than just an undecidable problem, you need some situation where A and ¬A do not form a true dichotomy. Nothing about the CH problem implies this. It doesn't matter whether or not you can identify which is the case, only that ¬A cover all possibilities other than A. We don't (yet) know the quadrillionth digit of Pi (at least not today - check again tomorrow), but it's either 4 or not 4.
    – Corey
    Jan 24 at 6:25
  • 1
    @Sam Our ability to know that it is either 4 or 5 is not predicated on our ability to know which one of those it is. If 4 or 5 are the only possible values, then it's one of those regardless of if we know which one it is or have a way of knowing.
    – reirab
    Jan 24 at 15:39

If "p or not p" has a truth value then it's truth value better be true or you've got an internally contradictory system, and you run afoul of the principle of explosion. Note that "p or not p is false" is logically equivalent to "not p and p is true", which is the canonical way of expressing an internal contradction.

You can prove “p or not p” via reductio: take some already proven true proposition x. Assume “not (p or not p)” for the undecidable p. Get “(p and not p)” from your assumption. Use this contradiction to derive “not x”.

The other route is to drop classical logic in favor of a paraconsistent or intuitionist logical formalism where the law of the excluded middle is not a tautology.

  • I'm not trying to argue that "p or not p" should be regarded as false. My point (and question) is that when we say it's true, we imply that one of the options must hold. And in the example I gave neither option holds, so what's the deal?
    – Sam
    Jan 18 at 18:32
  • @Sam So you want to build a logic where "x or y" need not have a well defined truth value, you can do that, but then you're building some more complicated formal system than is usually implied by these statements. Note that my link is to a section of the SEP article on paraconsistent logics, which might get at what you are thinking of.
    – Dave
    Jan 18 at 18:37
  • No, sorry, I'm not trying to go in that direction. I fully accept that "p or not p" is true, but I'm trying to find a way to interpret that truth in the context of undecidable statements like CH. It seems to me that "CH or not CH" is in some kind of limbo stage regarding its "real" truth value, I'm not being very formal here but I hope you get my meaning.
    – Sam
    Jan 18 at 18:53
  • 2
    The principle of explosion is a about the Law of Non-Contradiction, not the Law of the Excluded Middle.
    – Sandejo
    Jan 19 at 4:08
  • 2
    @Dave That logical equivalence holds in classical logic, but not in intuitionistic logic. Intuitionistic logic lacks LEM but it has the principle of explosion, so we do not need to resort to paraconsistency in order to accommodate a rejection of LEM. So Sandejo is correct to point out that explosion relates to non-contradiction rather than LEM.
    – Bumble
    Jan 19 at 13:25

how does someone who accepts the law of the excluded middle come to terms with the "truth" of the statement "CH of not CH"?

Accepting the law of the excluded middle essentially means you're talking about the classical bivalent logic. "CH", which is for our purposes neither true nor false, is not a proposition it that logic, so the truth of the statement containing "CH" simply cannot be evaluated.

Such a proposition could be handled by e.g. finite-value logic, but then you need to drop the law of the excluded middle.

  • I don't understand your statement about CH. It's a valid first order sentence in the language of formal set theory, and I'm identifying "true" with "provable", so "CH ∨ ¬CH" is true because, being a tautology (= LEM), it's provable (with a one-line proof). But nothing can be said about CH or ¬CH in this regard.
    – Sam
    Jan 20 at 15:04

The decidability and provability of any particular proposition P are irrelevant here. "P or not P" is derived directly from the definition of "not," as it is used in propositional logic. Here's how I think of it:

Let U denote the set of all possible combinations of truth values of all possible propositions.

Let P denote a subset of U wherein some arbitrary proposition is true.

Let "not P" denote the absolute complement of P.

Therefore, according to these definitions, the union of P and "not P" is identical to U, and sets P and "not P" are disjoint. In other words, we can conclude that all members of U are included in either P or "not P", and therefore that either P is true or "not P" is true, even when we have no knowledge of any particular member of U.

  • That would work if one had a clear idea of what U is, but that is not the case here, the "universe" of all sets is not a well defined concept..
    – Sam
    Jan 19 at 1:44
  • @Sam Is the word "possible" the sticking point?
    – Sequoyah
    Jan 19 at 1:58
  • Both "possbile" and "state" are troublesome but "universe" is the real problem. You can't talk about the possible states (whatever that means) of something you have not defined.
    – Sam
    Jan 19 at 3:10
  • @Sam Universe eliminated.
    – Sequoyah
    Jan 19 at 3:39
  • To say that "P or not P" is derivable from the definition of 'not' is question-begging. This is true for the semantics of classical negation, which is why LEM holds for classical logic, but other logics have a different semantics. In particular, intuitionistic 'not' has a semantics that does not support LEM or double negation elimination. The whole point of the question is in effect concerned with whether classical logic is applicable to the entire realm of mathematical propositions and this is ultimately a question in the philosophy of mathematics.
    – Bumble
    Jan 19 at 4:31

Thank you for your question and comments Sam. Like you, I have recently become interested in this topic, and so for what it’s worth I will add my two cents.

I have found that Per Martin-Löf’s Intuitionistic Type Theory, as a sort of formalization of Brouwer’s intuitionism, provides a plausible interpretation of logical assertions such as P ∨ ¬ P. In the type theoretic framework, a proposition is conceived as “the type of its proofs,” and a proof is a mathematical object that is constructed according to a precisely defined set of rules. Thus, if p is a proof of the proposition P, then one uses the notation p : P to indicate that p “has type” P, and a demonstration that “P is true” entails the construction of a proof object p : P. In this setting, to construct a proof of P ∨ ¬ P (which is also a type since it is a proposition), one must be able to provide a previously constructed object p : P or q : ¬ P. In the context of the Continuum Hypothesis, as you have already pointed out, there is no formalized proof of either CH or ¬ CH, and so it is not possible to construct an object of “type” CH ∨ ¬ CH. Hence, there is no basis for the judgement that the disjunctive proposition is true.

The essential philosophical claim of intuitionism is, in Arend Heyting’s words, that “a mathematical assertion affirms the fact that a certain mental mathematical construction has been effected.” To the extent that mathematics is at its core a mental activity, I am fairly convinced by his argument that “if ‘to exist’ does not mean ‘to be constructed,’ it must have some metaphysical meaning, and it cannot be the task of mathematics to investigate this meaning or to decide whether it is tenable or not.” What I find so appealing about Per Martin-Löf’s Intuitionist Type Theory is that incorporates these deep philosophical insights into a viable foundation for the practice of mathematics.

I have only recently encountered these ideas while reading about the ongoing project to formalize mathematics in theorem proving environments such as Lean and Coq, which are based on the language of Type Theory. For a more thorough treatment of this subject, I would recommend the lectures of Robert Harper at Carnegie Mellon University which can be found online.

  • Thanks for the reference to Intuitionistic Type Theory, never heard of it before but sounds quite interesting. The SEP has a long article on precisely that topic, looks good.
    – Sam
    Feb 24 at 23:31

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.