[FOM] Question on Decidability of S2S

[Leszek Kolodziejczyk]

>
> 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.
>

Yes, the version with the schemas appears correct. As for "a similar
equivalence that does not use axiom schemas", I take it that you would
formulate the r.h.s. as a Pi^1_3 reflection principle for Pi^1_2-CA_0. In
the case of the l.h.s., there is the annoying problem that you cannot
really say something like "every sentence accepted by Rabin's algorithm is
true" without a truth definition for all second-order formulas. But once
you restrict the l.h.s. to Pi^1_n sentences for some n \ge 3, or state the
correctness of Rabin's algorithm in some other reasonable fashion, then
indeed: the right-to-left implication remains provable in RCA_0, but the
question whether the left-to-right direction can be proved in something
significantly weaker than Pi^1_2-CA_0 becomes open.


> 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).
>

I agree that the question is interesting, though I am not ready to make a
conjecture one way or the other.

>
> 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.
>

I think that the "philosophical" part of your assessment hits the nail on
the head. I also expect that the technical part about EFA + superexp should
be true, but I have not attempted to verify this carefully.


Regards,
LK
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151019/4cfba048/attachment.html>