CZF 的一阶逻辑是直觉主义一阶逻辑
逻辑
2022-06-10 v2
摘要
我们证明 CZF 的一阶逻辑是直觉主义一阶逻辑。为此，我们引入了一种超限计算的新模型（集合寄存器机），并将由此得到的可实现性概念与 Beth 语义相结合。在此过程中，我们还证明了 CZF 的命题可容许规则恰为直觉主义命题逻辑的可容许规则。
引用
@article{arxiv.2112.00486,
title = {The first-order logic of CZF is intuitionistic first-order logic},
author = {Robert Passmann},
journal= {arXiv preprint arXiv:2112.00486},
year = {2022}
}
备注
Revised version, more precise title, 20 pages