References and Related Works

References

• J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis
• W. Pohlers, Proof Theory: The First Step into Impredicativity
• P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic
• R. Kaye, Models of Peano arithmetic
• 田中 一之, ゲーデルと 20 世紀の論理学
• 菊池 誠 (編者), 『数学における証明と真理 ─ 様相論理と数学基礎論』
• P. Blackburn, M. de Rijke, Y. Venema, "Modal Logic"
• Open Logic Project, "The Open Logic Text"
• R. Hakli, S. Negri, "Does the deduction theorem fail for modal logic?"
• G. Boolos, "The Logic of Provability"
• M. C. Fitting, V. W. Marek, and M. Truszczynski, "The Pure Logic of Necessitation"
• T. Kurahashi, "The provability logic of all provability predicates"
• W. Carnielli, C. Pizzi, "Modalities and Multimodalities"

Related Works

Here is the list of project particularly formalize mathematical logics. If you find something missing from this list or add, report via issues.

Lean 4

m4lvin/lean4-pdl

Propositional dynamic logics.

alexoltean61/hybrid_logic_lean

Hybrid logic. Syntax and semantics for hybrid logic are provided, and some facts and soundness have been proven. However completeness seems to have been not yet formalized.

• Andrei-Alexandru Oltean, "A Formalization of Hybrid Logic in Lean"

leanprover-community/con-nf

Formalizing the consistency of Quine's set theory "New Foundations": $\mathrm{Con}(\mathbf{NF})$.

• Website

Lean 3

flypitch

Independence of the continuum hypothesis.

• Jesse Michael Han and Floris van Doorn, "A Formal Proof of the Independence of the Continuum Hypothesis"

bbentzen/ipl

Intuitionistic propositional logic.

Hilbert-style deduction system, Kripke semantics and Henkin-style (constructing maximal prime set and canonical model) completeness proof.

• Huayo Guo, Dongheng Chen, Bruno Bentzen, "Verified completeness in Henkin-style for intuitionistic propositional logic"

bbentzen/mpl

Normal modal logic.

Hilbert-style deduction system, Kripke semantics and Henkin-style (constructing maximal consistent set and canonical model) completeness proof for $S5$.

• Bruno Bentzen, "A Henkin-style completeness proof for the modal logic S5"

paulaneeley/modal

Formalization of modal logic $S5$ and public announcement logic.

• Paula Neeley, "A Formalization of Dynamic Epistemic Logic"

minchaowu/ModalTab

Tableaux system for modal logic $\mathbf{K},\mathbf{KT},S4$.

• Minchao Wu, Rajeev Goré, "Verified Decision Procedures for Modal Logics"

ljt12138/Formalization-PAL

$S5$ and public announcement logic (PAL). Main result are recursion theorem (reducing public announce modality for any PAL formula) and completeness of $S5$.

• Jiatu Li, "Formalization of PAL⋅S5 in Proof Assistant"

Isabelle

Lawrence C. Paulson, "Gödel's Incompleteness Theorems"

Formalized Gödel's first and second incompleteness theorems. Remark the second incompleteness theorem is proved on hereditarily finite sets.

• paper: Lawrence C. Paulson, "A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets"

Christoph Benzmüller, Woltzenlogel Paleo, "Gödel's God in Isabelle/HOL"

Gödel's ontological argument of God's existence.

jrh13/hol-light/GL

Completeness of Gödel-Löb (provability) modal logic $\mathbf{GL}$ in HOL/Light.

• Marco Maggesi, Cosimo Perini Brogi, "Mechanising Gödel–Löb Provability Logic in HOL Light"

u5943321/Modal-Logic

Modal Logic, based on textbook "Modal Logic" by P. Blackburn, M. de Rijke, Y. Venema in HOL.

• Yiming Xu, "Formalizing Modal Logic in HOL"

Coq

ianshil/PhD_thesis

Coq formalization of several modal logics (related provability logic and etc.) and their caliculi.

• Ian Shillito, New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq.

hferee/UIML

Uniform interpolants for basic modal logic $\mathbf{K}$, Gödel-Löb provability logic $\mathbf{GL}$, intuitionistic strong Löb logic $\mathbf{iSL}$.

• demo
• Hugo Férée, Iris van der Giessen, Sam van Gool, Ian Shillito, "Mechanised uniform interpolation for modal logics K, GL and iSL"

ana-borges/QRC1-Coq

Quantified modal logic called Quantified Reflection Calculus with one modality $\mathsf{QR}{\mathsf{C}}_1$.

Christian Doczkal, Gert Smolka, "Completeness and decidability of converse PDL in the constructive type theory of Coq"

Propositional Dynamic Logic.

Christian Doczkal, Gert Smolka, "Constructive Formalization of Hybrid Logic with Eventualities"

Hybrid Logic.

Russell O'Connor's continuous works on Incompleteness Theorem

• Russell O’Connor, "Essential Incompleteness of Arithmetic Verified by Coq"

fondefjobn/S5-Formalization-in-Coq

Modal logic $S5$, its Kripke completeness.

• Lubor Budaj, "Formalization of modal logic $S5$ in the Coq proof assistant"

Floris van Doorn, "Propositional Calculus in Coq"

Hilbert deduction system, natural deduction system, and sequent calculus for classical propositional logic. Formalized completeness of natural deduction system, the provability equivalence of three calculi, cut-elimination for sequent calculus.

Christoph Benzmüller, Bruno Woltzenlogel Paleo, "Interacting with Modal Logics in the Coq Proof Assistant"

Modal logic and Gödel's ontological argument of existence of God.

mphilipse/coq-multi-agent-systems

Multi-agent epistemic modal logic ${S5}^n$.

• Michiel Philipse, "Distributed Knowledge Proofs in the Coq Proof Assistant"

Iris Project

Framework for concurrent saparation logic. Verified in Coq.