Skip to content
An Agda proof of (uniform) continuity of T-definable functionals via a syntactic approach
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

A syntactic approach to continuity of T-definable functionals

We give a new proof of the well-known fact that all functions (ℕ → ℕ) → ℕ 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 (ℕ → ℕ) → ℕ. 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.

An html rendering of the Agda code is available at the author's GitHub web page.



  • Agda version 2.6.0
You can’t perform that action at this time.