Boxdot Conjecture

This file defines the syntax and proof systems for modal logic, along with the Boxdot translation and the Boxdot Conjecture. We introduce:

• Formula: the inductive type for propositional modal formulas.
• t: the recursive Boxdot translation function.
• KProof and KTProof: axiomatizations of the basic K system and K plus T.
• NormalModalLogic: a structure capturing any normal modal logic.
• KT: the specific normal modal logic corresponding to K plus T.
• BoxdotConjecture: states that if a logic agrees with KT on all boxdot-translations, then it cannot be strictly larger than KT.

The Boxdot Conjecture was originally formulated by French and Humberstone and has been studied in several works. In particular, see:

References:

• Cluster Expansion and the Boxdot Conjecture, Emil Jeřábek, arXiv:1308.0994.
• The Boxdot Conjecture and the Generalized McKinsey Axiom, Christopher Steinsvold, Australasian Journal of Logic (AJL).

Jeřábek's proof of the Boxdot Conjecture has been formalised in Lean: https://github.com/FormalizedFormalLogic/Foundation. Note however that the statement's formalisation in that repository is different to the one presented in the current file.

inductive Arxiv.«1308.0994».Formula : Type

Formula is the inductive type of propositional modal formulas:

• Atom n is a propositional variable indexed by n.
• Falsum is the constant ⊥.
• Imp α β is implication (α → β).
• Nec α is the necessity operator □α.

• Atom : ℕ → Formula

  Atom n is a propositional variable indexed by n.

• Falsum : Formula

  Falsum is the constant ⊥.

• Imp : Formula → Formula → Formula

  Imp α β is implication (α → β).

• Nec : Formula → Formula

  Nec α is the necessity operator □α.

def Arxiv.«1308.0994».«term⊥» : Lean.ParserDescr

Falsum is the constant ⊥.

Equations

• Arxiv.«1308.0994».«term⊥» = Lean.ParserDescr.node `Arxiv.«1308.0994».«term⊥» 1024 (Lean.ParserDescr.symbol "⊥")

def Arxiv.«1308.0994».«term_~>_» : Lean.TrailingParserDescr

Imp α β is implication (α → β).

Equations

• One or more equations did not get rendered due to their size.

def Arxiv.«1308.0994».«term~_» : Lean.ParserDescr

~ α is the negation of α. ~ α is also equivalent to α ~> ⊥.

Equations

• Arxiv.«1308.0994».«term~_» = Lean.ParserDescr.node `Arxiv.«1308.0994».«term~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 0))

def Arxiv.«1308.0994».«term□_» : Lean.ParserDescr

Nec α is the necessity operator □α.

Equations

• Arxiv.«1308.0994».«term□_» = Lean.ParserDescr.node `Arxiv.«1308.0994».«term□_» 95 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 95))

@[reducible]

def Arxiv.«1308.0994».Conj (α β : Formula) : Formula

Conj α β is the conjunction α ∧ β. We define α & β as ~(α ~> ~β) for simplicity.

Equations

• Arxiv.«1308.0994».Conj α β = (α ~> β ~> Arxiv.«1308.0994».Formula.Falsum) ~> Arxiv.«1308.0994».Formula.Falsum

def Arxiv.«1308.0994».«term_&_» : Lean.TrailingParserDescr

Conj α β is the conjunction α ∧ β. We define α & β as ~(α ~> ~β) for simplicity.

Equations

• Arxiv.«1308.0994».«term_&_» = Lean.ParserDescr.trailingNode `Arxiv.«1308.0994».«term_&_» 85 86 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " & ") (Lean.ParserDescr.cat `term 85))

def Arxiv.«1308.0994».t (φ : Formula) : Formula

t φ is the Boxdot translation of a formula φ. Roughly, t is the mapping φ ↦ t φ from the language of monomodal logic into itself that preserves variables and the logical constant ⊥, commutes with the standard truth-functional operators, and is such that t □a = □t a & t a. This implementation follows the definition in Steinsvold (AJL).

Equations

• Arxiv.«1308.0994».t (α ~> β) = Arxiv.«1308.0994».t α ~> Arxiv.«1308.0994».t β
• Arxiv.«1308.0994».t α.Nec = Arxiv.«1308.0994».Conj (Arxiv.«1308.0994».t α).Nec (Arxiv.«1308.0994».t α)
• Arxiv.«1308.0994».t φ = φ

def Arxiv.«1308.0994».«term■_» : Lean.ParserDescr

t φ is the Boxdot translation of a formula φ. Roughly, t is the mapping φ ↦ t φ from the language of monomodal logic into itself that preserves variables and the logical constant ⊥, commutes with the standard truth-functional operators, and is such that t □a = □t a & t a. This implementation follows the definition in Steinsvold (AJL).

Equations

• Arxiv.«1308.0994».«term■_» = Lean.ParserDescr.node `Arxiv.«1308.0994».«term■_» 95 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "■") (Lean.ParserDescr.cat `term 95))

inductive Arxiv.«1308.0994».KProof : Set Formula → Formula → Prop

KProof Γ φ is the usual Hilbert‐style proof relation for the minimal normal modal logic K, with assumptions drawn from Γ.

• ax {Γ : Set Formula} {α : Formula} (h : α ∈ Γ) : KProof Γ α

  Assumption rule: if α ∈ Γ then α is provable from Γ.

• ax1 {Γ : Set Formula} {α β : Formula} : KProof Γ (α ~> β ~> α)

  Ax1: every instance of the schema α → (β → α) is a theorem.

• ax2 {Γ : Set Formula} {α β γ : Formula} : KProof Γ ((α ~> β ~> γ) ~> (α ~> β) ~> α ~> γ)

  Ax2: every instance of the schema (α ~> β ~> γ) ~> (α ~> β) ~> (α ~> γ) is a theorem.

• ax3 {Γ : Set Formula} {α β : Formula} : KProof Γ (((α ~> Formula.Falsum) ~> β ~> Formula.Falsum) ~> β ~> α)

  Ax3 (contraposition): every instance of the schema (~α ~> ~β) ~> (β ~> α) is a theorem.

• mp {Γ : Set Formula} {α β : Formula} : KProof Γ (α ~> β) → KProof Γ α → KProof Γ β

  Modus Ponens: if Γ ⊢ α ~> β and Γ ⊢ α, then Γ ⊢ β.

• nec {Γ : Set Formula} {α : Formula} : KProof ∅ α → KProof Γ α.Nec

  Necessitation: if ⊢ α then ⊢ □α.

• distr {Γ : Set Formula} {α β : Formula} : KProof Γ ((α ~> β).Nec ~> α.Nec ~> β.Nec)

  Distribution: every instance of the schema □(α ~> β) ~> (□α ~> □β) is a theorem.

inductive Arxiv.«1308.0994».KTProof : Set Formula → Formula → Prop

KTProof Γ φ denotes that φ is provable from the premises Γ in the normal modal logic KT (also called T). KT extends system K by adding the instances of the T-axiom schema □φ ~> φ to K’s usual axioms and rules of inference.

• lift_K {Γ : Set Formula} {α : Formula} (h : KProof Γ α) : KTProof Γ α

  Embedding of K proofs into KT.

• axT {Γ : Set Formula} {α : Formula} : KTProof Γ (α.Nec ~> α)

  T-axiom schema: every instance of □α ~> α is a theorem.

• mp {Γ : Set Formula} {α β : Formula} : KTProof Γ (α ~> β) → KTProof Γ α → KTProof Γ β

  Modus Ponens: if Γ ⊢ α ~> β and Γ ⊢ α, then Γ ⊢ β.

• nec {Γ : Set Formula} {α : Formula} : KTProof ∅ α → KTProof Γ α.Nec

  Necessitation: if ⊢ α then ⊢ □α.

theorem Arxiv.«1308.0994».KTExtendsK {Γ : Set Formula} {φ : Formula} (h : KProof Γ φ) : KTProof Γ φ

If KProof Γ φ, then KTProof Γ φ. In other words, KT extends K.

structure Arxiv.«1308.0994».NormalModalLogic : Type

A “normal modal logic” L is any Set Formula such that:

1. If K ⊢ φ, then φ ∈ L (L extends K)
2. If φ ∈ L and (φ ~> ψ) ∈ L, then ψ ∈ L (Closed under MP)
3. If φ ∈ L, then □φ ∈ L (Closed under Necessitation)

• thms : Set Formula

  thms is the set of formulas proveable in the logic.

• extK {φ : Formula} : KProof ∅ φ → φ ∈ self.thms

  extK means that if K ⊢ φ, then φ ∈ thms. That is, the logic extends system K.

• mp {φ ψ : Formula} : φ ∈ self.thms → φ ~> ψ ∈ self.thms → ψ ∈ self.thms

  mp means that if φ ∈ thms and (φ ~> ψ) ∈ thms, then ψ ∈ thms. That is, thms is closed under modus ponens.

• nec {φ : Formula} : φ ∈ self.thms → φ.Nec ∈ self.thms

  nec means that if φ ∈ thms, then □φ ∈ thms. Equivalently, thms is closed under necessitation

def Arxiv.«1308.0994».proves (L : NormalModalLogic) (φ : Formula) : Prop

Equations

• Arxiv.«1308.0994».proves L φ = (φ ∈ L.thms)

def Arxiv.«1308.0994».«term_⊢_» : Lean.TrailingParserDescr

Equations

• Arxiv.«1308.0994».«term_⊢_» = Lean.ParserDescr.trailingNode `Arxiv.«1308.0994».«term_⊢_» 85 86 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 85))

def Arxiv.«1308.0994».«term_⊆_» : Lean.TrailingParserDescr

Equations

• Arxiv.«1308.0994».«term_⊆_» = Lean.ParserDescr.trailingNode `Arxiv.«1308.0994».«term_⊆_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ ") (Lean.ParserDescr.cat `term 0))

def Arxiv.«1308.0994».KT : NormalModalLogic

KT is the specific normal modal logic whose theorems are exactly those provable in KTProof from the empty context.

This corresponds to K ⊕ (□φ → φ) as in both AJL (Steinsvold) and Jeřábek.

Equations

• One or more equations did not get rendered due to their size.

theorem Arxiv.«1308.0994».BoxdotConjecture (L : NormalModalLogic) (H : ∀ (φ : Formula), proves L (t φ) ↔ proves KT φ) : L.thms ⊆ KT.thms

Boxdot Conjecture: every normal modal logic that faithfully interprets KT by the boxdot translation is included in KT.