[FOM] Question on Decidability of S2S
Dmytro Taranovsky
dmytro at mit.edu
Sun Oct 18 21:10:10 EDT 2015
Dear Leszek Kolodziejczyk,
Thank you for the answers and the link to the paper. Research on
reverse mathematics of S2S is long overdue, and from your results it
appears that
RCA_0 + {P: P is true in S2S} proves the same statements as RCA_0 + {P:
P is Pi^1_3 and P is provable Pi^1_2-CA_0}
(see Corollary 3.3, Lemma 4.6 and Theorem 6.1 in your paper), but with a
lingering issue of proving in a weak base theory a similar equivalence
that does not use axiom schemas.
With regard to decidability, since S2S is already close to being
undecidable, adding additional structure will likely make it
undecidable, so I conjecture that over RCA_0, the only decidable
consistent theory of S2S is the standard theory (and any exception would
be interesting).
Philosophically, we can ask why does S2S require such impredicative
comprehension. The set of regular trees (of the right syntactic form)
is (as you wrote) an elementary submodel of S2S, and a regular tree can
be coded by a finite directed graph with a starting node, and hence by
an integer. EFA plus existence of the iterated exponential should
suffice for decidability of S2S over regular trees, with decidability
formalizable as existence of S2S satisfaction relation satisfying
appropriate properties. I think the general answer is that integers and
regular trees have certain closure properties (that allow decidability
of S2S), and arbitrary subsets of N also have these properties, but
without regularity the required closure can be highly nonrecursive.
Also, I should have been clear that I did not have a proof of positional
determinacy given ordinary determinacy; without the proof, the
equivalences in RCA_0 in my previous message are for appropriate
positional determinacy.
Sincerely,
Dmytro Taranovsky
More information about the FOM
mailing list