[FOM] Relevance of reverse mathematics to constructivity

[Vasco Brattka]

Reverse mathematics is definitely relevant for constructive
and computable mathematics.

 From the computable analysis perspective reverse mathematics
roughly captures the degree of unsolvability of non-uniform
results (with a few exceptions). Uniform results, however,
might be more "non-constructive" than reverse mathematics
indicates.

Here are four examples that highlight the similarities
and also the differences.

1. Hahn-Banach Theorem

The fact that the Hahn-Banach Theorem is not provable over
RCA_0 corresponds to the fact that there are computable
functionals without computable norm-preserving extension,
as proved by Nerode et al. This means that the
theorem neither is uniformly computable (i.e. the extension
operation itself is not computable) nor non-uniformly computable.

Since computable analysis is a model of Bishop style
constructive analysis, it follows that the theorem is
also not provable in that sense.

The fact that the Hahn-Banach Theorem is equivalent to WKL_0
over RCA_0 has its counterpart in the strong uniform sense of
computable analysis, as proved recently by Gherardi and
Marcone and in the intuitionistic sense of Bishop style
mathematics, as proved by Ishihara.

Hence, all three theories agree on this example.

2. Intermediate Value Theorem

This theorem is provable over RCA_0 with the help of classical
logic. It is also valid computably in the non-uniform computable
sense (for each computable function that changes its sign there
is a computable zero), but not in the uniform computable sense
(i.e. there is no algorithm to find a zero, given the function).

In the sense of computable analysis the Intermediate Value Theorem
is located strictly in between computable operations and the
Hahn-Banach Theorem. In a somewhat coarser sense it is equivalent
to the Hahn-Banach Theorem and WKL and this also holds in Bishop's style
constructive analysis (as proved by Bridges and Richman).

Here constructive and computable analysis are compatible, whereas
reverse analysis matches with the non-uniform computable level.

3. Baire Category Theorem

The version "in a complete separable metric space all sequences of
nowhere dense closed sets miss some point of the space" is provable
over RCA_0 and it is computable (in the fully uniform sense that one
can find a point, given the sequence) and it is provable in constructive
analysis.

Again, all three theories agree.

However, In reverse mathematics one can freely move on to the
contrapositive form (for all sequences of closed sets whose union is the
entire space, there is an index of a set that is somewhere dense), which
is not uniformly computable and hence not provable in Bishop's style
constructive analysis. However, this version of the theorem is trivially
non-uniformly computable (since the result is a natural number, which
is always computable).

In computable analysis the mentioned contrapositive version of the
Baire Category Theorem is complete for the class of functions computable
with finitely many mind changes (the effective counterpart of Delta^0_2-
measurable functions).

Once again, reverse mathematics matches with the non-uniform 
computability result and not with the uniform one. The same applies
to all sorts of theorems derived with the help of the contrapositive
form of the Baire Category Theorem (such as Banach's Inverse Mapping
Theorem etc.).

4. Heine-Borel Theorem

This theorem is equivalent to WKL_0 over RCA_0 and there is also
a version equivalent to WKL in Bishop's style constructive analysis
(this and other versions have been analyzed by Richman, Ishihara
and Schuster).

Although the theorem is non-constructive in the above mentioned
sense, it is fully computable in the sense of computable analysis.
This is because if the mere existence of finite subcovers is guranteed
classically, then one just has to search a suitable cover 
computationally in order to find one.

The last example illustrates that computable mathematics mainly deals 
with computations and not so much with existence. In particular,
non-constructive correctness proofs for algorithms are allowed.
If the existence of a finite subcover is guranteed classically, there
is no reason to believe that an algorithm searching for it will not
terminate (obviously, this algorithm will be very inefficient, but
that is another matter).

Reverse mathematics and constructive mathematics have in common
that they both focus on existence. However, the usage of classical
logic in reverse mathematics allows a correspondence only with
non-uniform results.

In computable analysis we have started a classification project
since we need finer classifications of our theorems than the ones
usually provided by reverse mathematics. Only these finer 
classifications explain in a detailed way the computational
differences between theorems that we see.

However, for this project reverse mathematics provides an extremely
valuable source of insights, tools and results and turned out to be
a good starting point for our analysis.

Even if one struggles to formulate exact transfer theorems between
reverse mathematics, on the one hand, and constructive and computable 
mathematics, on the other hand, one can obviously benefit from the
similarities of ideas and methods.

I believe that this indicates the relevance of reverse mathematics
for computable and constructive mathematics.

Regards

Vasco

PS More on "reverse computable analysis" can be found here:
    http://arxiv.org/abs/0905.4685
    http://arxiv.org/abs/0905.4679
    http://arxiv.org/abs/0808.1663
    http://arxiv.org/abs/1002.2800