疏离性与强外延性形式的消去
逻辑
2023-10-26 v1
摘要
我们引入了一种所有有限类型上的算术新版本，它将通常的版本扩展以包含外延性与外延相等的基本原语。这一新的混合版本使我们能够表述一种强形式的外延性，我们称之为逆外延性。受布劳威尔的疏离性概念启发，我们证明了逆外延性可以以一种改进了我们先前工作结果的方式被消去。我们还解释了诸如可实现性与函数解释之类的标准证明论解释如何扩展到此类混合系统，以及这可能与证明挖掘有何关联。
引用
@article{arxiv.2310.16493,
title = {Apartness and the elimination of strong forms of extensionality},
author = {Benno van den Berg},
journal= {arXiv preprint arXiv:2310.16493},
year = {2023}
}