[FOM] Question on Decidability of S2S (reply to Taranovsky)
Leszek Kolodziejczyk
lak at mimuw.edu.pl
Fri Oct 16 15:48:11 EDT 2015
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
More information about the FOM
mailing list