arXiv · 1709.09036
The strength of SCT soundness
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}(ω_3)$ over $\mathsf{RCA_0}$
Explore related subjects
Keep this discovery
Emanuele Frittaion, Florian Pelupessy, Silvia Steila, Keita Yokoyama. 2017-09-26. The strength of SCT soundness. https://arxiv.org/abs/1709.09036
Cite the original work for its findings. Save a collection to share your selection of sources.