[FOM] Query on independence results and constructive theories

[Stephen G Simpson]

praatika at mappi.helsinki.fi writes:
 > (1) If I don't remember wrong, at least some time ago, Delta-1-2 CA
 > (or something like it) was the strongest theory which could be
 > constructively justified. Is this still the state of affairs?

"Constructive justifiability" is open to interpretation.  In the
present context, namely subsystems of second-order arithmetic,
researchers in Gentzen-style proof theory have often identified
constructive justifiability with provable consistency using primitive
recursive notation systems for initial segments of the ordinal
numbers.  Under this identification, Pi^1_2 CA_0 (i.e., Pi^1_2
comprehension with restricted induction) was constructively justified
by Michael Rathjen's work a number of years ago.  This was a major
advance in Gentzen-style proof theory.

 > (2) Now Finite Krusakal's Theorem (and extended KT, and such) are
 > not provable in predicatively justifiable theories, but are they
 > still provable in a theory that is constructively justifable?

I think KT, EKT, FKT, etc. are provable in systems considerably weaker
than Pi^1_2 CA_0.  Isn't that correct?  If so, then the answer to this
question is yes.

 > (3) Are there any neat examples of theorems which are independent of 
 > Delta-1-2 CA, or whatever theories which are, today, known to be 
 > constructively acceptable? 

Last year Carl Mummert and I showed that a certain metrization theorem
in general topology is equivalent over Pi^1_1 comprehension to Pi^1_2
comprehension.  The theorem states that a countably based MF space is
completely metrizable if and only if it is regular.  Our paper is in
the Bulletin of Symbolic Logic, volume 11, 2005, pp. 526-533.  So, it
appears that this metrization theorem is just barely inside the
current bounds of constructive justifiability.

[ A countably based MF space is any topological space of the form
MF(P) = {maximal filters on P} where P is a countable partially
ordered set.  This class of topological spaces includes all complete
separable metric spaces and many other spaces. ]

Going beyond constructive justifiability, I believe Kazuyuki Tanaka
and his colleagues have shown that, for example, Pi^0_3 determinacy
(or is it Delta^0_4 determinacy) is not provable in Pi^1_2 CA_0 but is
provable in full second-order arithmetic.  They are doing some
interesting reverse mathematics in this area.

Of course Harvey Friedman has proved many independence results saying
that various mathematical theorems are not "constructively
justifiable" because they are independent of full second-order
arithmetic and stronger systems.  An example that I like, dating back
to the 1960s, is Pi^0_5 determinacy.  I am sure that Harvey can
provide other examples which are "neater" in various ways.  The word
"neat" is open to interpretation, but obviously Harvey has made a lot
of progress in this direction.

 > (4) If there is, is the proof of independence itself constructive?

In each case, the independence proof is constructive or can routinely
be turned into a constructive proof.

-- Steve

Stephen G. Simpson

Professor of Mathematics

Pennsylvania State University

http://www.math.psu.edu/simpson/.

research interests: mathematical logic, foundations of mathematics