The strength of SCT soundness

TL;DR

This paper investigates the soundness of the size-change termination (SCT) method within Reverse Mathematics, establishing its equivalence to a specific well-ordering principle over a base system.

Contribution

It proves that the SCT soundness statement is equivalent to the well-ordering of ω₃ over RCA₀, clarifying the logical strength of SCT in reverse mathematics.

Findings

SCT soundness is equivalent to WO(ω₃) over RCA₀.

The analysis extends previous work on size-change termination.

Provides a logical characterization 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}(\omega_3)$ over $\mathsf{RCA_0}$