[FOM] Intuitionists and excluded middle
Ron Rood
ron.rood at planet.nl
Sun Oct 16 10:07:30 EDT 2005
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
More information about the FOM
mailing list