Characteristic formulas for BSML

The world type of depth k of a world, over n atoms enumerated by e, records the truth values of these atoms and, for positive k, the set of depth k - 1 types of the world's successors. Each type has a characteristic (Hintikka) formula, an NE-free formula that holds at a world exactly when the world has that type. Two worlds have the same type exactly when they are k-bisimilar, once e enumerates every atom. The strong Hintikka formula of a set of types T is supported by a team exactly when the types of its worlds are those in T.

Main definitions

• verum, bigConj, bigDisj, bigDisjNE: ⊤ as p ∨ ¬p, finite conjunction and disjunction, and finite disjunction with each disjunct conjoined with NE.
• WorldType n k, worldType e M k w: the world types, and the type of a world.
• hintikka e k τ, strongHintikka e T: the Hintikka formulas of a type and of a set of types.

Main results

• realize_hintikka_iff: the Hintikka formula of τ holds at w iff w has type τ.
• worldType_eq_iff_worldBisim: two worlds have the same type iff they are k-bisimilar.
• realize_hintikka_worldType_iff: the Hintikka formula of w's type holds at w' iff w' is k-bisimilar to w.
• support_strongHintikka_iff: a team supports the strong Hintikka formula of T iff the types of its worlds are those in T.

Implementation notes

[AAY24] Definition 3.2 conjoins the depth k Hintikka formula of the world at depth k + 1; here only its literals are conjoined, which is equivalent and needs no truncation of types.

References

• [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice

⊤ and finite conjunction

def BSML.verum {Atom : Type u_3} [Inhabited Atom] : Formula Atom

The tautology p ∨ ¬p for the default atom is NE-free, true at every world and supported by every team. BSML has no tautology without atoms.

Equations

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

@[simp]

theorem BSML.realize_verum {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) : Realize M verum w

@[simp]

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

def BSML.bigConj {Atom : Type u_3} [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.realize_bigConj {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) (l : List (Formula Atom)) : Realize M (bigConj l) w ↔ ∀ φ ∈ l, Realize M φ w

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

Finite disjunction

@[simp]

theorem BSML.not_realize_falsum {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) : ¬Realize M Formula.falsum w

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

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

Equations

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

theorem BSML.realize_bigDisj {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (w : W) (l : List (Formula Atom)) : Realize M (bigDisj l) w ↔ ∃ φ ∈ l, Realize M φ w

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

theorem BSML.modalDepth_bigConj {Atom : Type u_3} [Inhabited Atom] {L : List (Formula Atom)} {k : ℕ} (hL : ∀ x ∈ L, x.modalDepth ≤ k) : (bigConj L).modalDepth ≤ k

theorem BSML.modalDepth_bigDisj {Atom : Type u_3} [Inhabited Atom] {L : List (Formula Atom)} {k : ℕ} (hL : ∀ x ∈ L, x.modalDepth ≤ k) : (bigDisj L).modalDepth ≤ k

def BSML.bigDisjNE {Atom : Type u_3} [Inhabited Atom] (L : List (Formula Atom)) : Formula Atom

bigDisjNE L is the disjunction of the formulas of L, each conjoined with NE.

Equations

• BSML.bigDisjNE L = BSML.bigDisj (List.map (fun (x : BSML.Formula Atom) => x.conj BSML.Formula.ne) L)

World types

def BSML.WorldType (n : ℕ) : ℕ → Type

A world type of depth k over n atoms gives the truth values of the atoms and, at positive depth, the set of the depth k - 1 types of the successors.

Equations

• BSML.WorldType n 0 = (Fin n → Bool)
• BSML.WorldType n k.succ = ((Fin n → Bool) × Finset (BSML.WorldType n k))

@[instance_reducible]

noncomputable instance BSML.WorldType.instDecidableEq {n : ℕ} (k : ℕ) : DecidableEq (WorldType n k)

Equations

• BSML.WorldType.instDecidableEq k = Classical.decEq (BSML.WorldType n k)

@[instance_reducible]

noncomputable instance BSML.WorldType.instFintype {n : ℕ} (k : ℕ) : Fintype (WorldType n k)

Equations

• BSML.WorldType.instFintype 0 = { elems := BSML.WorldType.instFintype._aux_1, complete := ⋯ }
• BSML.WorldType.instFintype k.succ = instFintypeProd (Fin n → Bool) (Finset (BSML.WorldType n k))

def BSML.WorldType.val {n k : ℕ} : WorldType n k → Fin n → Bool

τ.val gives the truth values of the atoms at the type τ.

Equations

• a.val = a
• τ.val = τ.1

noncomputable def BSML.worldType {W : Type u_1} {Atom : Type u_3} {n : ℕ} (e : Fin n → Atom) (M : ModalLogic.KripkeModel W Atom) (k : ℕ) : W → WorldType n k

worldType e M k w is the type of depth k of the world w, over the atoms enumerated by e.

Equations

• BSML.worldType e M 0 x✝ = fun (i : Fin n) => decide (M.val (e i) x✝)
• BSML.worldType e M k.succ x✝ = (fun (i : Fin n) => decide (M.val (e i) x✝), Finset.image (BSML.worldType e M k) (M.access x✝))

theorem BSML.val_worldType {W : Type u_1} {Atom : Type u_3} {n : ℕ} (e : Fin n → Atom) (M : ModalLogic.KripkeModel W Atom) (k : ℕ) (w : W) : (worldType e M k w).val = fun (i : Fin n) => decide (M.val (e i) w)

Hintikka formulas

def BSML.literal {Atom : Type u_3} {n : ℕ} (e : Fin n → Atom) (i : Fin n) (b : Bool) : Formula Atom

literal e i b is the i-th atom if b holds and its negation otherwise.

Equations

• BSML.literal e i b = if b = true then BSML.Formula.atom (e i) else (BSML.Formula.atom (e i)).neg

def BSML.literals {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) (a : Fin n → Bool) : Formula Atom

literals e a conjoins the literals of the assignment a.

Equations

• BSML.literals e a = BSML.bigConj (List.map (fun (i : Fin n) => BSML.literal e i (a i)) (List.finRange n))

noncomputable def BSML.hintikka {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) (k : ℕ) : WorldType n k → Formula Atom

The Hintikka formula of a type conjoins its literals and, at positive depth, the possibility of each successor type and the necessity of their disjunction.

Equations

• One or more equations did not get rendered due to their size.
• BSML.hintikka e 0 a = BSML.literals e a

noncomputable def BSML.strongHintikka {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) {k : ℕ} (T : Finset (WorldType n k)) : Formula Atom

The strong Hintikka formula of a set of types T is the disjunction of the formulas χ_τ ∧ NE for τ ∈ T.

Equations

• BSML.strongHintikka e T = BSML.bigDisjNE (List.map (BSML.hintikka e k) T.toList)

theorem BSML.neFree_literal {Atom : Type u_3} {n : ℕ} (e : Fin n → Atom) (i : Fin n) (b : Bool) : (literal e i b).NEFree

theorem BSML.neFree_literals {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) (a : Fin n → Bool) : (literals e a).NEFree

theorem BSML.neFree_hintikka {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) (k : ℕ) (τ : WorldType n k) : (hintikka e k τ).NEFree

theorem BSML.modalDepth_literals {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) (a : Fin n → Bool) : (literals e a).modalDepth ≤ 0

theorem BSML.modalDepth_hintikka {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) (k : ℕ) (τ : WorldType n k) : (hintikka e k τ).modalDepth ≤ k

theorem BSML.strongHintikka_empty {Atom : Type u_3} [Inhabited Atom] {n : ℕ} (e : Fin n → Atom) {k : ℕ} : strongHintikka e ∅ = Formula.falsum

Hintikka formulas characterize types

theorem BSML.realize_literal {W : Type u_1} {Atom : Type u_3} {n : ℕ} {e : Fin n → Atom} (M : ModalLogic.KripkeModel W Atom) (i : Fin n) (b : Bool) (w : W) : Realize M (literal e i b) w ↔ decide (M.val (e i) w) = b

theorem BSML.realize_literals {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] {n : ℕ} {e : Fin n → Atom} (M : ModalLogic.KripkeModel W Atom) (a : Fin n → Bool) (w : W) : Realize M (literals e a) w ↔ (fun (i : Fin n) => decide (M.val (e i) w)) = a

theorem BSML.realize_hintikka_iff {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] {n : ℕ} {e : Fin n → Atom} (M : ModalLogic.KripkeModel W Atom) (k : ℕ) (τ : WorldType n k) (w : W) : Realize M (hintikka e k τ) w ↔ worldType e M k w = τ

The Hintikka formula of τ holds at a world exactly when the world has type τ.

theorem BSML.worldType_eq_iff_worldBisim {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {n : ℕ} {e : Fin n → Atom} (he : Function.Surjective e) {M : ModalLogic.KripkeModel W Atom} {M' : ModalLogic.KripkeModel W' Atom} (k : ℕ) (w : W) (w' : W') : worldType e M k w = worldType e M' k w' ↔ ModalLogic.WorldBisim k M w M' w'

Two worlds have the same type exactly when they are k-bisimilar, once e enumerates every atom.

theorem BSML.realize_hintikka_worldType_iff {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} [Inhabited Atom] {n : ℕ} {e : Fin n → Atom} (he : Function.Surjective e) {M : ModalLogic.KripkeModel W Atom} {M' : ModalLogic.KripkeModel W' Atom} (k : ℕ) (w : W) (w' : W') : Realize M' (hintikka e k (worldType e M k w)) w' ↔ ModalLogic.WorldBisim k M w M' w'

The Hintikka formula of the type of w holds at w' exactly when w' is k-bisimilar to w ([AAY24] Theorem 3.3).

Team support

theorem BSML.support_verum {W : Type u_1} {Atom : Type u_3} [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_3} [Inhabited Atom] [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (l : List (Formula Atom)) (t : Finset W) : support M (bigConj l) t ↔ ∀ φ ∈ l, support M φ t

theorem BSML.support_bigDisj_hintikka_iff {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] {n : ℕ} {e : Fin n → Atom} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) {k : ℕ} (L : List (WorldType n k)) (t : Finset W) : support M (bigDisj (List.map (hintikka e k) L)) t ↔ ∀ w ∈ t, worldType e M k w ∈ L

A team supports a disjunction of Hintikka formulas iff each of its worlds has one of their types.

theorem BSML.support_strongHintikka_iff {W : Type u_1} {Atom : Type u_3} [Inhabited Atom] {n : ℕ} {e : Fin n → Atom} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) {k : ℕ} (T : Finset (WorldType n k)) (t : Finset W) : support M (strongHintikka e T) t ↔ Finset.image (worldType e M k) t = T

A team supports the strong Hintikka formula of T exactly when the types of its worlds are those in T ([AAY24] Definition 3.10).