A syntactic approach to continuity of T-definable functionals
A syntactic approach to continuity of T-definable functionals
复制标题
T 可定义泛函连续性的句法方法
DOI：
10.23638/lmcs-16(1:22)2020
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Chuangjie Xu
中科院分区：
文献类型：
--
作者：
Chuangjie Xu
我们给出了一个新的证明众所周知的事实，即所有的功能$（\mathbb{N} \to \mathbb {N}）\to \mathbb{N}$，这是可定义的哥德尔系统T是连续的通过语法的方法。与通常的语法方法不同，我们首先执行系统T到自身的翻译，其中自然数被翻译为函数$（\mathbb{N} \to \mathbb{N}）\to \mathbb{N}$。然后，我们归纳地定义了一个连续性谓词上的翻译元素，并证明了系统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 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 $(\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：
--
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Schwichtenberg H
通讯作者：
Schwichtenberg H