A SYNTACTIC APPROACH TO CONTINUITY OF T-DEFINABLE FUNCTIONALS

Xu, Chuangjie (2020): A SYNTACTIC APPROACH TO CONTINUITY OF T-DEFINABLE FUNCTIONALS. In: Logical Methods in Computer Science, Bd. 16, Nr. 1, 22

Abstract

We give a new proof of the well-known fact that all functions (N -> N) -> N which are definable in Godel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself in which natural numbers are translated to functions (N -> N) -> N. Then we inductively define a continuity predicate on the translated elements and show that the translation of any term in System T satisfies the continuity predicate. We obtain the desired result by relating terms and their translations via a parametrized logical relation. Our constructions and proofs have been formalized in the Agda proof assistant. Because Agda is also a programming language, we can execute our proof to compute moduli of continuity of T-definable functions.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Mathematik
• Themengebiete: 500 Naturwissenschaften und Mathematik > 510 Mathematik
• ISSN: 1860-5974
• Sprache: Englisch