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.
• charFormula M k w — the depth-k Hintikka formula: atomic type, ◇ of each successor type, and □ of the successor-type disjunction.
• classicalEval_charFormula_iff_bisim — the characterisation: v classically satisfies χ_w^k iff w and v are k-bisimilar.
• support_charFormula_singleton_iff_bisim — the team-semantic face: singleton support of χ_w^k is k-bisimilarity.

Todo

• Team characteristic formulas (θ_s^k = ⋁_{w ∈ s} (χ_w^k ∧ NE), Definition 3.10 of [AAY24]) and the convex, union-closed normal form that discharges expressiveCompleteness_converse.

⊤ and finite conjunction

def BSML.verum {Atom : Type u_2} [Inhabited Atom] : Formula 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

• BSML.verum = (BSML.Formula.atom default).disj (BSML.Formula.atom default).neg

@[simp]

theorem BSML.classicalEval_verum {W : Type u_1} {Atom : Type u_2} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) : classicalEval M verum w = true

@[simp]

theorem BSML.neFree_verum {Atom : Type u_2} [Inhabited Atom] : verum.NEFree

def BSML.bigConj {Atom : Type u_2} [Inhabited Atom] : List (Formula Atom) → Formula Atom

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

Equations

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

theorem BSML.classicalEval_bigConj {W : Type u_1} {Atom : Type u_2} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) (l : List (Formula Atom)) : classicalEval M (bigConj l) w = true ↔ ∀ φ ∈ l, classicalEval M φ w = true

theorem BSML.neFree_bigConj {Atom : Type u_2} [Inhabited Atom] (l : List (Formula Atom)) (h : ∀ φ ∈ l, φ.NEFree) : (bigConj l).NEFree

Atomic type (depth-0 Hintikka formula)

noncomputable def BSML.atomicType {W : Type u_1} {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) : Formula 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

• BSML.atomicType M w = BSML.bigConj (List.map (fun (p : Atom) => if M.val p w = true then BSML.Formula.atom p else (BSML.Formula.atom p).neg) Finset.univ.toList)

theorem BSML.neFree_atomicType {W : Type u_1} {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) : (atomicType M w).NEFree

theorem BSML.classicalEval_atomicType {W : Type u_1} {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel 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 BSML.classicalEval_atomicType_iff_bisim0 {W : Type u_1} {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w v : W) : classicalEval M (atomicType M w) v = true ↔ ModalLogic.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.

⊥ and finite disjunction

def BSML.falsum {Atom : Type u_2} [Inhabited Atom] : Formula Atom

⊥ as an NE-free BSML formula: p ∧ ¬p for the default atom. Classically false at every world.

Equations

• BSML.falsum = (BSML.Formula.atom default).conj (BSML.Formula.atom default).neg

@[simp]

theorem BSML.classicalEval_falsum {W : Type u_1} {Atom : Type u_2} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) : classicalEval M falsum w = false

@[simp]

theorem BSML.neFree_falsum {Atom : Type u_2} [Inhabited Atom] : falsum.NEFree

def BSML.bigDisj {Atom : Type u_2} [Inhabited Atom] : List (Formula Atom) → Formula Atom

Finite disjunction of a list of formulas; the empty disjunction is ⊥.

Equations

• BSML.bigDisj [] = BSML.falsum
• BSML.bigDisj (φ :: rest) = φ.disj (BSML.bigDisj rest)

theorem BSML.classicalEval_bigDisj {W : Type u_1} {Atom : Type u_2} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) (l : List (Formula Atom)) : classicalEval M (bigDisj l) w = true ↔ ∃ φ ∈ l, classicalEval M φ w = true

theorem BSML.neFree_bigDisj {Atom : Type u_2} [Inhabited Atom] (l : List (Formula Atom)) (h : ∀ φ ∈ l, φ.NEFree) : (bigDisj l).NEFree

Modal clauses of classical evaluation

theorem BSML.classicalEval_poss_iff {W : Type u_1} {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (ψ : Formula Atom) (w : W) : classicalEval M ψ.poss w = true ↔ ∃ v ∈ M.access w, classicalEval M ψ v = true

theorem BSML.classicalEval_nec_iff {W : Type u_1} {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (ψ : Formula Atom) (w : W) : classicalEval M ψ.nec w = true ↔ ∀ v ∈ M.access w, classicalEval M ψ v = true

Characteristic formulas

noncomputable def BSML.charFormula {W : Type u_1} {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) : ℕ → W → Formula Atom

The depth-k characteristic (Hintikka) formula of w: at depth 0 the atomic type; at depth k + 1 the atomic type, conjoined with ◇χ_v^k for each R-successor v and with □ of the disjunction of the successor types.

Equations

• One or more equations did not get rendered due to their size.
• BSML.charFormula M 0 x✝ = BSML.atomicType M x✝

theorem BSML.neFree_charFormula {W : Type u_1} {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (k : ℕ) (w : W) : (charFormula M k w).NEFree

theorem BSML.classicalEval_charFormula_iff_bisim {W : Type u_1} {Atom : Type u_2} [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (k : ℕ) (w v : W) : classicalEval M (charFormula M k w) v = true ↔ ModalLogic.WorldBisim k M w M v

Depth-k characterisation (the Hintikka half of Theorem 3.3 of [AAY24]): w's depth-k characteristic formula is classically satisfied at v iff w and v are k-bisimilar.

Team support of the auxiliary connectives

theorem BSML.support_verum {W : Type u_1} {Atom : Type u_2} [DecidableEq W] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (t : Finset W) : support M verum t

theorem BSML.support_bigConj_iff {W : Type u_1} {Atom : Type u_2} [DecidableEq W] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (l : List (Formula Atom)) (t : Finset W) : support M (bigConj l) t ↔ ∀ φ ∈ l, support M φ t

theorem BSML.support_charDisj_iff {W : Type u_1} {Atom : Type u_2} [DecidableEq W] [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (k : ℕ) (S t : Finset W) : support M (bigDisj (List.map (charFormula M k) S.toList)) t ↔ ∀ v ∈ t, ∃ w ∈ S, ModalLogic.WorldBisim k M w M v

Team support of a flat disjunction of characteristic formulas: every world of the team is k-bisimilar to some representative in S.

theorem BSML.support_charFormula_singleton_iff_bisim {W : Type u_1} {Atom : Type u_2} [DecidableEq W] [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (k : ℕ) (w v : W) : support M (charFormula M k w) {v} ↔ ModalLogic.WorldBisim k M w M v

On singleton teams, support of the characteristic formula is exactly k-bisimilarity — the team-semantic face of the characterisation, via the NE-free classical collapse.