FOM: Borel sets

[Kanovei]

> I have proposed to restrict attention to Borel sets

Steve 

there are proofs in descriptive set theory (eg one 
of known proofs of the Suslin theorem) which go on 
as follows. 

1) We assume the negation and work towards contradiction. 

2) At some step, we get a certain tree consisting of finite 
   sequences of integers.  

3) We prove, using the assumption at step 1), that the tree 
   has an infinite branch.

4) The branch leads to contradiction which proves the result. 

5) An inspection of step 3) shows, however, that to define 
   a branch we usually need Comprehension for formulas 
   which are combinations of Sigma11 and Pi11. 

Conclusion: you are going to admit only Borel definitions 
for *sets of reals* but you will most likely have to admit 
essentially non-Borel definitions for *reals* themselves, 
which does not look entirely consistent. 

(Perhaps my observation is silly if there exist proofs 
of the Suslin theorem and other similar results in the 
"predicative" 2nd order PA. I don't know such.)

Vladimir Kanovei