论哥德尔理论T中泛型的可定义性
逻辑
2014-10-14 v4 计算机科学中的逻辑
摘要
哥德尔理论T可以理解为简单类型lambda演算的理论，该演算被扩展以包含常量0、后继函数S以及用于对类型τ的对象进行原始递归的算子R_tau。已知在该理论中可定义的从非负整数到非负整数的函数恰好是非负整数的<ε_0-递归函数。作为该结果的推广，我们证明了当定义域和陪域被限制为纯闭正规形式时，在T中可定义的任意类型的泛型可以被编码为<ε_0-递归函数。
引用
@article{arxiv.1011.6353,
title = {On the definability of functionals in G\"odel's theory T},
author = {Matthew P. Szudzik},
journal= {arXiv preprint arXiv:1011.6353},
year = {2014}
}
备注
13 pages, 0 figures; metadata updated, other minor changes