# Do intutionists think the law of the excluded middle is universally, metaphysically false?

The law of the excluded middle (LEM) is that every well-formed formula of a sound logical system is either true or false. In systems that do not reject the law of the excluded middle, there can be undecidable propositions, which means that the syntax is incomplete. However, this would conventionally imply that the undecidable statement is either true or false, we just don’t know which.

Rejecting the law of the excluded middle means that “for all P, P or not P” does not hold.

What does this say about an intuitionist’s worldview?

For a Platonist, if I can prove that “Person A is the murderer” leads to contradiction, then one can resolutely believe that Person A is not the murderer.

Would an intuitionist earnestly believe that that conclusion does not follow? How do they interpret rejecting the LEM as a principle of reasoning in the world?

• Apr 10 at 3:59
• The sense of your example is clear, discrete, closed and finite as commonly understood, both Platonists and Intuitionists would agree, but algebraically speaking as you may already know there's no notion of set-theoretic complement at all for the relatively conservative intuitionistic logic proposition compared to the classical one thus LEM may not always hold, only with implication operation usually in the form of relative interior of some resultant set in the open set topological spaces Heyting lattice, and the interior may be undecidable per the openness and infinite choice-less nature... Apr 10 at 5:40
• To say that LEM is "universally false" means that it is contradictory: but the negation of LEM is not intuitionistically derivable. Apr 10 at 10:04
• "In systems that do not reject the law of the excluded middle, there can be undecidable propositions, which means that the syntax is incomplete." Why is a syntax necessarily incomplete if there is a trivalent logic at play?
– J D
Apr 10 at 12:00
• In your specific example, or more generally, if statement A leads to a contradiction, then 'not A' is true. This is valid without LEM. What cannot be proven in general is if 'not A' is contradictory, then A, because that requires the use of the double negation rule, which is logically equivalent to LEM. Apr 10 at 12:58

Intuitionists reject the LEM, but they don’t reject proof of negation. That is, if A can be demonstrated to imply an absurdity, then A is false to an intuitionist. See here https://ncatlab.org/nlab/show/BHK+interpretation for interpretations of propositions and connectives from an Intuitionistic point of view.

Roughly, a formula A is true to an Intuitionist exactly if there is a construction showing that A. A disjunction is true exactly if at least one of its disjuncts is true, and a conjunction is true when both conjuncts are true. An implication is true for an Intuitionist whenever there is an algorithm that can transform a proof of the antecedent into a proof of the consequent. An existential is true exactly if it is true for some element in the domain of discourse, and a universal is true whenever it is true for every element in the domain of discourse.

Intuitionists don’t typically assign truth values other than ‘true’ and ‘false,’ but those propositions that neither have a proof nor a disproof (yet) are not given truth values. The divergence from Classical Logic then isn’t that there are more than two truth values, but that not every proposition can be assigned a truth value yet, since that would be equivalent to the assertion that there is a construction demonstrating the truth or falsity of any proposition.

Intuitionists hold that we accumulate mathematical knowledge over time that does not contradict past knowledge, and that we hold onto going forward. Whether or not that’s actually true is controversial, but that’s beside the point. Either way, Intuitionists demand an explicit procedure for proving that a formula holds in order for it to be true, which is why they reject LEM.

In a nutshell, the answer to the title question is: no.

See: Luitzen Egbertus Jan Brouwer, Unreliability of the logical principles (new English transl. of the original 1908):

Now the principium tertii exclusi: this demands that every supposition is either correct or incorrect, mathematically: that of every supposed fitting in a certain way of systems in one another, either the termination or the blockage by impossibility, can be constructed. The question of the validity of the principium tertii exclusi is thus equivalent to the question concerning the possibility of unsolvable mathematical problems.

As long as only certain finite discrete systems are posited, the investigation into the possibility or impossibility of a fitting can always be terminated and leads to an answer, whence the principium tertii exclusi is a reliable principle of reasoning. That also infinite systems, with respect to so many properties, are controlled by finite means, is achieved by surveying the denumerably infinite sequence of the whole numbers by complete induction".

Brouwer speaks of mathematics and not metaphysically, and the principle is valid in finite contexts and in some infinite one as well. Thus, it cannot be "universally false".

In systems that do not reject the law of the excluded middle, there can be undecidable propositions, which means that the syntax is incomplete.

This is based on a very bad misconception. The generalized incompleteness theorems apply to every kind of formal system that can ever be devised (whether by humans or not), and they may be based on any kind of logic (whether classical or intuitionistic) or no logic at all! Whatever the case, the system will be unable to prove or disprove (the translation of) some basic statements about finite strings (or programs, or natural numbers). Look at the linked post. It gives a way to write down a completely explicit statement W of the form "The program D halts on input D and outputs 0." for any given formal system S, such that S cannot prove (the translation of) W or its negation. This means that you are forced to accept that S is incomplete for program behaviour.

Rejecting the law of the excluded middle means that “for all P, P or not P” does not hold. What does this say about an intuitionist’s worldview?

Nothing. This is based on yet another misconception. Intuitionistic FOL (IFOL) is a formal system, and in itself has no meaning. There are infinitely many totally completely interpretations we can construct for IFOL (e.g. Kripke frames, BHK), but these are mathematical interpretations, again not about the real world. Similarly there are infinitely many different interpretations of (classical) FOL (e.g. standard semantics, boolean-valued models), and the standard semantics is a privileged one because it allows us to interpret FOL in reality.

So you would have to ask any person who claims to be intuitionist what kind of statements he/she accepts LEM for.

For a Platonist, if I can prove that “Person A is the murderer” leads to contradiction, then one can resolutely believe that Person A is not the murderer. Would an intuitionist earnestly believe that that conclusion does not follow? How do they interpret rejecting the LEM as a principle of reasoning in the world?

It is completely untenable to reject such conclusions, because absolutely nothing in the real world disobeys classical FOL. What he/she might reject is LEM for statements that cannot be grounded in reality (e.g. some set-theoretic statements). Note that your above example is actually a bad one, because ( ( A ⊢ ⊥ ) ⊢ ¬A ) is valid in IFOL. But my point is that ( ( ¬A ⊢ ⊥ ) ⊢ A ), which is invalid in IFOL, is absolutely valid for any statement A about reality.

Also, intuitionistic logic is not the only option to deal with ungrounded statements. Kleene's 3-valued logic is another option.

• +1. A slight notational issue: you should write A -> F |- ~A (F is falsum, I’m on mobile so I can’t type these symbols) instead of having two turnstiles Apr 11 at 13:07
• @confusedcius: In sequent-style or Fitch-style systems, you can have two "⊢", and arguably that's what exactly is happening, though you are right that these two are in some sense different too. It's a matter of preference what to emphasize. Using "⊢" emphasizes that it's about deducing contradiction. Using "→" emphasizes that it's tied to implication semantics. Apr 11 at 14:43
• Hmm I haven’t seen that before, but maybe it’s because the sequent calculus and fitch style that I’ve seen is in classical logic. But is it really needed to have the sequent be part of the object language’s syntax if the deduction theorem holds? Wouldn’t that make the object/meta language distinction more confusing? Apr 11 at 16:08
• "It is completely untenable to reject such conclusions, because absolutely nothing in the real world disobeys classical FOL." citation very much needed.
– Yakk
Apr 11 at 18:30
• @confusedcius: For example see the LK sequent-calculus. You are right that there is a potential for confusion between the two "⊢", especially among beginners. But my post was just meant to convey the mathematics and to emphasize that there is no need to tie the discussion to the semantics of implication. The issue here is entirely about the link between ( ¬A ⊢ ⊥ ), which is simply about deducing (not about meaning), and A. Apr 12 at 11:04

The answer to the question in the title is "obviously no", since the sentence "true or not true" is provable.

Moreover:

The law of the excluded middle (LEM) is that every well-formed formula of a sound logical system is either true or false.

No. It says that for every proposition A, "A or not A" is an axiom. It's not about truth.

In systems that do not reject the law of the excluded middle, there can be undecidable propositions, which means that the syntax is incomplete. However, this would conventionally imply that the undecidable statement is either true or false, we just don’t know which.

This makes no sense.

Would an intuitionist earnestly believe that that conclusion does not follow?

No, because you show us a trivial statement in intuitionistic logic. Remind that in almost all logics, even weaker ones, "not A" is an abbreviation of "A implies false". Your argument is of the form:

• assume A implies false;
• deduce from the assumption A implies false.

For a Platonist, [...]. Would an intuitionist [...]?

In logic, we do not care about people, but about proofs. Either a proof assumes the law of excluded middle, either it doesn't (you just have to read the proof to see if "using the law of excluded middle" is written somewhere to find out). A proof is basically an algorithm that a disbeliever in its conclusion can use to find out which hypothesis he or she would reject. That's it. What people believe or not is irrelevant to the matter.