A Computational Interpretation of Modal Proofs
A Computational Interpretation of Modal Proofs
复制标题
模态证明的计算解释
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
A. Masini
中科院分区：
文献类型：
--
作者：
S. Martini;A. Masini
模态逻辑的证明论，虽然自五十年代以来被大量研究，但一直是一个微妙的主题，主要原因是显然不可能为内涵算子获得优雅，自然的系统（除了直觉逻辑的优秀例外）。例如，Segerberg，不早于1984[5]，观察到根岑格式，它对真函数和直觉算子非常有效，不能先验地期望对模态逻辑保持有效；把这一观察结果发挥到极限，人们甚至可以断言：“没有好的证明理论的逻辑是不自然的。”这样，我们就可以把所有的模态逻辑标记为“非自然的”（许多逻辑学家非常高兴！）。
Proof theory of modal logics, though largely studied since the fifties, has always been a delicate subject, the main reason being the apparent impossibility to obtain elegant, natural systems for intensional operators (with the excellent exception of intuitionistic logic). For example Segerberg, not earlier than 1984 [5], observed that the Gentzen format, which works so well for truth functional and intuitionistic operators, cannot be a priori expected to remain valid for modal logics; carrying to the limit this observation one could even assert that ‘logics with no good proof theory are unnatural.’ In such a way we should mark as ‘unnatural’ all modal logics (with great delight of a large number of logicians!).