最小化基础与其经典版本之间的等效一致性
逻辑
2024-07-31 v2
摘要
最小化基础（MF）是由第一作者与 G. Sambin 于 2005 年构思的，2009 年完全形式化，作为最相关的构造和经典数学基础的共同核心。为了更好地实现其最小化，MF 被设计为两层类型论，包含一个内涵层 mTT、一个外涵层 emTT，以及后者在前者中的解释。首先，我们展示了 MF 的两个层次确实通过将 mTT 解释到 emTT 中而是等效一致的。然后，我们展示了经典扩展 emTT^c 与 emTT 等效一致，通过对经典逻辑在直觉主义逻辑中的 G"odel-Gentzen 双否定翻译进行适当的扩展。作为结果，MF 被证明与经典的、以 Weyl 为代表的 predicative 数学相容，与最相关的构造数学基础相反。最后，我们展示了 MF 的等效一致性链可以直接扩展到其不确定版本，以推导出 Coquand-Huet 的 Calculus of Constructions 配合基本归纳类型版本等效一致于其外涵和经典版本。
引用
@article{arxiv.2407.09940,
title = {Equiconsistency of the Minimalist Foundation with its classical version},
author = {Maria Emilia Maietti and Pietro Sabelli},
journal= {arXiv preprint arXiv:2407.09940},
year = {2024}
}