What is the idea behind "p or not p" being a tautology?

Question

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"?

Answer 1

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

Answer 2

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.

Answer 3

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.

Answer 4

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.

Answer 5

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.

Answer 6

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.

Answer 7

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.

Answer 8

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.

Answer 9

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.

Answer 10

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.