Formalized Formal Logic

This project is aim to formalize some various results of mathematical logic in Lean Theorem Prover.

This book provides explanation and summaries of formalized concepts, theorems, propositions. Proofs of them are not explained, refer to the code or the references.

Full documentation is here.

Main Results

Classical Propositional Logic

• Soundness and completeness.

First-Order Logic

The list of main formalized results in first-order (Predicate) logics.

• Soundness and completeness.
• Gödel's First Incompleteness Theorem.
• Gödel's Second Incompleteness Theorem.

Superintuitionistic Propositional Logic

The list of main formalized results in superintuitionistic propositional logics.

• Soundness and completeness for Kripke semantics.
• Law of Excluded Middle doesn't hold in intuitionistic logic.
• Disjunctive property of intuitionistic logic.

Standard Modal Logic

The list of main formalized in standard modal logics.

• Definability of Kripke frame.
• Soundness and completeness for Kripke semantics.
• Gödel-McKensey-Tarski Theorem and Modal companion.

Import Graph

Generated by import-graph

Foundation

PDF version

Arithmetization

PDF version

Incompleteness

PDF version

Usage

Add following to lakefile.lean.

require logic from git "https://github.com/FormalizedFormalLogic/Foundation"

Contributing

Discuss

GitHub Discussion is here. Feel free to correct mistakes, ask questions or share ideas.

Documentation

To compile this book, you need mdbook and some plugins.

• mdbook
• mdbook-katex for KaTeX

mdbook serve md

mdbook build md

But you don't have to install to simply correct mistakes and write documents, since it can be previewed by your editor's markdown preview.

Developing

VSCode settings

Some notation is not prepared default by lean 4 extension for VSCode. Here is example .vscode/settings.json.

{
  "lean4.input.customTranslations": {
    "cand": "⋏",
    "cor": "⋎",
    "boxdot": "⊡",
    "^F": "ꟳ"
  }
}

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.

Definitions and Notations

TODO:

Computability

TODO:

Classical Propositional Logic

Syntax and Semantics for Classical Propositional Logic

Deduction System

We adupt the Tait-calculus as a deduction system of classical propositional logic.

  abbrev Sequent (α : Type*) := List (Formula α)

  inductive Derivation : Sequent α → Type _
  | axL (Δ a)   : Derivation (Formula.atom a :: Formula.natom a :: Δ)
  | verum (Δ)   : Derivation (⊤ :: Δ)
  | or {Δ p q}  : Derivation (p :: q :: Δ) → Derivation (p ⋎ q :: Δ)
  | and {Δ p q} : Derivation (p :: Δ) → Derivation (q :: Δ) → Derivation (p ⋏ q :: Δ)
  | wk {Δ Γ}    : Derivation Δ → Δ ⊆ Γ → Derivation Γ
  | cut {Δ p}   : Derivation (p :: Δ) → Derivation (~p :: Δ) → Derivation Δ

  instance : OneSided (Formula α) := ⟨Derivation⟩

• LO.Propositional.Classical.Derivation

Semantics

Soundness and Completeness

The soundness theorem is proved by induction of derivation.

  instance (T : Theory α) : Sound T (Semantics.models (Valuation α) T)

• LO.Propositional.Classical.instSoundTheoryFormulaSetValuationModels

The conpleteness theorem is also proved by constructing maximal consistent theory.

  instance (T : Theory α) : Complete T (Semantics.models (Valuation α) T)

• LO.Propositional.Classical.instCompleteTheoryFormulaSetValuationModels

First-Order Logic

TODO:

Term and Formula

Notation

Quantification of formulae are defined using de Bruijn index, but we can write terms and formulae by usual binder notation using macro.

variables x y z is just an example and can take any number of idents. e is an expression of term/formula.

Binder Notation

Binder notation of term takes either form:

• Term: ‘x y z. e’, Formula: “x y z. e”
  • x y z is the symbol for the bound variables, k:num-variables denotes the terms in Semiterm L ξ (n + $k)/Semiformula L ξ (n + $k). (n can be variable)
• Term: ‘x y z | e’, Formula: “x y z | e”
  • x y z is the symbol for the free variables, k:num-variables denotes the terms in Semiterm L ξ n/Semiformula L ξ n. (n can be variable)
• Term: ‘e’, Formula: “e”
  • An abbreviation of ‘ . e’/“ . e”

Expression of term/formula

Deduction System for First-Order Logic

Semantics for First-Order Logic

Completeness Theorem

Arithmetics

In this formalization, we prefer developing arithmetic model theoretic, i.e. show $T\models \sigma$ instead of $T⊢\sigma$ (They are equivalent thanks to the completeness theorem.). This approach has several advantages:

1. In general, writing a formalized proof (in formalized system!) is very tedious. Meta-proofs, on the other hand, tend to be relatively concise.
2. Many definitions and proofs of logic and algebra in Mathlib can be used.
3. Metaprogramming can streamline the proof process (especially definability).
4. It is easy to extend predicates and functions. When adding predicates or functions, it is necessary to extend its language by extension by definition in case of formalized proof, but not in model theoretic approach.

This procedure is done as follows. Suppose we wish to prove that the totality of an exponential function can be proved in $\mathsf{I}{\Sigma }_1$. First, the graph of the exponential function must be defined. This is achieved by the following two definitions.

1. Semantic definition.

   def Exponential {M : Type*} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐈𝚺₀] :
       M → M → Prop
   

2. Syntactic definition that expresses the semantic definition.

   def exponentialDef : 𝚺₀-Semisentence 2
   
       lemma Exponential.defined :
           𝚺₀-Relation (Exponential : M → M → Prop) via exponentialDef
       ```
   
   Then prove the totality.
   

theorem Exponential.total  {M : Type*} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐈𝚺₀] (x : M) : ∃ y, Exponential x y

Since Exponential and Exponential.total are defined in all the model of $\mathsf{I}{\Sigma }_1$, 𝐈𝚺₁ ⊢! ∀' ∃' exponentialDef is obtained by the completeness theorem. This was the result we wanted to achieve.

Defined Predicates and Functions

Theories of Arithmetics

Theory $\mathsf{I}{\Sigma }_0$

These results are included in Arithmetization.

Exponential

The graph of exponential $\mathrm{Exp}(x,y)$ is definable by ${\Sigma }_0$-fomrula, and its inductive properties are proved in $\mathsf{I}{\Sigma }_0$.

instance exponential_definable [M ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation (Exponential : M → M → Prop)

• LO.Arith.exponential_definable

lemma exponential_zero_one [M ⊧ₘ* 𝐈𝚺₀] :
    Exponential 0 1

• LO.Arith.Exponential.exponential_zero_one

lemma exponential_succ_mul_two [M ⊧ₘ* 𝐈𝚺₀] {x y : M} :
    Exponential (x + 1) (2 * y) ↔ Exponential x y

• LO.Arith.Exponential.exponential_succ_mul_two

Other basic functions, such as $\log x,|x|$ are defined by using exponential.

Theory $\mathsf{I}{\Sigma }_1$

These results are included in Arithmetization.

Exponential

It is proved that the graph of exponential is definable by ${\Sigma }_0$-formula, and their inductive properties are provable in $\mathsf{I}{\Sigma }_0$. In $\mathsf{I}{\Sigma }_1$, we can further prove their entireness.

Theory of Hereditary Finite Sets in $\mathsf{I}{\Sigma }_1$

Weak theory of sets in $V_{\omega }$ (Hereditary Finite Sets) can be developed inside $\mathsf{I}{\Sigma }_1$ using Ackermann coding and bit predicate. Hereafter, we will use the notation $i\in a$ in the sense of bit predicate:

lemma mem_iff_bit [M ⊧ₘ* 𝐈𝚺₁] {i a : M} : i ∈ a ↔ Bit i a

• LO.Arith.mem_iff_bit

The following comprehension holds.

theorem finset_comprehension₁ [M ⊧ₘ* 𝐈𝚺₁]
    {P : M → Prop} (hP : (Γ, 1)-Predicate P) (a : M) :
    ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

• LO.Arith.finset_comprehension₁

The basic concepts of set theory, such as union, inter, cartesian product, and mapping, etc. are defined.

Seq

$\mathrm{Seq}(s)$ iff $s$ is a mapping and its domain is $[0,l)$ for some $l$.

def Seq [M ⊧ₘ* 𝐈𝚺₁] (s : M) : Prop := IsMapping s ∧ ∃ l, domain s = under l

• LO.Arith.Seq

Primitive Recursion

Let $f(\vec{v})$, $g(\vec{v},x,z)$ be a ${\Sigma }_1$-function. There is a ${\Sigma }_1$-function ${\mathsf{PR}}_{f,g}(\vec{v},u)$ such that:

$$\begin{array}{rl}{\mathsf{PR}}_{f,g}(\vec{v},0)& =f(\vec{v})\\ {\mathsf{PR}}_{f,g}(\vec{v},u+1)& =g(\vec{v},u,{\mathsf{PR}}_{f,g}(\vec{v},u))\end{array}$$

structure Formulae (k : ℕ) where
  zero : 𝚺₁-Semisentence (k + 1)
  succ : 𝚺₁-Semisentence (k + 3)

structure Construction {k : ℕ} (p : Formulae k) where
  zero : (Fin k → M) → M
  succ : (Fin k → M) → M → M → M
  zero_defined : DefinedFunction zero p.zero
  succ_defined : DefinedFunction (fun v ↦ succ (v ·.succ.succ) (v 1) (v 0)) p.succ

variable {k : ℕ} {p : Formulae k} (c : Construction M p) (v : Fin k → M)

def Construction.result (u : M) : M

theorem Construction.result_zero :
    c.result v 0 = c.zero v

theorem Construction.result_succ (u : M) :
    c.result v (u + 1) = c.succ v u (c.result v u)

• Formulae, Construction, Construction.result, Construction.result_zero, Construction.result_succ

Fixpoint

Let ${\Phi }_C(\vec{v},x)$ be a predicate, which takes a class $C$ as a parameter. Then there is a ${\Sigma }_1$-predicate ${\mathsf{Fix}}_{\Phi }(\vec{v},x)$ such that

$${\mathsf{Fix}}_{\Phi }(\vec{v},x)⟺{\Phi }_{\{z\mid {\mathsf{Fix}}_{\Phi }(\vec{v},z)\}}(\vec{v},x)$$

if $\Phi$ satisfies following conditions:

1. $\Phi$ is ${\Delta }_1$-definable if $C$ is a set. i.e., a predicate $(c,\vec{v},x)\mapsto {\Phi }_{\{z\mid \mathrm{Bit}(z,c)\}}(\vec{v},x)$ is ${\Delta }_1$-definable.
2. Monotone: $C\subseteq C^{\prime }$ and ${\Phi }_C(\vec{v},x)$ implies ${\Phi }_{C^{\prime }}(\vec{v},x)$.
3. Finite: ${\Phi }_C(\vec{v},x)$ implies the existence of a $m$ s.t. ${\Phi }_{\{z\in C\mid z<m\}}(\vec{v},x)$.

structure Blueprint (k : ℕ) where
  core : 𝚫₁-Semisentence (k + 2)

structure Construction (φ : Blueprint k) where
  Φ : (Fin k → M) → Set M → M → Prop
  defined : Arith.Defined (fun v ↦ Φ (v ·.succ.succ) {x | x ∈ v 1} (v 0)) φ.core
  monotone {C C' : Set M} (h : C ⊆ C') {v x} : Φ v C x → Φ v C' x

class Construction.Finite (c : Construction M φ) where
  finite {C : Set M} {v x} : c.Φ v C x → ∃ m, c.Φ v {y ∈ C | y < m} x

variable {k : ℕ} {φ : Blueprint k} (c : Construction M φ) [Finite c] (v : Fin k → M)

def Construction.Fixpoint (x : M) : Prop

theorem Construction.case :
    c.Fixpoint v x ↔ c.Φ v {z | c.Fixpoint v z} x

• Blueprint, Construction, Construction.Finite, Construction.Fixpoint, Construction.case

${\mathsf{Fix}}_{\Phi }(\vec{v},x)$ is ${\Delta }_1$ if $\Phi$ satisfies strong finiteness:

class Construction.StrongFinite (c : Construction M φ) where
  strong_finite {C : Set M} {v x} : c.Φ v C x → c.Φ v {y ∈ C | y < x} x

• StrongFinite

Also structural induction holds.

theorem Construction.induction [c.StrongFinite]
    {P : M → Prop} (hP : (Γ, 1)-Predicate P)
    (H : ∀ C : Set M, (∀ x ∈ C, c.Fixpoint v x ∧ P x) → ∀ x, c.Φ v C x → P x) :
    ∀ x, c.Fixpoint v x → P x

• LO.Arith.Fixpoint.Construction.induction

Gödel's First Incompleteness Theorem

A deduction system $\mathcal{S}$ is complete iff it can prove or refute every sentence $\sigma$. Otherwise, $\mathcal{S}$ is incomplete.

def System.Complete {F S} [System F S] [LogicalConnective F] (𝓢 : S) : Prop :=
    ∀ f, 𝓢 ⊢! f ∨ 𝓢 ⊢! ~f

• System.Complete

Theorem

Let $T$ be a ${\Delta }_1$-definable arithmetic theory, stronger than ${\mathsf{R}}_0$ and ${\Sigma }_1$-sound.

Representeation Theorem

Theorem: Let $S$ be a r.e. set. Then, there exists a formula ${\phi }_S(x)$ such that $n\in S⟺T⊢{\phi }_S(\overline{n})$ for all $n\in \mathbb{N}$.

lemma re_complete
    [𝐑₀ ≼ T] [Sigma1Sound T]
    {p : ℕ → Prop} (hp : RePred p) {x : ℕ} :
    p x ↔ T ⊢! ↑((codeOfRePred p)/[‘↑x’] : Sentence ℒₒᵣ) 

• re_complete

Main Theorem

Theorem: ${\Sigma }_1$-sound and ${\Delta }_1$-definable first-order theory, which is stronger than ${\mathsf{R}}_0$, is incomplete.

• Proof.

  Define a set of formulae with one variable. $$D:=\{\phi \mid T⊢\neg \phi (┌\phi ┐)\}$$ $D$ is r.e. since $T$ is ${\Delta }_1$-definable. (one could use Craig's trick to weaken this condition to ${\Sigma }_1$, but I will not do that here.)

  By the representation theorem, there exists a ${\Sigma }_1$ formula $\rho (x)$ that represents $D$. i.e.,

  $$T⊢\rho (┌\phi ┐)⟺T⊢\neg \phi (┌\phi ┐)$$

  Let $\gamma :=\rho (┌\rho ┐)$. The next follows immediately.

  $$T⊢\gamma ⟺T⊢\neg \gamma$$

  Thus, as $T$ is consistent, $\gamma$ is undecidable from $T$. ∎

theorem goedel_first_incompleteness
  (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable] :
  ¬System.Complete T

• goedel_first_incompleteness

Gödel's Second Incompleteness Theorem

Recall that inside $\mathsf{I}{\Sigma }_1$ we can do basic set theory and primitive recursion. Many inductive notions and functions on them are defined in ${\Delta }_1$ or ${\Sigma }_1$ using the fixpoint construction.

We work inside an arbitrary model $V$ of $\mathsf{I}{\Sigma }_1$.

Coding of Terms and Formulae

Term

Define $T_C$ as follows.

$$\begin{array}{rlrl}u\in T_C& ⟺& & (\exists z)[u=\widehat{\#z}]\vee \\ & & & (\exists x)[u=\widehat{\&x}]\vee \\ & & & (\exists k,f,v)[{\mathrm{Func}}_k(f)\wedge \mathrm{Seq}(v)\wedge k=\mathrm{lh}(v)\wedge (\forall i,z)[⟨i,z⟩\in v\to z\in C]\wedge u=\widehat{f^k(v)}]\end{array}$$

$\hat{\bullet }$ is a quasi-quotation. $$\begin{array}{rlrl}\text{bounded variable: }& & \widehat{\#z}& :=⟨0,z⟩+1\\ \text{free variable: }& & \widehat{\&x}& :=⟨1,x⟩+1\\ \text{function: }& & \widehat{f^k(v)}& :=⟨2,f,k,v⟩+1\end{array}$$

$T_C$ is ${\Delta }_1$ (if $C$ is a finite set) and monotone. Let $\mathrm{UTerm}(t)$ be a fixpoint of $T_C$. It is ${\Delta }_1$ since $T_C$ satisfies strong finiteness. Define the function $\mathrm{termBV}(t)$ inductively on $\mathrm{UTerm}$ meaning the largest bounded variable $+1$ that appears in the term. Define $\mathrm{Semiterm}(n,t):=\mathrm{UTerm}(t)\wedge \mathrm{termBV}(t)\le n$.

Formula

Similarly, Define $F_C$:

$$\begin{array}{rlrl}u\in F_C& ⟺& & (\exists k,R,v)[{\mathrm{Rel}}_k(R)\wedge \text{v is a list of UTerm of length k}\wedge u=\widehat{R^k(v)}]\vee \\ & & & (\exists k,R,v)[{\mathrm{Rel}}_k(R)\wedge \text{v is a list of UTerm of length k}\wedge u=\widehat{\neg R^k(v)}]\vee \\ & & & [u=\hat{\top }]\vee \\ & & & [u=\hat{\perp }]\vee \\ & & & (\exists p\in C,q\in C)[u=\widehat{p\wedge q}]\vee \\ & & & (\exists p\in C,q\in C)[u=\widehat{p\vee q}]\vee \\ & & & (\exists p\in C)[u=\widehat{\forall p}]\vee \\ & & & (\exists p\in C)[u=\widehat{\exists p}]\end{array}$$

$$\begin{array}{rl}\widehat{R^k(v)}& :=⟨0,R,k,v⟩+1\\ \widehat{\neg R^k(v)}& :=⟨1,R,k,v⟩+1\\ \hat{\top }& :=⟨2,0⟩+1\\ \hat{\perp }& :=⟨3,0⟩+1\\ \widehat{p\wedge q}& :=⟨4,p,q⟩+1\\ \widehat{p\vee q}& :=⟨5,p,q⟩+1\\ \widehat{\forall p}& :=⟨6,p⟩+1\\ \widehat{\exists p}& :=⟨7,p⟩+1\end{array}$$

$F_C$ is ${\Delta }_1$ and monotone. Let $\mathrm{UFormula}(p)$ be a fixpoint of $F_C$ and define

$$\mathrm{Semiformula}(n,p)⟺\mathrm{UFormula}(p)\wedge \mathrm{bv}(p)\le n$$

The function $\mathrm{bv}(p)$ is defined inductively on $\mathrm{UFormula}$ meaning the largest bounded variable $+1$ that appears in the formula.

$\mathrm{UFormula}(p)$ and $\mathrm{Semiormula}(n,p)$ are again ${\Delta }_1$ since $F_C$ satisfies strong finiteness.

Formalized Provability

Let $T$ be ${\Delta }_1$-definable theory. Define $D_C$:

$$\begin{array}{rlrl}d\in D_C& ⟺& & (\forall p\in \mathrm{sqt}(d))[\mathrm{Semiformula}(0,p)]\wedge \\ & & [& (\exists s,p)[d=\widehat{\text{AXL}(s,p)}\wedge p\in s\wedge \hat{\neg }p\in s]\vee \\ & & & (\exists s)[d=\widehat{\top \text{-INTRO}(s)}\wedge \hat{\top }\in s]\vee \\ & & & (\exists s,p,q)(\exists d_p,d_q\in C)[d=\widehat{\wedge \text{-INTRO}(s,p,q,d_p,d_q)}\wedge \widehat{p\wedge q}\in s\wedge \mathrm{sqt}(d_p)=s\cup \{p\}\wedge \mathrm{sqt}(d_q)=s\cup \{q\}]\vee \\ & & & (\exists s,p,q)(\exists d\in C)[d=\widehat{\vee \text{-INTRO}(s,p,q,d)}\wedge \widehat{p\vee q}\in s\wedge \mathrm{sqt}(d)=s\cup \{p,q\}]\vee \\ & & & (\exists s,p)(\exists d\in C)[d=\widehat{\forall \text{-INTRO}(s,p,d)}\wedge \widehat{\forall p}\in s\wedge \mathrm{sqt}(d)=s^{+}\cup \{p^{+}[\&0]\}]\vee \\ & & & (\exists s,p,t)(\exists d\in C)[d=\widehat{\exists \text{-INTRO}(s,p,t,d)}\wedge \widehat{\exists p}\in s\wedge \mathrm{sqt}(d)=s\cup \{p(t)\}]\vee \\ & & & (\exists s)(\exists d^{\prime }\in C)[d=\widehat{\mathrm{WK}(s,d^{\prime })}\wedge s\supseteq \mathrm{sqt}(d^{\prime })]\\ & & & (\exists s)(\exists d^{\prime }\in C)[d=\widehat{\mathrm{SHIFT}(s,d^{\prime })}\wedge s=\mathrm{sqt}(d^{\prime }{)}^{+}]\\ & & & (\exists s,p)(\exists d_1,d_2\in C)[d=\widehat{\mathrm{CUT}(s,p,d_1,d_2)}\wedge \mathrm{sqt}(d_1)=s\cup \{p\}\wedge \mathrm{sqt}(d_2)=s\cup \{\neg p\}]\\ & & & (\exists s,p)[d=\widehat{\mathrm{ROOT}(s,p)}\wedge p\in s\wedge p\in T]]\end{array}$$

$$\begin{array}{rl}\widehat{\text{AXL}(s,p)}& :=⟨s,0,p⟩+1\\ \widehat{\top \text{-INTRO}(s)}& :=⟨s,1,0⟩+1\\ \widehat{\wedge \text{-INTRO}(s,p,q,d_p,d_q)}& :=⟨s,2,p,q,d_p,d_q⟩+1\\ \widehat{\vee \text{-INTRO}(s,p,q,d)}& :=⟨s,3,p,q,d⟩+1\\ \widehat{\forall \text{-INTRO}(s,p,d)}& :=⟨s,4,p,d⟩+1\\ \widehat{\exists \text{-INTRO}(s,p,t,d)}& :=⟨s,5,p,t,d⟩+1\\ \widehat{\text{WK}(s,d)}& :=⟨s,6,d⟩+1\\ \widehat{\text{SHIFT}(s,d)}& :=⟨s,7,d⟩+1\\ \widehat{\text{CUT}(s,p,d_1,d_2)}& :=⟨s,8,p,d_1,d_2⟩+1\\ \widehat{\text{ROOT}(s,p)}& :=⟨s,9,p⟩+1\\ \mathrm{sqt}(d)& :={\pi }_1(d-1)\end{array}$$

$p^{+}$ is a shift of a formula $p$. $s^{+}$ is a image of shift of $s$. Take fixpoint ${\mathrm{Derivation}}_T(d)$.

$$\begin{array}{rl}{\mathrm{Derivable}}_T(\Gamma )& :=(\exists d)[{\mathrm{Derivation}}_T(d)\wedge \mathrm{sqt}(d)=\Gamma ]\\ {\mathrm{Bew}}_T(p)& :={\mathrm{Derivable}}_T(\{p\})\end{array}$$

Following holds for all formula (not coded one) $\phi$ and finite set $\Gamma$.

• Sound: $\mathbb{N}\models {\mathrm{Bew}}_T(┌\phi ┐)⟹T⊢\phi$

  lemma LO.Arith.Language.Theory.Provable.sound :
      (T.codeIn ℕ).Provable ⌜p⌝ → T ⊢! p 
  

  • LO.Arith.Language.Theory.Provable.sound
• D1: $T⊢\phi ⟹V\models {\mathrm{Bew}}_T(┌\phi ┐)$

  theorem LO.Arith.provable_of_provable :
      T ⊢! p → (T.codeIn V).Provable ⌜p⌝ 
  

  • LO.Arith.provable_of_provable
• D2: ${\mathrm{Bew}}_T(┌\phi \to \psi ┐)\&{\mathrm{Bew}}_T(┌\phi ┐)⟹{\mathrm{Bew}}_T(┌\psi ┐)$
• Formalized ${\Sigma }_1$-completeness: Let $\sigma$ be a ${\Sigma }_1$-sentence. $V\models \sigma ⟹V\models {\mathrm{Bew}}_{T+{\mathsf{R}}_0}(┌\sigma ┐)$

  theorem LO.Arith.sigma₁_complete (hσ : Hierarchy 𝚺 1 σ) :
      V ⊧ₘ₀ σ → T.Provableₐ (⌜σ⌝ : V)
  

  • LO.Arith.sigma₁_complete

Now assume that $U$ is a theory of arithmetic stronger than ${\mathsf{R}}_0$ and $T$ be a theory of arithmetic stronger than $\mathsf{I}{\Sigma }_1$. The following holds, thanks to the completeness theorem.

• $U⊢\sigma ⟺T⊢{\mathrm{Bew}}_U(┌\sigma ┐)$
  • LO.FirstOrder.Arith.provableₐ_complete
• $T⊢{\mathrm{Bew}}_U(┌\sigma \to \pi ┐)\to {\mathrm{Bew}}_U(┌\sigma ┐)\to {\mathrm{Bew}}_U(┌\pi ┐)$
  • LO.FirstOrder.Arith.provableₐ_D2
• $T⊢{\mathrm{Bew}}_U(┌\sigma ┐)\to {\mathrm{Bew}}_U(┌{\mathrm{Bew}}_U(┌\sigma ┐)┐)$
  • LO.FirstOrder.Arith.provableₐ_D3

Second Incompleteness Theorem

Assume that $T$ is ${\Delta }_1$-definable and stronger than $\mathsf{I}{\Sigma }_1$.

Fixpoint Lemma

Since the substitution is ${\Sigma }_1$, There is a formula $\mathrm{ssnum}(y,p,x)$ such that, for all formula $\phi$ with only one variable and $x,y\in V$,

$$\mathrm{ssnum}(y,┌\phi ┐,x)⟺y=┌\phi (\overline{x})┐$$

holds. (overline $\overline{\bullet }$ denotes the (formalized) numeral of $x$)

Define a sentence ${\mathrm{fixpoint}}_{\theta }$ for formula (with one variable) $\theta$ as follows.

$$\begin{array}{rl}{\mathrm{fixpoint}}_{\theta }& :={\mathrm{diag}}_{\theta }(\overline{┌{\mathrm{diag}}_{\theta }┐})\\ {\mathrm{diag}}_{\theta }(x)& :=(\forall y)[\mathrm{ssnum}(y,x,x)\to \theta (y)]\end{array}$$

Lemma: $T⊢{\mathrm{fixpoint}}_{\theta }\leftrightarrow \theta (┌{\mathrm{fixpoint}}_{\theta }┐)$

• Proof. $$\begin{array}{rl}{\mathrm{fixpoint}}_{\theta }& \equiv (\forall x)[\mathrm{ssnum}(x,┌{\mathrm{diag}}_{\theta }┐,┌{\mathrm{diag}}_{\theta }┐)\to \theta (x)]\\ & \leftrightarrow \theta (┌{\mathrm{diag}}_{\theta }(\overline{┌{\mathrm{diag}}_{\theta }┐})┐)\\ & \equiv \theta (┌{\mathrm{fixpoint}}_{\theta }┐)\end{array}$$ ∎

theorem LO.FirstOrder.Arith.diagonal (θ : Semisentence ℒₒᵣ 1) :
    T ⊢!. fixpoint θ ⭤ θ/[⌜fixpoint θ⌝]

• LO.FirstOrder.Arith.diagonal

Main Theorem

Define Gödel sentence ${\mathrm{G}}_T$: $${\mathrm{G}}_T:={\mathrm{fixpoint}}_{\neg {\mathrm{Bew}}_T(x)}$$

Lemma: Gödel sentence is undecidable, i.e., $T⊬\mathrm{G}$ if $T$ is consistent, and $T⊬\neg \mathrm{G}$ if $\mathbb{N}\models T$.

lemma goedel_unprovable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
    T ⊬ ↑𝗚

lemma not_goedel_unprovable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
    T ⊬ ∼↑𝗚

• goedel_unprovable
• not_goedel_unprovable

Define formalized incompleteness sentence ${\mathrm{Con}}_T$: $${\mathrm{Con}}_T:=\neg {\mathrm{Bew}}_T(┌\perp ┐)$$

Lemma: $T⊢{\mathrm{Con}}_T\leftrightarrow G_T$

lemma consistent_iff_goedel
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] :
    T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚

• consistent_iff_goedel

Theorem: $T$ cannot prove its own consistency, i.e., $T⊬{\mathrm{Con}}_T$ if $T$ is consistent. Moreover, ${\mathrm{Con}}_T$ is undecidable from $T$ if $\mathbb{N}\models T$.

theorem goedel_second_incompleteness
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
    T ⊬ ↑𝗖𝗼𝗻 

theorem inconsistent_undecidable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
    System.Undecidable T ↑𝗖𝗼𝗻

• goedel_second_incompleteness
• inconsistent_undecidable

Interpretation

Superintuitionistic Logic

Intuitionistic Logic is defined roughly that classical logic without law of excluded middle.

And superintuitionistic logic is some axioms add to intuitionistic logic.

Axioms

Deduction System

Our Hilbert-style deduction system for propositional logic is designed to take parameters. These parameters are as follows.

structure DeductionParameter (α) where
  axiomSet : AxiomSet α

• axiomSet is set of formulas (axioms), For example, 𝗘𝗙𝗤, 𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠.

In this formalization, logics that we usually refer to as $\mathbf{Int}$ (Intuitionistic Propositional Logic), $\mathbf{Cl}$ (Classical Propositional Logic), etc. is characterized by deduction parameter.

Well-Known Systems

Glivenko's Theorem

If $\phi$ is provable in classical logic, double negation inserted $\neg \neg \phi$ is provable in intuitionistic logic.

theorem iff_provable_dn_efq_dne_provable: 𝐈𝐧𝐭 ⊢! ~~p ↔ 𝐂𝐥 ⊢! p

Kripke Semantics

TODO:

Soundness for Kripke Semantics

instance : Sound 𝓓 𝔽(Ax(𝓓))

Completeness for Kripke Semantics

Standard completeness proof using canonical models, etc.

instance : Complete 𝐈𝐧𝐭 𝔽(Ax(𝐈𝐧𝐭))

Rejection Law of Excluded Middle

Law of Excluded Middle (LEM) is not always provable in intuitionistic logic.

theorem noLEM : ∃ (p : Formula α), 𝐈𝐧𝐭 ⊬! p ⋎ ~p := by

Thus, intuitionistic logic is proper weaker than classical logic, since LEM is always provable in classical logic.

theorem strictReducible_intuitionistic_classical : 𝐈𝐧𝐭 <ₛ 𝐂𝐥

Disjunctive Property

Intuitionistic Logic have Disjunctive Property (DP).

class Disjunctive (𝓢 : S) : Prop where
  disjunctive : ∀ {p q}, 𝓢 ⊢! p ⋎ q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

instance : Disjunctive 𝐈𝐧𝐭

Standard Modal Logic

As a general term for various modal logics commonly known as $\mathbf{K}$, $S4$, etc., we refer to the logic defined on a language that includes the modal operators $\square$ (Box) and $◊$ (Diamond), where $◊$ is defined as the dual of $\square$ (i.e., $◊\phi \equiv \neg \square \neg \phi$), as Standard Modal Logic¹.

Be cautious similar notations for different concepts. We use $\text{TEX}$ notation for concept that unrelated to our formalization, and code block `` for related our formalization.

• $\mathsf{K}$ (\sf K) is axiom schema unrelated to formalization.
• $\mathbf{K}$ (\bf K) is logic unrelated to formalization.
• 𝗞 (Mathematical Sans-Serif Bold) is AxiomSet in formalization.
• 𝐊 (Mathematical Bold Capital) is DeductionParameter in formalization.

Axioms

As an example, describe about axiom $\mathsf{K}$. Other axioms such as $\mathsf{T}$ and $4$ follow the same manner.

-- Axiom schema
abbrev System.Axioms.K (p q : F) := □(p ⟶ q) ⟶ □p ⟶ □q

abbrev Modal.Standard.AxiomSet (α : Type*) := Set (Modal.Standard.Formula α)

abbrev Modal.Standard.AxiomSet.K : AxiomSet α := { System.Axioms.K p q | (p) (q) }

notation "𝗞" => Modal.Standard.AxiomSet.K

Well-Known Axioms

Geach Axioms

Geach Axiom is defined as ${\mathsf{ga}}_{i,j,m,n}\equiv {◊}^i{\square }^{m}p\to {\square }^j{◊}^{n}p$.

structure Geach.Taple where
  i : ℕ
  j : ℕ
  m : ℕ
  n : ℕ

abbrev Geach (l : Geach.Taple) (p : F) := ◇^[l.i](□^[l.m]p) ⟶ □^[l.j](◇^[l.n]p)
notation "𝗴𝗲(" t ")" => AxiomSet.Geach t

Some axioms is generalized as Geach axioms (Above table, Geach: ✅). For example $\mathsf{T}\equiv {\mathsf{ga}}_{0,0,1,0}$ and $4\equiv {\mathsf{ga}}_{0,2,1,0}$.

Deduction System for Modal Logic

Our Hilbert-style deduction system for modal logic is designed to take parameters. These parameters are as follows.

structure DeductionParameter (α) where
  axiomSet : AxiomSet α
  nec : Bool

• axiomSet is set of formulas (axioms), For example, 𝗞, 𝗞 ∪ 𝗧 ∪ 𝟰.
• nec is flag to contain necessitation rule.

The parameter is called Normal if axiomSet includes 𝗞 and nec is true.

In this formalization, modal logics that we usually refer to as $\mathbf{K}$, $S4$, etc. is characterized by deduction parameter.

Geach Logic

def AxiomSet.MultiGeach : List Axioms.Geach.Taple → AxiomSet α
  | [] => 𝗞
  | x :: xs => (AxiomSet.Geach x) ∪ (AxiomSet.MultiGeach xs)
notation "𝗚𝗲(" l ")" => AxiomSet.MultiGeach l

def DeductionParameter.Geach (l : List Axioms.Geach.Taple) : DeductionParameter α where
  axiomSet := 𝗚𝗲(l)
  nec := true
notation "𝐆𝐞(" l ")" => DeductionParameter.Geach l

If 𝓓 is some 𝐆𝐞(l), 𝓓 is called Geach.

class IsGeach (𝓓 : DeductionParameter α) where
  taples : List Axioms.Geach.Taple
  char : 𝓓 = 𝐆𝐞(taples)

Soundness for Kripke Semantics

Let deduction system of 𝓓 has necessitation. If 𝓓 ⊢! p then p is valid on every frame in 𝔽(Ax(𝓓)).

instance [HasNec 𝓓] : Sound 𝓓 𝔽(Ax(𝓓))

Consistency of Deduction System via Kripke Semantics

From soundness theorem, if 𝔽(Ax(𝓓)) is nonempty, deduction system of 𝓓 is consistent (i.e. not every formula is provable in 𝓓).

instance [FrameClass.IsNonempty 𝔽(Ax(𝓓))] : System.Consistent 𝓓

It is immediately apparent, frameclass of 𝔽(Ax(𝐊)) is nonempty, thus 𝐊 is consistent.

instance : FrameClass.IsNonempty 𝔽(Ax(𝐊))

instance : System.Consistent 𝐊

• LO.System.Consistent 𝐊

Futhermore, if 𝓓 is Geach, then its frameclass is nonempty, thus it is consistent.

instance [𝓓.IsGeach] : FrameClass.IsNonempty 𝔽(Ax(𝓓))

instance [𝓓.IsGeach] : System.Consistent 𝓓

Completeness for Kripke Semantics

Completeness for Kripke Semantics (shortly called, Kripke Completeness) proved by usual way with Canonical frames and models.

If every axioms in Ax(𝓓) is valid in Canonical frame of 𝓓, 𝓓 is called Canonical.

class Canonical (𝓓 : DeductionParameter α) [Inhabited (MCT 𝓓)] where
  realize : (CanonicalFrame 𝓓) ⊧* Ax(𝓓)

If 𝓓 is canonical and consistent, then 𝓓 is complete for 𝔽(Ax(𝓓)).

instance [System.Consistent 𝓓] [Canonical 𝓓] : Complete 𝓓 𝔽(Ax(𝓓))

Immediately apparent that 𝐊 is canonical and 𝐊 is consistent mentioned above, then 𝐊 is complete.

instance : Canonical 𝐊

instance : Complete 𝐊 𝔽(Ax(𝐊))

Futhermore, if 𝓓 is Geach, then 𝓓 is canonical, thus it is complete.

instance [𝓓.IsGeach] : Canonical 𝓓

instance [𝓓.IsGeach] : Complete 𝓓 𝔽(Ax(𝓓))

On Gödel-Löb Logic

Logics Equivalent to GL

Let's introduce Henkin Axiom 𝗛, Löb Rule (𝐋), Henkin Rule (𝐇).

protected abbrev H := □(□p ⟷ p) ⟶ □p

class LoebRule where
  loeb {p : F} : 𝓢 ⊢ □p ⟶ p → 𝓢 ⊢ p

class HenkinRule where
  henkin {p : F} : 𝓢 ⊢ □p ⟷ p → 𝓢 ⊢ p

• 𝐊𝟒𝐇 is defined normal logic that axioms are 𝗞, 𝟰, 𝗛.
• 𝐊𝟒(𝐋) is defined as 𝐊𝟒 extended (𝐋).
• 𝐊𝟒(𝐇) is defined as 𝐊𝟒 extended (𝐇).

These logics are equivalent to 𝐆𝐋.

lemma reducible_GL_K4Loeb : 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)
lemma reducible_K4Loeb_K4Henkin: 𝐊𝟒(𝐋) ≤ₛ 𝐊𝟒(𝐇)
lemma reducible_K4Henkin_K4H : 𝐊𝟒(𝐇) ≤ₛ 𝐊𝟒𝐇
lemma reducible_K4Henkin_GL : 𝐊𝟒𝐇 ≤ₛ 𝐆𝐋

--- Obviously `𝐆𝐋 =ₛ 𝐊𝟒(𝐋) =ₛ 𝐊𝟒(𝐇) =ₛ 𝐊𝟒𝐇`, since transitivity of `≤ₛ` and definition of `=ₛ`.

Note: 𝐊𝐇 (normal logic that axioms are 𝗞, 𝗛) is proper weak logic of 𝐆𝐋 and not Kripke complete.

Frame Definability of GL

Strength between Logics

It is immediately apparent that, when 𝓓₁​ and 𝓓₂ are same inference rule¹, the logical strength between 𝓓₁ and 𝓓₂ is determined by the subset of their axiom set.

lemma reducible_of_subset (hNec : L₁.nec ≤ L₂.nec) (hAx : Ax(L₁) ⊆ Ax(L₂)) : L₁ ≤ₛ L₂ := by

lemma reducible_K_KT : 𝐊 ≤ₛ 𝐊𝐓

• LO.Modal.Standard.Deduction.reducible_of_subset
• LO.Modal.Standard.reducible_K_KT

However, even without the subset of axiomset, it is possible to analyze the strength of logic via Kripke semantics, specifically by analyzing the properties of frames defined by the axioms. For example, since seriality follows from reflexivity, $\mathbf{KT}$ is stronger than $\mathbf{KD}$ ($\mathsf{K}\cup \mathsf{D}⊈\mathsf{K}\cup \mathsf{T}$).

lemma reducible_of_definability
  [Sound 𝓓₁​ 𝔽(Ax(𝓓₁​))] [Complete 𝓓₂ 𝔽(Ax(𝓓₂))]
  [Definability Ax(𝓓₁​) P₁] [Definability Ax(𝓓₂) P₂]
  (hs : ∀ {F : Frame}, P₂ F → P₁ F)
  : 𝓓₁​ ≤ₛ 𝓓₂

theorem reducible_KD_KT : 𝐊𝐃 ≤ₛ 𝐊𝐓

• LO.Modal.Standard.Kripke.reducible_of_definability
• LO.Modal.Standard.reducible_KD_KT

By same argument, the equivalence of provability between logics can be analyzed. $S5$ is equivalent to $KT4B$ ($\mathsf{K}\cup \mathsf{T}\cup 5\ne \mathsf{K}\cup \mathsf{T}\cup 4\cup \mathsf{B}$).

lemma equiv_of_iff_definability
  [Sound 𝓓₁​ 𝔽(Ax(𝓓₁​))] [Sound 𝓓₂ 𝔽(Ax(𝓓₂))]
  [Complete 𝓓₁​ 𝔽(Ax(𝓓₁​))] [Complete 𝓓₂ 𝔽(Ax(𝓓₂))]
  [Definability Ax(𝓓₁​) P₁] [Definability Ax(𝓓₂) P₂]
  (h : ∀ {F : Frame}, P₁ F ↔ P₂ F) : 𝓓₁​ =ₛ 𝓓₂

theorem equiv_S5_KT4B : 𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁

• LO.Modal.Standard.Kripke.equiv_of_iff_definability
• LO.Modal.Standard.equiv_S5_KT4B

Undefinability of Frame Property

There is no axiom set that irreflexivity of frame defines. In other words, as long as the inference rule of 𝓓 is only necessitation, no matter what axiom sets of 𝓓 has, deduction system of 𝓓 cannot be represent irreflexive Kripke frame.

theorem Kripke.undefinability_irreflexive : ¬∃ (Ax : AxiomSet α), (∀ {F : Frame}, (Irreflexive F.Rel) ↔ F ⊧* Ax)

• LO.Modal.Standard.Kripke.undefinability_irreflexive

Modal Companion

Gödel-McKensey-Tarski Theorem

Through a translation called Gödel Translation from propositional logic formula to modal logic formula, intuitionistic logic $\mathbf{Int}$ can be embedded into $S4$. (This theorem is known as Gödel-McKensey-Tarski Theorem.)

def GoedelTranslation : Superintuitionistic.Formula α → Formula α

postfix:75 "ᵍ" => GoedelTranslation

theorem provable_efq_iff_provable_S4
  {p : Superintuitionistic.Formula α}
  : 𝐈𝐧𝐭 ⊢! p ↔ 𝐒𝟒 ⊢! pᵍ

• LO.Modal.Standard.provable_efq_iff_provable_S4

Modal Companion

The generalized version of this relationship is called Modal Companion. $(\mathbf{Int},S4)$ has modal companion.

class ModalCompanion (i𝓓 : Superintuitionistic.DeductionParameter α) (m𝓓 : Modal.Standard.DeductionParameter α) where
  companion : ∀ {p : Superintuitionistic.Formula α}, i𝓓 ⊢! p ↔ m𝓓 ⊢! pᵍ

instance : ModalCompanion 𝐈𝐧𝐭 𝐒𝟒

• LO.Modal.Standard.instModalCompanionIntuitionisticS4