[FOM] Re: Constructive analysis

[Andrej Bauer]

Bas' equation
                      TTE ~ BISH + CC + MP + FT

should be amended with two axioms that get used all the time:

                 TTE ~ BISH + CC + MP + FT + NC + SE

Here NC is "number choice" or "countable choice", namely, for any set A,
a total relation from natural numbers to A has a choice function:

  (forall n : N. some a : A. phi(n, a)) ==>
     (some f : N --> A. forall n : N. phi(n ,f(n)))

The second axiom, SE, is the axiom of not-not stable equality, i.e.,
for any set A, and all x, y in A,

                     (not (not (x = y)) ==> x = y

(By the way, what is "continuous choice"? Perhaps Bass meant
"countable choice"?)

The exact relationship between TTE and "BISH + CC + MP + FT + NC + SE"
can be explained in terms of realizability, as follows.

There is a realizability model T, denoted as Rep(N^N, eff(N^N)) or
some such, which is a category that has two crucial properties making
it interesting for computable analysis:

(i)
    it contains all countably based T_0-spaces, which suffices to do
    most of classical analysis. (It actually contains more than that,
    so that even spaces of distributions and similar things are
    present).

(ii)
    in T it makes sense to ask, in general, whether a map f : X --> Y
    is computable in the sense of Turing. Even more, it makes sense to
    ask, in general, whether any given "for all-exists" statement can
    be "computably realized".

Such happy marriage of topology and computability is of course
relevant to computable analysis, which is why the "TTE people" like it
so much. In essence, TTE _is_ the study of the realizability model T.
Since the construction of T is performed in ZFC (probably just a small
part of it), we can use all tools available in ZFC to prove theorems
about T. In this sense, the TTE school "uses classical logic" to prove
results about "computability".

The logic and the axiom system

                    BISH + CC + MP + FT + NC + SE                (*)

is related to TTE because it can be soundly interpreted in T. Thus, an
alternative way of doing TTE is to develop analysis a la Bishop within
the system (*), and then interpret it in T. In principle, this
approach is less powerful than using ZFC, but in my opinion is much
more elegant because it is conceptually cleaner and more abstract.

In fact, most (if not all) theorems and the proofs generated by the
TTE school, can easily be seen to be T-interpretations of theorems and
proofs carried out in (*). In this sense, the TTE people do not really
use all the power of ZFC.

When asked about their preference for using ZFC over (*), the TTE
people usually claim ZFC to be "simpler to use" and "generally better
known by normal mathematicians". I strongly disagree with the former
and take the latter as evidence that "normal" mathematicians are in
need of "abnormal" education.

An analogous story can be told about the "Russian school", the system

                         BISH + CT + MP + NC + SE

and the realizability model known as PER(K_1).


Andrej Bauer
Institute for Mathematics, Physics, and Mechanics
Ljubljana, Slovenia