Typed atoms and small world models for free-choice scenarios

Shared scenario substrate for BSML- and QBSML-based free-choice studies ([Alo22], [AvO23], [Yan23]). Replaces ad-hoc string atoms ("coffee", "tea", ...) in scenario constructions, where a typo silently compiles to false under the match p with | "coffee" => ... | _ => false fallthrough pattern.

Main declarations

• FCAtom — typed propositional atoms: a/b cover the disjuncts of binary FC inferences; c is reserved for embedded scenarios involving a third proposition.
• QVar — the shared toy variable type for quantified FC scenarios (QBSML); the first-order counterpart of FCAtom.
• PowerSet2World — the 2² = 4 truth assignments to two atoms ([Alo22] Figure 1: w_∅, w_a, w_b, w_ab), with the typed holds truth table.

Studies instantiate BSMLModel's String-keyed val field by pattern-matching on the canonical names via FCAtom.toName. Eliminating the String layer entirely (making BSMLModel.val : FCAtom → α → Bool) would require parameterizing BSMLFormula and BSMLModel over the atom type — a substrate-wide refactor deferred to a separate effort.

inductive Core.Logic.Modal.BSML.FCAtom : Type

Typed atom enum for free-choice scenarios.

• a : FCAtom

  First disjunct (e.g. coffee, Paris, boat).

• b : FCAtom

  Second disjunct (e.g. tea, Rome, bus).

• c : FCAtom

  Third atom for embedded scenarios (negative free choice).

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instDecidableEqFCAtom : DecidableEq FCAtom

Equations

• Core.Logic.Modal.BSML.instDecidableEqFCAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Logic.Modal.BSML.instReprFCAtom.repr : FCAtom → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instReprFCAtom : Repr FCAtom

Equations

• Core.Logic.Modal.BSML.instReprFCAtom = { reprPrec := Core.Logic.Modal.BSML.instReprFCAtom.repr }

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instFintypeFCAtom : Fintype FCAtom

Equations

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

def Core.Logic.Modal.BSML.FCAtom.toName : FCAtom → String

Canonical String name of an atom. Used at BSMLModel.val boundaries where the substrate's val : String → α → Bool field forces String.

Equations

• Core.Logic.Modal.BSML.FCAtom.a.toName = "a"
• Core.Logic.Modal.BSML.FCAtom.b.toName = "b"
• Core.Logic.Modal.BSML.FCAtom.c.toName = "c"

inductive Core.Logic.Modal.BSML.QVar : Type

Single variable x — the shared toy variable type for quantified FC scenarios (QBSML studies); the first-order counterpart of FCAtom.

• x : QVar

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instDecidableEqQVar : DecidableEq QVar

Equations

• Core.Logic.Modal.BSML.instDecidableEqQVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Logic.Modal.BSML.instReprQVar.repr : QVar → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instReprQVar : Repr QVar

Equations

• Core.Logic.Modal.BSML.instReprQVar = { reprPrec := Core.Logic.Modal.BSML.instReprQVar.repr }

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instFintypeQVar : Fintype QVar

Equations

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

inductive Core.Logic.Modal.BSML.PowerSet2World : Type

Power-set-of-{a,b}: the 4 truth assignments to two propositional atoms.

Names follow [Alo22] Figure 1 (w_∅, w_a, w_b, w_ab):

• nothing = w_∅: neither a nor b
• onlyA = w_a: only a
• onlyB = w_b: only b
• both = w_ab: both a and b

• nothing : PowerSet2World
• onlyA : PowerSet2World
• onlyB : PowerSet2World
• both : PowerSet2World

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instDecidableEqPowerSet2World : DecidableEq PowerSet2World

Equations

• Core.Logic.Modal.BSML.instDecidableEqPowerSet2World x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Logic.Modal.BSML.instReprPowerSet2World.repr : PowerSet2World → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instReprPowerSet2World : Repr PowerSet2World

Equations

• Core.Logic.Modal.BSML.instReprPowerSet2World = { reprPrec := Core.Logic.Modal.BSML.instReprPowerSet2World.repr }

@[implicit_reducible]

instance Core.Logic.Modal.BSML.instFintypePowerSet2World : Fintype PowerSet2World

Equations

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

def Core.Logic.Modal.BSML.PowerSet2World.holds : PowerSet2World → FCAtom → Bool

Truth-table for the two-atom power set. The third atom (c) is unsatisfiable in this baseline 4-world model — embedded scenarios needing c should use a larger world type.

Equations

• Core.Logic.Modal.BSML.PowerSet2World.both.holds Core.Logic.Modal.BSML.FCAtom.a = true
• Core.Logic.Modal.BSML.PowerSet2World.both.holds Core.Logic.Modal.BSML.FCAtom.b = true
• Core.Logic.Modal.BSML.PowerSet2World.onlyA.holds Core.Logic.Modal.BSML.FCAtom.a = true
• Core.Logic.Modal.BSML.PowerSet2World.onlyA.holds Core.Logic.Modal.BSML.FCAtom.b = false
• Core.Logic.Modal.BSML.PowerSet2World.onlyB.holds Core.Logic.Modal.BSML.FCAtom.a = false
• Core.Logic.Modal.BSML.PowerSet2World.onlyB.holds Core.Logic.Modal.BSML.FCAtom.b = true
• Core.Logic.Modal.BSML.PowerSet2World.nothing.holds Core.Logic.Modal.BSML.FCAtom.a = false
• Core.Logic.Modal.BSML.PowerSet2World.nothing.holds Core.Logic.Modal.BSML.FCAtom.b = false
• x✝.holds Core.Logic.Modal.BSML.FCAtom.c = false

@[reducible, inline]

abbrev Core.Logic.Modal.BSML.PowerSet2World.satisfies : PowerSet2World → FCAtom → Bool

Synonym used by Studies that prefer the predicate spelling.

Equations

• Core.Logic.Modal.BSML.PowerSet2World.satisfies = Core.Logic.Modal.BSML.PowerSet2World.holds