极小主义基础与同伦类型论的兼容性
逻辑
2024-01-30 v5
摘要
极小主义基础（简称MF）是由Maietti与Sambin于2005年构想、后由Maietti于2009年完全形式化的一种用于构造性数学的两层基础。MF通过为文献中 most relevant 的数学基础选择MF中适当层级并以兼容方式（即保持逻辑与集合论构造子含义）翻译，充当它们之间的公共核心。两层结构由一个内涵层、一个外延层以及后者在前者的解释构成，以便从涉及日常数学实践中所用外延构造的数学证明中提取内涵计算内容。2013年文献中出现一种全新的构造性数学基础，称为同伦类型论（简称HoTT），它是Voevodsky单值基础且具有计算性质的一例。迄今尚无MF任何层级被证明与文献中任一单值基础兼容。本文我们证明MF两层均与HoTT兼容。此结果得益于HoTT的特殊性：其通过假设Voevodsky单值公理与高阶归纳商类型，将类型论的内涵特征与外延特征相结合。作为相关后果，MF继承了全新的可计算模型。
引用
@article{arxiv.2207.03802,
title = {The Compatibility of the Minimalist Foundation with Homotopy Type Theory},
author = {Michele Contente and Maria Emilia Maietti},
journal= {arXiv preprint arXiv:2207.03802},
year = {2024}
}