判断存在逻辑及其与证明无关性的关系
计算机科学中的逻辑
2024-05-24 v1 逻辑
摘要
我们引入了一个简单的自然演绎系统，用于对“存在 的证明”这种形式的判断进行推理，以遵循 Martin-Löf 区分判断与命题的方法论，探索判断存在的概念。在该系统中，存在判断可以被内化为一种命题存在的模态概念，该概念与截断模态（获得证明无关性的关键工具）和松弛模态密切相关。我们以 Curry-Howard 同构的风格为存在模态提供了计算解释，并证明了相应的系统具有强规范化或主语归约等一些理想的性质。
关键词
引用
@article{arxiv.2405.14481,
title = {A logic of judgmental existence and its relation to proof irrelevance},
author = {Ivo Pezlar},
journal= {arXiv preprint arXiv:2405.14481},
year = {2024}
}