普适证明论：直觉主义模态逻辑中的可行可接纳性
逻辑
2022-10-18 v3 计算机科学中的逻辑
摘要
在本文中，我们引入模态语言及其片段上的一类通用序列式演算，以把握所有构造上可接受的系统的本质。称这些演算为“构造的”，我们证明任何满足温和技术条件的足够强的构造序列式演算，均可行地接纳所有Visser规则，即存在一个多项式时间算法，读取Visser规则前提的证明并给出其结论的证明。作为一个正向应用，我们展示了Visser规则在若干直觉主义模态逻辑序列式演算中的可行可接纳性，包括 、 以及它们通过模态公理 、、、、有界宽度与深度模态公理和命题松弛逻辑的扩张。在负面方面，我们证明若一个足够强的直觉主义模态逻辑（满足温和技术条件）不接纳至少一条Visser规则，则它不可能具有构造序列式演算。由此，除 外没有任何中间逻辑具有构造序列式演算。
引用
@article{arxiv.2209.08911,
title = {Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics},
author = {Amirhossein Akbar Tabatabai and Raheleh Jalali},
journal= {arXiv preprint arXiv:2209.08911},
year = {2022}
}