Talk:S2S (mathematics)

Initial message

    The article was an interesting challenge to write. The subject is certainly important, and I was surprised there was no article already, though it has some coverage in other articles. Part of it is the difficulty of writing a good article here. The subject is rich, but the results are scattered across many technical papers. Also, the decidability proof of S2S was described by some as notoriously complex, but its key ideas are important in their own right for even a time-constrained reader to understand the subject. And even though I knew the decidability proof beforehand, writing the article was a learning experience, and led me to a new discovery (a reasonable complete axiomatization of S2S [1]; its inclusion in the article will wait).
    For the template, I suggest quality class B and priority Mid for both WikiProjects; I refrained from just setting it myself. Despite care in exposition and largely comprehensive content, I am sure that plenty of improvements can be made. However, given the wide range of reader backgrounds, it is unavoidable that some time-constrained readers will just skip certain parts or use them for a vague but helpful intuition. Dmytro (talk) 16:07, 14 November 2022 (UTC)

β-models

In the section Formula complexity, β-model is defined as "an ω-model whose set-theoretic counterpart is transitive", and in order to show the implication some models $L_{\alpha }(r)$ are constructed. I'm skeptical that transitivity of the model $(L_{\alpha }(r),\in )$ is sufficient for it to be a β-model, for example $L_{\omega _{1}^{CK}}$ is not a β-model because of the Harrison ordering.

In "How unprovable is Rabin's decidability theorem?", the closest I can find to the proof of (3)→(4) is Theorem 6.1, in which the set theory ${\mathsf {Lim}}(\preceq _{1})$ and cofinal $\prec _{\Sigma _{1}}$-towers are mentioned, however after stating that $\Pi _{2}^{1}{\mathsf {-CA}}_{0}$ corresponds to this axiom, instead of being used to construct a minimal β-model, it is used to show an explicitly $\Pi _{3}$ proposition has a $\Pi _{2}$ form. (However, they do also remark that ${\mathsf {Lim}}(\preceq _{1})$ proves Axiom β, but if by compactness there are non-wellfounded models of ${\mathsf {Lim}}(\preceq _{1})$ then this is not enough to construct a β-model.) C7XWiki (talk) 00:06, 17 March 2023 (UTC)

The quoted characterization of β models holds for models of ATR₀ (and conversely, all β models satisfy ATR); ATR₀ is a $\Pi _{2}^{1}$ consequence of $\Pi _{1}^{1}{\mathsf {-CA}}_{0}$ (so ${\mathsf {Lim}}(\preceq _{1})$ is more than enough). Also, in the proof sketch some arrows were reversed; I fixed it. Dmytro (talk) 16:40, 19 March 2023 (UTC)