FormalConjectures/Arxiv/1308.0994/BoxdotConjecture.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 1 contain sorry, 0 declared as axioms

Boxdot Conjecture

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

References:

Imports (1)
Imported by 1 file
  1. inductive Arxiv.«1308.0994».Formula Formula is the inductive type of propositional modal formulas: * Atom n is a propositional variable indexed by n line 46 source

    Source documentation

    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 □α.

    no axioms what this means

    inductive Formula : Type
  /-- `Atom n` is a propositional variable indexed by `n`. -/
  | Atom : Nat → Formula
  /--  `Falsum` is the constant ⊥. -/
  | Falsum : Formula
  /-- `Imp α β` is implication `(α → β)`. -/
  | Imp : Formula → Formula → Formula
  /-- `Nec α` is the necessity operator `□α`. -/
  | Nec : Formula → Formula

open Formula
…
  2. def Arxiv.«1308.0994».Conj Conj α β is the conjunction α ∧ β line 72 source

    Source documentation

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

    no axioms what this means

    Statement uses: Arxiv.«1308.0994».Formula

    Proof uses: Arxiv.«1308.0994».Formula.Imp, Arxiv.«1308.0994».Formula.Falsum

    def Conj (α β : Formula) : Formula := ~(α ~> ~β)
…

    Mentions: Arxiv.«1308.0994».Formula

  3. def Arxiv.«1308.0994».t t φ is the Boxdot translation of a formula φ line 83 source

    Source documentation

    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).

    standard axioms: propext what this means

    Statement uses: Arxiv.«1308.0994».Formula

    2 instances, coercions and auxiliary constants left out.

    def t (φ : Formula) : Formula :=
…

    Mentions: Arxiv.«1308.0994».Formula

  4. def Arxiv.«1308.0994».Formula.subst Formula.subst σ φ is the uniform substitution of σ n for each propositional variable Atom n in φ line 96 source

    Source documentation

    Formula.subst σ φ is the uniform substitution of σ n for each propositional variable Atom n in φ.

    no axioms what this means

    Statement uses: Nat, Arxiv.«1308.0994».Formula

    2 instances, coercions and auxiliary constants left out.

    def Formula.subst (σ : ℕ → Formula) : Formula → Formula
  | Atom n => σ n
  | ⊥ => ⊥
  | α ~> β => subst σ α ~> subst σ β
  | □α => □(subst σ α)


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

    Mentions: Arxiv.«1308.0994».Formula, Arxiv.«1308.0994».KProof

  5. inductive Arxiv.«1308.0994».KProof KProof Γ φ is the usual Hilbert‐style proof relation for the minimal normal modal logic K, with assumptions drawn from Γ line 107 source

    Source documentation

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

    no axioms what this means

    Statement uses: Set, Arxiv.«1308.0994».Formula

    inductive KProof : Set Formula → Formula → Prop
/-- Assumption rule: if `α ∈ Γ` then `α` is provable from `Γ`. -/
| ax {Γ} {α} (h : α ∈ Γ) : KProof Γ α
/-- Ax1: every instance of the schema `α → (β → α)` is a theorem. -/
| ax1 {Γ} {α β} : KProof Γ (α ~> β ~> α)
/-- Ax2: every instance of the schema `(α ~> β ~> γ) ~> (α ~> β) ~> (α ~> γ)` is a theorem. -/
| ax2 {Γ} {α β γ} : KProof Γ ((α ~> β ~> γ) ~> (α ~> β) ~> (α ~> γ))
/-- Ax3 (contraposition): every instance of the schema `(~α ~> ~β) ~> (β ~> α)` is a theorem. -/
| ax3 {Γ} {α β} : KProof Γ (((~α) ~> (~β)) ~> (β ~> α))
/-- Modus Ponens: if `Γ ⊢ α ~> β` and `Γ ⊢ α`, then `Γ ⊢ β`. -/
| mp {Γ} {α β} (_ : KProof Γ (α ~> β)) (_ : KProof Γ α) : KProof Γ β
/-- Necessitation: if `⊢ α` then `⊢ □α`. -/
…

    Mentions: Arxiv.«1308.0994».Formula

  6. inductive Arxiv.«1308.0994».KTProof KTProof Γ φ denotes that φ is provable from the premises Γ in the normal modal logic KT (also called T) line 129 source

    Source documentation

    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.

    no axioms what this means

    Statement uses: Set, Arxiv.«1308.0994».Formula

    inductive KTProof : Set Formula → Formula → Prop
/-- Embedding of K proofs into KT. -/
| lift_K {Γ} {α} (h : KProof Γ α) : KTProof Γ α
/-- T-axiom schema: every instance of `□α ~> α` is a theorem. -/
| axT {Γ} {α} : KTProof Γ (□ α ~> α)
/-- Modus Ponens: if `Γ ⊢ α ~> β` and `Γ ⊢ α`, then `Γ ⊢ β`. -/
| mp {Γ} {α β} (_ : KTProof Γ (α ~> β)) (_ : KTProof Γ α) : KTProof Γ β
/-- Necessitation: if `⊢ α` then `⊢ □α`. -/
| nec {Γ} {α} (_ : KTProof ∅ α) : KTProof Γ (□ α)


open KProof KTProof
…

    Mentions: Arxiv.«1308.0994».Formula, Arxiv.«1308.0994».KProof

  7. lemma Arxiv.«1308.0994».KTExtendsK If KProof Γ φ, then KTProof Γ φ line 147 source

    Source documentation

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

    no axioms what this means

    Statement uses: Set, Arxiv.«1308.0994».Formula, Arxiv.«1308.0994».KProof, Arxiv.«1308.0994».KTProof

    Proof uses: Arxiv.«1308.0994».KTProof.lift_K

    lemma KTExtendsK {Γ φ} (h : KProof Γ φ) : KTProof Γ φ :=
…

    Mentions: Arxiv.«1308.0994».KProof, Arxiv.«1308.0994».KTProof

  8. lemma Arxiv.«1308.0994».KProof.subst Provability in K is closed under uniform substitution line 152 source

    Source documentation

    Provability in K is closed under uniform substitution.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Set, Arxiv.«1308.0994».Formula, Nat, Arxiv.«1308.0994».KProof, Set.image, Arxiv.«1308.0994».Formula.subst

    Proof uses: Arxiv.«1308.0994».KProof.rec, Membership.mem, Arxiv.«1308.0994».KProof.ax, Exists.intro, And, Eq, And.intro, rfl, Arxiv.«1308.0994».KProof.ax1, Arxiv.«1308.0994».KProof.ax2, Arxiv.«1308.0994».KProof.ax3, Arxiv.«1308.0994».Formula.Imp, Arxiv.«1308.0994».KProof.mp, EmptyCollection.emptyCollection, Arxiv.«1308.0994».KProof.nec, Eq.mp, congrFun', congrArg, Set.image_empty, Arxiv.«1308.0994».KProof.distr

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

    lemma KProof.subst {Γ φ} (σ : ℕ → Formula) (h : KProof Γ φ) :
    KProof (Formula.subst σ '' Γ) (φ.subst σ) := by
…

    Mentions: Arxiv.«1308.0994».Formula, Arxiv.«1308.0994».KProof, Arxiv.«1308.0994».Formula.subst

  9. lemma Arxiv.«1308.0994».KTProof.subst Provability in KT is closed under uniform substitution line 165 source

    Source documentation

    Provability in KT is closed under uniform substitution.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Set, Arxiv.«1308.0994».Formula, Nat, Arxiv.«1308.0994».KTProof, Set.image, Arxiv.«1308.0994».Formula.subst

    Proof uses: Arxiv.«1308.0994».KTProof.rec, Arxiv.«1308.0994».KProof, Arxiv.«1308.0994».KTProof.lift_K, Arxiv.«1308.0994».KProof.subst, Arxiv.«1308.0994».KTProof.axT, Arxiv.«1308.0994».Formula.Imp, Arxiv.«1308.0994».KTProof.mp, EmptyCollection.emptyCollection, Arxiv.«1308.0994».KTProof.nec, Eq.mp, congrFun', congrArg, Set.image_empty

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

    lemma KTProof.subst {Γ φ} (σ : ℕ → Formula) (h : KTProof Γ φ) :
    KTProof (Formula.subst σ '' Γ) (φ.subst σ) := by
…

    Mentions: Arxiv.«1308.0994».Formula, Arxiv.«1308.0994».KTProof, Arxiv.«1308.0994».Formula.subst

  10. structure Arxiv.«1308.0994».NormalModalLogic A “normal modal logic” L is any Set Formula such that: 1 line 181 source

    Source documentation

    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)
    4. If φ ∈ L, then φ.subst σ ∈ L for every substitution σ (Closed under Uniform Substitution)

    no axioms what this means

    structure NormalModalLogic : Type where
…
  11. def Arxiv.«1308.0994».proves line 197 source

    no axioms what this means

    Statement uses: Arxiv.«1308.0994».NormalModalLogic, Arxiv.«1308.0994».Formula

    Proof uses: Membership.mem, Set, Arxiv.«1308.0994».NormalModalLogic.thms

    1 instances, coercions and auxiliary constants left out.

  12. def Arxiv.«1308.0994».KT KT is the specific normal modal logic whose theorems are exactly those provable in KTProof from the empty context line 207 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Arxiv.«1308.0994».NormalModalLogic

    Proof uses: Arxiv.«1308.0994».NormalModalLogic.mk, Set.ofPred, Arxiv.«1308.0994».Formula, Arxiv.«1308.0994».KTProof, EmptyCollection.emptyCollection, Set

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

    Open to load the checked before-and-after goal states.

    def KT : NormalModalLogic := by
…

    Mentions: Arxiv.«1308.0994».NormalModalLogic

  13. theorem Arxiv.«1308.0994».BoxdotConjecture The formal proof was done by Mashu Noguchi et al sorry line 237 source

    Source comment

    The formal proof was done by Mashu Noguchi et al. see linked repo for the full list of contributors

    depends on sorry what this means

    Statement uses: Arxiv.«1308.0994».NormalModalLogic, Arxiv.«1308.0994».Formula, Iff, Arxiv.«1308.0994».proves, Arxiv.«1308.0994».t, Arxiv.«1308.0994».KT, LE.le, Set, Arxiv.«1308.0994».NormalModalLogic.thms

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem BoxdotConjecture (L : NormalModalLogic) (H : ∀ φ, L ⊢ ■ φ ↔ KT ⊢ φ) : L.thms ⊆ KT.thms := by
…

    Mentions: Arxiv.«1308.0994».NormalModalLogic, Arxiv.«1308.0994».KT