Quantified bilateral state-based modal logic (QBSML)

QBSML ([AvO23]) is the first-order extension of BSML ([Alo22], [Ant21]). A formula is evaluated bilaterally — supported or anti-supported — at a state: a finite set of indices ⟨w, g⟩ pairing a world with a partial variable assignment. Quantifiers are interpreted by extending states, disjunction by splitting them, and the non-emptiness atom NE — the only source of non-classical behaviour — by state non-emptiness.

Main definitions

• Index, State.worldProj: indices ⟨w, g⟩ and the world projection s↓.
• State.extendIndividual, State.extendUniversal, State.extendFunctional: the state extensions s[x/d], s[x], s[x/h].
• State.modalLift: a set of worlds, paired with one assignment.
• Formula: the formula language; Formula.nec is the derived □; Formula.NEFree the NE-free fragment.
• Model, Model.ofMonadic: models, as ModalStructures over the monadic signature with constants (Language.monadic Pred)[[Const]].
• eval, support, antiSupport: bilateral evaluation.

Implementation notes

• The paper takes □ primitive and derives ◇; we invert this, so eval's poss clauses match the paper's derived ◇-clauses.
• The paper's requirement that all indices of a state share an assignment domain is not enforced at the type level; the state operations preserve it.
• Each eval clause is an operation on team properties applied to the support sets of the subformulas: the propositional and modal clauses are those of Team/Operations.lean (Team.flat, Team.tensor, Team.ne), the quantifier clauses State.univ and State.exi below. The closure inductions of QBSML/Properties.lean are folds over their lemmas.

Indices

@[reducible, inline]

abbrev 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ᵢ⟩), with gᵢ a PartialAssign.

Equations

• QBSML.Index W Var Domain = (W × PartialAssign Var Domain)

@[reducible, inline]

abbrev 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 QBSML.Index.assign {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} (i : Index W Var Domain) : PartialAssign Var Domain

The assignment component of an index.

Equations

• i.assign = i.2

def 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 ↑d)

@[simp]

theorem 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 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 ↑d

The world projection

def 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

• QBSML.State.worldProj s = Finset.image QBSML.Index.world s

@[simp]

theorem 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 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 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 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

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

def 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

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

def 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

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

Membership characterisations

@[simp]

theorem 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 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 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 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 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 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 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 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 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 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 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 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 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 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 (Logic/Team/QBSML/FreeChoice.lean).

The quantifier clauses as operations on team properties

The universal-extension clause is the preimage of a property along s ↦ s[x], and the functional-extension clause asks for some functional, non-empty on the state, whose extension lies in the property. These are the operations the quantifier cases of the closure inductions in QBSML/Properties.lean consume, beside those of Team/Operations.lean. Union closure of the functional clause needs downward closure of the property, which is why QBSML's union closure is confined to the NE-free fragment.

def QBSML.State.extendUniversalHom {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (x : Var) : SupBotHom (Finset (Index W Var Domain)) (Finset (Index W Var Domain))

Universal extension s ↦ s[x] as a map of the bounded join-semilattice of states.

Equations

• QBSML.State.extendUniversalHom x = { toFun := fun (s : Finset (QBSML.Index W Var Domain)) => QBSML.State.extendUniversal s x, map_sup' := ⋯, map_bot' := ⋯ }

@[simp]

theorem QBSML.State.extendUniversalHom_apply {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (x : Var) (s : Finset (Index W Var Domain)) : (extendUniversalHom x) s = extendUniversal s x

def QBSML.State.univ {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (x : Var) (P : Team.TeamProperty (Index W Var Domain)) : Team.TeamProperty (Index W Var Domain)

The universal-extension clause: s[x] ∈ P.

Equations

• QBSML.State.univ x P = ⇑(QBSML.State.extendUniversalHom x) ⁻¹' P

def QBSML.State.exi {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] (x : Var) (P : Team.TeamProperty (Index W Var Domain)) : Team.TeamProperty (Index W Var Domain)

The functional-extension clause: s[x/h] ∈ P for some h non-empty on s.

Equations

• QBSML.State.exi x P = {s : Finset (QBSML.Index W Var Domain) | ∃ (h : QBSML.Index W Var Domain → Finset Domain), (∀ i ∈ s, (h i).Nonempty) ∧ QBSML.State.extendFunctional s x h ∈ P}

@[simp]

theorem QBSML.State.mem_univ {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} {s : Finset (Index W Var Domain)} [Fintype Domain] : s ∈ univ x P ↔ extendUniversal s x ∈ P

@[simp]

theorem QBSML.State.mem_exi {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} {s : Finset (Index W Var Domain)} : s ∈ exi x P ↔ ∃ (h : Index W Var Domain → Finset Domain), (∀ i ∈ s, (h i).Nonempty) ∧ extendFunctional s x h ∈ P

theorem QBSML.State.isLowerSet_univ {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} [Fintype Domain] (hP : IsLowerSet P) : IsLowerSet (univ x P)

theorem QBSML.State.supClosed_univ {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} [Fintype Domain] (hP : SupClosed P) : SupClosed (univ x P)

theorem QBSML.State.empty_mem_univ {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} [Fintype Domain] (hP : ∅ ∈ P) : ∅ ∈ univ x P

theorem QBSML.State.isLowerSet_exi {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} (hP : IsLowerSet P) : IsLowerSet (exi x P)

theorem QBSML.State.supClosed_exi {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} (hP : IsLowerSet P) (hP' : SupClosed P) : SupClosed (exi x P)

Union closure of the functional clause needs downward closure of P: the two functionals are merged with s's taking precedence, so the merged extension of s ∪ t is the union of s's extension with the extension of t \ s, a subteam of t's.

theorem QBSML.State.empty_mem_exi {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] {x : Var} {P : Team.TeamProperty (Index W Var Domain)} (hP : ∅ ∈ P) : ∅ ∈ exi x P

Modal pairing

def 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 : PartialAssign 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

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

@[simp]

theorem 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 : PartialAssign Var Domain} {i : Index W Var Domain} : i ∈ modalLift X g ↔ i.world ∈ X ∧ i.assign = g

@[simp]

theorem 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 : PartialAssign Var Domain) : modalLift {w} g = {(w, g)}

@[simp]

theorem 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 : PartialAssign Var Domain) : worldProj (modalLift X g) = X

theorem 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 : PartialAssign 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 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 : PartialAssign Var Domain} (h : s ⊆ modalLift X g) : worldProj s ⊆ X

The formula language

inductive QBSML.Formula (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 Formula.nec.

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

  Monadic predicate applied to a variable.

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

  Monadic predicate applied to an individual constant.

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

  Non-emptiness atom: state is non-empty.

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

  Bilateral negation: swap support/anti-support.

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

  Conjunction.

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

  Split (tensor) disjunction.

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

  Possibility modal.

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

  Existential quantifier.

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

  Universal quantifier.

def QBSML.instReprFormula.repr {Var✝ : Type u_6} {Const✝ : Type u_7} {Pred✝ : Type u_8} [Repr Var✝] [Repr Const✝] [Repr Pred✝] : Formula Var✝ Const✝ Pred✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• QBSML.instReprFormula.repr QBSML.Formula.ne prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QBSML.Formula.ne")).group prec✝

@[instance_reducible]

instance QBSML.instReprFormula {Var✝ : Type u_6} {Const✝ : Type u_7} {Pred✝ : Type u_8} [Repr Var✝] [Repr Const✝] [Repr Pred✝] : Repr (Formula Var✝ Const✝ Pred✝)

Equations

• QBSML.instReprFormula = { reprPrec := QBSML.instReprFormula.repr }

def QBSML.Formula.nec {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (φ : Formula Var Const Pred) : Formula 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 QBSML.Formula.NEFree {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} : Formula 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 Logic/Team/QBSML/Properties.lean.

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

theorem QBSML.Formula.NEFree.nec {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} {φ : Formula Var Const Pred} (h : φ.NEFree) : φ.nec.NEFree

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

Atom substitution

def QBSML.Formula.mapAtoms {Var : Type u_2} {Const : Type u_4} {Pred : Type u_5} (fp : Pred → Var → Formula Var Const Pred) (fc : Pred → Const → Formula Var Const Pred) : Formula Var Const Pred → Formula 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 Logic/Team/QBSML/Properties.lean), so each such operation — e.g. [Yan23]'s reinterpretation function in Studies/Yan2023.lean — needs only its two atom lemmas.

Equations

• QBSML.Formula.mapAtoms fp fc (QBSML.Formula.pred P x_1) = fp P x_1
• QBSML.Formula.mapAtoms fp fc (QBSML.Formula.predc P c) = fc P c
• QBSML.Formula.mapAtoms fp fc QBSML.Formula.ne = QBSML.Formula.ne
• QBSML.Formula.mapAtoms fp fc φ.neg = (QBSML.Formula.mapAtoms fp fc φ).neg
• QBSML.Formula.mapAtoms fp fc (φ.conj ψ) = (QBSML.Formula.mapAtoms fp fc φ).conj (QBSML.Formula.mapAtoms fp fc ψ)
• QBSML.Formula.mapAtoms fp fc (φ.disj ψ) = (QBSML.Formula.mapAtoms fp fc φ).disj (QBSML.Formula.mapAtoms fp fc ψ)
• QBSML.Formula.mapAtoms fp fc φ.poss = (QBSML.Formula.mapAtoms fp fc φ).poss
• QBSML.Formula.mapAtoms fp fc (QBSML.Formula.exi x_1 φ) = QBSML.Formula.exi x_1 (QBSML.Formula.mapAtoms fp fc φ)
• QBSML.Formula.mapAtoms fp fc (QBSML.Formula.univ x_1 φ) = QBSML.Formula.univ x_1 (QBSML.Formula.mapAtoms fp fc φ)

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

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

Models

@[reducible, inline]

abbrev QBSML.Model (W : Type u_6) (Domain : Type u_7) (Const : Type u_8) (Pred : Type u_9) : Type (max (max (max u_6 u_7) u_8) 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 with constants: accessibility R plus the world-indexed interpretation I, carried as a family of mathlib structures (FirstOrder.Language.ModalStructure) — true by construction, not by bridge.

Equations

• QBSML.Model W Domain Const Pred = ((FirstOrder.Language.monadic Pred).withConstants Const).ModalStructure W Domain

@[reducible, inline]

abbrev QBSML.predSymb {Const : Type u_4} {Pred : Type u_5} (P : Pred) : ((FirstOrder.Language.monadic Pred).withConstants Const).Relations 1

The unary relation symbol of the predicate P.

Equations

• QBSML.predSymb P = Sum.inl P

def QBSML.Model.ofMonadic {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) : Model W Domain Const Pred

The QBSML model with accessibility access, constant interpretation κ, and valuation V.

Equations

• QBSML.Model.ofMonadic access κ V = { access := access, interp := fun (w : W) => inferInstance }

@[simp]

theorem QBSML.predInterp_ofMonadic {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) : FirstOrder.Language.ModalStructure.relInterp₁ (Model.ofMonadic access κ V) (predSymb P) w d ↔ V w P d

@[simp]

theorem QBSML.constInterp_ofMonadic {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) : FirstOrder.Language.ModalStructure.constInterp (Model.ofMonadic access κ V) ((FirstOrder.Language.monadic Pred).con c) w = κ w c

Bilateral evaluation

def 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 : Model W Domain Const Pred) : Bool → Formula 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.
• QBSML.eval M true QBSML.Formula.ne x✝ = (x✝ ∈ Team.ne)
• QBSML.eval M false QBSML.Formula.ne x✝ = (x✝ ∈ {∅})
• QBSML.eval M true ψ.neg x✝ = QBSML.eval M false ψ x✝
• QBSML.eval M false ψ.neg x✝ = QBSML.eval M true ψ x✝
• QBSML.eval M true (φ.conj ψ) x✝ = (QBSML.eval M true φ x✝ ∧ QBSML.eval M true ψ x✝)
• QBSML.eval M false (φ.conj ψ) x✝ = (x✝ ∈ Team.tensor {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M false φ t} {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M false ψ t})
• QBSML.eval M true (φ.disj ψ) x✝ = (x✝ ∈ Team.tensor {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M true φ t} {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M true ψ t})
• QBSML.eval M false (φ.disj ψ) x✝ = (QBSML.eval M false φ x✝ ∧ QBSML.eval M false ψ x✝)
• QBSML.eval M true (QBSML.Formula.univ x_3 ψ) x✝ = (x✝ ∈ QBSML.State.univ x_3 {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M true ψ t})
• QBSML.eval M false (QBSML.Formula.univ x_3 ψ) x✝ = (x✝ ∈ QBSML.State.exi x_3 {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M false ψ t})
• QBSML.eval M true (QBSML.Formula.exi x_3 ψ) x✝ = (x✝ ∈ QBSML.State.exi x_3 {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M true ψ t})
• QBSML.eval M false (QBSML.Formula.exi x_3 ψ) x✝ = (x✝ ∈ QBSML.State.univ x_3 {t : Finset (QBSML.Index W Var Domain) | QBSML.eval M false ψ t})

@[reducible, inline]

abbrev 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 : Model W Domain Const Pred) (φ : Formula Var Const Pred) (s : Finset (Index W Var Domain)) : Prop

Support: positive evaluation.

Equations

• QBSML.support M φ s = QBSML.eval M true φ s

@[reducible, inline]

abbrev 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 : Model W Domain Const Pred) (φ : Formula Var Const Pred) (s : Finset (Index W Var Domain)) : Prop

Anti-support: negative evaluation.

Equations

• QBSML.antiSupport M φ s = QBSML.eval M false φ s

@[simp]

theorem 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 : Model W Domain Const Pred) (φ : Formula Var Const Pred) (s : Finset (Index W Var Domain)) : support M φ.neg s ↔ antiSupport M φ s

@[simp]

theorem 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 : Model W Domain Const Pred) (φ : Formula Var Const Pred) (s : Finset (Index W Var Domain)) : antiSupport M φ.neg s ↔ support M φ s