[FOM] Question on Decidability of S2S
Dmytro Taranovsky
dmytro at mit.edu
Wed Oct 14 18:43:14 EDT 2015
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
More information about the FOM
mailing list