Supplement to Luitzen Egbertus Jan Brouwer
Strong Counterexamples
Here is the argument for Brouwer's strong counterexample to one form of PEM that he mentions in his paper from 1928, ‘Betrachtungen über den Formalismus’ (‘Reflections on Formalism’). We will show that
¬∀x∈where P(x) = ‘x is rational’ and(P(x)
¬P(x))
is the
intuitionistic continuum. Accordingly, in this context real numbers are
to be understood intuitionistically (namely, as convergent choice
sequences).
We first show that the continuum cannot be split, that is, there are
no non-empty spreads A and B such that
A∪B =
and A∩B = Ø. For assume there are; then
the function
f :
→
defined by
f(x) = {
0 if x ∈ A 1 if x ∈ B
is total and therefore, by Brouwer's continuity theorem (generalized
from [0,1] to
),
continuous. But then f must be constant,
so either A or B is equal to
,
and the other spread must be empty. This however contradicts the
assumption that both A and B are non-empty.
From the fact that the continuum can't be split it follows that
∀x∈(P(x)
¬P(x)) is false. For if it were true, we could
obtain a splitting of the continuum by letting f assign 0 to
the rational real numbers (A), and 1 to the irrational ones
(B); but this is impossible, as just shown. Hence,
¬∀x∈(P(x)
¬P(x)).
Brouwer established that
can't be split in 1927, in footnote 10 of ‘Definitionsbereiche
von Funktionen’ (‘On the Domains of Definition of
Functions’).
Other strong counterexamples that Brouwer devised are
- ¬∀x∈(¬¬x < 0 → x < 0)
(Brouwer, 1949a)
- ¬∀x∈(x ≠ 0 → x < 0
x > 0) (Brouwer, 1949b)
These are based on the fan theorem and on the mathematical theory of the ‘creating subject’ (Heyting, 1956, chs. III and VIII; van Atten, 2003, chs.4 and 5).