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?
 A: 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.
A: 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.
