FOM: Borel sets

[Kanovei]

>From: Stephen G Simpson <simpson at math.psu.edu>

>On the other hand, I have analyzed particular proofs of and the
>inherent logical strength of some well-known classical theorems about
>Borel sets.
...........
>So in these cases we may be seeing a kind of "Methodenreinheit" or
>"methodological purity".

Steve

let me formulate and then discuss the following goal: 

1) find a Borel justification of Borel mathematics. 
   
To describe what I mean, I assume that 

2) PA is an arithmetical justification of arithmetic 
   because its axioms support arithmetical reasoning 
   and do not lead to any non-arithmetical object, 

(Let us leave aside some number of arithmetical theorems 
unprovable by PA.), and 

3) ZFC is a set theoretic justification of set theory 
   -- by similar reasons. 

The first attempt would be to take the 
predicative 2nd order PA. This adequately describes 
Borel sets of finite rank but seems insufficient for 
the whote totality of Borel sets. Indeed, to intriduce 
a fresh example, consider the Borel measure. 

4) We have to prove that every Borel set is measurable. 

Naturally this means the following:

5) Consider a "Borel code", that is, a countable 
   wellfounded tree, to the endpoints of which rational 
   intervals are attached, and it is supposed that each 
   intermediate node performs the complement of the 
   union of the sets computed for immediate successor nodes. 
   Assume that ALL THOSE UNIONS ARE 2-WISE DISJOINT UNIONS, 
   just to make the computation straightforward. 
   -- 
   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 
(if is not even equivalend over a weaker theory). 
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. 

(There are even simpler examples, like the set of all 
pairs <a,x> such that a is a Borel code while x a real 
which belongs to the Borel set coded by a. I took that 
one which seems more meaningful.)

This argument reflects an old observation going back to 
Luzin (at least) that assuming the totality of all 
countable ordinals we naturally obtain some non-Borel stuff. 

This is why I take the liberty to conclude that 

6) Borel sets do not admit a Borel justification  
   
(By means of finitary logic. Infinitary logic should 
treat them easily and naturally.) 

Vladimir Kanovei