FOM: reverse math/recursion theory: effective algebra

[Stephen G Simpson]

In this posting I discuss the relationship between reverse mathematics
and effective algebra.  Executive summary: These subjects have very
different goals and results, but methodologically there is substantial
(though not complete) overlap.

Scope:

Under effective algebra I include both (1) recursive algebra and (2)
constructive algebra.  I would welcome further discussion of these
issues with recursion theorists and constructivists, here on the FOM
list.  To their credit, the constructivists are very interested in
constructive algebra.  On the other hand, it's a shame that recursion
theorists regard recursive mathematics as a mere "application" rather
than an essential part of their subject.

Background:

The goal of reverse mathematics is to find out which set existence
axioms are needed to prove mathematical theorems.  I won't rehearse
this here and now, because chapter one of my forthcoming book on
reverse mathematics is available on-line at
http://www.math.psu.edu/simpson/sosoa/.  See also pages 145-146 of

  [1] Friedman/Simpson/Smith, Countable algebra and set existence
  axioms, Annals of Pure and Applied Logic, 25, 1983, pp. 141-181.
  [2] Addendum, 28, 1985, pp. 320-321.

A seminal paper in "reverse algebra" (i.e. reverse mathematics in the
realm of algebra) is [1] and there are other papers by Simpson, Smith,
Hatzikiriakou, ....  In recursive algebra, there are numerous papers
by Metakides/Nerode, Remmel, Downey, ... and the forthcoming Handbook
of Recursive Mathematics (Elsevier 1998).  For constructive algebra,
up-to-date information is available in the books of Fred Richman and
his colleagues.

1. Recursive algebra:

As an example of what goes on in recursive algebra, consider the well
known and classical Artin/Schreier theorem: every formally real field
is orderable.  Ershov in Theory of Numerations III constructed a
recursive formally real field which is not recursively orderable.  He
did this by encoding a recursively inseparable pair of r.e. sets in a
certain way.  This provided a *recursive counterexample* showing that
the Artin/Schreier theorem is "recursively false".  What this really
means is that a certain statement about recursive algebraic
structures, although superficially analogous to the Artin/Schreier
theorem, is false.

The reverse mathematics treatment is quite different.  The result
there is that the Artin/Schreier theorem for countable fields is
*equivalent* to weak K"onig's lemma, provably in RCA_0.  An immediate
corollary is that the set existence axioms of WKL_0 suffice to prove
the Artin/Schreier theorem, but those of RCA_0 do not suffice.  Note
that we are referring to the Artin/Schreier theorem itself, not to a
recursive analog.  So the reverse mathematics standpoint is very
different from that of Ershov.

Of course Ershov's coding idea is a key ingredient in the proof of the
above-mentioned reverse mathematics result, and this result has
Ershov's as an easy corollary.  Note however that the other half of
the equivalence, i.e. the fact that the Artin/Schreier theorem is
provable in WKL_0, is somewhat delicate and has no counterpart in
Ershov's work or in recursive algebra generally.

At the same time, there are certain other aspects of recursive algebra
which are not reflected in reverse mathematics.  For example,
Metakides/Nerode showed that any Pi^0_1 subclass of 2^omega is
recursively homeomorphic to the space of orderings of some recursive
field.  This refinement of Ershov's construction has no counterpart in
reverse mathematics.  

As another example of this aspect, let me mention the following result
of reverse mathematics: WKL_0 is equivalent over RCA_0 to the
statement that every commutative ring has a prime ideal.  A question
for the recursive algebraists: Is it true or false that any Pi^0_1
subclass of 2^omega is recursively homeomorphic to the space of prime
ideals of some recursive commutative ring?  This statement was
announced in [1] but withdrawn in [2].

I would welcome any suggestions for how to expand the scope of reverse
mathematics to encompass refinements involving Pi^0_1 classes, while
still preserving intellectual coherence.

2. Constructive algebra:

The axioms of RCA_0 are "constructive" in the sense that they are
formally consistent with the statement that every total function from
N into N is recursive.  Since much of the work in reverse algebra
involves proving certain algebraic results in RCA_0, one might assume
the existence of a close relationship to constructive algebra.

In actual fact, there are substantial differences.  The most profound
differences are philosophical: The constructivists believe that
mathematical objects are purely mental constructions, while reverse
mathematics makes no such assumption.  Furthermore, the meaning which
the constructivists assign to the logical connectives and quantifiers
is incompatible with the classical interpretation, and of course the
constructivists set themselves apart by rejecting the law of the
excluded middle.

There are also some purely formal differences.  The constructivists
assume unrestricted induction on N, but RCA_0 does not even include
Pi^0_2 induction, and this lack frequently prevents a direct
translation of proofs from the constructivist literature into RCA_0.
(But of course reverse mathematics draws on constructive techniques to
the extent possible.)

There is also an important stylistic difference, centered on the issue
of "extra data".  When a theorem of classical mathematics fails
constructively, the constructivists often respond by devising a
modified theorem which is constructively valid.  These modified
theorems often include clumsy "extra data" hypotheses.  By contrast,
the response of reverse mathematics is not to abandon the theorem, but
rather to "reverse" the theorem by showing that it is equivalent to
the set existence axioms needed to prove it.  Such responses are
dictated by the goals of the responders.  The constructivists aim to
transform all of mathematics into constructions, while reverse
mathematics aims to discover the set existence assumptions which are
implicit in mathematics *as it stands*.  Occasionally, very strong set
existence axioms arise in this way.

I hope that some recursion theorists and constructivists will respond
to this posting, so we can get a good discussion going.

-- Steve