[FOM] Intermediate value theorem (and ASD)

[Paul Taylor]

Aaron Avron said (under the subject line "When is it
appropriate to treat isomorphism as identity?") that
geometric intuitions dictate that the mean-value theorem
(if f(0)<0 and f(1)>0 then f(x)=0 for some x in [0,1])
should be valid for any adequate notion of "continuous function".

The following remarks are based on Sections 1 and 2 of my paper
"A lambda calculus for real analysis", which you can get from
    www.PaulTaylor.EU/ASD/lamcra/
Also, my construction, with Andrej Bauer, of the Dedekind reals in
ASD, a calculus that DOES NOT USE THE POWERSET, or any sets, is at
    www.PaulTaylor.EU/ASD/dedras/

Following Errett Bishop's dictum that "If God has mathematics that
needs to be done, let Him do it Himself",  I suggest that the debate
over the intermediate value theorem is rather sterile unless it is
conducted in the setting of actually wanting to CALCULATE a number
(or Euclidean point)  x  that satisfies f(x)=0.

In the standard constructive account (which, as you will see,
I do not regard as the end of the story) of the intermediate
value theorem, there are two theorems:

(1) The "approximate" one: for ANY continuous function as above,
and any epsilon>0, there is some point x for which |f(x)|<epsilon.

(2) The "restricted" one: if the function satisfies a certain
"non-hovering" or "locally non-constant" pre-condition, then there
is (indeed, we can find) x such that f(x)=0.   The pre-condition
asks that any inhabited open interval contain a non-zero value of f,
in other words it excludes the existence of a non-trivial interval
on which f=0.

(Peter Schuster (TCS 305 (2003) 433-455) has also given a third
result, based on a uniqueness condition that I regret I cannot
recall precisely, but this doesn't quite fit into my story anyway.)

I don't know what kind of mathematics Aaron believs that Adam and
Eve did in the Garden of Eden where geometric intuition prevailed.
Maybe all of their functions were differentiable, and/or they used
Newton's algorithm to solve equations.

IF THE FUNCTION IS AMENABLE TO SOLUTION BY NEWTON'S METHOD
THEN IT ALREADY SATISFIES THE NON-HOVERING PRE-CONDITION.

I am not a numerical analyst, but would invite any numerical
analysts who might be reading this to examine the pre-conditions
of any other algorithms they know.  I believe that they will
always be able to prove the non-hovering condition from these
pre-conditions.  I would be very interested to hear otherwise.

In other words, the classical mathematician who is not satisfied
with the standard constructive intermediate value theorem (2)
has no genuine interest in actually obtaining solutions of
equations.

(In any case, you can deduce the classical theorem from the
constructive one by an easy application of excluded middle:
either the function hovers, ie it has an interval of zeroes,
or else it doesn't and the constructive result applies.)

Now I shall introduce some ideas of my own, for which you should
note that I call myself a "constructive" mathematician, but
I am NOT a follower of Bishop, and in particular I DO BELIEVE
that [0,1] is compact in the "finite open sub-cover" sense.

It seems to me that, in order to be able to grasp x with f(x)=0,
you need a foothold on the function, ie points y and z with
f(y)<0 and f(z)>0.

DEFINITION   By a "STRADDLING INTERVAL", I mean such a pair,
[y,z] or [z,y], with f(y)<0 and f(z)>0.  If we want to solve
equations in R^n, this notion is generalised to a sphere that
"encloses" zero, in the sense that f!=0 on the sphere, but 0
lies in the interior of the image of the ball.

NOTATION  For any open set U,  write <>U   ("diamond", "possibly"
or "may") if U contains a straddling interval.

PROPOSITION   If f doesn't hover then <> takes ("arbitrary")
unions to disjunctions.  On this pre-condition, the proof uses
connectedness of R, but there is a much easier proof if f is
an open map, for example if it is continuously differentiable
with non-zero derivative.

Since it preserves "arbitrary" unions, in particular it preserves
directed ones, so  <>  is actually a Scott-continuous function
of U,  ie from the topology on R to the Sierpinski space.

Plainly, I'm not going to introduce one modal operator without
its friend:

NOTATION   Consider the function f on a compact domain and let
Z be its closed and compact subspace of all zeroes.   For any
open set U,  write   []U  ("box", "necessarily", "must")  if
U contains (covers) Z.

THEOREM   []  and  <>  satisfy the mixed modal laws
  [](U cup V) => []U or <>V     <>(U cap V) <=  []U and <>V
if the function is non-singular.   If it is singular,  the
first law fails but the second is still true.

Therefore, in place of the sterile debate about whether the
intermediate theorem is "really" true of "all" functions,
we have an analysis of the situation in which the zeroes of
a function with parameters are described by two functions
of higher type that are continuous in (U and) those parameters,
THROUGHOUT the paramater space.

For example, the function could be a cubic polynomial whose
coefficients are the parameters.  Then  [] and <> vary continuously
in the parameters, satisfying one modal law everywhere and
the other everywhere apart from at coincidences of the zeroes.

Notice that I wrote "arbitrary" with quotes around it.   This
is because I am interested in combining this topological
question with recursion theory, in which this word is replaced
by "recursively enumerable".   The latter phrase and my diamond
operator are manifestations of the notion of "overtness".
Classical mathematicians are completely blind to this notion,
because in their world all spaces are overt by "force majeure".

This leads into my research programme "Abstract Stone Duality",
which Andrej Bauer has already mentioned in response to Aaron
Avron's comments.   ASD is a re-axiomatisation of computable
constructive general topology in a language that only mentions
topological ideas.  It makes absolutely no recourse to set theory,
even in the form of elementary toposes or type theories such
as that of Per Martin-Lof.   Last year, Andrej wrote a program
that solves equations using the ASD language, and in particular
Dedekind cuts instead of Cauchy sequences.

Finally, as this is my first posting to FOM, I should introduce
myself.   I am a categorist by training, and wrote a book called
"Practical Foundations of Mathematics"  (CUP, 1999).  In this,
the phrase "category of sets and functions" means any elementary topos
with natural numbers, but not necessarily excluded middle, choice
or replacement.  The final pages of the text give my version of
replacement in a categorical setting.   I have been working on
the ASD programme since the book was published.

Paul Taylor
www.PaulTaylor.EU
pt09 @ PaulTaylor.EU