[FOM] Re: Constructive analysis

[Vasco Brattka]

Andrej's nice characterization of TTE is a major step forward towards
a precise comparison of computable and constructive analysis. 

However, I have some comments on the alternative of using 
intuitionistic logic with the system 

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

and doing computable analysis directly (using classical logic).

Andrej wrote

> 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.

I do not believe that the whole question can be reduced to a 
matter of education. Of course, both alternative approaches
have their merits. 

Doing TTE directly means that representations (i.e. realizations) of 
objects are present all the time. On the first sight, this seems to be 
less elegant than decoupling intuitionistic proofs using (*) and their 
realizations. But one should not underestimate the intuition and guidance 
which is inherent in the representation based approach.

On the one hand, some theorems of TTE become rather artificial
if expressed in intuitionistic logic and the system (*).
(For instance, theorems of type
 "If x is A and  x is effectively B, then x is effectively C.",
 as mentioned by Bas.)
Although it might be possible to express these theorems in (*),
one can have some serious doubts whether one would ever have 
thought about these results without having in mind their realizations
in the concrete model.

On the other hand, as soon as negative results are concerned
(negative in the sense that something is not computable), one typically 
has to refer to the realizability model (or to some other results
which are already known to be unprovable in (*)).

In other words: although the system (*) leads to a nice decoupling
of TTE into intuitionistic proofs and their realizations, this also
leads to a decoupling in the mode of thinking. Especially, as
long as it is not clear whether a certain result can be proved or not,
one has to switch between the positive mode (thinking in (*)) and
the negative mode (thinking in the realizability model).

All this can be done in a uniform way in TTE. And writing up proofs
in TTE is not necessarily that technical; in many cases abstract
proofs can be written up in a way which is, in the end, not that
different from using the system (*). 

Vasco

_______________________________________________________________________

Vasco Brattka
FernUniversitaet           Phone: +49-2331-987-2723
Theoretische Informatik I    Fax: +49-2331-987-319 
Informatikzentrum            WWW: www.informatik.fernuni-hagen.de/thi1/ 
D-58084 HAGEN                     vasco.brattka 
Germany                   E-Mail: Vasco.Brattka at FernUni-Hagen.de  
_______________________________________________________________________


> 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
>