[FOM] Intermediate value theorem (and ASD)

[Paul Taylor]

I'm sorry for getting Arnon Avron's name wrong.  He has asked:

> Does any of the constructions you mention of R provide an isomorphism
> of R^2 with the Euclidean Plane *as was grasped by Euclid*
> (and I believe by all other people, living and dead)?

Euclidean geometry is a more or less clearly defined system
that, in modern terms, has a model in the field extension of
the rationals that is obtained by adding all real square roots.
This is (I believe) decidable.  Also, it does not (necessarily)
involve any of the order-theoretic or topological notions that
would make the intermediate value theorem an interesting question
from the point of view of the present discussion.   I suspect
that the same would be true of any particular stage of real
mathematical history prior to 1820 that you might choose.

>> I don't know what kind of mathematics Arnon believs that Adam and
>> Eve did in the Garden of Eden where geometric intuition prevailed.

> There is no sufficient evidence about Adam and Eve,

This what makes them useful as a rhetorical device for the "age of
innocence" that Arnon seems to be trying to evoke.   If readers will
bear with me, and look at what I actually say instead of what they
presume that I am saying, they will see that this is my point of view too.

> Thus geometric intuitions dictate that the mean-value theorem
> (if f(0)<0 and f(1)>0 then f(a)=0 for some a in [0,1])
> should be valid for any adequate notion of a "continuous function"
> (i.e. a notion which has pretensions to correspond to
> the idea of a function whose graph can be drawn with a pencil
> without leaving the paper). As far as I know, this theorem fails
> for the constructive theory of the reals (and continuous
> functions on them).

I stated the standard constructive versions in my previous posting.

>> Maybe all of [Adam and Eve's] functions were differentiable,
>> and/or they used Newton's algorithm to solve equations.

> Euclid was constructive *without doing calculations*. He proved
> existence of points by CONSTRUCTING them (using abstract instruments),
> not by calculating approximations of them.

> Euclid definitely did not identify curves with functions. You seem
> to forget the correct order of things. Curves are intuitive and
> come first. Differentiable functions are only (rather problematic)
> approximations.

If you are drawing a curve with a pencil then, according to Newton's
laws of motion, it will move in a straight line unless you apply a force,
in which case it will accelerate.  These are notions of (double)
differentiability, so Newton's method of finding the point of
intersection of the curve with the axis apply.

Actually, I am not correct in suggesting that the issue with the
intermediate value theorem lies in non-differentiable functions.
The counterexample that is usually found in constructive treatments
is a piecewise linear function that looks like this:

                              /
                        -----/
                       /

Brian Davies, in his discussion of "Pluralism in Mathematics",
uses the curve  y = x^45 instead, but that relies on the identification
of the plane with R^2, to which you object.

Given a pencil-drawn curve that is pretty close to the axis (reference
straight line) but does move away from it somewhere on opposite sides,
how do you imagine finding WHERE it crosses?  Maybe you will use a
microscope,  or an electron microscope, and eventually pin-point the
individual carbon atoms in the graphite of the pencil curves.
Then we run into problems of physics and the identification
of the physical piece of paper with the "ideal" Euclidean plane.
But I will try to bear with you, abandoning physics as well as arithmetic.

Using our idealised mathematical microscrope, I think that, in order
to find a particular crossing-point, we have to be able to identify
miniature versions of the hypothesis of the intermediate value theorem
at every possible magnification.  That is, arbitrarily small
"straddling intervals" in the sense that I defined before.  This
idea is explored in "A lambda calculus for real analysis".

So, in the case of the two counterexamples above, the best that you
can get is an INTERVAL "somewhere along which" the curve "crosses"
the line, rather than a point.

I am sorry if I am still being stupid in not grasping Arnon's
> direct intuition concerning the meaning and TRUTH of the
> theorems of the Euclidean Geometry
or
> the Euclidean Plane *as was grasped by Euclid*
> (and I believe by all other people, living and dead)
so maybe he could explain where I am going wrong.

Turning to the construction of R and friends,

> And do constructivists have any theory/grasp of the *geometrical*
> plane which is independent of their theory (theories?) of the real
> numbers?

Yes, please use the plural, because (for example) Brouwer, Bishop
and I disagree with each other.

>> ASD, a calculus that DOES NOT USE THE POWERSET, or any sets

> So it uses something else, which is no less problematic (like A->B
> or A^B or whatever). Nobody can do what cannot be done.

I think what Arnon means here is that this cannot be done in the
framework of set theory.   This is a bit like saying that you can't
write programs in FORTRAN without using FOR loops. Of course - this
is what FORTRAN is like, but there are other programming languages.

Plainly the notion of real number is in some sense more powerful
than that of the integers or rationals,  so SOMETHING else is
needed.  Using quotes for as yet undefined terms, for me a "real
number" is given by a "Dedekind cut", which consists of two parts.
The left part is an "ascending real", which is a "predicate" that
says of a rational number whether it is less than the "real"
number that is being defined.  Unlike Cauchy sequences, such
predicates emerge very naturally in many situations, for example
from Riemann integration.

You may think that this "predicate" has to be a subset, and the
whole real line is a set of pairs of subsets.  That is one way
to see what my construction means if you come from a set theoretical
background, but it is not what *I* mean by it.

Firstly, the "predicate" (defining an ascending real) and the "type"
(of real numbers) are linguistic ideas and not material ones: they say
what it means for some string of symbols to denote an (ascending) real.

Secondly, the notions of (higher order) predicate and subset in set
theory are vastly more powerful than that of a recursively enumerable
subset.

Logically, an ascending real is given by a Sigma^0_1 formula
with a rational variable.   More usefully, it is a program, and
Andrej Bauer has implemented a prototype that computes with such
programs.   However, this is no more dependent on a particular
programming language or formulation of recursion theory or predicate
calculus than it is on set theory.  Also, whilst the techniques
of category theory and type theory were used in the development
of the ASD calculus, it stands on its own feet and it not intended
to be interpreted in a topos, or a type theory such as Martin-Lof's.

Now let me return to Arnon's question about the intermediate value
theorem in the Euclidean plane.  I'm genuinely not clear what
distinction he has in mind between this and R^2, given that
the interpretation of algebra in geometry and vice versa were
understood by the Greeks and Arabs.

Maybe Arnon's point is that he doesn't want to introduce arithmetic.
In fact, I had constructed the Dedekind completion of a dense linear
order, and proved my version of the intermediate value theorem,
BEFORE Andrej and I defined the arithmetic operations.  This is how
the first paper (dedras - The Dedekind Reals in Abstract Stone
Duality, with Andrej Bauer) is organised.  The second paper
(lamcra - A Lambda Calculus for Real Analysis), which can be
read independently,  was subsequently reorganised, with the
arithmetic early on, simply because this is conventional.

Section 4 of lamcra, which begins the description of the ASD
calculus, does what Adam and Even would have done - it introduces
the arithmetic operations and relations.   Section 5 uses
the lambda calculus to express the predicates that I mentioned
above.  Section 6 introduces Dedekind cuts and illustrates the
calculus by showing that any Cauchy sequence has a limit.
Section 7 begins the discussion of topology, and so on.

Paul Taylor
www.PaulTaylor.EU/ASD/analysis
pt09 @ PaulTaylor.EU

[This merges two private replies to Arnon, so I am sorry
if the flow of the resulting narrative is broken in places.]