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 Language.monadicWithConstants.
• eval, support, antiSupport: bilateral evaluation.
• ModalStructure.IsStateBased, ModalStructure.IsIndisputable: frame conditions via s↓.

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.

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 (some 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 (some 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).

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 a a_1) = fp a a_1
• QBSML.Formula.mapAtoms fp fc (QBSML.Formula.predc a a_1) = fc a a_1
• QBSML.Formula.mapAtoms fp fc QBSML.Formula.ne = QBSML.Formula.ne
• QBSML.Formula.mapAtoms fp fc a.neg = (QBSML.Formula.mapAtoms fp fc a).neg
• QBSML.Formula.mapAtoms fp fc (a.conj a_1) = (QBSML.Formula.mapAtoms fp fc a).conj (QBSML.Formula.mapAtoms fp fc a_1)
• QBSML.Formula.mapAtoms fp fc (a.disj a_1) = (QBSML.Formula.mapAtoms fp fc a).disj (QBSML.Formula.mapAtoms fp fc a_1)
• QBSML.Formula.mapAtoms fp fc a.poss = (QBSML.Formula.mapAtoms fp fc a).poss
• QBSML.Formula.mapAtoms fp fc (QBSML.Formula.exi a a_1) = QBSML.Formula.exi a (QBSML.Formula.mapAtoms fp fc a_1)
• QBSML.Formula.mapAtoms fp fc (QBSML.Formula.univ a a_1) = QBSML.Formula.univ a (QBSML.Formula.mapAtoms fp fc a_1)

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.monadicWithConstants Const Pred).ModalStructure W Domain

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) => FirstOrder.Language.monadicWithConstantsStructure (κ w) (V w) }

@[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) 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) 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.pred P x_3) x✝ = ∀ i ∈ x✝, ∃ (d : Domain), i.assign x_3 = some d ∧ FirstOrder.Language.ModalStructure.relInterp₁ M P i.world d
• QBSML.eval M false (QBSML.Formula.pred P x_3) x✝ = ∀ i ∈ x✝, ∃ (d : Domain), i.assign x_3 = some d ∧ ¬FirstOrder.Language.ModalStructure.relInterp₁ M P i.world d
• QBSML.eval M true (QBSML.Formula.predc P c) x✝ = ∀ i ∈ x✝, FirstOrder.Language.ModalStructure.relInterp₁ M P i.world (FirstOrder.Language.ModalStructure.constInterp M c i.world)
• QBSML.eval M false (QBSML.Formula.predc P c) x✝ = ∀ i ∈ x✝, ¬FirstOrder.Language.ModalStructure.relInterp₁ M P i.world (FirstOrder.Language.ModalStructure.constInterp M c i.world)
• QBSML.eval M true QBSML.Formula.ne x✝ = x✝.Nonempty
• 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 true (φ.disj ψ) x✝ = ∃ (t₁ : Finset (QBSML.Index W Var Domain)) (t₂ : Finset (QBSML.Index W Var Domain)), Team.splitsAs x✝ t₁ t₂ ∧ QBSML.eval M true φ t₁ ∧ 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 ψ.poss x✝ = ∀ i ∈ x✝, ∃ X ⊆ M.access i.world, X.Nonempty ∧ QBSML.eval M true ψ (QBSML.State.modalLift X i.assign)
• QBSML.eval M false ψ.poss x✝ = ∀ i ∈ x✝, QBSML.eval M false ψ (QBSML.State.modalLift (M.access i.world) i.assign)
• QBSML.eval M true (QBSML.Formula.univ x_3 ψ) x✝ = QBSML.eval M true ψ (QBSML.State.extendUniversal x✝ x_3)
• QBSML.eval M false (QBSML.Formula.univ x_3 ψ) x✝ = ∃ (h : QBSML.Index W Var Domain → Finset Domain), (∀ i ∈ x✝, (h i).Nonempty) ∧ QBSML.eval M false ψ (QBSML.State.extendFunctional x✝ x_3 h)
• QBSML.eval M true (QBSML.Formula.exi x_3 ψ) x✝ = ∃ (h : QBSML.Index W Var Domain → Finset Domain), (∀ i ∈ x✝, (h i).Nonempty) ∧ QBSML.eval M true ψ (QBSML.State.extendFunctional x✝ x_3 h)
• QBSML.eval M false (QBSML.Formula.exi x_3 ψ) x✝ = QBSML.eval M false ψ (QBSML.State.extendUniversal x✝ x_3)

@[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

theorem 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 : Model W Domain Const Pred) : Bilateral.IsBilateral (support M) (antiSupport M) Formula.neg

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

Frame conditions via the world projection

def FirstOrder.Language.ModalStructure.IsStateBased {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] (M : QBSML.Model W Domain Const Pred) (s : Finset (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 Team.IsStateBased applied to State.worldProj s, sharing BSML's frame-condition substrate.

Equations

• FirstOrder.Language.ModalStructure.IsStateBased M s = Team.IsStateBased M.access (QBSML.State.worldProj s)

def FirstOrder.Language.ModalStructure.IsIndisputable {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] (M : QBSML.Model W Domain Const Pred) (s : Finset (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.ModalStructure.IsIndisputable M s = Team.IsIndisputable M.access (QBSML.State.worldProj s)

@[instance_reducible]

instance 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 : Model W Domain Const Pred) (s : Finset (Index W Var Domain)) : Decidable (FirstOrder.Language.ModalStructure.IsStateBased M s)

Equations

• QBSML.instDecidableIsStateBasedOfFintype M s = id inferInstance

@[instance_reducible]

instance 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 : Model W Domain Const Pred) (s : Finset (Index W Var Domain)) : Decidable (FirstOrder.Language.ModalStructure.IsIndisputable M s)

Equations

• QBSML.instDecidableIsIndisputableOfFintype M s = id inferInstance