[FOM] Question on Decidability of S2S (reply to Taranovsky)

[Leszek Kolodziejczyk]

Dmytro Taranovsky asks:

>> Is S2S with quantification restricted to recursive sets decidable?
>>
>> Recall that S2S is the monadic second order theory over the complete
>> infinite binary tree.

This looks a potentially interesting question. I don't know the  
answer, but Henryk Michalewski and I recently proved that the  
statement "the Pi^1_3 fragment of S2S is decidable" is unprovable even  
in Delta^1_3-CA_0. The argument is based on the expressibility of  
determinacy statements in S2S, but it also makes essential use of  
nonstandard levels of the difference hierarchy over Sigma^0_2, so our  
result says nothing about decidability in omega-models.

Our paper can be found at: http://arxiv.org/abs/1508.06780

The answer to your other question:

>> * 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?

seems to be a rather straightforward "yes". The reason is that by (the  
proof of) Rabin's theorem, there is an automaton recognizing the set  
of those labellings X of the binary tree for which phi(X) holds. Any  
nonempty set of labellings recognized by an automaton contains a  
so-called regular labelling (basically, one in which finitely many  
patterns appear over and over again). Each regular labelling is  
definable in S2S.

You also say:

>> 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.)

Would you be able to provide a more precise statement of the above, or  
a reference? Proofs of Rabin's theorem usually make use of what you  
call "history-free" (a.k.a. positional) determinacy of certain  
Bool(Sigma^0_2) games. I do think that over omega-models of RCA_0,  
positional determinacy and ordinary determinacy are equivalent, but  
I'm not aware of a published reference, and the only way in which I  
would know how to prove this is rather involved (I believe the result  
is implicit in the work of Michael Möllerfeld on the arithmetical  
mu-calculus). On the other hand, Henryk and I were not able to prove  
the implication from ordinary to positional determinacy in RCA_0, nor  
in fact in any theory much weaker than Pi^1_2-CA_0.


Regards,
Leszek Kołodziejczyk