A Henkin-Style Completeness Proof for the Modal Logic S5

被引：7
作者：
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
相关论文
共 14 条
[1]  
Carneiro M, 2018, LEAN 3 MATH LIB MATH
[2]  
Coquand C., 2002, Higher-Order and Symbolic Computation, V15, P57, DOI 10.1023/A:1019964114625
[3]   THE CALCULUS OF CONSTRUCTIONS [J].
COQUAND, T ;
HUET, G .
INFORMATION AND COMPUTATION, 1988, 76 (2-3) :95-120
[4]  
Doczkal Christian, 2014, Interactive Theorem Proving. 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Proceedings: LNCS 8558, P226, DOI 10.1007/978-3-319-08970-6_15
[5]  
Doczkal Christian, 2012, Certified Programs and Proofs. Second International Conference (CPP 2012). Proceedings, P224, DOI 10.1007/978-3-642-35308-6_18
[6]  
From A.H, 2018, EPISTEMIC LOGIC
[7]   Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus [J].
Herbelin, Hugo ;
Lee, Gyesik .
LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, 2009, 5514 :209-+
[8]  
Hughes George E., 1996, A New Introduction to Modal Logic
[9]  
Negri S., 2009, Acts of knowledge: History, P247
[10]  
Norell Ulf, 2009, LNCS, V5832, P230, DOI [10.1007/978-3-642-04652-0_5, DOI 10.1007/978-3-642-04652-0_5]
12