直觉主义肯定自由逻辑中的限定描述
计算机科学中的逻辑
2021-08-12 v1 逻辑
摘要
本文给出了一个用于二元量词 的推理规则，以在直觉主义肯定自由逻辑内形式化包含限定描述的句子。 绑定一个变量并由两个公式构成一个公式。 意为“那个 是 ”。该系统被证明具有所期望的证明论性质：证明了其中的演绎可以化为正规形。讨论最后将此处推荐的限定描述形式化方法与使用语项形成算子 （其中 意为“那个 F”）的更常见方法进行了比较。
关键词
引用
@article{arxiv.2108.01978,
title = {Definite Descriptions in Intuitionist Positive Free Logic},
author = {Nils Kürbis},
journal= {arXiv preprint arXiv:2108.01978},
year = {2021}
}