FOM: Borel sets and Borelian mathematics

[Solomon Feferman]

Since shifting to fom-digest, I have been away from the daily fray of fom
postings, so some of this and the following message may be somewhat behind
the times.  But I was in the danger of becoming a fom-junkie and am trying
this form of detoxification at least for a while.  

Let me return to Steve Simpson's interesting posting of 6 Dec proposing
the investigation of various theorems about Borel sets via a simple
third-order system TBU_0.  Formulation of such a system and pursuit of
specific problems in its framework is a natural chapter in the efforts to
describe in logical terms "what rests on what".  Simpson points to the
historical interest of this in terms of the French school of analysts
surrounding Borel, Lebesgue, Baire and their followers (cf. Gregory
Moore's history of AC, *Zermelo's Axiom of Choice*).  As he himself says,
there is a conceptual penumbra in the resulting mathematics involving
analytic and other kinds of definable sets in the beginnings of systematic
Descriptive Set Theory (DST), and so one may question (I believe this was
Kanovei's point) whether the restriction to the language of TBU_0 is
appropriate for encompassing "Borelian mathematics".  Admittedly that is
looser than dealing with principles where the intended interpretation of
the third order variables is just the Borel sets, but one should ask
whether that is not the more appropriate sort of thing to do in this
direction.  I had suggested one quite different approach to the formal
representation of Borelian mathematics in my article "Theories of finite
type related to mathematical practice" in the *Handbook of Mathematical
Logic* edited by Jon Barwise; cf. sections 3.3 and 3.4 there, but I think
one should pursue even more flexible formulations in terms of theories of
variable type a la my system W that I have described in earlier postings.
The point is that the natural introduction and treatment of basic
properties of Borel sets and the development of Borelian mathematics
more generally is via countably infinitary inductive definitions, 
and these are treated formally in the theory denoted by proof theorists as
ID_1.  There countable ordinals are represented in tree form showing their
build-up, and one has similar representations of Borel sets; there are
associated principles of proof by induction and definition by recursion.
One can account for some of this in the second-order fragment of TBU_0,
which Simpson says he has determined to be ATR_0, but that is clearly
limited in expressive and proof-theoretical power.  ATR_0 is of strength
full predicative analysis, with ordinal Gamma_0, while ID_1 may be
considered to be the first natural impredicative system of interest, whose
proof-theoretic ordinal was located by William Howard many
years ago in the Bachmann systems of ordinal representation.  Now I think
it would be natural to formulate a theory which is to ID_1 as W is to
ACA_0.  This would be a subsystem of my system T_1 from the paper "A
language and axioms for explicit mathematics" in *Algebra and Logic* (J.
Crossley, ed.), LNM 450 (1975), obtained by restricting the IG (Inductive
Generation) axiom to just that corresponding to ID_1.  Within that one
could of course cut out subsystems for a more refined study of what rests
on what in Borelian mathematics.  For example, some properties only depend
on the fixed-point (FP) property of these inductive definitions, and not that
they are least fixed points.  The FPs have been studied in terms of systems
denoted ID^_n.  A very neat connection between these and ATR_0 (and thence
new proof that its ordinal is Gamma-0) was found by Jeremy Avigad, making
use of a natural intermediate uniform second-order formulation of
fixed-point axioms in his article "On the relationship between ATR_0 and
ID^<omega" in JSL 60 (1996), pp.768ff.

An alternative formal approach within the explicit mathematics program
returns to the suggestion in the Handbook article referenced above, to add
axioms for the Suslin quantifier as a functional E_1 to T_1 minus the IG
axioms.  Proof-theoretical work on this has already been carried out by
Jaeger and Strahm; cf. the report by them, together with Kahle, in the
article "On applicative theories" in *Logic in Florence '95* (Cantini, et
al., eds.), but what has to be seen is how much actual Borelian
mathematics can be carried out there.

One more specific question if these matters are pursued as suggested: how
should determinacy be formulated there, and what can be said about its
status?  The essential point is that (following the lead of Errett Bishop)
the concepts of function and set (or class more generally) are not treated
on a par in explicit mathematics: functions are prior conceptually to
classes, and axioms for them fall under the applicative group.  Thus 2^N
is not conflated with P(N), and Borel subsets of 2^N are treated
through their countable tree representations and not as third-order
objects.  So Borel determinacy may take a different form (and have a
different meaning) here than as viewed within ZFC.  

Sol Feferman