[FOM] Intuitionists and excluded middle

[Ron Rood]

This is a note of qualification with respect to the current discussion 
on whether or not to accept the law of the excluded middle (LEM) as a 
valid logical principle, and how this issue relates to "constructivism."

Brouwer and many of his followers had certain difficulties with LEM 
(though Brouwer did not reject this principle in general; for example, 
he accepted "A(x) or not-A(x)" for decidable predicates A). While 
Brouwer may certainly be considered as a constructivist of a sort, not 
every constructivist had difficulties with this particular principle. 
Kant, for one, may be considered a constructivist: using his own 
specific notion of construction, he considered construction as an 
essential feature of the mathematical method, and the mathematical 
method of proof in particular. At the same time, however, Kant 
considered proofs by reductio as legitimate, I mean, proofs which 
proceed from the assumption that a proposition is false, via a 
contradiction, to the conclusion that this proposition is true (see, 
e.g., p. B817 and p. B820 from the Critique of Pure Reason).

(Let us call such proofs proofs by *strong* reductio, in 
contradistinction from proofs which proceed by *weak* reductio. The 
latter proceed from the assumption that a proposition is true, via a 
contradiction, to the conclusion that this proposion is false. Note: if 
one accepts proofs by strong reductio, then one is also committed to 
accepting proofs by weak reductio. Proofs by weak reductio are 
acceptable in intuitionistic propositional logic; proofs by strong 
reductio are not)

Given that Kant accepted proofs by strong reductio, it follows that he 
accepted LEM:

1. not-(p or not-p)				assumption
2. p							assumption
3. p or not-p					from 2
4. (p or not-p) and not-(p or not-p)	from 1 and 3
5. not-p						from 2 and 4 (weak reductio)
6. p or not-p					from 5
7. (p or not-p) and not-(p or not-p)	from 1 and 6
8. p or not-p					from 1 and 7 (strong reductio)

The conclusion I draw is that the rejection of LEM as a universal 
logical principle is not intrinsically bound up with constructivism per 
se. There is no such thing. I would also say that the eventual 
rejection of LEM should not be turned on the supposed "uselessness" of 
proofs based on LEM. For example, one proof of Brouwer's fixed point 
theorem (every continuous mapping from the unit ball in R^n to itself 
has a fixed point) in algebraic topology proceeds by strong 
reductio.(*) Other examples of proofs by strong reductio in algebraic 
topology can be mentioned besides.(**) I see no reason to consider 
these proofs as "useless" (though they do not provide a witness of the 
object that is claimed to exist). Generally speaking, besides other 
virtues, I would say that algebraic topology throws a useful and 
interesting light on many traditional topological problems.  But of 
course, a lot depends on what one understands by a *usefull* proof. For 
example, a proof may be considered useful in the sense that it furthers 
mathematical research. Alternatively, it may be considered useful in 
the sense that is serves a particular application of mathematics. At 
any rate,  I would hold instead that the issue of whether or not one 
accepts the law of the excluded middle is bound up with one's 
understanding of *construction* to begin with (considered as a feature 
of mathematical proof). Ultimately, however, I believe it requires us 
to seriously consider, or reconsider, the question: "what is 
mathematical proof?"

(*) The proof I have in mind proceeds in very broad outlines as 
follows. Let X be a topological space and let Y be a subspace of X. 
Call r : X -> Y a *retract* if r is continuous and if r | Y is the 
identity mapping. Denote the unit ball in R^n as B^n. Denote the 
boundary of B^n as S^(n-1) (the (n-1)-dimensional unit sphere). We also 
need the following:

Lemma: there is no retract B^n -> S^(n-1).

Now, let f : B^n -> B^n be continuous. Suppose f has no fixed point. 
Define r : B^n -> S^(n-1) as follows: r(x) is the point of intersection 
of the ray { x + t(x - f(x)) : t >= 0} and S^(n-1). Since f has no 
fixed point, r(x) is indeed unique. Further, r is continuous and
r | S^(n-1) = 1. In other words, r is a retract, which contradicts the 
lemma stated above.

(**) For example, of the so-called "hairy ball theorem", i.e., the 
theorem saying that every vector field on S^2n (the 2n-dimensional unit 
sphere) vanishes somewhere.

Ron Rood