FOM: the historical and logical pedigree of the Borel universe

[Stephen G Simpson]

(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

 Kanovei said:
  > 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,
 1987.
 
  > 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
 265-291.

-- Steve Simpson