[FOM] Re: Constructive analysis

[Peter Lietz]

Concerning the discussion about the relationship between computable
and constructive analysis:

First off, I would like to say that I wouldn't go as far as equating
computable analysis (in whichever flavor) with some set of axioms.

It is indeed the case that computability results can be achieved by
proving, say, the totality of some relation in a formal system of
constructive mathematics (some extension of BISH) and then applying
e.g. a realizability interpretation. I am very much in favor of this
approach, because it avoids concretely dealing with representations,
as one would otherwise have to do in TTE. Also, simple non-computability
results can be achieved by deriving non-constructive principles from
some assumption. Mind, however, that the more impressive results in
computable analysis are often of a mixed and more subtle nature, see
e.g. the harder direction of Pour-El and Richard's first main theorem.
I disagree with Andrej's statement that "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 BISH + CC + MP
+ FT + NC + SE". Take for example Vasco Brattka's account on the
`Computability of Banach Space Principles'. One result is that if T
is a computable, continuous, bijective operator between Banach spaces
then its inverse is computable, too, but an algorithm for the inverse
cannot be computed uniformly from an algorithm of T. I am not aware of
a proof in constructive logic that would allow to derive this result
(it is probably possible using the negative translation massively).

In order to achieve computability results, one approach is to use
Kleene's function realizability. From a proof of the theorem \forall f
\exists g A(f,g) one can extract an algorithm h such that \forall f
A(f,h|f) is realized. This in turn means that \forall f A(f,h|f) is
provable using GC (generalized continuity). Much rather we would want
the correctness of the extracted algorithm to be classically true, or
better yet, constructively true. This is in fact the case if A is in
CC (the conservative class). The formula A being in CC is not a severe
restriction in practice, in fact A is even negative very often. But this
also means that GC won't be very helpful for the proof of the totality
of the relation A in the first place.

An alternative approach is to use the function realizability
interpretation combined with truth and a classical target system. This
one validates only classically acceptable axioms and so no restriction
on the logical structure of A is needed. It validates principles such
as MP and FAN (if assumed on the target side) which allow for a slight
simplification of BISH. The motivation for the question I posted to
FOM on Aug 1st was exactly this. Another principle that is validated
by this interpretation is the `double negation shift' (thanks to Jaap
van Oosten and Dana Scott for helpful answers via email in reply to my
question).

As far as `stability of equality' is concerned, I would tend to view it
as a theorem that one can prove for the reals (or any metric space)
and not as an axiom. In the framework of higher order logic (including
extensionality of entailment) SE is even inconstructive.


Peter


----------------------------------
Peter Lietz, PhD student
Department of Mathematics
Darmstadt University of Technology
----------------------------------