Characteristic (Hintikka) formulas for BSML — foundation

[AAY24] [Ant25]

The expressive-completeness converse for BSML (expressiveCompleteness_converse in BSML/ExpressiveCompleteness.lean) needs characteristic formulas: for each world w and depth k, an NE-free formula χ_w^k such that a singleton {v} supports it exactly when v is k-bisimilar to w. This file builds the foundation — finite conjunction over an NE-free language and the depth-0 (atomic type) characterisation — and proves it against the classical single-world evaluation classicalEval (BSML/Bridge.lean).

Working through classicalEval is the simplification that makes this tractable: characteristic formulas are NE-free, so by Bridge.neFree_flat_eq their team support reduces to pointwise classicalEval, and the construction becomes the standard classical modal Hintikka characterisation.

Main declarations

• verum, bigConj — ⊤ (as p ∨ ¬p) and finite conjunction, both NE-free.
• atomicType M w — the depth-0 Hintikka formula: the conjunction of atomic literals true at w.
• classicalEval_atomicType_iff_bisim0 — {v} (classically) satisfies w's atomic type iff v and w are 0-bisimilar (WorldBisim 0).

Todo

• Depth-k+1 Hintikka formula (atomic type ∧ ◇ each successor type ∧ □ disjunction of successor types) and the characterisation classicalEval (charFormula k w) v = true ↔ WorldBisim k M w M v by induction on k. Then lift to team support via Bridge.neFree_flat_eq (currently private; expose it) for the Hennessy-Milner theorem, feeding the normal form that discharges expressiveCompleteness_converse.

⊤ and finite conjunction

def Core.Logic.Modal.BSML.verum {Atom : Type u_2} [Inhabited Atom] : BSMLFormula Atom

⊤ as an NE-free BSML formula: p ∨ ¬p for the default atom. Classically evaluates to true at every world; supported by every team. Requires an atom ([Inhabited Atom]): BSML has no atom-free closed ⊤.

Equations

• Core.Logic.Modal.BSML.verum = (Core.Logic.Modal.BSML.BSMLFormula.atom default).disj (Core.Logic.Modal.BSML.BSMLFormula.atom default).neg

@[simp]

theorem Core.Logic.Modal.BSML.classicalEval_verum {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} [Inhabited Atom] (M : BSMLModel W Atom) (w : W) : classicalEval M verum w = true

@[simp]

theorem Core.Logic.Modal.BSML.isNEFree_verum {Atom : Type u_2} [Inhabited Atom] : verum.isNEFree = true

def Core.Logic.Modal.BSML.bigConj {Atom : Type u_2} [Inhabited Atom] : List (BSMLFormula Atom) → BSMLFormula Atom

Finite conjunction of a list of formulas; the empty conjunction is ⊤.

Equations

• Core.Logic.Modal.BSML.bigConj [] = Core.Logic.Modal.BSML.verum
• Core.Logic.Modal.BSML.bigConj (φ :: rest) = φ.conj (Core.Logic.Modal.BSML.bigConj rest)

theorem Core.Logic.Modal.BSML.classicalEval_bigConj {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} [Inhabited Atom] (M : BSMLModel W Atom) (w : W) (l : List (BSMLFormula Atom)) : classicalEval M (bigConj l) w = true ↔ ∀ φ ∈ l, classicalEval M φ w = true

theorem Core.Logic.Modal.BSML.isNEFree_bigConj {Atom : Type u_2} [Inhabited Atom] (l : List (BSMLFormula Atom)) (h : ∀ φ ∈ l, φ.isNEFree = true) : (bigConj l).isNEFree = true

Atomic type (depth-0 Hintikka formula)

noncomputable def Core.Logic.Modal.BSML.atomicType {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : BSMLModel W Atom) (w : W) : BSMLFormula Atom

The atomic type of w: the conjunction over all atoms p of the literal p (when w ⊨ p) or ¬p (when w ⊭ p). The depth-0 characteristic formula.

Equations

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

theorem Core.Logic.Modal.BSML.isNEFree_atomicType {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : BSMLModel W Atom) (w : W) : (atomicType M w).isNEFree = true

theorem Core.Logic.Modal.BSML.classicalEval_atomicType {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : BSMLModel W Atom) (w v : W) : classicalEval M (atomicType M w) v = true ↔ ∀ (p : Atom), M.val p v = M.val p w

The atomic type of w is classically satisfied at v exactly when v and w assign every atom the same value.

theorem Core.Logic.Modal.BSML.classicalEval_atomicType_iff_bisim0 {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : BSMLModel W Atom) (w v : W) : classicalEval M (atomicType M w) v = true ↔ WorldBisim 0 M w M v

Depth-0 characterisation: w's atomic type is classically satisfied at v iff v and w are 0-bisimilar. The base case of the characteristic- formula characterisation.