Quantified Bilateral State-based Modal Logic (QBSML) — Core Definitions #
@cite{aloni-vanormondt-2023} @cite{aloni-2022} @cite{anttila-2021}
QBSML is the first-order extension of Aloni's BSML, presented in Aloni & van Ormondt 2023 (J Logic Lang Inf 32:539-567) "Modified Numerals and Split Disjunction: The First-Order Case".
What changes from BSML #
The propositional BSML (Aloni 2022) is recovered when assignments are empty. QBSML extends along three axes:
- Indices replace worlds:
Index = W × Assignment(Aloni & van Ormondt §3, Definition 4.2). A state isFinset Indexrather thanFinset W. - Predicates with variables (no constants for now; monadic predicates sufficient for free-choice scenarios).
- Quantifiers:
∀xand∃xevaluated via state extensions.
What stays the same #
Everything else carries over from BSML:
- Bilateral evaluation (support + anti-support, polarity flip via negation)
- Split disjunction via
Core.Logic.Team.splitsAs - NE atom (
s ≠ ∅) - Pragmatic enrichment recursion (NE conjuncts in each clause; deferred to a follow-up file)
- Frame conditions on accessibility (state-based, indisputable) via the
s↓projection — Aloni & van Ormondt Definition 4.10
The point of this file is substrate validation: QBSML's support should
fit into Core.Logic.Team.flat_iff_downwardClosed_unionClosed_emptyTeam's
shape exactly as BSML's does — same template, different Point type.
Scope #
This file: types, state operations, support relation. No Anttila 2.2.8 proofs
(those go in Properties.lean to validate the substrate). No pragmatic
enrichment (separate Enrichment.lean). No free-choice theorems (separate
study files under Phenomena/FreeChoice/Studies/).
Simplifications vs the paper #
- Monadic predicates only:
pred : Pred → Var → Formula. The paper's generalPⁿ(t₁, ..., tₙ)with arbitrary arity and term language (constants + variables) is more general. Monadic suffices for Universal FC, Distribution, Obviation. Higher arities and constants can be added later; the substrate abstraction doesn't change. - Single fixed domain
D: the paper'sM = ⟨W, D, R, I⟩has D as part of the model. We useDomain : Type*as a parameter on the model and require[Fintype Domain]for the universal extension. Polymorphic + finite. - Predicate interpretation is per-world:
pInterp : Pred → W → Finset Domain— at world w, predicate p picks out a Finset of Domain elements. This is the "rigid" predicate semantics; the paper's slightly more general setup uses an interpretation functionI : (W × Const ∪ Pⁿ) → D ∪ 𝒫(Dⁿ).
An assignment is a partial function from variables to domain values.
Aloni & van Ormondt §4 Definition 4.2: gᵢ : V → D. We use Option D
to represent the partiality.
The paper enforces that all indices in a state share the same domain
(dom(gᵢ) = dom(gⱼ)). We don't enforce this at the type level; instead,
state operations preserve the invariant.
Equations
- Semantics.QBSML.Assignment Var Domain = (Var → Option Domain)
Instances For
An index is a (world, assignment) pair. Aloni & van Ormondt §4 Definition
4.2: i = ⟨wᵢ, gᵢ⟩.
Equations
- Semantics.QBSML.Index W Var Domain = (W × Semantics.QBSML.Assignment Var Domain)
Instances For
The assignment component of an index.
Equations
- i.assign = i.2
Instances For
The "world projection" s↓ of a state of indices: the set of worlds
appearing in some index. Aloni & van Ormondt §4 Definition 4.10:
s↓ := {w | ∃g, (w, g) ∈ s}.
Frame conditions on R (state-based, indisputable) are defined relative
to s↓ rather than s, so QBSML reuses BSML's notions via this
projection.
Equations
- Semantics.QBSML.State.worldProj s = Finset.image Prod.fst s
Instances For
Update an assignment at a single variable: g[x/d](y) = d if y = x,
else g(y).
Equations
- g.update x d y = if y = x then some d else g y
Instances For
DecidableEq on assignments follows from Fintype on the variable space plus DecidableEq on the codomain (Option Domain via Domain).
Equations
- Semantics.QBSML.instDecidableEqAssignment x✝¹ x✝ = decEq x✝¹ x✝
DecidableEq on indices: pair of decidable types.
Equations
- Semantics.QBSML.instDecidableEqIndex = inferInstance
Individual extension s[x/d]: assign x to d in every index.
Aloni & van Ormondt §4 Definition 4.5: s[x/d] := {i[x/d] | i ∈ s}.
Equations
- Semantics.QBSML.State.extendIndividual s x d = Finset.image (fun (i : Semantics.QBSML.Index W Var Domain) => i.update x d) s
Instances For
Universal extension s[x]: extend with every domain value at x.
Aloni & van Ormondt §4 Definition 4.6: s[x] := {i[x/d] | i ∈ s, d ∈ D}.
Requires [Fintype Domain] to range over the entire domain.
Equations
- Semantics.QBSML.State.extendUniversal s x = Finset.univ.biUnion fun (d : Domain) => Semantics.QBSML.State.extendIndividual s x d
Instances For
Functional extension s[x/h]: for each i in s, extend with d's drawn
from h(i) (a non-empty subset of D).
Aloni & van Ormondt §4 Definition 4.7: s[x/h] := {i[x/d] | i ∈ s, d ∈ h(i)}.
Used to interpret existential quantification: ∃x φ iff M, s[x/h] ⊨ φ
for some functional h.
Equations
- Semantics.QBSML.State.extendFunctional s x h = s.biUnion fun (i : Semantics.QBSML.Index W Var Domain) => Finset.image (fun (d : Domain) => i.update x d) (h i)
Instances For
Modal pairing R(wᵢ)[gᵢ]: pair each accessible world with the
assignment of the original index. Used in modal evaluation
(Aloni & van Ormondt §4 Definition 4.9).
Equations
- Semantics.QBSML.State.modalLift X g = Finset.image (fun (v : W) => (v, g)) X
Instances For
Universal extension of empty team is empty.
Functional extension of empty team is empty.
Universal extension is monotone in the team.
Universal extension distributes over union.
Functional extension distributes over union of teams.
Functional extension is monotone in the team (for fixed h).
QBSML formula language (Aloni & van Ormondt §4 Definition 4.1).
Parameterized over variable type Var and predicate type Pred. We use
monadic predicates (Pred → Var → Formula) — sufficient for free-choice
scenarios. Higher arities (Pred → List Var → Formula) and a term
language (constants + variables) can be added without changing the
substrate abstraction.
□ is NOT primitive — defined as □φ := ¬◇¬φ (QBSMLFormula.nec).
- pred
{Var : Type u_1}
{Pred : Type u_2}
: Pred → Var → QBSMLFormula Var Pred
Monadic predicate application.
- ne
{Var : Type u_1}
{Pred : Type u_2}
: QBSMLFormula Var Pred
Non-emptiness atom: state is non-empty.
- neg
{Var : Type u_1}
{Pred : Type u_2}
: QBSMLFormula Var Pred → QBSMLFormula Var Pred
Bilateral negation: swap support/anti-support.
- conj
{Var : Type u_1}
{Pred : Type u_2}
: QBSMLFormula Var Pred → QBSMLFormula Var Pred → QBSMLFormula Var Pred
Conjunction.
- disj
{Var : Type u_1}
{Pred : Type u_2}
: QBSMLFormula Var Pred → QBSMLFormula Var Pred → QBSMLFormula Var Pred
Split (tensor) disjunction.
- poss
{Var : Type u_1}
{Pred : Type u_2}
: QBSMLFormula Var Pred → QBSMLFormula Var Pred
Possibility modal.
- exi
{Var : Type u_1}
{Pred : Type u_2}
: Var → QBSMLFormula Var Pred → QBSMLFormula Var Pred
Existential quantifier.
- univ
{Var : Type u_1}
{Pred : Type u_2}
: Var → QBSMLFormula Var Pred → QBSMLFormula Var Pred
Universal quantifier.
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
□φ := ¬◇¬φ — necessity as an abbreviation, mirroring BSML.
Instances For
A formula is NE-free if it does not contain the NE atom. For NE-free formulas, QBSML reduces to classical first-order modal logic on singleton states (Aloni & van Ormondt analogue of Anttila Proposition 2.2.16).
Equations
- (Semantics.QBSML.QBSMLFormula.pred a a_1).isNEFree = true
- Semantics.QBSML.QBSMLFormula.ne.isNEFree = false
- a.neg.isNEFree = a.isNEFree
- (a.conj a_1).isNEFree = (a.isNEFree && a_1.isNEFree)
- (a.disj a_1).isNEFree = (a.isNEFree && a_1.isNEFree)
- a.poss.isNEFree = a.isNEFree
- (Semantics.QBSML.QBSMLFormula.exi a a_1).isNEFree = a_1.isNEFree
- (Semantics.QBSML.QBSMLFormula.univ a a_1).isNEFree = a_1.isNEFree
Instances For
A QBSML model. Aloni & van Ormondt §4 Definition 4.2: M = ⟨W, D, R, I⟩.
We use Domain : Type* as a parameter and [Fintype Domain] for the
universal extension. The interpretation function is split: accessibility
R : W → Finset W and predicate interpretation
pInterp : Pred → W → Finset Domain.
- access : W → Finset W
Accessibility relation (per-world set of accessible worlds).
- pInterp : Pred → W → Finset Domain
Predicate interpretation: at world
w, predicateppicks out the Finset of domain elements satisfying it.
Instances For
Bilateral evaluation of QBSML formulas. Aloni & van Ormondt §4 Definition 4.9.
eval M true φ s is support (M, s ⊨ φ); eval M false φ s is
anti-support (M, s ⊧ φ). Negation flips polarity, making DNE
definitional.
Key shape: Bool → Form → Finset Index → Prop — exactly the template
Core.Logic.Team.flat_iff_downwardClosed_unionClosed_emptyTeam is
parameterized over (with Point := Index W Var Domain). The substrate
test is whether the property + flatness theorems compose identically
to BSML's.
Equations
- One or more equations did not get rendered due to their size.
- Semantics.QBSML.eval M true (Semantics.QBSML.QBSMLFormula.pred P x_3) x✝ = ∀ i ∈ x✝, ∃ (d : Domain), i.assign x_3 = some d ∧ d ∈ M.pInterp P i.world
- Semantics.QBSML.eval M false (Semantics.QBSML.QBSMLFormula.pred P x_3) x✝ = ∀ i ∈ x✝, ∃ (d : Domain), i.assign x_3 = some d ∧ d ∉ M.pInterp P i.world
- Semantics.QBSML.eval M true Semantics.QBSML.QBSMLFormula.ne x✝ = x✝.Nonempty
- Semantics.QBSML.eval M false Semantics.QBSML.QBSMLFormula.ne x✝ = (x✝ = ∅)
- Semantics.QBSML.eval M true ψ.neg x✝ = Semantics.QBSML.eval M false ψ x✝
- Semantics.QBSML.eval M false ψ.neg x✝ = Semantics.QBSML.eval M true ψ x✝
- Semantics.QBSML.eval M true (φ.conj ψ) x✝ = (Semantics.QBSML.eval M true φ x✝ ∧ Semantics.QBSML.eval M true ψ x✝)
- Semantics.QBSML.eval M false (φ.disj ψ) x✝ = (Semantics.QBSML.eval M false φ x✝ ∧ Semantics.QBSML.eval M false ψ x✝)
- Semantics.QBSML.eval M true ψ.poss x✝ = ∀ i ∈ x✝, ∃ X ⊆ M.access i.world, X.Nonempty ∧ Semantics.QBSML.eval M true ψ (Semantics.QBSML.State.modalLift X i.assign)
- Semantics.QBSML.eval M false ψ.poss x✝ = ∀ i ∈ x✝, Semantics.QBSML.eval M false ψ (Semantics.QBSML.State.modalLift (M.access i.world) i.assign)
- Semantics.QBSML.eval M true (Semantics.QBSML.QBSMLFormula.univ x_3 ψ) x✝ = Semantics.QBSML.eval M true ψ (Semantics.QBSML.State.extendUniversal x✝ x_3)
- Semantics.QBSML.eval M false (Semantics.QBSML.QBSMLFormula.exi x_3 ψ) x✝ = Semantics.QBSML.eval M false ψ (Semantics.QBSML.State.extendUniversal x✝ x_3)
Instances For
Support: positive evaluation.
Equations
- Semantics.QBSML.support M φ s = Semantics.QBSML.eval M true φ s
Instances For
Anti-support: negative evaluation.
Equations
- Semantics.QBSML.antiSupport M φ s = Semantics.QBSML.eval M false φ s
Instances For
QBSML's support and antiSupport form a paraconsistent bilateral
logic (Core.Logic.Bilateral.IsBilateral) under QBSMLFormula.neg.
Same shape as BSML's isBilateral, lifted to Index W Var Domain —
point-polymorphism at work. The of_iff helper resolves the
metavariables that previously required explicit Form/Result
annotations.
QBSML's isStateBased: defined via the s↓ projection composed with
Core.Logic.Team.isStateBased. The same Core function as BSML uses,
just applied to the world-set of the team rather than the team itself.
Aloni & van Ormondt §4 Definition 4.10: R is state-based on (M, s) iff
R(w) = s↓ for all w ∈ s↓. Specialization-via-composition exemplifies
the foundational mathlib pattern: same Core definition, different
instantiation via projection.
Equations
Instances For
QBSML's isIndisputable: same Core function, applied to s↓.