Linglib.Studies.AloniAnttilaYang2024

Formalisation of two extensions of BSML introduced in [AAY24] (Notre Dame J. Formal Logic 65(4), 2024):

BSMLOr — BSML extended with the global disjunction ⨼ (Definition 2.1; written ∨∨ in some sources).
BSMLEmpty — BSML extended with the emptiness operator ⊘ (Definition 2.1).

Both extend BSML's BSMLModel (worlds + accessibility + valuation) and inherit the bilateral support/anti-support semantics. The new connectives are characterised by Fact 2.7 in the paper:

Logic	Has `NE`	Has `⨼`	Downward-closed	Union-closed
BSML	yes	no	when NE-free	always
BSMLOr	yes	yes	when NE-free	when ⨼-free
BSMLEmpty	yes	no	when NE-free	always

The "when NE-free" / "when ⨼-free" entries express Fact 2.7's universal statement uniformly across all three logics — NE is the only obstruction to downward closure; ⨼ is the only obstruction to union closure.

The closure-property classification matches the audit's family-axis insight: each extension occupies a different cell of the (IsLowerSet, SupClosed, ⊥ ∈ ·) profile lattice.

Main declarations #

BSMLOr.Formula / BSMLEmpty.Formula — syntax (Definition 2.1).
BSMLOr.eval / BSMLEmpty.eval — bilateral semantics (Definition 2.3), parametric in polarity.
BSMLOr.support / BSMLOr.antiSupport (and the BSMLEmpty analogues) — convenience abbreviations.
BSMLOr.isBilateral / BSMLEmpty.isBilateral — instances of Core.Logic.Bilateral.IsBilateral, reusing the BSML substrate.
BSMLEmpty.supClosed_support — union-closure of BSML⊘ formulas (Fact 2.7; the second-consumer evidence that BSML's substrate generalises).
BSMLOr.ofBSML / BSMLEmpty.ofBSML — embedding BSMLFormula into each extension, preserving semantics (eval_ofBSML theorems).

Implementation notes #

The paper's BSML includes ⊥ (weak contradiction) as a primitive, whereas linglib's BSMLFormula (Aloni 2022) does not (the original defines ⊥ := p ∧ ¬p). The extension formula types here include ⊥ to match [AAY24]; the embedding BSMLFormula → Formula therefore has no preimage for ⊥.

BSMLOr's global disjunction ⨼ is the team-semantic inquisitive disjunction — the support clause is propositional disjunction at the team level, in contrast to disj's split-existential. Crucially, ⨼ is the only BSML-family connective that breaks union closure (Fact 2.7, proof in [AAY24]).

BSMLEmpty's emptiness operator ⊘φ is supported when s ⊨ φ or s = ∅. It is essentially a restricted ⨼: ⊘φ ≡ φ ⨼ ⊥. But since BSMLEmpty omits ⨼, union closure is preserved.

Todo #

§3.2 Expressive-completeness theorems — BSMLOr is expressively complete for bisimulation-invariant state properties; BSMLEmpty for the union-closed ∩ bisimulation-invariant fragment. The bisim-invariance half is done (Theorem 3.8 above for both BSMLOr and BSMLEmpty); the converse direction requires Hintikka formulas for states (Definition 3.10) and finite atom sets. See [Ant25] Chapter 3.
§4 Natural-deduction axiomatisations for each of BSML, BSMLOr, BSMLEmpty. Soundness + completeness theorems; [Ant25] Chapter 4 has the updated proofs.
Free-choice prediction theorem: state the narrow-scope FC inference [◇(p ∨ q)]⁺ ⊨ ◇p ∧ ◇q (and the analogous cancellation under negation, Example (2) of the paper) over BSMLEmpty. Requires extending BSML/Enrichment.lean's [·]⁺ to target BSMLEmpty.Formula. Currently the file formalises the vehicle (syntax + semantics) but never fires the gun (FC prediction).
Fact 2.5 (negation normal form) and Fact 2.8 (ML embedding) — provable but not load-bearing for the closure-property story.
BSMLOr-specific theorem: supClosed_support_of_isGDFree (Fact 2.7 second part — ⨼-free fragment is union-closed). Requires defining the isGDFree predicate over BSMLOr.Formula.

State-based Modal Logics for Free Choice — Aloni, Anttila & Yang 2024 #

Main declarations #

Implementation notes #

Todo #

BSMLOr — BSML with global disjunction ⨼ #

Modal depth and bisim invariance for BSMLOr (Theorem 3.8) #

BSMLEmpty — BSML with emptiness operator ⊘ #

Fact 2.7: BSMLEmpty is union-closed #

Modal depth and bisim invariance for BSMLEmpty (Theorem 3.8) #

Embeddings: BSMLFormula ↪ extension formulas #

BSMLOr — BSML with global disjunction `⨼` #

BSMLEmpty — BSML with emptiness operator `⊘` #