一句话：用 System T 自翻译、连续性谓词和参数化逻辑关系，给出 T-可定义泛函连续性的新语法证明并在 Agda 中形式化。
本文重新证明 Gōdel System T 中所有可定义函数 (N→N)→N 均连续这一已知事实。与通常语法方法不同，作者先将 System T 翻译到自身，把自然数翻译为 (N→N)→N 型函数；随后在翻译后的元素上归纳定义连续性谓词，证明每个 System T 项的翻译都满足该谓词。通过参数化逻辑关系关联原项与其翻译，得到目标连续性结果。全部构造与证明在 Agda 证明助手中形式化；由于 Agda 也是编程语言，该证明可执行以计算 T-可定义函数的连续性模。
We give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ 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 $(\mathbb{N} \to \mathbb{N}) \to \mathbb{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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1904-09794,
title = {A syntactic approach to continuity of T-definable functionals},
author = {Chuangjie Xu},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:22)2020}
}