# Systems without the law of excluded middle

If my understanding is correct (indeed, I think Wikipedia says this same thing) there are systems of logic in which the law of excluded middle does not hold. I can see how in some kind of generalization of logic we could have a system without the law of excluded middle, but then are these just abstract notions?

By that I mean, it seems that the 'standard' way of 'using' logic seems to be with the law of excluded middle, indeed if someone makes a sensible statement (i.e. not intentionally trying to be tricky) it seems to be either true or false. So do these systems which reject the law of excluded middle have a use, or deeper implication, or are they just generalizations in some sense?

• Just to be clear, are you asking if people use logics without LEM because of some "deeper" issues or just as an abstraction of classical logic? – Asaf Karagila Mar 28 '15 at 8:05
• John Bell talks about this in A Primer of Infinitesimal Analysis. LEM is not generally affirmable in smooth infinitesimal analysis (it doesn't apply to the infinitesimals) but it does apply in the underlying logic to certain types of statement. It fails 'just enough' to make the system work. – user117644 Mar 28 '15 at 8:05
• IMHO, rejecting LEM may be nothing more than an over-reaction to the internal contradictions of naive set theory, Russell's Paradox in particular. As with other radical "solutions," they seem to be throwing out the baby with the bathwater. I really can't imagine that the current, wildly successful system of mathematics (in which RP was resolved a century ago) will ever be replaced by a system that doesn't allow you to remove a double negation. – Dan Christensen Mar 28 '15 at 16:08
• @DanChristensen but they are not really exclusive. You probably could have some people doing math without lem and some people doing math with lem, co-existing peacefully (though I am not sure if any government would want to fund the former). – user631975 Apr 21 at 22:36

Some statements are genuinely neither exclusively true nor false. It may be because the axiom set is insufficient to prove a statement, or it may be that the axiom set is too strong and can prove some statement to be both true and false.

Consider 3 different ways of defining true or false:

• True if provable from axioms, false if disprovable from axioms
• True if intuition (or a model) suggests it is true, false otherwise
• An expression is true or false if it is matched by some grammar $G$ (though not necessarily sure which)

The first way is how Hilbert (and others) would have described true/false in mathematical terms. The second way Godel (and others) used to analyze the first way. The third is the law of the excluded middle.

The third definition is what most people who study mathematics but not necessarily logic use. One may write $\forall x ~:~ x > y$ and say "it must be true or false, because it is a well written statement". And $\forall > x ~ y @$ is neither true nor false because it is garbage. Or maybe $x > 1$ isn't necessarily true or false because it isn't a complete statement, as the $x$ is unquantified. The problem with this intuitive approach is that it implicitly creating a grammar (an algorithmically defined set of of strings) and associating true/false with this grammar.

This is not necessarily compatible with the first definition of truth, given above. What if all statements that follow from axioms don't necessarily form a nice decidable grammar? In fact, Godel's incompleteness theorems say that that is the case.

So in very carefully defined logics (such as what would be used to prove correctness of avionics software, where incorrectness leads to people dying), whether a statement is true or false is left to be proved. Rather than assuming the excluded middle, that some set of grammatically defined strings are necessarily true or false, rather whether a statement is true or false is left to be proven. In casual usage, this is no big deal, but in formal logic, the excluded middle can't safely be assumed as an axiom.

There is both a use and a deeper implication. Let me start with the deeper implication. At the beginning of the 20th century, there was a so-called foundational crisis in mathematics. Out of this, several schools of philosophy of mathematics emerged, one of which was intuitionism, fronted by L. E. J. Brouwer. Brouwer's idea was that mathematics is a creation of the humand mind and exists only in people's minds. Hence, he only accepted those mathematical truths which could be constructed in some sense. Now, the problem with the law of excluded middle (LEM) from this point of view, is that it allows you to make use of the reductio ad absurdum (RAA) proof technique which in turn allows you to prove things without actually constructing the thing you are proving. Essentially, RAA argues that since it can not be the case that $\neg P$, using LEM it must be the case that $P$, but it does not actually give a way to construct $P$.

This is a fairly esoteric and philosophical discussion, but it turns out to actually have some use. When we have a constructive proof, i.e. a proof that actually constructs what is to be proven, the proof also gives a procedure or an algorithm for doing this construction. Think of the Gram-Schmidt process, for example. The theorem says that every finite-dimensional inner product space has an orthonormal basis, but since the proof is constructive, it also gives an algorithm for actually generating such an orthonormal basis. This turns out to be extremely useful in many applications.