pith. sign in

arxiv: 1709.09036 · v1 · pith:KL3BIDTZnew · submitted 2017-09-26 · 🧮 math.LO

The strength of SCT soundness

Emanuele Frittaion , Florian Pelupessy , Silvia Steila , Keita Yokoyama This is my paper
classification 🧮 math.LO
keywords soundnessanalyzecombinatorialconditioncontextcontinuecriterionequivalent
0
0 comments X
read the original abstract

In this paper we continue the study, from Frittaion, Steila and Yokoyama (2017), on size-change termination in the context of Reverse Mathematics. We analyze the soundness of the SCT method. In particular, we prove that the statement "any program which satisfies the combinatorial condition provided by the SCT criterion is terminating" is equivalent to $\mathrm{WO}(\omega_3)$ over $\mathsf{RCA_0}$

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary

    cs.LO 2026-04 unverdicted novelty 5.0

    Operational inexpressibility is identified as the property that blocks derivations depending on input dimension from constraining the target in term-rewriting systems, with the step-duplicating primitive recursor as t...

  2. Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary

    cs.LO 2026-04 unverdicted novelty 5.0

    The paper defines operational inexpressibility for step-duplicating primitive recursors in term rewriting and classifies sound responses into construction or confession methods while linking them to reflection hierarc...