Hybrid logic

Stream: Is there code for X?

[Lars Ericson]

Would there be any appetite to include hybrid logic in mathlib? Not sure if it would go in Logic proper or somewhere else. I cooked up a short version of it:

import Mathlib.Logic.Basic

-- Define the basic types for hybrid logic
inductive World : Type
| mk : Nat → World

-- HybridPropositions in hybrid logic
inductive HybridProp : Type
| atom : String → HybridProp
| nom : World → HybridProp
| neg : HybridProp → HybridProp
| and : HybridProp → HybridProp → HybridProp
| or : HybridProp → HybridProp → HybridProp
| impl : HybridProp → HybridProp → HybridProp
| box : HybridProp → HybridProp
| diamond : HybridProp → HybridProp
| at : World → HybridProp → HybridProp
| downarrow : (World → HybridProp) → HybridProp

-- Notation for easier reading
notation "~" p => HybridProp.neg p
notation p "∧" q => HybridProp.and p q
notation p "∨" q => HybridProp.or p q
notation p "→" q => HybridProp.impl p q
notation "□" p => HybridProp.box p
notation "◇" p => HybridProp.diamond p
notation "@" w p => HybridProp.at w p
notation "↓" f => HybridProp.downarrow f

-- Define the model for hybrid logic
structure Model where
  worlds : Set World
  valuation : String → Set World
  relation : World → World → Prop

-- Define satisfaction relation
def satisfies : Model → World → HybridProp → Prop
| m, w, HybridProp.atom p => w ∈ m.valuation p
| _, w, HybridProp.nom v => w = v
| m, w, HybridProp.neg p => ¬(satisfies m w p)
| m, w, HybridProp.and p q => (satisfies m w p) ∧ (satisfies m w q)
| m, w, HybridProp.or p q => (satisfies m w p) ∨ (satisfies m w q)
| m, w, HybridProp.impl p q => (satisfies m w p) → (satisfies m w q)
| m, w, HybridProp.box p => ∀ v, m.relation w v → satisfies m v p
| m, w, HybridProp.diamond p => ∃ v, m.relation w v ∧ satisfies m v p
| m, _, HybridProp.at v p => satisfies m v p  -- Use explicit constructor here
| m, w, HybridProp.downarrow f => satisfies m w (f w)

-- Define axioms and lemmas for hybrid logic reasoning

-- Axiom: If we are in world `i` and we can reach `j`, then `@i φ → @j φ` for any formula φ
axiom at_implies (m : Model) (i j : World) (φ : HybridProp) :
  m.relation i j → satisfies m i (HybridProp.at i φ → HybridProp.at j φ)

-- Axiom: If `@i ◇j` holds, then `@i ◇@j i`
axiom diamond_at (m : Model) (i j : World) :
  satisfies m i (HybridProp.diamond (HybridProp.nom j)) →
  satisfies m i (HybridProp.diamond (HybridProp.at j (HybridProp.nom i)))

-- Axiom: If `@i ◇@j i` holds, then `◇@j i`
axiom diamond_at_elim (m : Model) (i j : World) :
  satisfies m i (HybridProp.diamond (HybridProp.at j (HybridProp.nom i))) →
  satisfies m i (HybridProp.diamond (HybridProp.at j (HybridProp.nom i)))

-- Now define the theorem and prove it
theorem hybrid_logic_theorem (m : Model) (i j : World) :
  satisfies m i (HybridProp.at i (HybridProp.diamond (HybridProp.nom j)) →
    HybridProp.diamond (HybridProp.at j (HybridProp.nom i))) := by
  -- Unfold the implication
  intros h
  -- Apply the diamond_at axiom to get `@i ◇@j i`
  have h1 := diamond_at m i j h
  -- Apply the diamond_at_elim axiom to get `◇@j i`
  exact diamond_at_elim m i j h1

Then I found a bachelor's thesis which goes into more depth with Lean implementation on github.

Hybrid and modal logics have decision procedures for model checking which could also be coded in Lean. Modal logic is used for circuit checking. Hybrid logic has potential uses for explainable AI. It is an interesting area which seems to be a natural application for Lean.

[Kim Morrison]

We don't use axioms in Mathlib, so you would need a "deeper" embedding.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I'd say the embedding is 'deep' enough since there is an inductive type of formulas and a notion of model, it's just that the notion of model is not restrictive enough to make the axioms provable (and they should be provable, I'm guessing, with a correct notion of model); in fact they are false:

def badModel : Model where
  worlds := Set.univ
  valuation p := if p == "p" then {World.mk 0} else ∅
  relation := fun ⟨i⟩ ⟨j⟩ => i < j

example : False := by
  have : ¬satisfies badModel ⟨0⟩ (HybridProp.at ⟨0⟩ (.atom "p") → HybridProp.at ⟨1⟩ (.atom "p")) := by
    intro h
    simp [satisfies, badModel] at h
  exact this (at_implies badModel ⟨0⟩ ⟨1⟩ _ (by simp [badModel]))

[Lars Ericson]

To look at badModel I thought of trying to look at Andrei-Alexandru Oltean's Lean implementation in Github using the Lean 4 web editor. This implementation follows a 1998 paper by Blackburn and Tzakova. The initial fragment from that I tried was

import Std.Logic
open Classical

theorem test (a b : Nat) : a = b → a + 1 = b + 1 := by intro h; simp [h]

def TypeIff (a : Type u) (b : Type v) := Prod (a → b) (b → a)
def TypeIff.intro (a : Type u) (b : Type v) : (a → b) → (b → a) → (TypeIff a b) := by
  apply Prod.mk
def TypeIff.mp  (p : TypeIff a b) : a → b := p.1
def TypeIff.mpr (p : TypeIff a b) : b → a := p.2

theorem TypeIff.refl : TypeIff a a := by
  apply TypeIff.intro <;> (intro; assumption)

This breaks in 2 ways:

• It doesn't like import Std.Logic
• Removing that line, it doesn't like TypeIff.Refl saying

type of theorem 'TypeIff.refl' is not a proposition
  {a : Type u_1} → TypeIff a a

Am I looking at Lean 3 or has Lean 4 moved enough since 10 months ago that this doesn't work any more? Note: I'm happy to move this to "new members" if it is a better discussion there. Not to re-invent the wheel I want to get Oltean's code to work in the Lean 4 Web and then try to understand the badModel example in that implementation. Any help on the error would be greatly appreciated.

[Ruben Van de Velde]

Note that the repository declares what version of lean it works with: https://github.com/alexoltean61/hybrid_logic_lean/blob/main/lean-toolchain

[Lars Ericson]

OK about 1 1/2 years ago, which is a long time in Lean 4. I will linearize the .lean files and see if I can get them going on Lean 4 web, and then look at the badModel example after that.

[Malvin Gattinger]

I'm interested in this too, and in modal logic in general :wave:

Do you have a specific reason to work in the online editor and not in the whole repository?

Edit: I now noticed that the project has no license file. Maybe @Alex Oltean could add that or otherwise clarify if reusing and republishing the code is fine? If so, I can share a copy of the repo updated with some sorrys added to at least compile until the bottom of the Truth.lean file which I guess should be enough to translate badModel to the Model type there?

[Lars Ericson]

I am working in the online editor because for short codes it is easier than figuring out how to download Lean to my Ubuntu PC and keep it up to date. For the first issue above where Lean didn't like

theorem TypeIff.refl : TypeIff a a := by
  apply TypeIff.intro <;> (intro; assumption)

the fix is to change theorem to def:

def TypeIff.refl : TypeIff a a := by
  apply TypeIff.intro <;> (intro; assumption)

I guess in Lean 4 of 1.5 years ago, theorem and def were synonyms, and now theorem more strictly expects a prop.

For context on this , my PhD thesis advisor at NYU was Bud Mishra. Bud got his PhD thesis under Ed Clarke at CMU. He and Ed applied model checking on temporal logic propositions to validate electrical circuits. Bud is now interested in applying hybrid logic to check assertions about signalling chains in biology. So same idea but different application domain. We would like to use Lean as the setting for this. A subgoal is then have a correct implementation of hybrid logic in Lean. I assumed that since @Alex Oltean put the GitHub and thesis out there, that it is open source and fair use to build on, but having a license for his code would add certainty.

[Kim Morrison]

Really, setting up Lean is much less work than linearising a few files in the web editor!

[Lars Ericson]

Thanks @Kim Morrison I will give it a try. I am out of my comfort zone when I see lakefiles and toolchains and mathlibs and standard libs and so on. It is less demanding for small amounts of code to just drop the code into the web editor because no installation or understanding of the Lean system build process is required.

For this task, for Hybrid/Util.lean, a small number of tweaks are needed to get today's Lean 4 happy with the code. I had to change a few theorems to defs and make one def be noncomputable:

-- Updated to latest Lean 4 from https://github.com/alexoltean61/hybrid_logic_lean/tree/main/Hybrid/Util.lean

import Mathlib.Data.Set.Basic
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Countable.Basic
import Mathlib.Logic.Equiv.List

open Classical

theorem test (a b : Nat) : a = b → a + 1 = b + 1 := by intro h; simp [h]

def TypeIff (a : Type u) (b : Type v) := Prod (a → b) (b → a)

def TypeIff.intro (a : Type u) (b : Type v) : (a → b) → (b → a) → (TypeIff a b) := by
  apply Prod.mk

def TypeIff.mp  (p : TypeIff a b) : a → b := p.1

def TypeIff.mpr (p : TypeIff a b) : b → a := p.2

def TypeIff.refl : TypeIff a a := by
  apply TypeIff.intro <;> (intro; assumption)

def TypeIff.trans {h1 : TypeIff a b} {h2 : TypeIff b c} : TypeIff a c := by
  apply TypeIff.intro
  . intro h
    exact h2.mp (h1.mp h)
  . intro h
    exact h1.mpr (h2.mpr h)

infix:300 "iff" => TypeIff

noncomputable def choice_intro (q : α → Sort u) (p : α → Prop) (P : ∃ a, p a) : (∀ a, p a → q a) → q P.choose := by
  intro h
  exact (h P.choose P.choose_spec)

theorem eq_symm : (a = b) ↔ (b = a) := by
  apply Iff.intro <;> intro h <;> exact h.symm

@[simp]
theorem double_negation : ¬¬p ↔ p :=
  Iff.intro
  (λ h =>
    Or.elim (Classical.em p)
    (λ hp  => hp)
    (λ hnp => absurd hnp h)
  )
  (λ p => λ np => absurd p np)

@[simp]
theorem implication_disjunction : (p → q) ↔ (¬p ∨ q) := by
  apply Iff.intro
  . intro impl
    exact byCases
      (λ hp  :  p => Or.inr (impl hp))
      (λ hnp : ¬p => Or.inl hnp)
  . intros disj hp
    exact Or.elim disj
      (λ hnp : ¬p => False.elim (hnp hp))
      (λ hq  :  q => hq)

@[simp]
theorem negated_disjunction : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  Iff.intro
    (fun hpq : ¬(p ∨ q) =>
      And.intro
        (fun hp : p =>
          show False from hpq (Or.intro_left q hp)
        )
        (fun hq : q =>
          show False from hpq (Or.intro_right p hq)
        )
    )
    (fun hpq : ¬p ∧ ¬q =>
      (fun disj : p ∨ q =>
        show False from
          Or.elim
           disj
           (fun hp : p => hpq.left hp)
           (fun hq : q => hpq.right hq)
      )
    )

@[simp]
theorem negated_conjunction : ¬(p ∧ q) ↔ ¬p ∨ ¬q := by
  apply Iff.intro
  . intro h
    by_cases hp : p
    . by_cases hq : q
      . exact False.elim (h ⟨hp, hq⟩)
      . apply Or.inr
        assumption
    . apply Or.inl
      assumption
  . intro h
    intro hpq
    apply Or.elim h
    . intro hnp
      exact hnp hpq.left
    . intro hnq
      exact hnq hpq.right

@[simp]
theorem negated_impl : ¬(p → q) ↔ p ∧ ¬q :=
  Iff.intro
    (fun hyp : ¬(p → q) =>
      byCases
      -- case 1 : p
        (fun hp : p =>
          byCases
          -- case 1.a : p and q
            (fun hq : q =>
              ⟨
                hp, show ¬q from (fun _ => show False from hyp (fun _ => hq))
              ⟩
            )
          -- case 1.b : p and non q
            (fun hnq : ¬q => ⟨hp, hnq⟩)
        )
      -- case 2 : non p
        (fun hnp : ¬p => show (p ∧ ¬q) from False.elim
          (show False from hyp
            (show (p → q) from fun p : p =>
              (show q from False.elim (hnp p))
            )
          )
        )
    )
    (fun hyp : p ∧ ¬ q =>
      fun impl : p → q =>
        absurd (impl hyp.left) hyp.right
    )



universe u
@[simp]
theorem negated_universal {α : Type u} {p : α → Prop} : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
    Iff.intro
    (fun h1 : ¬ ∀ x, p x =>
      byContradiction
      (fun hcon1 : ¬ ∃ x, ¬ p x =>
        have neg_h1 := (fun a : α =>
          byContradiction
          (fun hcon2 : ¬ p a => show False from hcon1 (⟨a, hcon2⟩))
        )
        show False from h1 neg_h1
      )
    )
    (fun h2 : ∃ x, ¬ p x =>
      (fun hxp : ∀ x, p x =>
        match h2 with
        | ⟨w, hw⟩ => show False from hw (hxp w)
      )
    )

@[simp]
theorem negated_existential {α : Type u} {p : α → Prop} : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
    Iff.intro
    (fun h1 : ¬ ∃ x, p x =>
      (fun a : α =>
        fun hpa: p a => show False from h1 ⟨a, hpa⟩
      )
    )
    (fun h2 : ∀ x, ¬ p x =>
      (fun hex : ∃ x, p x =>
        match hex with
        | ⟨w, hw⟩ => show False from (h2 w) hw
      )
    )

@[simp]
theorem conj_comm : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (fun hpq : p ∧ q =>
      ⟨hpq.right, hpq.left⟩
    )
    (fun hqp : q ∧ p =>
      ⟨hqp.right, hqp.left⟩
    )

theorem disj_comm : p ∨ q ↔ q ∨ p :=
  Iff.intro
    (fun hpq : p ∨ q =>
      Or.elim
        hpq
        (fun hp : p => Or.intro_right q hp)
        (fun hq : q => Or.intro_left p hq)
    )
    (fun hqp : q ∨ p =>
      Or.elim
        hqp
        (fun hq : q => Or.intro_right p hq)
        (fun hp : p => Or.intro_left q hp)
    )

theorem contraposition (p q : Prop) : (p → q) ↔ (¬q → ¬p) := by
  apply Iff.intro
  . intro hpq
    intro hnq hp
    exact hnq (hpq hp)
  . intro hnqp
    intro hp
    by_cases c : q
    . exact c
    . exact False.elim ((hnqp c) hp)

[Malvin Gattinger]

I think some of these theorems are already in Mathlib or elsewhere, should not be needed or might even be dangerous to have as they are in the repository or here above. For example, conj_comm is docs#and_comm from Init.Core. And I think it should not be marked with simp because then the simplifier would get into an infinite loop.

@[simp]
theorem conj_comm : p ∧ q ↔ q ∧ p

I assume you already know it, but for others reading this thread maybe: One can find these using apply?:

theorem disj_comm : p ∨ q ↔ q ∨ p := by apply? -- Try this: exact `Or.comm`

[Lars Ericson]

Thanks @Malvin Gattinger. This Utils file was just the first item in the chain when linearizing the package of files into a single text. I will review to remove definitions already in mathlib.

[Lars Ericson]

So using apply? Lean tells me that the bulk of these are redundant:

-- Updated to latest Lean 4 from https://github.com/alexoltean61/hybrid_logic_lean/tree/main/Hybrid/Util.lean

import Mathlib.Data.Set.Basic
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Countable.Basic
import Mathlib.Logic.Equiv.List

open Classical

theorem eq_symm : (a = b) ↔ (b = a) := by exact eq_comm
  -- apply Iff.intro <;> intro h <;> exact h.symm

-- @[simp]
theorem double_negation : ¬¬p ↔ p := by exact Decidable.not_not
/-  Iff.intro
  (λ h =>
    Or.elim (Classical.em p)
    (λ hp  => hp)
    (λ hnp => absurd hnp h)
  )
  (λ p => λ np => absurd p np)-/

-- @[simp]
theorem implication_disjunction : (p → q) ↔ (¬p ∨ q) := by exact Decidable.imp_iff_not_or
/-  apply Iff.intro
  . intro impl
    exact byCases
      (λ hp  :  p => Or.inr (impl hp))
      (λ hnp : ¬p => Or.inl hnp)
  . intros disj hp
    exact Or.elim disj
      (λ hnp : ¬p => False.elim (hnp hp))
      (λ hq  :  q => hq)-/

-- @[simp]
theorem negated_disjunction : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by exact not_or
/-  Iff.intro
    (fun hpq : ¬(p ∨ q) =>
      And.intro
        (fun hp : p =>
          show False from hpq (Or.intro_left q hp)
        )
        (fun hq : q =>
          show False from hpq (Or.intro_right p hq)
        )
    )
    (fun hpq : ¬p ∧ ¬q =>
      (fun disj : p ∨ q =>
        show False from
          Or.elim
           disj
           (fun hp : p => hpq.left hp)
           (fun hq : q => hpq.right hq)
      )
    )-/

-- @[simp]
theorem negated_conjunction : ¬(p ∧ q) ↔ ¬p ∨ ¬q := by exact Decidable.not_and_iff_or_not
/-  apply Iff.intro
  . intro h
    by_cases hp : p
    . by_cases hq : q
      . exact False.elim (h ⟨hp, hq⟩)
      . apply Or.inr
        assumption
    . apply Or.inl
      assumption
  . intro h
    intro hpq
    apply Or.elim h
    . intro hnp
      exact hnp hpq.left
    . intro hnq
      exact hnq hpq.right-/

-- @[simp]
theorem negated_impl : ¬(p → q) ↔ p ∧ ¬q := by exact Decidable.not_imp_iff_and_not
/-  Iff.intro
    (fun hyp : ¬(p → q) =>
      byCases
      -- case 1 : p
        (fun hp : p =>
          byCases
          -- case 1.a : p and q
            (fun hq : q =>
              ⟨
                hp, show ¬q from (fun _ => show False from hyp (fun _ => hq))
              ⟩
            )
          -- case 1.b : p and non q
            (fun hnq : ¬q => ⟨hp, hnq⟩)
        )
      -- case 2 : non p
        (fun hnp : ¬p => show (p ∧ ¬q) from False.elim
          (show False from hyp
            (show (p → q) from fun p : p =>
              (show q from False.elim (hnp p))
            )
          )
        )
    )
    (fun hyp : p ∧ ¬ q =>
      fun impl : p → q =>
        absurd (impl hyp.left) hyp.right
    )-/

-- universe u
-- [simp]
theorem negated_universal {α : Type u} {p : α → Prop} : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := by
  exact Decidable.not_forall
/-    Iff.intro
    (fun h1 : ¬ ∀ x, p x =>
      byContradiction
      (fun hcon1 : ¬ ∃ x, ¬ p x =>
        have neg_h1 := (fun a : α =>
          byContradiction
          (fun hcon2 : ¬ p a => show False from hcon1 (⟨a, hcon2⟩))
        )
        show False from h1 neg_h1
      )
    )
    (fun h2 : ∃ x, ¬ p x =>
      (fun hxp : ∀ x, p x =>
        match h2 with
        | ⟨w, hw⟩ => show False from hw (hxp w)
      )
    )-/

-- @[simp]
theorem negated_existential {α : Type u} {p : α → Prop} : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) := by
  exact not_exists
/-    Iff.intro
    (fun h1 : ¬ ∃ x, p x =>
      (fun a : α =>
        fun hpa: p a => show False from h1 ⟨a, hpa⟩
      )
    )
    (fun h2 : ∀ x, ¬ p x =>
      (fun hex : ∃ x, p x =>
        match hex with
        | ⟨w, hw⟩ => show False from (h2 w) hw
      )
    )-/

-- @[simp]
theorem conj_comm : p ∧ q ↔ q ∧ p := by exact And.comm
/-  Iff.intro
    (fun hpq : p ∧ q =>
      ⟨hpq.right, hpq.left⟩
    )
    (fun hqp : q ∧ p =>
      ⟨hqp.right, hqp.left⟩
    )-/

theorem disj_comm : p ∨ q ↔ q ∨ p := by exact Or.comm
/-  Iff.intro
    (fun hpq : p ∨ q =>
      Or.elim
        hpq
        (fun hp : p => Or.intro_right q hp)
        (fun hq : q => Or.intro_left p hq)
    )
    (fun hqp : q ∨ p =>
      Or.elim
        hqp
        (fun hq : q => Or.intro_right p hq)
        (fun hp : p => Or.intro_left q hp)
    )
-/

theorem contraposition (p q : Prop) : (p → q) ↔ (¬q → ¬p) := by exact Iff.symm Decidable.not_imp_not
/-  apply Iff.intro
  . intro hpq
    intro hnq hp
    exact hnq (hpq hp)
  . intro hnqp
    intro hp
    by_cases c : q
    . exact c
    . exact False.elim ((hnqp c) hp)-/

def TypeIff (a : Type u) (b : Type v) := Prod (a → b) (b → a)

def TypeIff.intro (a : Type u) (b : Type v) : (a → b) → (b → a) → (TypeIff a b) := by
  apply Prod.mk

def TypeIff.mp  (p : TypeIff a b) : a → b := p.1

def TypeIff.mpr (p : TypeIff a b) : b → a := p.2

def TypeIff.refl : TypeIff a a := by exact intro a a (fun a => a) fun a => a
--  apply TypeIff.intro <;> (intro; assumption)

def TypeIff.trans {h1 : TypeIff a b} {h2 : TypeIff b c} : TypeIff a c := by
  -- refine intro a c ?a✝ ?a✝¹ -- suggested by apply?, can't make it work
  apply TypeIff.intro
  . intro h
    exact h2.mp (h1.mp h)
  . intro h
    exact h1.mpr (h2.mpr h)

infix:300 "iff" => TypeIff

noncomputable def choice_intro (q : α → Sort u) (p : α → Prop) (P : ∃ a, p a) : (∀ a, p a → q a) → q P.choose := by
  intro h
  exact (h P.choose P.choose_spec)

For TypeIff.trans, apply? suggested refine intro a c ?a✝ ?a✝¹ but that gave an error

type mismatch
  intro a c ?a
has type
  (c → a) → TypeIff a c : Type (max ?u.2404 ?u.2407)
but is expected to have type
  TypeIff a c : Type (max ?u.2404 ?u.2407)

[Damiano Testa]

You can do TypeIff.trans as

def TypeIff.trans {h1 : TypeIff a b} {h2 : TypeIff b c} : TypeIff a c :=
  intro _ _ (h2.mp ∘ h1.mp) (h1.mpr ∘ h2.mpr)

[Malvin Gattinger]

Ignoring the license issue for now until we get a reply, here is a fork that partly compiles with current Lean https://github.com/m4lvin/hybrid_logic_lean

[Lars Ericson]

Thanks @Malvin Gattinger . Your Form.list_noms is more compact than mine. You do

  def Form.list_noms : (Form N) → List (NOM N)
  | nom  i   => [i]
  | impl φ ψ => (List.merge φ.list_noms ψ.list_noms).dedup -- NOTE: used GE.ge before
  | box φ    => φ.list_noms
  | bind _ φ => φ.list_noms
  | _        => []

for

def Form.list_noms : (Form N) → List (NOM N)
| nom  i   => [i]
| impl φ ψ => (List.merge GE.ge φ.list_noms ψ.list_noms).dedup
| box φ    => φ.list_noms
| bind _ φ => φ.list_noms
| _        => []

My solution (really: Perplexity.AI's, after several iterations) was more verbose:

instance : Ord (NOM S) where
  compare x y := compare x.letter y.letter

def Form.list_noms : (Form N) → List (NOM N)
| nom  i   => [i]
| impl φ ψ => (List.merge φ.list_noms ψ.list_noms (fun (a b : NOM N) => compare a b != .lt)).dedup
| box φ    => φ.list_noms
| bind _ φ => φ.list_noms
| _        => []

[Luigi Massacci]

On the topic of getting this in mathlib, I think you’ll run into the same problems as previous attempts to do so for similar “syntactic structures”, such as lambda calculi and other logical calculi, in that it’s hard to get the generality right (see for example these previous conversations on Zulip) At the same time, it is indeed probably useful to have it be part of a larger project as opposed to languishing on a personal repo. You might have better luck joining the FormalizedFormalLogic project (formerly lean4logic) which already has a bit of modal logic (and a lot of other mathematical logic). You should discuss this with @Palalansoukî and @SnO2WMaN though.

[Lars Ericson]

Thanks @Luigi Massacci. If I read it right, what is in mathlib's Logic folder is the first order logic assumed by Lean itself, and that no other logic would be at home in that folder. The model theory only for that FOL is in separate folder ModelTheory. Other logics like modal, temporal, deontic or hybrid logic can defined by their terms, axioms and rules of inference as Lean types. It seems that once those are defined, proofs and models could be constructed using the Lean language similarly to proofs in FOL. I will read the conversations to try to understand where the hard part is of coding another logic and proving theorems using its rules versus proving theorems in FOL. It's not clear where in Mathlib's hierarchy you would put the logics of the FormalizedFormalLogic github and the Hybrid logic github.

[SnO2WMaN]

@Luigi Massacci @Lars Ericson

Since I was mentioned, I'd like to share my personal option as responsible for formalizing the modal logic side of Formalized Formal Logic (FFL).
I'm also interested in formalizing Hybrid Logic, their semantics and caliculi. And In fact, I'm currently starting to formalize K@ (possibly the weakest hybrid logic system(?)) in my private repository (when success, I'll move to FFL.) If you have more interest, feel free to discuss in FFL's discussions.

[Lars Ericson]

Thanks @SnO2WMaN I look forward to K@. How does that compare to @Alex Oltean's thesis implementation? I am still playing with converting that to latest Lean 4, just as a learning exercise.

[Matthew Fairtlough]

Hey folks this is just to introduce myself, I'm keen to join in with some modal logic formalization and I've posted something about my proposal for developing a specific intuitionistic modal logic on FFL's discussions. Will be interested to know what you think.

[SnO2WMaN]

@Lars Ericson

I've heard from someone familiar with, the system of hybrid logic that @Alex Oltean 's trying to formalize is the most expressive and therefore complex system. K@, I've trying to formalize, is refer to Blackburn & ten Carte 2006, this system have completeness for its semantics, and more, have pure-completeness: (roughly saying, add the axioms defines the property of frames (e.g. reflexivity, irreflexivity: this cannot be defined in standard modal logic, ...) to K@ becomes automatically sound & complete for the class which every frame has these property). My immediate goal is to formalize pure-completeness.

[Lars Ericson]

@SnO2WMaN by K@ do you mean ${\bf K}_{\mathcal H(@)}$ of Blackburn and Cate?

[SnO2WMaN]

yes.

[Lars Ericson]

Which repo in Formalized Formal Logic in Lean is K@ theorem proving and which is model checking? Are both done for K@ or is there remaining work to be done?

[Lars Ericson]

I finished my first pass at linearizing the code in https://github.com/alexoltean61/hybrid_logic_lean as discussed above. I came up with 1384 lines that check in today's Lean 4 and another 3686 lines that either have admits or sorrys or fail the simplifier or are dependent on things which have those issues or which are incomplete proofs. The github is in a frozen archival state. It seems it was a work in progress when it was frozen. I have to go back and read more closely to see where the logic it was aiming to implement lies in the hierarchy that includes K@. If I need this particular logic then it might be more productive to step back and rethink what the implementation should provide in terms of goals of being able to prove theorems and being able to check models. Proving theorems and checking models are two different activities but we can generically say that we want both in the "interface" or implementation specification that we would expect of any logic.

Two attached files give the lines that checked and the lines that were problematic.
Hybrid_checks.lean
Hybrid_problematic.lean

[SnO2WMaN]

Lars Ericson said:

Which repo in Formalized Formal Logic in Lean is K@ theorem proving and which is model checking? Are both done for K@ or is there remaining work to be done?

Currently there's not (it's only in my local pc). When I make a some progress, I let you know.

[Lars Ericson]

When you complete your implementation of ${\bf K}_{\mathcal H(@)}$, where would you like to see it in mathlib?

Suppose you went on to implement ${\bf K}_{\mathcal H(@,\forall)}$ and ${\bf K}_{\mathcal H(@,\downarrow)}$. Would it be possible to implement these so propositions and proofs in ${\bf K}_{\mathcal H(@)}$ could be easily upcasted to ${\bf K}_{\mathcal H(@,\cdot)}$ and expressions that are in ${\bf K}_{\mathcal H(@,\cdot)}$ but also contained in ${\bf K}_{\mathcal H(@)}$ could be easily downcasted? If you had this, would it fit in the same place in mathlib?

Oltean's thesis starts with a notion of hybrid signature $\mathcal L$ and then speaks about ${\mathcal L}(\forall)$-WFFs. Can we translate ${\mathcal L}(\forall)$ into terms of ${\mathcal H}(@,\forall)$ and pick a single consistent notation for hierarchies of hybrid logics?

[SnO2WMaN]

Lars Ericson said:

When you complete your implementation of ${\bf K}_{\mathcal H(@)}$, where would you like to see it in mathlib?

Suppose you went on to implement ${\bf K}_{\mathcal H(@,\forall)}$ and ${\bf K}_{\mathcal H(@,\downarrow)}$. Would it be possible to implement these so propositions and proofs in ${\bf K}_{\mathcal H(@)}$ could be easily upcasted to ${\bf K}_{\mathcal H(@,\cdot)}$ and expressions that are in ${\bf K}_{\mathcal H(@,\cdot)}$ but also contained in ${\bf K}_{\mathcal H(@)}$ could be easily downcasted? If you had this, would it fit in the same place in mathlib?

Oltean's thesis starts with a notion of hybrid signature $\mathcal L$ and then speaks about ${\mathcal L}(\forall)$-WFFs. Can we translate ${\mathcal L}(\forall)$ into terms of ${\mathcal H}(@,\forall)$ and pick a single consistent notation for hierarchies of hybrid logics?

Some people asked about porting mathlib for FFL, so I left the answer. FFL don't have plan to mathlib. The main reason is formalizing logic is strongly depending the way to formalize its representation (formulae, deduction systems, etc.), so it cannot be useful as "library", we think. The discussion / references is below.

https://github.com/orgs/FormalizedFormalLogic/discussions/159#discussion-7458557

[Lars Ericson]

There are many systems of logic, coming with language, proof rules and models and theorems about soundness and completeness. Systems of logic are mathematical structures like everything else in Lean. They are generalizable to the extent that many other structures have been generalized in Lean. Proofs in a logic are mathematical objects that can be upcasted and downcasted in the same way that objects of other mathematical structures in Lean can be coerced. It is more a matter of design and taste rather than infeasibility to use Lean for logics (plural). Maybe the underlying type theory of Lean is technically insufficient to do this. I don't think this is an open question. Someone who knows the type theory should be able to say if Lean can do the job. The task seems like just as much fun as encoding rings, fields, groups and so on in Lean. Given that it is fun, it is also fun to think about where this kind of work would fit in mathlib, given that there doesn't seem to be much in that way up to now.

Here is what Perplexity.AI has to say about the subject (in the absence of any human logicians jumping in):

Based on the information provided, it seems that Lean 4's type theory should be sufficient to express the core elements of hybrid logic, including its language, proof system rules, and model theory. Here are some key points that support this:

1. Lean 4 is based on a dependent type theory (calculus of constructions with inductive types), which provides a very expressive foundation for formalizing logics and their metatheory [1].

2. Lean 4 allows defining custom inductive types, which can be used to represent the syntax of hybrid logic, including nominals, satisfaction operators, and binders [6].

3. The function types in Lean 4 can be used to represent the semantics and model theory of hybrid logic, including Kripke models and assignments [6][8].

4. Lean's proof system, including tactics and automation features, can likely be used to implement proof rules for hybrid logic [5][6].

5. There is precedent for formalizing modal and hybrid logics in theorem provers based on similar type theories. For example, hybrid logic has been formalized in Coq, which uses a similar dependent type theory [11].

6. Lean 4 provides features like sections and variables that can help manage the complexity of formalizing logics and their metatheory [13].

7. The expressive power of Lean 4's type theory should be sufficient to capture the semantics of hybrid logic operators like nominals, satisfaction operators, and binders [1][6].

8. Recent work has successfully formalized aspects of hybrid logic in Lean 4, suggesting its suitability for this task [12].

That said, formalizing the full metatheory of hybrid logic (including completeness proofs, etc.) would likely be a substantial undertaking requiring significant expertise in both hybrid logic and Lean 4. The details of how best to represent certain aspects (e.g., variable binding, model theory) may require some careful design choices.

It's worth noting that while Lean 4 should be theoretically capable of expressing hybrid logic, the practical aspects of such a formalization (e.g., usability, proof automation) would depend on the specific implementation choices and additional libraries/tactics developed to support reasoning in the formalized logic.

Citations:
[1] https://en.wikipedia.org/wiki/Lean_(proof_assistant)
[2] https://www.reddit.com/r/ProgrammingLanguages/comments/1ec4trb/lean4lean_formalizing_the_type_theory_of_lean/
[3] https://en.wikipedia.org/wiki/Calculus_of_constructions
[4] https://www.sciencedirect.com/science/article/pii/S1570868310000479
[5] https://www.sciencedirect.com/science/article/pii/S1570868305000443
[6] https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html
[7] https://en.wikipedia.org/wiki/Hybrid_logic
[8] https://carlosareces.github.io/content/papers/files/logkca07.pdf
[9] https://www.cs.cmu.edu/~rwh/students/reed.pdf
[10] https://arxiv.org/abs/2207.01288
[11] https://carlosareces.github.io/content/papers/files/hml-arecestencate.pdf
[12] https://ilds.ro/2024/01/logic-seminar-talk-formalizing-hybrid-modal-logic-in-lean/
[13] http://anggtwu.net/snarf/https/lean-lang.org/theorem_proving_in_lean4/print.pdf

[Lars Ericson]

For the sorrys and admits in this github, @Alex Oltean discussed on Youtube an area in his translation of Blackburn and Tzakova 1998 where he uses a doubly infinite nominal construction in the proof of Theorem 3.16 that becomes too difficult to carry through in Lean.

This is left as a to-do. Was this construction necessary? Is it in the paper proof? Is there another path through to implement the paper proof that doesn't use this construction or something else that is easier to get through? Maybe someone here has some insight on this. It seems like a fun puzzle to solve which has plenty of context so it is a well posed and circumscribed problem.

[Lars Ericson]

I'm playing with this now. In today's Lean 4, this gets an infinite recursion error on the simp:

  instance : IsTotal (NOM S) GE.ge where
    total := by simp [NOM.le, LE.le, Nat.le_total]

but this works:

instance : IsTotal (NOM S) GE.ge where
  total := λ a => λ b =>
    match Nat.le_total a.letter b.letter with
    | Or.inl h => Or.inr h
    | Or.inr h => Or.inl h