直觉集合论中选择原理与前提规则的独立性
逻辑
2024-12-02 v1
摘要
选择原理与前提独立性原理在刻画 Kreisel 的修正实现和 G"odel 的 Dialectica 诠释方面发挥着重要作用。本文我们证明了许多直觉集合论在 上的有限类型对应的规则下是封闭的。我们还证明了形如 的语句具有存在性属性（或存在可定义性），其中变量 取值范围在有限类型 的对象上。这特别适用于 （建构齐维尔-弗兰克尔集合论）和 （直觉齐维尔-弗兰克尔集合论），这两个系统已知不具备一般的存在性属性。在技术层面，本文采用一种将通用实现与真理相结合的方法，其中要求底层的部分组合代数包含所有有限类型的对象。
关键词
引用
@article{arxiv.2411.19907,
title = {Choice and independence of premise rules in intuitionistic set theory},
author = {Emanuele Frittaion and Takako Nemoto and Michael Rathjen},
journal= {arXiv preprint arXiv:2411.19907},
year = {2024}
}