重访经典 S4 的证明论
计算机科学中的逻辑
2015-09-22 v3
摘要
Dag Prawitz 于 1965 年提出了将 Gentzen 型自然演绎系统扩展至 S4 模态概念的方法。Maria da Paz Medeiros 在 2006 年指出经典 S4 的规范化证明不成立，并提出了一种逻辑等价系统 NS4 的新规范化证明。然而，Yuuki Andou 在 2009 年指出了 Medeiros 在其证明中使用的关键引理证明中存在的两个问题。本文给出了该关键引理的证明，从而完成了 NS4 的规范化证明。
引用
@article{arxiv.1211.0242,
title = {Revisiting the proof theory of Classical S4},
author = {Bruno Lopes and Cecília Englander and Fernanda Lobo and Marcela Cruz},
journal= {arXiv preprint arXiv:1211.0242},
year = {2015}
}
备注
10 pages