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.
• TwoAtomWorld — 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 KripkeModel's String-keyed val field by pattern-matching on the canonical names via FCAtom.toName. Eliminating the String layer entirely (making KripkeModel.val : FCAtom → α → Bool) would require parameterizing Formula and KripkeModel over the atom type — a substrate-wide refactor deferred to a separate effort.

inductive 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).

@[instance_reducible]

instance BSML.instDecidableEqFCAtom : DecidableEq FCAtom

Equations

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

def BSML.instReprFCAtom.repr : FCAtom → ℕ → Std.Format

Equations

• BSML.instReprFCAtom.repr BSML.FCAtom.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.FCAtom.a")).group prec✝
• BSML.instReprFCAtom.repr BSML.FCAtom.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.FCAtom.b")).group prec✝
• BSML.instReprFCAtom.repr BSML.FCAtom.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.FCAtom.c")).group prec✝

@[instance_reducible]

instance BSML.instReprFCAtom : Repr FCAtom

Equations

• BSML.instReprFCAtom = { reprPrec := BSML.instReprFCAtom.repr }

@[instance_reducible]

instance BSML.instInhabitedFCAtom : Inhabited FCAtom

Equations

• BSML.instInhabitedFCAtom = { default := BSML.instInhabitedFCAtom.default }

@[instance_reducible]

instance BSML.instFintypeFCAtom : Fintype FCAtom

Equations

• BSML.instFintypeFCAtom = { elems := {BSML.FCAtom.a, BSML.FCAtom.b, BSML.FCAtom.c}, complete := BSML.instFintypeFCAtom._proof_1 }

def BSML.FCAtom.toName : FCAtom → String

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

Equations

• BSML.FCAtom.a.toName = "a"
• BSML.FCAtom.b.toName = "b"
• BSML.FCAtom.c.toName = "c"

inductive 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

@[instance_reducible]

instance BSML.instDecidableEqQVar : DecidableEq QVar

Equations

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

def BSML.instReprQVar.repr : QVar → ℕ → Std.Format

Equations

• BSML.instReprQVar.repr BSML.QVar.x prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.QVar.x")).group prec✝

@[instance_reducible]

instance BSML.instReprQVar : Repr QVar

Equations

• BSML.instReprQVar = { reprPrec := BSML.instReprQVar.repr }

@[instance_reducible]

instance BSML.instFintypeQVar : Fintype QVar

Equations

• BSML.instFintypeQVar = { elems := { val := ↑BSML.QVar.enumList, nodup := BSML.QVar.enumList_nodup }, complete := BSML.instFintypeQVar._proof_1 }

inductive BSML.TwoAtomWorld : 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 : TwoAtomWorld
• onlyA : TwoAtomWorld
• onlyB : TwoAtomWorld
• both : TwoAtomWorld

@[instance_reducible]

instance BSML.instDecidableEqTwoAtomWorld : DecidableEq TwoAtomWorld

Equations

• BSML.instDecidableEqTwoAtomWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BSML.instReprTwoAtomWorld.repr : TwoAtomWorld → ℕ → Std.Format

Equations

• BSML.instReprTwoAtomWorld.repr BSML.TwoAtomWorld.nothing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.TwoAtomWorld.nothing")).group prec✝
• BSML.instReprTwoAtomWorld.repr BSML.TwoAtomWorld.onlyA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.TwoAtomWorld.onlyA")).group prec✝
• BSML.instReprTwoAtomWorld.repr BSML.TwoAtomWorld.onlyB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.TwoAtomWorld.onlyB")).group prec✝
• BSML.instReprTwoAtomWorld.repr BSML.TwoAtomWorld.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.TwoAtomWorld.both")).group prec✝

@[instance_reducible]

instance BSML.instReprTwoAtomWorld : Repr TwoAtomWorld

Equations

• BSML.instReprTwoAtomWorld = { reprPrec := BSML.instReprTwoAtomWorld.repr }

@[instance_reducible]

instance BSML.instFintypeTwoAtomWorld : Fintype TwoAtomWorld

Equations

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

def BSML.TwoAtomWorld.holds : TwoAtomWorld → 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

• BSML.TwoAtomWorld.both.holds BSML.FCAtom.a = true
• BSML.TwoAtomWorld.both.holds BSML.FCAtom.b = true
• BSML.TwoAtomWorld.onlyA.holds BSML.FCAtom.a = true
• BSML.TwoAtomWorld.onlyA.holds BSML.FCAtom.b = false
• BSML.TwoAtomWorld.onlyB.holds BSML.FCAtom.a = false
• BSML.TwoAtomWorld.onlyB.holds BSML.FCAtom.b = true
• BSML.TwoAtomWorld.nothing.holds BSML.FCAtom.a = false
• BSML.TwoAtomWorld.nothing.holds BSML.FCAtom.b = false
• x✝.holds BSML.FCAtom.c = false

@[reducible, inline]

abbrev BSML.TwoAtomWorld.satisfies : TwoAtomWorld → FCAtom → Bool

Synonym used by Studies that prefer the predicate spelling.

Equations

• BSML.TwoAtomWorld.satisfies = BSML.TwoAtomWorld.holds