A syntactic approach to continuity of T-definable functionals

MaRDI QIDQ6317548arXivFDO

Authors Chuangjie Xu

Publication date 22 April 2019

Published in arXiv

Mathematics Subject Classification ID

Type theory (03B38) Combinatory logic and lambda calculus (03B40) Functionals in proof theory (03F10) Other constructive mathematics (03F65)

arXiv classification

cs.LOmath.LO

Abstract: We give a new proof of the well-known fact that all functions $(mathbbNomathbbN)omathbbN$ which are definable in G"odel'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 $(mathbbNomathbbN)omathbbN$. 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.

This page was built for publication: A syntactic approach to continuity of T-definable functionals

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