FOM: question about s1s and s2s

[Alexander Rabinovich]

William Ian Gasarch wrote:As is well known

>
> S1S (second order theory with one successor)
> and
> S2S (second order theory with two successor's, bascially theory
>         of infinite trees)
>
> are DECIDABLE.
>
> QUESTION: What if you restrict the quantification of sets
> to a nice subclass.
>
> a) Is S2S still decidable if you restrict the quantification to
> be over COMPUTABLE sets?
>
> b) ... arithmetic sets?
>
> c) ... hyperarithmetic sets?
>
> d) what about S1S?
>
> Easy result:
> Let \phi(X) be an S1S statement with ONE set var
> (it can have many number vars.)
>
> (\exists X)[\phi(X)] is true
>
> iff
>
> (\exists X recursive)[\phi(X)] is true.
>
> (This is easy- if an omega aut is nonempty then
> it accepts a set that has a char string of the form
>

Let phi(X,Y) be a formula  in S2S.
Consider the following regular interpretation of set quantifiers:
\exists Z is interpreted  as ``exists a regular subset Z''.

Rabin proved  that under the standard interpretation
of set quantifiers and under regular interpretation the formula
has the same meaning (over the full binary tree).


Hence  S2S sentence is true
under the standard interpretation iff it is true
under regular interpretation.

Therefore  S2S  is  decidable if you restrict the quantification to
be over regular sets,  COMPUTABLE sets,
arithmetic sets,
hyperarithmetic sets and any family of sets which contains regular sets.

The same results holds for S1S.

Here are some other related results:

The monadic second order theory (MLO)  of reals
is decidable when you restrict quantification
to F_\sigma sets (Rabin).
However, MLO  is undecidable when quantification is over
arbitrary subsets of reals (Shelah).

Maybe Shelah also proved that MLO over the reals
 is still decidable
for quantification over Borel sets (or up to some level of Borel
hierarchy).


[1] M. O. Rabin (1969).
 Decidability of second order theories and automata on
  infinite trees.  In  Trans. Amer. Math. Soc., 141,pp 1-35.
[2]  S. Shelah (1975).
The monadic theory of order.  Annals of Mathematics 102:379--419.


Alexander Rabinovich
Dept. of  Computer Science
Tel Aviv University
rabino at math.tau.ac.il