第二阶（直觉主义）时态逻辑的证明论与语义
计算机科学中的逻辑
2026-02-09 v1 逻辑
摘要
我们发展了直觉主义模态逻辑的第二阶扩展，允许对命题进行语法和语义上的量化。第二阶逻辑的一个关键特征是其有能力从负性片段定义正向连词。妥当地，我们能够仅使用 boxes（盒子）以及包含正向和反向模态（“时态”模态）即可恢复 diamond（钻石）及其相关理论。我们提出了“第二阶直觉主义时态逻辑”的公理化、证明论和模型论定义，最终证明它们全部相等。特别是，我们通过 proof search argument 证明了以标签序列演算的完备性，同时也得到 cut-admissibility 结果。我们的 methodology 也适用于经典版本的第二阶时态逻辑，我们与直觉主义情况并行发展。
引用
@article{arxiv.2602.06253,
title = {The proof theory and semantics of second-order (intuitionistic) tense logic},
author = {Justus Becker and Anupam Das and Sonia Marin and Paaras Padhiar},
journal= {arXiv preprint arXiv:2602.06253},
year = {2026}
}