FOM: the historical and logical pedigree of the Borel universe

[Kanovei]

>From: Stephen G Simpson <simpson at math.psu.edu>
>Something I didn't mention earlier: ATR_0 is strong enough to
> prove some advanced theorems on Borel sets.

Steve 

people could be curious how far the induction 
along wf trees allows to get. How about:

1) Kondo uniformization

2) Theorem that a Borel set with countable sections 
   is a countable union of Borel curves. (Ant its 
   remarkable generalization by Louveau.)

3) Theorem that "if all uncountable CA contain perfect 
   subsets then all A_2 are L measurable". 

Note that 1) is different from many of your examples 
as it needs 2nd rather than 1st periodicity theorem, 
2) is also different as it needs 3rd periodicity, while 
3) is an example of statement which has been profed 
"by forcing" but there is no evidence that it goes 
beyond second order PA (unlike e.g. the Borel determinacy).

Is there perhaps a comprehensive (and available) reference 
for the whole setup ? 

Vladimir Kanovei