English

The strength of SCT soundness

Logic 2017-09-27 v1

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 WO(ω3)\mathrm{WO}(\omega_3) over RCA0\mathsf{RCA_0}

Keywords

Cite

@article{arxiv.1709.09036,
  title  = {The strength of SCT soundness},
  author = {Emanuele Frittaion and Florian Pelupessy and Silvia Steila and Keita Yokoyama},
  journal= {arXiv preprint arXiv:1709.09036},
  year   = {2017}
}

Comments

30 pages