Modal Inclusion Logic (MIL)

[AHY24] [Ant25]

Modal inclusion logic ML(⊆) extends classical modal logic with an inclusion atom x⃗ ⊆ y⃗ meaning: for every tuple of x⃗-truth-values realised at some world in the team, the same tuple is realised as a tuple of y⃗-truth-values at some world in the team. Introduced for team semantics by Galliani; the modal variant ML(⊆) is axiomatised in [AHY24] (Archive for Mathematical Logic 2025; arXiv:2312.02285), which is also [Ant25] Chapter 5.

Unlike BSML / MDL, MIL is unilateral: there is only a support relation, no separate anti-support. Negation is restricted to classical sub-formulas and defined by pointwise team-extension of classical Kripke negation. This file follows AHY 2024's exact Definition 2.2 and provides single-polarity eval.

Closure profile

Property	BSML (with NE)	MDL	MIL
IsLowerSet	broken by NE	✓	broken by incl
SupClosed	✓	broken by dep	✓
∅ ∈ support	✓	✓	✓

MIL shares its closure profile cell (— ✓ ✓) with BSML-with-NE and BSMLEmpty — same closure cell, different syntactic mechanism (the inclusion atom rather than NE breaks DC; UC is preserved because two teams that each witness an inclusion provide a superset of witnesses in the union).

Main declarations

• Formula — MIL syntax (AHY 2024 Definition 2.1).
• eval — single-polarity team-semantic evaluation (AHY 2024 Definition 2.2).
• support — alias for eval.
• Formula.modalDepth — depth of nested ◇/□.
• supClosed_support — every MIL formula has sup-closed support (AHY 2024 §2, "Union closure").
• support_empty — every formula is supported on the empty team (AHY 2024 §2, "Empty Team Property").
• not_isLowerSet_incl_of_witness — constructive witness that the inclusion atom breaks downward closure.

Implementation notes

The paper's inclusion atom takes equal-length lists of classical formulas α₁...αₙ ⊆ β₁...βₙ. We simplify to lists of atoms — each pair encoded as (Atom × Atom). This loses some expressive power but matches concrete instances and avoids mutual recursion with a separate classical-formula type.

The paper allows ¬α only when α is a classical formula. We allow neg syntactically over any MIL formula and define its semantics by the same pointwise team-extension as the paper. Under the paper's syntactic restriction this case is unreachable for non-classical sub-formulas; we extend the definition uniformly because team-extended pointwise classical negation is well-defined regardless.

The ◇ clause uses AHY 2024's lax semantics (Definition 2.2): a successor team S must satisfy both S ⊆ R[T] (the reach constraint) and T ⊆ R⁻¹[S] (the back constraint). The paper's footnote 1 notes that with the strict semantics (functional successor selection), MIL would lose union closure. We follow the paper in using lax.

Sibling logics in Core/Logic/Modal/

• Modal/Kripke.lean — the carrier type.
• Modal/Dependence.lean — MDL (Väänänen 2008), bilateral, dep atoms.
• Modal/Inclusion.lean (this file) — MIL, unilateral, inclusion atoms.
• Modal/Independence.lean (future) — modal independence logic.

Todo

• AHY 2024 §3 — expressive completeness and normal forms for MIL.
• AHY 2024 §4 — natural deduction axiomatisation + completeness proof.
• AHY 2024 §5 — the variant logics ML(▽) and ML(▽) (might-operator and singular might-operator). Should each get its own file once the substrate proves itself.
• Bisim invariance for MIL — same shape as BSML's; AHY 2024 §3.1 uses this for the expressive completeness proof.

Syntax (AHY 2024 Definition 2.1)

inductive Core.Logic.Modal.Inclusion.Formula (Atom : Type u_3) : Type u_3

MIL syntax. The paper's α₁...αₙ ⊆ β₁...βₙ is encoded as a list of pairs [(α₁, β₁), ..., (αₙ, βₙ)]. Both ◇ and □ are primitives.

• atom {Atom : Type u_3} (p : Atom) : Formula Atom

  Atomic proposition.

• bot {Atom : Type u_3} : Formula Atom

  Weak contradiction ⊥.

• incl {Atom : Type u_3} (xys : List (Atom × Atom)) : Formula Atom

  Inclusion atom x⃗ ⊆ y⃗.

• neg {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

  Classical negation (restricted to classical formulas in the paper; we allow on any formula for uniform recursion).

• conj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom

  Conjunction.

• disj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom

  Tensor disjunction.

• poss {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

  Possibility modal ◇ (lax semantics).

• nec {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

  Necessity modal □.

@[implicit_reducible]

instance Core.Logic.Modal.Inclusion.instReprFormula {Atom✝ : Type u_3} [Repr Atom✝] : Repr (Formula Atom✝)

Equations

• Core.Logic.Modal.Inclusion.instReprFormula = { reprPrec := Core.Logic.Modal.Inclusion.instReprFormula.repr }

def Core.Logic.Modal.Inclusion.instReprFormula.repr {Atom✝ : Type u_3} [Repr Atom✝] : Formula Atom✝ → ℕ → Std.Format

Equations

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

Semantics (AHY 2024 Definition 2.2)

def Core.Logic.Modal.Inclusion.eval {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) : Formula Atom → Finset W → Prop

Single-polarity team-semantic evaluation.

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.Modal.Inclusion.eval M (Core.Logic.Modal.Inclusion.Formula.atom p) x✝ = ∀ w ∈ x✝, M.val p w = true
• Core.Logic.Modal.Inclusion.eval M Core.Logic.Modal.Inclusion.Formula.bot x✝ = (x✝ = ∅)
• Core.Logic.Modal.Inclusion.eval M (Core.Logic.Modal.Inclusion.Formula.incl xys) x✝ = ∀ w₁ ∈ x✝, ∃ w₂ ∈ x✝, ∀ xy ∈ xys, M.val xy.1 w₁ = true ↔ M.val xy.2 w₂ = true
• Core.Logic.Modal.Inclusion.eval M ψ.neg x✝ = ∀ w ∈ x✝, ¬Core.Logic.Modal.Inclusion.eval M ψ {w}
• Core.Logic.Modal.Inclusion.eval M (ψ₁.conj ψ₂) x✝ = (Core.Logic.Modal.Inclusion.eval M ψ₁ x✝ ∧ Core.Logic.Modal.Inclusion.eval M ψ₂ x✝)
• Core.Logic.Modal.Inclusion.eval M ψ.poss x✝ = ∃ S ⊆ x✝.biUnion M.access, (∀ w ∈ x✝, ∃ s ∈ S, s ∈ M.access w) ∧ Core.Logic.Modal.Inclusion.eval M ψ S
• Core.Logic.Modal.Inclusion.eval M ψ.nec x✝ = Core.Logic.Modal.Inclusion.eval M ψ (x✝.biUnion M.access)

@[reducible, inline]

abbrev Core.Logic.Modal.Inclusion.support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : Prop

Support: alias for eval. MIL is unilateral (no separate anti-support), but the name support is the conventional one in team semantics.

Equations

• Core.Logic.Modal.Inclusion.support M φ t = Core.Logic.Modal.Inclusion.eval M φ t

@[simp]

theorem Core.Logic.Modal.Inclusion.support_atom {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (p : Atom) (t : Finset W) : support M (Formula.atom p) t ↔ ∀ w ∈ t, M.val p w = true

@[simp]

theorem Core.Logic.Modal.Inclusion.support_bot {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (t : Finset W) : support M Formula.bot t ↔ t = ∅

@[simp]

theorem Core.Logic.Modal.Inclusion.support_incl {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (xys : List (Atom × Atom)) (t : Finset W) : support M (Formula.incl xys) t ↔ ∀ w₁ ∈ t, ∃ w₂ ∈ t, ∀ xy ∈ xys, M.val xy.1 w₁ = true ↔ M.val xy.2 w₂ = true

@[simp]

theorem Core.Logic.Modal.Inclusion.support_neg {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : support M φ.neg t ↔ ∀ w ∈ t, ¬support M φ {w}

@[simp]

theorem Core.Logic.Modal.Inclusion.support_conj {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : support M (φ.conj ψ) t ↔ support M φ t ∧ support M ψ t

@[simp]

theorem Core.Logic.Modal.Inclusion.support_disj {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : support M (φ.disj ψ) t ↔ ∃ (t₁ : Finset W) (t₂ : Finset W), Team.splitsAs t t₁ t₂ ∧ support M φ t₁ ∧ support M ψ t₂

@[simp]

theorem Core.Logic.Modal.Inclusion.support_poss {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : support M φ.poss t ↔ ∃ S ⊆ t.biUnion M.access, (∀ w ∈ t, ∃ s ∈ S, s ∈ M.access w) ∧ support M φ S

@[simp]

theorem Core.Logic.Modal.Inclusion.support_nec {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : support M φ.nec t ↔ support M φ (t.biUnion M.access)

Modal depth

def Core.Logic.Modal.Inclusion.Formula.modalDepth {Atom : Type u_2} : Formula Atom → ℕ

Modal depth of a MIL formula.

Equations

• (Core.Logic.Modal.Inclusion.Formula.atom a).modalDepth = 0
• Core.Logic.Modal.Inclusion.Formula.bot.modalDepth = 0
• (Core.Logic.Modal.Inclusion.Formula.incl a).modalDepth = 0
• a.neg.modalDepth = a.modalDepth
• (a.conj a_1).modalDepth = max a.modalDepth a_1.modalDepth
• (a.disj a_1).modalDepth = max a.modalDepth a_1.modalDepth
• a.poss.modalDepth = a.modalDepth + 1
• a.nec.modalDepth = a.modalDepth + 1

Sup-closure: the defining property of the inclusion family

(AHY 2024 §2 — "Union closure: if M, Tᵢ ⊨ φ for all i ∈ I ≠ ∅,
then M, ⋃_{i ∈ I} Tᵢ ⊨ φ") 

theorem Core.Logic.Modal.Inclusion.supClosed_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ : Formula Atom) : SupClosed {t : Finset W | support M φ t}

Every MIL formula has sup-closed support. Single-polarity induction is cleaner than BSML's joint-bilateral form because there's no antiSupport to track.

Empty team property (AHY 2024 §2)

theorem Core.Logic.Modal.Inclusion.support_empty {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) (φ : Formula Atom) : support M φ ∅

Inclusion breaks downward closure (the defining feature)

theorem Core.Logic.Modal.Inclusion.not_isLowerSet_incl_of_witness {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} {a b : Atom} {w₁ w₂ : W} {M : KripkeModel W Atom} (hne : w₁ ≠ w₂) (hpair : M.val a w₁ = true ↔ M.val b w₂ = true) (hself : M.val a w₂ = true ↔ M.val b w₂ = true) (hwit : ¬(M.val a w₁ = true ↔ M.val b w₁ = true)) : ¬IsLowerSet {t : Finset W | support M (Formula.incl [(a, b)]) t}

The inclusion atom breaks downward closure: a constructive counterexample. With two distinct worlds w₁, w₂ where:

• M.val a w₁ = M.val b w₂ (so w₂ witnesses w₁'s a-as-b in {w₁,w₂})
• M.val a w₂ = M.val b w₂ (so w₂ self-witnesses)
• M.val a w₁ ≠ M.val b w₁ (so {w₁} alone fails) the team {w₁, w₂} supports a ⊆ b but the subteam {w₁} does not.

This shows MIL's inclusion atom violates downward closure (the defining negative property of the inclusion family — Anttila Ch 5 contrasts MIL with dependence logic on exactly this axis).

Soundness for the closure cell (Definability bridge)

theorem Core.Logic.Modal.Inclusion.soundFor_unionClosed_inter_empty {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : KripkeModel W Atom) : Team.SoundFor (support M) (Team.unionClosedProperties ∩ Team.emptyTeamProperties)

MIL is sound for its closure cell: every MIL-definable team property is union-closed and has the empty-team property. This is the soundness half of the expressive-completeness theorem for ML(⊆) ([AHY24]; [Ant25] Ch 5 shows ML(⊆) is complete for the union-closed modal properties with the empty-team property, modulo bounded bisimulation).

Composes supClosed_support and support_empty through the Team/Definability.lean bridge — the first consumer of that substrate. The converse (every such property is MIL-definable, via the inclusion normal form) is the open half.