FOM: question about s1s and s2s
alexr at dcs.ed.ac.uk
Fri Jun 15 08:59:38 EDT 2001
William Ian Gasarch wrote:As is well known
> S1S (second order theory with one successor)
> 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
> (\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,
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
 M. O. Rabin (1969).
Decidability of second order theories and automata on
infinite trees. In Trans. Amer. Math. Soc., 141,pp 1-35.
 S. Shelah (1975).
The monadic theory of order. Annals of Mathematics 102:379--419.
Dept. of Computer Science
Tel Aviv University
rabino at math.tau.ac.il
More information about the FOM