文章基本信息

标题：Completeness of Modal Proofs in First-Order Predicate Logic
本地全文：下载
作者：Tatsuya Abe
期刊名称：Information and Media Technologies
电子版ISSN：1881-0896
出版年度：2008
卷号：3
期号：1
页码：13-25
DOI：10.11185/imt.3.13
出版社：Information and Media Technologies Editorial Board
摘要：Characterizing modal logic in first-order predicate logic is a hot research topic in mathematical logic. Van Benthem provided an elegant characterization in which the standard translation of modal formulas coincides with the class of first-order predicate formulas invariant for bisimulations. Whereas he characterized modal logic in first-order predicate logic at the level of formulas, we characterize modal logic in first-order predicate logic at the level of proofs. Specifically, we provide a complete translation from a term calculus based on intuitionistic modal logic into Barendregt's λP. This characterization, identified as the equality of proofs, is considered significant because a term calculus based on intuitionistic modal logic is expected to realize staged computation.