Quantified bilateral state-based modal logic (QBSML)

Core definitions for QBSML, the first-order extension of BSML ([Alo22], [Ant21]) presented in [AvO23]: indices pair a world with a partial assignment, states are finite sets of indices, and the formula language adds predicates and quantifiers, the latter evaluated via state extensions. Bilateral evaluation, split disjunction (via Core.Logic.Team.splitsAs), and the NE atom carry over from BSML; frame conditions are inherited through the world projection s↓, so support fits the Core.Logic.Team.isFlat_iff template at the point type Index W Var Domain exactly as BSML's does at W (see Core/Logic/Modal/QBSML/Properties.lean).

Main declarations

• Assignment, Index: partial variable assignments and world–assignment pairs ([AvO23] Definition 4.2).
• State.extendIndividual, State.extendUniversal, State.extendFunctional: the state extensions s[x/d], s[x], s[x/h] interpreting quantifiers ([AvO23] Definitions 4.5–4.7).
• State.modalLift, State.worldProj: pairing accessible worlds with an assignment, and the world projection s↓.
• QBSMLFormula: the formula language ([AvO23] Definition 4.1), with □ derived as QBSMLFormula.nec.
• QBSMLFormula.IsNEFree: the NE-free fragment.
• monadicLang, monadicStructure: the monadic first-order signature on Const and Pred and its structures, as a mathlib FirstOrder.Language.
• QBSMLModel (an abbreviation for FirstOrder.Language.KripkeStructure over monadicLang), eval, support, antiSupport: bilateral evaluation ([AvO23] Definition 4.9), with the interpretation carried as a world-indexed family of mathlib structures.
• isBilateral: support/antiSupport form a Core.Logic.Bilateral.IsBilateral under QBSMLFormula.neg.
• KripkeStructure.IsStateBased, KripkeStructure.IsIndisputable: frame conditions via s↓ ([AvO23] Definition 4.10).

Implementation notes

• Predicates are monadic and the paper's terms t := c | x appear as the two atom constructors pred (variable) and predc (constant), so there is no separate term type: [AvO23] interprets Pⁿ(t₁ … tₙ) for arbitrary arity; higher arities can be added without changing the substrate abstraction.
• The paper's domain D (part of M = ⟨W, D, R, I⟩) is a Domain : Type* parameter, with [Fintype Domain] where the universal extension must range over all of it. The interpretation I is a world-indexed family of mathlib first-order structures: QBSMLModel is FirstOrder.Language.KripkeStructure over the monadic signature, and KripkeStructure.pInterp / KripkeStructure.cInterp read the world-dependent (non-rigid) predicate and constant denotations off Structure.RelMap / Structure.funMap.
• The paper requires all indices in a state to share an assignment domain (dom gᵢ = dom gⱼ); this is not enforced at the type level — the state operations preserve it.
• □ is not primitive: the paper takes □ primitive and derives ◇; we invert this, so eval's poss clauses match the paper's derived ◇-clauses and QBSMLFormula.nec matches its primitive □.

Assignments and indices

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.Assignment (Var : Type u_4) (Domain : Type u_5) : Type (max u_4 u_5)

A partial assignment of domain values to variables ([AvO23] Definition 4.2: gᵢ : V → D); Option D represents the partiality.

Equations

• Core.Logic.Modal.QBSML.Assignment Var Domain = (Var → Option Domain)

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.Index (W : Type u_4) (Var : Type u_5) (Domain : Type u_6) : Type (max u_4 u_6 u_5)

An index is a (world, assignment) pair ([AvO23] Definition 4.2: i = ⟨wᵢ, gᵢ⟩).

Equations

• Core.Logic.Modal.QBSML.Index W Var Domain = (W × Core.Logic.Modal.QBSML.Assignment Var Domain)

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.Index.world {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} (i : Index W Var Domain) : W

The world component of an index.

Equations

• i.world = i.1

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.Index.assign {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} (i : Index W Var Domain) : Assignment Var Domain

The assignment component of an index.

Equations

• i.assign = i.2

def Core.Logic.Modal.QBSML.Assignment.update {Var : Type u_2} {Domain : Type u_3} [DecidableEq Var] (g : Assignment Var Domain) (x : Var) (d : Domain) : Assignment Var Domain

Update an assignment at a single variable: g[x/d](y) = d if y = x, else g(y).

Equations

• g.update x d = Function.update g x (some d)

def Core.Logic.Modal.QBSML.Index.update {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq Var] (i : Index W Var Domain) (x : Var) (d : Domain) : Index W Var Domain

Update an index's assignment ([AvO23] Definitions 4.3–4.4: i[x/d] := ⟨wᵢ, gᵢ[x/d]⟩, with the assignment update gᵢ[x/d] as mathlib's Function.update).

Equations

• i.update x d = (i.world, Function.update i.assign x (some d))

@[simp]

theorem Core.Logic.Modal.QBSML.Index.world_update {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq Var] (i : Index W Var Domain) (x : Var) (d : Domain) : (i.update x d).world = i.world

@[simp]

theorem Core.Logic.Modal.QBSML.Index.assign_update {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq Var] (i : Index W Var Domain) (x : Var) (d : Domain) : (i.update x d).assign = Function.update i.assign x (some d)

The world projection

def Core.Logic.Modal.QBSML.State.worldProj {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] (s : Finset (Index W Var Domain)) : Finset W

The world projection s↓ of a state of indices: the set of worlds appearing in some index ([AvO23] Definition 4.10: s↓ := {w | ∃g, (w, g) ∈ s}). Frame conditions on accessibility are stated relative to s↓, so QBSML reuses BSML's notions via this projection.

Equations

• Core.Logic.Modal.QBSML.State.worldProj s = Finset.image Core.Logic.Modal.QBSML.Index.world s

@[simp]

theorem Core.Logic.Modal.QBSML.State.mem_worldProj {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] {s : Finset (Index W Var Domain)} {w : W} : w ∈ worldProj s ↔ ∃ i ∈ s, i.world = w

theorem Core.Logic.Modal.QBSML.State.worldProj_mono {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] {s t : Finset (Index W Var Domain)} (h : s ⊆ t) : worldProj s ⊆ worldProj t

theorem Core.Logic.Modal.QBSML.State.worldProj_nonempty {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] {s : Finset (Index W Var Domain)} (h : s.Nonempty) : (worldProj s).Nonempty

State extensions

def Core.Logic.Modal.QBSML.State.extendIndividual {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] (s : Finset (Index W Var Domain)) (x : Var) (d : Domain) : Finset (Index W Var Domain)

Individual extension s[x/d]: assign x to d in every index ([AvO23] Definition 4.5: s[x/d] := {i[x/d] | i ∈ s}).

Equations

• Core.Logic.Modal.QBSML.State.extendIndividual s x d = Finset.image (fun (i : Core.Logic.Modal.QBSML.Index W Var Domain) => i.update x d) s

def Core.Logic.Modal.QBSML.State.extendUniversal {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (s : Finset (Index W Var Domain)) (x : Var) : Finset (Index W Var Domain)

Universal extension s[x]: extend with every domain value at x ([AvO23] Definition 4.6: s[x] := {i[x/d] | i ∈ s, d ∈ D}). Requires [Fintype Domain] to range over the entire domain.

Equations

• Core.Logic.Modal.QBSML.State.extendUniversal s x = Finset.univ.biUnion fun (d : Domain) => Core.Logic.Modal.QBSML.State.extendIndividual s x d

def Core.Logic.Modal.QBSML.State.extendFunctional {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] (s : Finset (Index W Var Domain)) (x : Var) (h : Index W Var Domain → Finset Domain) : Finset (Index W Var Domain)

Functional extension s[x/h]: for each i ∈ s, extend with values drawn from h i ([AvO23] Definition 4.7: s[x/h] := {i[x/d] | i ∈ s, d ∈ h(i)}). Interprets existential quantification: ∃x φ iff M, s[x/h] ⊨ φ for some functional h.

Equations

• Core.Logic.Modal.QBSML.State.extendFunctional s x h = s.biUnion fun (i : Core.Logic.Modal.QBSML.Index W Var Domain) => Finset.image (fun (d : Domain) => i.update x d) (h i)

Membership characterisations

@[simp]

theorem Core.Logic.Modal.QBSML.State.mem_extendIndividual {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {s : Finset (Index W Var Domain)} {x : Var} {d : Domain} {j : Index W Var Domain} : j ∈ extendIndividual s x d ↔ ∃ i ∈ s, i.update x d = j

@[simp]

theorem Core.Logic.Modal.QBSML.State.mem_extendUniversal {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {s : Finset (Index W Var Domain)} {x : Var} {j : Index W Var Domain} : j ∈ extendUniversal s x ↔ ∃ (d : Domain), ∃ i ∈ s, i.update x d = j

@[simp]

theorem Core.Logic.Modal.QBSML.State.mem_extendFunctional {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {s : Finset (Index W Var Domain)} {x : Var} {h : Index W Var Domain → Finset Domain} {j : Index W Var Domain} : j ∈ extendFunctional s x h ↔ ∃ i ∈ s, ∃ d ∈ h i, i.update x d = j

Extension algebra

theorem Core.Logic.Modal.QBSML.State.extendIndividual_empty {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] (x : Var) (d : Domain) : extendIndividual ∅ x d = ∅

theorem Core.Logic.Modal.QBSML.State.extendIndividual_union {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] (s t : Finset (Index W Var Domain)) (x : Var) (d : Domain) : extendIndividual (s ∪ t) x d = extendIndividual s x d ∪ extendIndividual t x d

theorem Core.Logic.Modal.QBSML.State.extendIndividual_mono {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {s t : Finset (Index W Var Domain)} (x : Var) (d : Domain) (hsub : s ⊆ t) : extendIndividual s x d ⊆ extendIndividual t x d

theorem Core.Logic.Modal.QBSML.State.extendUniversal_empty {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (x : Var) : extendUniversal ∅ x = ∅

theorem Core.Logic.Modal.QBSML.State.extendUniversal_union {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (s t : Finset (Index W Var Domain)) (x : Var) : extendUniversal (s ∪ t) x = extendUniversal s x ∪ extendUniversal t x

theorem Core.Logic.Modal.QBSML.State.extendUniversal_mono {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {s t : Finset (Index W Var Domain)} (x : Var) (hsub : s ⊆ t) : extendUniversal s x ⊆ extendUniversal t x

theorem Core.Logic.Modal.QBSML.State.extendFunctional_empty {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] (x : Var) (h : Index W Var Domain → Finset Domain) : extendFunctional ∅ x h = ∅

theorem Core.Logic.Modal.QBSML.State.extendFunctional_union {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] (s t : Finset (Index W Var Domain)) (x : Var) (h : Index W Var Domain → Finset Domain) : extendFunctional (s ∪ t) x h = extendFunctional s x h ∪ extendFunctional t x h

theorem Core.Logic.Modal.QBSML.State.extendFunctional_mono {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {s t : Finset (Index W Var Domain)} (x : Var) (h : Index W Var Domain → Finset Domain) (hsub : s ⊆ t) : extendFunctional s x h ⊆ extendFunctional t x h

theorem Core.Logic.Modal.QBSML.State.extendUniversal_eq_extendFunctional {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (s : Finset (Index W Var Domain)) (x : Var) : extendUniversal s x = extendFunctional s x fun (x : Index W Var Domain) => Finset.univ

The universal extension is the functional extension with the constant full-domain functional.

theorem Core.Logic.Modal.QBSML.State.extendFunctional_filter_of_update_mem {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {s t : Finset (Index W Var Domain)} {x : Var} (hpar : ∀ j ∈ t, ∃ i ∈ s, ∃ (d : Domain), i.update x d = j) : (extendFunctional s x fun (i : Index W Var Domain) => {d : Domain | i.update x d ∈ t}) = t

Witness reconstruction: a state t consisting of x-updates of indices of s is recovered exactly as the functional extension of s by the functional collecting, at each index, the values whose updates land in t. The shared Finset surgery behind the existential-witness steps of the free-choice facts (Core/Logic/Modal/QBSML/FreeChoice.lean).

Modal pairing

def Core.Logic.Modal.QBSML.State.modalLift {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [Fintype Var] [DecidableEq Domain] (X : Finset W) (g : Assignment Var Domain) : Finset (Index W Var Domain)

Modal pairing R(wᵢ)[gᵢ]: pair each accessible world with the assignment of the original index. Used in modal evaluation ([AvO23] Definition 4.9).

Equations

• Core.Logic.Modal.QBSML.State.modalLift X g = Finset.image (fun (v : W) => (v, g)) X

@[simp]

theorem Core.Logic.Modal.QBSML.State.mem_modalLift {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [Fintype Var] [DecidableEq Domain] {X : Finset W} {g : Assignment Var Domain} {i : Index W Var Domain} : i ∈ modalLift X g ↔ i.world ∈ X ∧ i.assign = g

@[simp]

theorem Core.Logic.Modal.QBSML.State.modalLift_singleton {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [Fintype Var] [DecidableEq Domain] (w : W) (g : Assignment Var Domain) : modalLift {w} g = {(w, g)}

@[simp]

theorem Core.Logic.Modal.QBSML.State.worldProj_modalLift {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [Fintype Var] [DecidableEq Domain] (X : Finset W) (g : Assignment Var Domain) : worldProj (modalLift X g) = X

theorem Core.Logic.Modal.QBSML.State.modalLift_worldProj_of_subset {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [Fintype Var] [DecidableEq Domain] {s : Finset (Index W Var Domain)} {X : Finset W} {g : Assignment Var Domain} (h : s ⊆ modalLift X g) : modalLift (worldProj s) g = s

A state contained in a modal pairing is recovered by projecting its worlds and pairing them back with the same assignment: every index of s ⊆ State.modalLift X g carries the assignment g.

theorem Core.Logic.Modal.QBSML.State.worldProj_subset_of_subset_modalLift {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [Fintype Var] [DecidableEq Domain] {s : Finset (Index W Var Domain)} {X : Finset W} {g : Assignment Var Domain} (h : s ⊆ modalLift X g) : worldProj s ⊆ X

The formula language

inductive Core.Logic.Modal.QBSML.QBSMLFormula (Var : Type u_6) (Const : Type u_7) (Pred : Type u_8) : Type (max (max u_6 u_7) u_8)

QBSML formula language ([AvO23] Definition 4.1), parameterized over variable type Var, constant type Const, and (monadic) predicate type Pred. The paper's terms t := c | x appear as the two atom constructors. □ is not primitive — see QBSMLFormula.nec.

• pred {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : Pred → Var → QBSMLFormula Var Const Pred

  Monadic predicate applied to a variable.

• predc {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : Pred → Const → QBSMLFormula Var Const Pred

  Monadic predicate applied to an individual constant.

• ne {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : QBSMLFormula Var Const Pred

  Non-emptiness atom: state is non-empty.

• neg {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

  Bilateral negation: swap support/anti-support.

• conj {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

  Conjunction.

• disj {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

  Split (tensor) disjunction.

• poss {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

  Possibility modal.

• exi {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : Var → QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

  Existential quantifier.

• univ {Var : Type u_6} {Const : Type u_7} {Pred : Type u_8} : Var → QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

  Universal quantifier.

@[implicit_reducible]

instance Core.Logic.Modal.QBSML.instReprQBSMLFormula {Var✝ : Type u_6} {Const✝ : Type u_7} {Pred✝ : Type u_8} [Repr Var✝] [Repr Const✝] [Repr Pred✝] : Repr (QBSMLFormula Var✝ Const✝ Pred✝)

Equations

• Core.Logic.Modal.QBSML.instReprQBSMLFormula = { reprPrec := Core.Logic.Modal.QBSML.instReprQBSMLFormula.repr }

def Core.Logic.Modal.QBSML.instReprQBSMLFormula.repr {Var✝ : Type u_6} {Const✝ : Type u_7} {Pred✝ : Type u_8} [Repr Var✝] [Repr Const✝] [Repr Pred✝] : QBSMLFormula Var✝ Const✝ Pred✝ → ℕ → Std.Format

Equations

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

def Core.Logic.Modal.QBSML.QBSMLFormula.nec {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (φ : QBSMLFormula Var Const Pred) : QBSMLFormula Var Const Pred

Necessity, derived: □φ := ¬◇¬φ. [AvO23] takes □ primitive and ◇ := ¬□¬ derived; we invert this, so eval's poss clauses match the paper's derived ◇-clauses and nec matches its primitive □.

Equations

• φ.nec = φ.neg.poss.neg

inductive Core.Logic.Modal.QBSML.QBSMLFormula.IsNEFree {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} : QBSMLFormula Var Const Pred → Prop

The NE-free fragment: formulas not containing the NE atom. On this fragment QBSML reduces to classical first-order modal logic ([AvO23] analogue of [Ant21] Proposition 2.2.16); see Core/Logic/Modal/QBSML/Properties.lean.

• pred {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (P : Pred) (x : Var) : (QBSMLFormula.pred P x).IsNEFree
• predc {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (P : Pred) (c : Const) : (QBSMLFormula.predc P c).IsNEFree
• neg {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} {φ : QBSMLFormula Var Const Pred} : φ.IsNEFree → φ.neg.IsNEFree
• conj {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} {φ ψ : QBSMLFormula Var Const Pred} : φ.IsNEFree → ψ.IsNEFree → (φ.conj ψ).IsNEFree
• disj {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} {φ ψ : QBSMLFormula Var Const Pred} : φ.IsNEFree → ψ.IsNEFree → (φ.disj ψ).IsNEFree
• poss {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} {φ : QBSMLFormula Var Const Pred} : φ.IsNEFree → φ.poss.IsNEFree
• exi {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (x : Var) {φ : QBSMLFormula Var Const Pred} : φ.IsNEFree → (QBSMLFormula.exi x φ).IsNEFree
• univ {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (x : Var) {φ : QBSMLFormula Var Const Pred} : φ.IsNEFree → (QBSMLFormula.univ x φ).IsNEFree

theorem Core.Logic.Modal.QBSML.QBSMLFormula.IsNEFree.nec {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} {φ : QBSMLFormula Var Const Pred} (h : φ.IsNEFree) : φ.nec.IsNEFree

The derived □φ := ¬◇¬φ preserves NE-freeness.

Atom substitution

def Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (fp : Pred → Var → QBSMLFormula Var Const Pred) (fc : Pred → Const → QBSMLFormula Var Const Pred) : QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

Substitute a formula for each atom, commuting with every connective and quantifier (and fixing NE). The generic congruence machinery for atom-rewriting operations: an atom map whose images are bilaterally equivalent to the atoms is salva veritate (eval_mapAtoms_iff in Core/Logic/Modal/QBSML/Properties.lean), so each such operation — e.g. [Yan23]'s reinterpretation function in Studies/Yan2023.lean — needs only its two atom lemmas.

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc (Core.Logic.Modal.QBSML.QBSMLFormula.pred a a_1) = fp a a_1
• Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc (Core.Logic.Modal.QBSML.QBSMLFormula.predc a a_1) = fc a a_1
• Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc Core.Logic.Modal.QBSML.QBSMLFormula.ne = Core.Logic.Modal.QBSML.QBSMLFormula.ne
• Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a.neg = (Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a).neg
• Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc (a.conj a_1) = (Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a).conj (Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a_1)
• Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc (a.disj a_1) = (Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a).disj (Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a_1)
• Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a.poss = (Core.Logic.Modal.QBSML.QBSMLFormula.mapAtoms fp fc a).poss

theorem Core.Logic.Modal.QBSML.QBSMLFormula.IsNEFree.mapAtoms {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} {fp : Pred → Var → QBSMLFormula Var Const Pred} {fc : Pred → Const → QBSMLFormula Var Const Pred} (hfp : ∀ (P : Pred) (x : Var), (fp P x).IsNEFree) (hfc : ∀ (P : Pred) (c : Const), (fc P c).IsNEFree) {φ : QBSMLFormula Var Const Pred} (h : φ.IsNEFree) : (QBSMLFormula.mapAtoms fp fc φ).IsNEFree

An atom substitution with NE-free images preserves NE-freeness.

The monadic signature and models

def Core.Logic.Modal.QBSML.monadicLang (Const : Type u) (Pred : Type v) : FirstOrder.Language

The monadic signature on Const and Pred: one individual constant per Const, one unary relation symbol per Pred — [AvO23] Definition 4.1's signature (terms t := c | x, monadic relations).

Equations

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

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.monadicConst {Const : Type u_6} {Pred : Type u_7} (c : Const) : (monadicLang Const Pred).Constants

A constant as a symbol of the monadic signature (defeq; the parametric analogue of mathlib's per-symbol abbreviations, cf. Fragments/English/Toy.lean).

Equations

• Core.Logic.Modal.QBSML.monadicConst c = c

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.monadicRel {Const : Type u_6} {Pred : Type u_7} (P : Pred) : (monadicLang Const Pred).Relations 1

A predicate as a relation symbol of the monadic signature (defeq).

Equations

• Core.Logic.Modal.QBSML.monadicRel P = P

@[reducible]

def Core.Logic.Modal.QBSML.monadicStructure {Const : Type u_6} {Pred : Type u_7} {Domain : Type u_8} (κ : Const → Domain) (V : Pred → Domain → Prop) : (monadicLang Const Pred).Structure Domain

The monadicLang Const Pred structure a constant interpretation and a predicate valuation induce.

Equations

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

@[simp]

theorem Core.Logic.Modal.QBSML.monadicStructure_relMap {Const : Type u_6} {Pred : Type u_7} {Domain : Type u_8} (κ : Const → Domain) (V : Pred → Domain → Prop) (P : Pred) (v : Fin 1 → Domain) : FirstOrder.Language.Structure.RelMap (monadicRel P) v ↔ V P (v 0)

@[simp]

theorem Core.Logic.Modal.QBSML.monadicStructure_funMap {Const : Type u_6} {Pred : Type u_7} {Domain : Type u_8} (κ : Const → Domain) (V : Pred → Domain → Prop) (c : Const) (v : Fin 0 → Domain) : FirstOrder.Language.Structure.funMap (monadicConst c) v = κ c

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.QBSMLModel (W : Type u_6) (Domain : Type u_7) (Const : Type u_8) (Pred : Type u_9) : Type (max (max (max u_8 u_6) u_7) u_9)

A QBSML model ([AvO23] Definition 4.2: M = ⟨W, D, R, I⟩) is a constant-domain first-order Kripke structure over the monadic signature: accessibility R plus the world-indexed interpretation I, carried as a family of mathlib structures (FirstOrder.Language.KripkeStructure) — true by construction, not by bridge.

Equations

• Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred = (Core.Logic.Modal.QBSML.monadicLang Const Pred).KripkeStructure W Domain

def FirstOrder.Language.KripkeStructure.pInterp {W : Type u_6} {Domain : Type u_7} {Const : Type u_8} {Pred : Type u_9} (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred) (P : Pred) (w : W) (d : Domain) : Prop

The predicate denotation at a world, read off the model's structure family via Structure.RelMap — the world-relativized I(w)(Pⁿ) of [AvO23] Definition 4.2, specialised to monadic P (cf. Semantics.Composition.Model.pred₁ext).

Equations

• FirstOrder.Language.KripkeStructure.pInterp M P w d = FirstOrder.Language.Structure.RelMap (Core.Logic.Modal.QBSML.monadicRel P) fun (x : Fin 1) => d

def FirstOrder.Language.KripkeStructure.cInterp {W : Type u_6} {Domain : Type u_7} {Const : Type u_8} {Pred : Type u_9} (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred) (c : Const) (w : W) : Domain

The constant denotation at a world — the world-relative I(w)(c) of [AvO23] Definitions 4.2 and 4.8, read off Structure.funMap (cf. Semantics.Composition.Model.const).

Equations

• FirstOrder.Language.KripkeStructure.cInterp M c w = FirstOrder.Language.Structure.funMap (Core.Logic.Modal.QBSML.monadicConst c) default

@[simp]

theorem FirstOrder.Language.KripkeStructure.pInterp_monadicStructure {W : Type u_6} {Domain : Type u_7} {Const : Type u_8} {Pred : Type u_9} (access : W → Finset W) (κ : W → Const → Domain) (V : W → Pred → Domain → Prop) (P : Pred) (w : W) (d : Domain) : { access := access, interp := fun (w : W) => Core.Logic.Modal.QBSML.monadicStructure (κ w) (V w) }.pInterp P w d ↔ V w P d

@[simp]

theorem FirstOrder.Language.KripkeStructure.cInterp_monadicStructure {W : Type u_6} {Domain : Type u_7} {Const : Type u_8} {Pred : Type u_9} (access : W → Finset W) (κ : W → Const → Domain) (V : W → Pred → Domain → Prop) (c : Const) (w : W) : { access := access, interp := fun (w : W) => Core.Logic.Modal.QBSML.monadicStructure (κ w) (V w) }.cInterp c w = κ w c

Bilateral evaluation

def Core.Logic.Modal.QBSML.eval {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) : Bool → QBSMLFormula Var Const Pred → Finset (Index W Var Domain) → Prop

Bilateral evaluation of QBSML formulas ([AvO23] Definition 4.9): eval M true φ s is support (M, s ⊨ φ), eval M false φ s anti-support (M, s ⫤ φ). Negation flips the polarity, making double-negation elimination definitional.

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.Modal.QBSML.eval M true (Core.Logic.Modal.QBSML.QBSMLFormula.pred P x_3) x✝ = ∀ i ∈ x✝, ∃ (d : Domain), i.assign x_3 = some d ∧ FirstOrder.Language.KripkeStructure.pInterp M P i.world d
• Core.Logic.Modal.QBSML.eval M true Core.Logic.Modal.QBSML.QBSMLFormula.ne x✝ = x✝.Nonempty
• Core.Logic.Modal.QBSML.eval M false Core.Logic.Modal.QBSML.QBSMLFormula.ne x✝ = (x✝ = ∅)
• Core.Logic.Modal.QBSML.eval M true ψ.neg x✝ = Core.Logic.Modal.QBSML.eval M false ψ x✝
• Core.Logic.Modal.QBSML.eval M false ψ.neg x✝ = Core.Logic.Modal.QBSML.eval M true ψ x✝
• Core.Logic.Modal.QBSML.eval M true (φ.conj ψ) x✝ = (Core.Logic.Modal.QBSML.eval M true φ x✝ ∧ Core.Logic.Modal.QBSML.eval M true ψ x✝)
• Core.Logic.Modal.QBSML.eval M false (φ.disj ψ) x✝ = (Core.Logic.Modal.QBSML.eval M false φ x✝ ∧ Core.Logic.Modal.QBSML.eval M false ψ x✝)
• Core.Logic.Modal.QBSML.eval M true ψ.poss x✝ = ∀ i ∈ x✝, ∃ X ⊆ M.access i.world, X.Nonempty ∧ Core.Logic.Modal.QBSML.eval M true ψ (Core.Logic.Modal.QBSML.State.modalLift X i.assign)
• Core.Logic.Modal.QBSML.eval M false ψ.poss x✝ = ∀ i ∈ x✝, Core.Logic.Modal.QBSML.eval M false ψ (Core.Logic.Modal.QBSML.State.modalLift (M.access i.world) i.assign)
• Core.Logic.Modal.QBSML.eval M true (Core.Logic.Modal.QBSML.QBSMLFormula.univ x_3 ψ) x✝ = Core.Logic.Modal.QBSML.eval M true ψ (Core.Logic.Modal.QBSML.State.extendUniversal x✝ x_3)
• Core.Logic.Modal.QBSML.eval M false (Core.Logic.Modal.QBSML.QBSMLFormula.exi x_3 ψ) x✝ = Core.Logic.Modal.QBSML.eval M false ψ (Core.Logic.Modal.QBSML.State.extendUniversal x✝ x_3)

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.support {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) : Prop

Support: positive evaluation.

Equations

• Core.Logic.Modal.QBSML.support M φ s = Core.Logic.Modal.QBSML.eval M true φ s

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.antiSupport {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) : Prop

Anti-support: negative evaluation.

Equations

• Core.Logic.Modal.QBSML.antiSupport M φ s = Core.Logic.Modal.QBSML.eval M false φ s

@[simp]

theorem Core.Logic.Modal.QBSML.support_neg {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) : support M φ.neg s ↔ antiSupport M φ s

@[simp]

theorem Core.Logic.Modal.QBSML.antiSupport_neg {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) : antiSupport M φ.neg s ↔ support M φ s

theorem Core.Logic.Modal.QBSML.isBilateral {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) : Bilateral.IsBilateral (support M) (antiSupport M) QBSMLFormula.neg

support and antiSupport form a paraconsistent bilateral logic (Core.Logic.Bilateral.IsBilateral) under QBSMLFormula.neg, like BSML's isBilateral at the point type Index W Var Domain.

Frame conditions via the world projection

def FirstOrder.Language.KripkeStructure.IsStateBased {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred) (s : Finset (Core.Logic.Modal.QBSML.Index W Var Domain)) : Prop

R is state-based on (M, s): every world in s↓ sees exactly s↓ ([AvO23] Definition 4.10). Defined via Core.Logic.Team.IsStateBased applied to State.worldProj s, sharing BSML's frame-condition substrate.

Equations

• FirstOrder.Language.KripkeStructure.IsStateBased M s = Core.Logic.Team.IsStateBased M.access (Core.Logic.Modal.QBSML.State.worldProj s)

def FirstOrder.Language.KripkeStructure.IsIndisputable {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred) (s : Finset (Core.Logic.Modal.QBSML.Index W Var Domain)) : Prop

R is indisputable on (M, s): all worlds in s↓ see the same accessible set ([AvO23] Definition 4.10).

Equations

• FirstOrder.Language.KripkeStructure.IsIndisputable M s = Core.Logic.Team.IsIndisputable M.access (Core.Logic.Modal.QBSML.State.worldProj s)

@[implicit_reducible]

instance Core.Logic.Modal.QBSML.instDecidableIsStateBasedOfFintype {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [Fintype W] (M : QBSMLModel W Domain Const Pred) (s : Finset (Index W Var Domain)) : Decidable (FirstOrder.Language.KripkeStructure.IsStateBased M s)

Equations

• Core.Logic.Modal.QBSML.instDecidableIsStateBasedOfFintype M s = id inferInstance

@[implicit_reducible]

instance Core.Logic.Modal.QBSML.instDecidableIsIndisputableOfFintype {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [Fintype W] (M : QBSMLModel W Domain Const Pred) (s : Finset (Index W Var Domain)) : Decidable (FirstOrder.Language.KripkeStructure.IsIndisputable M s)

Equations

• Core.Logic.Modal.QBSML.instDecidableIsIndisputableOfFintype M s = id inferInstance