FOM: Constructivity, recursion theory, recursive counterexamples

[Harvey Friedman]

1. I'M WRONG!!

The posting of Simpson 10:08AM 7/1100, partly in response to my earlier
posting of 3:40AM 7/7/00, as well as some private communications with
experts in the reverse mathematics of recursion theory, indicate that my
simple minded idea (in my earlier posting) that provability or
nonprovability in ISigma_1 holds any key in understanding when priority
arguments are or are not necessary is grossly inadequate.

2. CONSTRUCTIVE THEOREMS PROVED USING SOPHISTICATED RECURSION THEORY?

One special significance of constructivity in mathematics is supposed to be
its deep relationship with computational content. The basic thesis is that
essentially nonconstructive mathematics has no computational meaning or
content.

In that earlier posting, I also discussed the matter of constructive
provability. I do know one thing since I wrote that. It is straightforward
to show that any reasonable formulation of the existence of a one-one
partial enumeration of the partial recursive functions cannot be proved
constructively; e.g., in HA = Heyting Arithmetic.

It does appear to me to that recursion theory from the most elementary and
basic development taught in a general logic course at the undergraduate
level (e.g., enumeration, Smn, creative sets, r.e. recurively nonseparable
sets, relationships between partial recursive functions and r.e. sets,
etcetera), as well as various r.e. completeness results connected with
group theory and topology, are not only constructive but proved in weak
systems of arithmetic, far weaker than ISigma_1.

Also it does appear to me that once one gets into the usual combinatorially
subtle recursion theory starting with Friedberg and later, it does seem
that one is using not only stronger systems of arithmetic, but also one
loses any reasonable constructive content in the normal sense of the word.

3. A QUESTION.

This raises the following question:

To what extent can technically sophisticated techniques from recursion
theory be used to provide constructive information?

My impression of every talk in recursion theory I have ever attended with
sophisticated recursion theoretic methods presented involves clearly
nonconstructive reasoning of the kind known not to be replaceable by
constructive reasoning. Furthermore, it is not at all clear how to create
constructively meaningful replacements.

It seems to me that the vast majority of the currently celebrated theorems
of mathematics currently have either

i) - in the realm of the discrete or the continuous - have been given
constructive proofs or are expected to have constructive proofs. Certainly,
it is not known that they have no constructive proofs.
ii) - in the realm of real analysis - have at least satisfactory
constructively meaningful replacements. For classical real analysis, this
has been worked out most famously in Bishop's Foundations of Constructive
Analysis book.

4. RECURSIVE COUNTEREXAMPLES.

There are now a huge number of theorems of the following form:

*) there exists a recursive example of something where something or other
is not recursive.

When this is proved by coding, resulting in getting something that codes a
complete r.e. set, one seems to be able to do it constructively. Hence one
gets a suitably constructive proof of *), where not recursive is given a
constructively meaningful - and strong - interpretation.

However, there are also plenty of examples of such statements which are
normally proved using a priority argument. In these cases does one get a
constructive proof of the original statement in any reasonable sense?

It would appear not, if "not recursive" is given its normal constructively
meaningful interpretation. I.e., that given any recursive function there is
a place at which it differs.

Also, in the context of theorems like *), it appears that if the proof is a
coding of a complete r.e. set or the like, then not only is the proof
constructive in a strong sense, but it also is carried out in a weak
fragment of arithmetic. What fragment of arithmetic can proofs of theorems
like *) be carried out when the known proofs use more sophisticated
recursion theoretic techniques?