FOM: A QUESTION about Decidability of S2S
William Ian Gasarch
gasarch at cs.umd.edu
Thu May 24 16:42:22 EDT 2001
A QUESTION from Jeremy Avigad and William Gasarch
(email answers or references or thoughts to
avigad at cmu.edu
and
gasarch at cs.umd.edu
and/or
post to FOM)
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
uvvvvvv...
)
More information about the FOM
mailing list