FOM: question about s1s and s2s

William Ian Gasarch gasarch at
Thu Jun 14 12:00:57 EDT 2001

(I posted this to FOUNDATIONS OF MATH email list
and emailed it to your OLD email address.  Since
I now have your new email address at microsoft, and
I got some more info, I ask you the following)

A QUESTION from Jeremy Avigad and William Gasarch

(email answers or references or thoughts to
avigad at 
gasarch at
post to FOM)

As is well known

S1S (second order theory with one successor)
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 


(\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



APPENDUM: someone emailed me a reference to a paper of
Siefkas, where he SEEMS to show that S1S is decidable over
recursive set. But he's such a bad writer its hard to tell.
Is this true and is there a good writeup somewhere?

More information about the FOM mailing list