A Henkin-style completeness proof for the modal logic S5

In Pietro Baroni, Christoph Benzmüller & Yì N. Wáng (eds.), Logic and Argumentation: Fourth International Conference, CLAR 2021, Hangzhou, China, October 20–22. Springer. pp. 459-467 (2021)
Download Edit this record How to cite View on PhilPapers
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, 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.
PhilPapers/Archive ID
Upload history
Archival date: 2021-10-23
View other versions
Added to PP index

Total views
46 ( #58,733 of 65,545 )

Recent downloads (6 months)
46 ( #18,577 of 65,545 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.