[FOM] Question on Decidability of S2S

[Dmytro Taranovsky]

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