[FOM] Relevance of reverse mathematics to constructivity

[Carl Mummert]

On Tue, Mar 16, 2010 at 2:46 PM, Timothy Y. Chow <tchow at alum.mit.edu>
wrote to FOM:
> Simpson's results on Hilbert's basis theorem are very interesting in their
> own right, but I confess that I do not understand what they have to do
> with the question of the supposed "non-constructiveness" of Hilbert's
> proof, as that question is usually understood.

I don't find there is a single sense in which "non-constructive" is
usually understood. Unlike the situation with "effective", which has
become virtually a synonym for "Turing computable", there are still
many contradictory notions of "constructive" in use.

For example, consider the choice scheme AC_{00} which says: if one has
a definable relation R on the natural numbers such that for every n
there exists an m with R(n,m), then there is a function f from the set
of natural numbers to itself such that R(n,f(n)) holds for all n. This
principle is accepted in Bishop-style constructive mathematics, but it
is not valid in constructive set theory.  Each of these has some claim
to the term "constructive mathematics". The issue whether choice
principles such as AC_{00} are truly "constructive" seems to depend on
which framework for constructive mathematics is employed.

To go back to your original question,  I would say that the reverse
mathematics framework provides a way to measure one _particular_
notion of constructivity, which could be called "constructivity
relative to RCA_0".  The work on intuitionistic reverse mathematics by
Ishihara and others demonstrates that it is equally possible to work
in a base system that does not include the law of the excluded middle.

The use of RCA_0 in this way is a typical example of the modern method
in foundations, in which we take an interesting but vague question
("How non-constructive is the Hilbert basis theorem"), replace it with
one or more formal questions ("What is the reverse mathematics
strength of the Hilbert basis theorem"), answer the formal question,
and then use this to inform our opinion on the vague question.

It is not obvious from the initial definitions that reverse
mathematics actually measures some generalized notion of
"constructivity", but it becomes more clear with experience. One piece
of evidence for this claim is the close connection between reverse
mathematics and computability. For example, there is an omega-model of
RCA_0 consisting of exactly the computable sets, so one "cannot prove
the existence of a non-computable set in RCA_0". Similarly, there is
an omega-model of ACA_0 consisting of exactly the arithmetical sets.

Another piece of evidence is that many mathematical theorems fall into
the big five equivalence classes.  This seems to indicate that there
is an underlying phenomenon at work, which is usually called
"non-constructivity" in the reverse mathematics literature.  There is
a clear intuitive sense that as we move to stronger subsystems in the
big five, they become less constructive, at least in the amount of
non-computability that they entail.  Thus, in this sense, reverse
mathematics measures the constructivity of theorems in terms of the
constructivity of the big five subsystems.

However, reverse mathematics is not simply measuring
non-computability. For example, reverse math collapses the entire
arithmetical hierarchy down to the single system ACA_0. In computable
analysis, the difference between problems that require 0' and problems
that require 0'' is much more important.  Thus reverse mathematics
measures a different sort of generalized constructivity than
computable analysis.

> Using classical logic, one can prove the
> existence of something in a very weak system without giving any indication
> of how to "construct" it.  Conversely, is there any reason to suppose that
> if a statement is unprovable in RCA_0 (say) then it is "non-constructive"?

In most cases, it is not just the unprovability in RCA_0 that is
shown, but the equivalence of a mathematical theorem with some axiom
system stronger than RCA_0. Given that sort of reversal, if we
recognize the stronger axiom system as non-constructive, then we can
recognize the theorem as equally non-constructive relative to RCA_0.

However, recent work that I have done with Jeff Hirst gives a
different answer to your question.  We show that whenever a Pi^1_2
statement of the correct syntactic form is provable in a certain
theory of intuitionistic arithmetic, a "uniform version" of the
statement will be provable in a conservative extension of RCA_0 (and,
in particular, the original formula will be provable in RCA_0).  The
uniform version of a Pi^1_2 formula is the usual Sigma^2_1 formula
obtained by Skolemizing the universal quantifier of the Pi^1_2
formula. Moreover, the theory of intuitionistic arithmetic that we use
includes the full scheme for the axioms of choice, which would be much
stronger than RCA_0 in classical logic.

Thus, if a Pi^1_2 formula meeting the hypotheses of our theorem is not
provable in RCA_0, the original formula is not provable in the
intuitionistic system we consider. This allows one to directly obtain
results about the unprovability of statements in intuitionistic
arithmetic from results about the unprovability of the uniform
versions of those statements in RCA_0.   Our paper on these results is
in preparation.

- Carl