极小基础的外延Kleene实现语义
逻辑
2015-05-06 v2
摘要
我们为 Maietti 和 Sambin 于2005年提出、Maietti 于2009年完成的二级极小基础 MF 构建了 Kleene 实现语义。借助该语义，我们证明了 MF 的两个层级均与（扩展的）形式 Church 论题 CT 一致。MF 由两个层级组成，一个内涵层级称为 mTT，一个外延层级称为 emTT，基于 Martin-Löf 类型论的若干版本。借助两个层级间的联系，只需为内涵层级构建语义即可获得外延层级的语义。因此这里我们仅为内涵层级 mTT 构建实现语义。该语义是 Beeson 1985 中为带一个宇宙的外延一阶 Martin-Löf 类型论所构建的实现语义的修正。因此它形式化于 Feferman 的归纳定义经典算术理论中。它被称为外延 Kleene 实现语义，因为它验证了类型论函数 extFun 的外延相等性，如 Beeson 1985 中那样。我们对 Beeson 语义所做的主要修正在于以证明无关的方式解释在 MF 中原始定义的命题。因此，我们获得了 CT 的有效性。回顾 extFun+CT+AC 在有限类型算术上不一致，我们得出结论：我们的语义不验证完整的选择公理 AC。相反，Beeson 的语义确实验证 AC，因为它是 Martin-Löf 理论的一个定理，但它不验证 CT。我们在此提出的语义似乎是 MF 外延层级 emTT 的最佳 Kleene 实现语义。事实上 Beeson 的语义对 emTT 不可行，因为加入其上的完整 AC 会导出排中律。
引用
@article{arxiv.1502.02864,
title = {An extensional Kleene realizability semantics for the Minimalist Foundation},
author = {Maria Emilia Maietti and Samuele Maschio},
journal= {arXiv preprint arXiv:1502.02864},
year = {2015}
}