The strength of SCT soundness

DOI10.1093/LOGCOM/EXY003MaRDI QIDQ4612439zbMATH OpenOpenAlexWikidataFDO

Authors Emanuele Frittaion, Florian Pelupessy, Silvia Steila, Keita Yokoyama

Publication date 31 January 2019

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1709.09036

zbMATH Keywords

reverse mathematicssoundnessRamsey's theorem for pairssize-change terminationwell-ordering principles

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Ramsey theory (05D10) Second- and higher-order arithmetic and fragments (03F35)

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 $mathrmWO(omeg{a}_3)$ over $mathsfRC{A}_0$

Recommendations

• The strength of the SCT criterion
• A rational test for strong stabilization
• The strong test ideal
• The Soundness Paradox
• scientific article; zbMATH DE number 1842510
• scientific article; zbMATH DE number 1191248
• The robustness of robust implementation
• The consistency strength of choiceless failures of SCH
• Strong D-stability
• scientific article; zbMATH DE number 4111942

Cited in

(2)

• An intuitionistic analysis of size-change termination
• The strength of the SCT criterion

This page was built for publication: The strength of SCT soundness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4612439)