A Henkin-Style Completeness Proof for the Modal Logic S5

被引：4
|
作者：
Bentzen, Bruno [1 ]
机构：
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
LOGIC AND ARGUMENTATION, CLAR 2021 | 2021年 / 13040卷
关键词：
Modal logic; Completeness; Formal methods; Lean; CALCULUS;
D O I：
10.1007/978-3-030-89391-0_25
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell [8], but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical connectives and necessity as the only primitive modal operator. The full source code is available online and has been typechecked with Lean 3.4.2.
引用
收藏
页码：459 / 467
页数：9
相关论文
共 50 条
  • [1] A HENKIN-STYLE PROOF OF COMPLETENESS FOR FIRST-ORDER ALGEBRAIZABLE LOGICS
    Cintula, Petr
    Noguera, Carles
    [J]. JOURNAL OF SYMBOLIC LOGIC, 2015, 80 (01) : 341 - 358
  • [2] A SIMPLE HENKIN-STYLE COMPLETENESS PROOF FOR GODEL3-VALUED LOGIC G3
    Robes, Gemma
    [J]. LOGIC AND LOGICAL PHILOSOPHY, 2014, 23 (04) : 371 - 390
  • [3] On Satisfiability Problem in Modal Logic S5
    Salhi, Yakoub
    [J]. PROCEEDINGS OF THE 35TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING (SAC'20), 2020, : 948 - 955
  • [4] Knowledge Compilation in the Modal Logic S5
    Bienvenu, Meghyn
    Fargier, Helene
    Marquis, Pierre
    [J]. PROCEEDINGS OF THE TWENTY-FOURTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-10), 2010, : 261 - 266
  • [5] Evidence reconstruction of epistemic modal logic S5
    Rubtsova, Natalia
    [J]. COMPUTER SCIENCE - THEORY AND APPLICATIONS, 2006, 3967 : 313 - 321
  • [6] A deep inference system for the modal logic S5
    Stouppa P.
    [J]. Studia Logica, 2007, 85 (2) : 199 - 214
  • [7] Rooted Hypersequent Calculus for Modal Logic S5
    Mohammadi, Hamzeh
    Aghaei, Mojtaba
    [J]. LOGICA UNIVERSALIS, 2023, 17 (03) : 269 - 295
  • [8] Rooted Hypersequent Calculus for Modal Logic S5
    Hamzeh Mohammadi
    Mojtaba Aghaei
    [J]. Logica Universalis, 2023, 17 : 269 - 295
  • [9] Hypersequential Argumentation Frameworks: An Instantiation in the Modal Logic S5
    Borg, AnneMarie
    Arieli, Ofer
    [J]. PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS (AAMAS' 18), 2018, : 1097 - 1104
  • [10] Ground nonmonotonic modal logic S5:: New results
    Galindo, MO
    Pérez, JAN
    Ramírez, JRA
    Macías, VB
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2005, 15 (05) : 787 - 813
12345