FOM: question about s1s and s2s

Alexander Rabinovich alexr at
Fri Jun 15 08:59:38 EDT 2001

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

[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

More information about the FOM mailing list