FOM: the historical and logical pedigree of the Borel universe
Stephen G Simpson
simpson at math.psu.edu
Mon Dec 15 18:46:59 EST 1997
(1) The historical pedigree of the Borel universe
In his December 18 posting, Walter Felscher says:
> Having just returned from reading the Cinq Lettres in the
> library, I can assure that these do not contain any
> intimation of proposals to restrict attention to Borel sets.
> What reference is Mr. Simpson then basing his claims on ?
I'm pretty sure I have seen this proposal in the writings of Borel
and/or Baire. I'm trying to locate a primary reference. In the
meantime, have a look at A. Heyting's "Fondements des
Math'ematiques", iii + 91 pages, Gauthier-Villars, Paris, 1955.
Pages 6-11 contain a section entitled "Le semi-intuitionnisme
Fran,caise" discussing the views of the so-called French empiricists,
i.e. Borel, Baire, Lebesgue, Lusin, et al. Subsection 4 is entitled
"Ensembles bor'eliens" and in it Heyting says the following:
Les recherches les plus fructueuses ont port'e sur les questions de
fondements pour la th'eorie des ensembles de points et des
fonctions r'eelles. BOREL a 'et'e conduit `a sa th'eorie des
ensembles bor'eliens (appel'es d'abord par lui ensembles
mesurables, plus tard ensembles bien d'efinis, aujourd'hui en
France d'apr`es LEBESGUE ensembles mesurables B) par ses
r'eflexions sur les fondements de la th'eorie des ensembles. ....
Le concept d'ensemble bor'elien est suffisamment g'en'eral pour
qu'il semble ad'equat de limiter l'analyse `a la consid'eration de
tels ensembles. ....
(2) The logical pedigree of the Borel universe
> Then there must exist a function defined on the tree
> which correctly computes the measures of all intermediate
> sets (including the "root" set).
> Most likely your ATR or ATR_0 suffices to prove this
Yes, that's right. ATR_0 is enough to do this for all Borel codes.
This is in the Ph.D. thesis of Xiaokang Yu, "Measure Theory in Weak
Subsystems of Second Order Arithmetic", Pennsylvania State University,
> However it is clear that this axiom (as you described it)
> fails to be "Borel" in the way commented by 2) above,
> just because its formulation leads to a non-Borel set
> (e.g. the set of all pairs <a,x> such that a is a code
> of ordinal while x a real coding the accomplished
> inductive construction) -- despite the fact that each
> induction step is innocuous.
The above construction carried out for any particular lightface Borel
well-founded tree is lightface Borel. By "lightface Borel" I mean
hyperarithmetical. If you consider it as being carried out all at
once for all well-founded trees, then of course it isn't lightface
Borel, because the set of well-founded trees is non-Borel.
Nevertheless, it is definable by a Pi^1_1 formula, as usual.
> This is why I take the liberty to conclude that
> 6) Borel sets do not admit a Borel justification
I don't accept this conclusion. My claim is exactly that ATR_0 or
conservative extensions of it such as TBU_0 *do* constitute a Borel
justification of Borel sets, if I understand what you mean by "Borel
justification", in terms of methodological purity.
1. The principal axiom of ATR_0 asserts precisely that "Borel
constructions" can be carried out. By a "Borel construction" I mean
an arithmetical construction iterated along a given countable
well-ordering, or if you prefer, along a given countable well-founded
tree. Such constructions are precisely what is needed in order to
make sense of the concept of Borel sets in terms of Borel codes, and
this concept is undoubtedly the right one to use.
2. The omega-models of ATR_0 are closely related to "lightface Borel"
sets, and ATR_0 has the same logical strength as predicative analysis,
as I explained earlier.
3. As I also mentioned earlier, ATR_0 is just strong enough (in the
sense of reverse mathematics) to prove many of the classical theorems
on Borel sets, e.g. Lusin's theorem and the Borel domain theorem.
4. Something I didn't mention earlier: ATR_0 is strong enough to
prove some advanced theorems on Borel sets. For instance, (a) a form
of Silver's theorem on Borel and coanalytic equivalence relations, (b)
a version of the Harrington-Shelah theorem on Borel quasiorderings.
References for this are chapter V of my book, and Alberto Marcone's
paper "Borel quasi-orderings in subsystems of second-order
arithmetic", Annals of Pure and Applied Logic, 1991, volume 54, pages
-- Steve Simpson
More information about the FOM