[FOM] Intuitionists and excluded-middle

[Lew Gordeew]

REVISED
---------------------------------
Hendrik Boom <hendrik at pooq.com> wrote: 
> Take the rational c that Paul Halmos provides us between a and b.
> Then (c+b)/2 is irrational, and between a and b.

Good job! We can thus directly obtain the desired constructive function f
from H = {(a,b) in R: a < b} to R such that a < f(a,b) < b and f(a,b) is
irrational, if so are both a and b. To this end, choose rational
approximations I=[p,q], of a, and J=[r,s], of b, whose diameter is so small
that q < r, and then let f(a,b):= (q+b)/2 (or (a+q)/2 or (r+b)/2 or
(a+r)/2). Since by definition p < a < q and r < b < s, this yields the
result.

REMARK. Obviously this construction fails for a = b. Also note that "=" is
not decidable in the constructive continuum. Now let us replace open
half-space H by closed half-space H* = {(a,b) in R: a <= b} and ask if there
is a constructive proof of the sentence

S: (forall reals a <= b)(thereis real c)
((a, b both irrational and a < b) -> (c irrational and a < c < b))

Since H* is closed, by standard compactness arguments, a constructive proof
of S would provide us with _classically_ continuous function f: H* -> R such
that f(a,b) is irrational and a < f(a,b) < b, provided that a, b are both
irrational and a < b.

So perhaps S is a more appropriate constructive counterpart of Halmos
problem?

Regards,
LG

-- 
Telefonieren Sie schon oder sparen Sie noch?
NEU: GMX Phone_Flat http://www.gmx.net/de/go/telefonie