[FOM] Question on Decidability of S2S

[Dmytro Taranovsky]

Is S2S with quantification restricted to recursive sets decidable?

Recall that S2S is the monadic second order theory over the complete 
infinite binary tree.  It is remarkable as being essentially the most 
expressive natural decidable theory known.  Its decidability is also 
remarkable given its ability to express certain statements that require 
impredicative comprehension.  For every fixed natural number n, S2S can 
express a statement that over RCA_0 is equivalent to determinacy of the 
nth level of the difference hierarchy of (boldface) Sigma^0_2 sets.  
(Conversely, this determinacy for all n suffices for decidability.  
Also, the determinacy in S2S is a certain history-free determinacy, 
which implies and I believe has been shown equivalent to ordinary 
determinacy.)  Thus, the true theory of S2S fails in the minimal natural 
models of RCA, ACA, Pi^1_1-CA and Pi^1_1-TR.  This leaves the question 
about the nature of the theory of S2S in such models and whether it is 
decidable.

Recursiveness may not be the most natural condition on sets for S2S.  A 
related question is
* If  thereis X phi(X)  is true (phi is an S2S formula with exactly one 
free variable), must there be such an X that is definable in S2S?
If yes, then sets definable in S2S form the minimal model of S2S (using 
sets in place of second order logic).

Sincerely,
Dmytro Taranovsky