FOM: Borel sets and Methodenreinheit

[Stephen G Simpson]

Kanovei writes:
 > Conclusion: you are going to admit only Borel definitions 
 > for *sets of reals* but you will most likely have to admit 
 > essentially non-Borel definitions for *reals* themselves, 
 > which does not look entirely consistent. 
 > 
 > (Perhaps my observation is silly if there exist proofs 
 > of the Suslin theorem and other similar results in the 
 > "predicative" 2nd order PA. I don't know such.)

Dear Vladimir,

This isn't silly at all.  We know of several theorems about Borel sets
which, in a sense, need concepts and methods that go far beyond Borel
sets, in order to prove them.  I have in mind theorems such as (1)
Borel determinacy and some of its consequences, (2) your own result
that the Borel constituents of a non-Borel analytic set are unbounded
in Borel rank, (3) certain theorems of Friedman and Stanley.  To prove
these theorems we need to go not only beyond Borel sets, but beyond
the powerset of the reals.  For (1) and (2) we need uncountably many
applications of the powerset axiom; for (3) we need more.

(I'm getting some of this information from Greg Hjorth.  I'm not sure
why Greg is declining to get involved in this FOM discussion.)

On the other hand, I have analyzed particular proofs of and the
inherent logical strength of some well-known classical theorems about
Borel sets.  I have shown that these theorems are provable in ATR_0
and in some cases equivalent to ATR_0.  Souslin's theorem is provable
in ATR_0, but not equivalent to ATR_0.  Lusin's theorem (any two
disjoint analytic sets can be separated by a Borel set) and the
perfect set theorem (every uncountable analytic set contains a perfect
set, or every uncountable closed set contains a perfect set) and the
domain theorem (the domain of a single-valued Borel relation is Borel)
are provable in and indeed equivalent to ATR_0, a la reverse
mathematics.  This material is in chapter V of my forthcoming book on
subsystems of second order arithmetic.

So in these cases we may be seeing a kind of "Methodenreinheit" or
"methodological purity".  At least this is how Robert Tragesser seems
to want to view such matters.  (I myself am neither a methodological
purist nor a Serb.  On the other hand, I am a fan of Aristotle.  Could
this be an example of how everybody is a racist without even knowing
it, as the left wing in the United States now asserts?  Just kidding.)

Background on ATR_0:

ATR_0 is one of the subsystems of second order arithmetic that arise
naturally in reverse mathematics.  The principal axiom of ATR_0 is
arithmetical transfinite recursion, which means that we can iterate
arithmetical comprehension along any countable well ordering.
(Arithmetical comprehension means asserting the existence of a set of
integers defined by a formula containing only quantification over
integers.)  This ATR axiom is known to be equivalent to many ordinary
mathematical theorems, over a weak base theory.  In a sense ATR_0 is
impredicative, because any omega-model of ATR_0 necessarily contains
sets of integers (i.e. "reals") which are not hyperarithmetical.  In
another sense ATR_0 is predicative, because the hyperarithmetical sets
of integers form the intersection of all omega-models of ATR_0.
Furthermore, ATR_0 is predicatively reducible: it is conservative for
Pi^1_1 sentences over Feferman's system of predicative analysis.  (A
set of integers is hyperarithmetical if and only if it is lightface
Delta^1_1.  Is this what you meant by "Borel definitions for reals",
above?  My remarks may bear on exactly the question that you asked.)

-- Steve