Subsection 5.1.5 Law of the Excluded Middle
We’ve just said that we will import all of the identities of Boolean logic into our system of predicate logic. There is one special case that we should say a bit more about.
The Law of the Excluded Middle:
For any statement P: P ∨ ¬P
The Law of the Excluded Middle (LEM) is a useful theorem proving tool.
Watch the video for a good example. In it, we prove that there exist irrational numbers x and y such that:\(x^y\) is rational.
Classical logic, following Aristotle, assumes both LEM and the Principle of Noncontradiction:
For any statement P: ¬(P ∧ ¬P)
In Boolean logic, both of these rules are tautologies:
|P||¬P||P ∨ ¬P||P ∧ ¬P||¬(P ∧ ¬P)|
In predicate logic, they are not. They (or some variant) must be asserted as premises. The Principle of Noncontradiction is not controversial, since it’s not possible to build a useful logical system without it.
LEM, however, is slightly controversial. There are philosophers and mathematicians (such as constructivists) who don’t assume it.
But consider the following derivation:
 ¬(P ∧ ¬P) Principle of Noncontradiction
 ¬P ∨ ¬ ¬ P De Morgan
 ¬P ∨ P Double Negation
 P ∨ ¬P Commutativity
Line  is exactly LEM. We have derived it from the (noncontroversial) Principle of Noncontradiction. Why then, must LEM be assumed as a separate premise if we want to use it? The answer is that, in predicate logic, Double Negation is not a tautology. It too is rejected by the constructivists.
Arguments for rejecting LEM (and Double Negation) fall into at least two categories:
Philosophical and mathematical ones. For example, mathematicians from the constructivist school do not want to accept, as a proof of the existence of some object x with property P, anything short of the exhibition of a specific such x or a concrete procedure for finding it.
Essentially linguistic ones. There are English sentences that, on first analysis, seem to contradict LEM in the sense that they do not appear to be either true or false. Further analysis often shows that the issue is the mapping from English into logic, rather than a logical problem with the LEM.
We will follow Aristotle and assume the Law of the Excluded Middle. Then we can prove Double Negation by running the derivation we just did, but backwards. (Alternatively, we could assume Double Negation and then prove LEM.)
 x is an integer Premise
 x is not negative Premise
 x is a positive integer LEM , 
 x is an integer Premise
 x is not even Premise
 x is an odd integer LEM ,