[AvO23]: modified numerals and split disjunction

Aloni & van Ormondt 2023 introduce QBSML, the first-order extension of [Alo22]'s BSML, and analyse modified numerals as split disjunctions (at least n φ ↦ n ∨ more, at most n φ ↦ n ∨ less), so that the neglect-zero enrichment [·]⁺ derives their ignorance, obviation, distribution, free-choice and negation profile (paper §5). The universal facts (3, 5–10) are substrate theorems in Logic/Team/QBSML/FreeChoice.lean; this file instantiates them at a concrete model and proves the paper's one countermodel claim.

Main declarations

• univAccessModel — universal-access model over BSML.TwoAtomWorld.
• fact3_ignorance … fact10_negation — the paper's §5 facts, as instances of the substrate theorems.
• fact4_obviation — [∀x(Px ∨ Qx)]⁺ ⊭ ∀x(◇Px ∧ ◇Qx), by the paper's Fig. 14 countermodel.
• support_univPxOrQx_iff, models_stUnivPxOrQxSentence_iff — Proposition 4.1 at the concrete model, the translations computed by rfl.

Implementation notes

QBSML.eval admits a Decidable instance in principle, but the split-disjunction clause quantifies over pairs of subteams (2^12 × 2^12 at this file's model sizes), so kernel decide is infeasible for whole-formula claims; the Fact 4 countermodel is proved by hand, with decide confined to finite side conditions. The propositional facts (3, 7, 8, 10) are stated with the individual constants of the paper's Definition 4.1 (Formula.predc atoms, world-relative ModalStructure.constInterp), the quantified facts with variable atoms — both as in the paper. Atoms and worlds come from Logic/Team/BSML/Scenarios.lean, so this file and Studies/Aloni2022.lean target the same world space.

Predicates and variables

inductive AloniVanOrmondt2023.Predicate : Type

• P : Predicate
• Q : Predicate

@[instance_reducible]

instance AloniVanOrmondt2023.instDecidableEqPredicate : DecidableEq Predicate

Equations

• AloniVanOrmondt2023.instDecidableEqPredicate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AloniVanOrmondt2023.instReprPredicate : Repr Predicate

Equations

• AloniVanOrmondt2023.instReprPredicate = { reprPrec := AloniVanOrmondt2023.instReprPredicate.repr }

def AloniVanOrmondt2023.instReprPredicate.repr : Predicate → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AloniVanOrmondt2023.instFintypePredicate : Fintype Predicate

Equations

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

The concrete model

def AloniVanOrmondt2023.univAccessModel : QBSML.Model BSML.TwoAtomWorld BSML.FCAtom BSML.FCAtom Predicate

Universal-access model on TwoAtomWorld: every world is accessible, and both predicates hold of d at w iff w models the atom d. Cf. Aloni2022.deonticModel.

Equations

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

Formulas

def AloniVanOrmondt2023.Pa : QBSML.Formula BSML.QVar BSML.FCAtom Predicate

Equations

• AloniVanOrmondt2023.Pa = QBSML.Formula.predc AloniVanOrmondt2023.Predicate.P BSML.FCAtom.a

def AloniVanOrmondt2023.Pb : QBSML.Formula BSML.QVar BSML.FCAtom Predicate

Equations

• AloniVanOrmondt2023.Pb = QBSML.Formula.predc AloniVanOrmondt2023.Predicate.P BSML.FCAtom.b

def AloniVanOrmondt2023.Px {Const : Type u_1} : QBSML.Formula BSML.QVar Const Predicate

Equations

• AloniVanOrmondt2023.Px = QBSML.Formula.pred AloniVanOrmondt2023.Predicate.P BSML.QVar.x

def AloniVanOrmondt2023.Qx {Const : Type u_1} : QBSML.Formula BSML.QVar Const Predicate

Equations

• AloniVanOrmondt2023.Qx = QBSML.Formula.pred AloniVanOrmondt2023.Predicate.Q BSML.QVar.x

def AloniVanOrmondt2023.univPossPxOrQx {Const : Type u_1} : QBSML.Formula BSML.QVar Const Predicate

The universal-FC premise ∀x◇(Px ∨ Qx) (paper's Fact 9 schema).

Equations

• AloniVanOrmondt2023.univPossPxOrQx = QBSML.Formula.univ BSML.QVar.x (AloniVanOrmondt2023.Px.disj AloniVanOrmondt2023.Qx).poss

def AloniVanOrmondt2023.univPxOrQx {Const : Type u_1} : QBSML.Formula BSML.QVar Const Predicate

The distribution premise ∀x(Px ∨ Qx) (paper's Facts 4–6 schema).

Equations

• AloniVanOrmondt2023.univPxOrQx = QBSML.Formula.univ BSML.QVar.x (AloniVanOrmondt2023.Px.disj AloniVanOrmondt2023.Qx)

theorem AloniVanOrmondt2023.Pa_neFree : Pa.NEFree

theorem AloniVanOrmondt2023.Pb_neFree : Pb.NEFree

theorem AloniVanOrmondt2023.Px_neFree {Const : Type u_1} : Px.NEFree

theorem AloniVanOrmondt2023.Qx_neFree {Const : Type u_1} : Qx.NEFree

Proposition 4.1 at the concrete model

theorem AloniVanOrmondt2023.support_univPxOrQx_iff {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} {v : QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom → BSML.QVar → BSML.FCAtom} (hv : ∀ i ∈ s, ∀ (y : BSML.QVar), i.assign y = some (v i y)) : QBSML.support univAccessModel univPxOrQx s ↔ ∀ i ∈ s, (FirstOrder.Language.Formula.all₁ BSML.QVar.x ((FirstOrder.Language.monadicRel Predicate.P).formula₁ (FirstOrder.Language.var BSML.QVar.x) ⊔ (FirstOrder.Language.monadicRel Predicate.Q).formula₁ (FirstOrder.Language.var BSML.QVar.x))).RealizeAt univAccessModel.interp i.world (v i)

The (unenriched) universal premise ∀x(Px ∨ Qx) translates into mathlib first-order syntax, and its support is classical Formula.Realize at every index — [AvO23] Proposition 4.1 instantiated at univAccessModel. The translation hypothesis is discharged by rfl: the compiler computes.

theorem AloniVanOrmondt2023.support_possPxOrQx_iff {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} {v : QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom → BSML.QVar → BSML.FCAtom} (hv : ∀ i ∈ s, ∀ (y : BSML.QVar), i.assign y = some (v i y)) : QBSML.support univAccessModel (Px.disj Qx).poss s ↔ ∀ i ∈ s, FirstOrder.Language.ModalFormula.Realize univAccessModel i.world ((FirstOrder.Language.monadicRel Predicate.P).modalFormula₁ (FirstOrder.Language.var BSML.QVar.x) ⊔ (FirstOrder.Language.monadicRel Predicate.Q).modalFormula₁ (FirstOrder.Language.var BSML.QVar.x)).diamond (v i)

The narrow-scope FC premise ◇(Px ∨ Qx) translates into the modal layer over the monadic signature, and its support is Kripke satisfaction at every index — the full [AvO23] Proposition 4.1 (modals included) at univAccessModel, the translation discharged by rfl.

def AloniVanOrmondt2023.univPxOrQxModal : (FirstOrder.Language.monadicWithConstants BSML.FCAtom Predicate).ModalFormula BSML.QVar

The modal image of ∀x(Px ∨ Qx) under toModal?.

Equations

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

def AloniVanOrmondt2023.stUnivPxOrQx : (FirstOrder.Language.monadicWithConstants BSML.FCAtom Predicate).correspondence.Formula (BSML.QVar ⊕ ℕ)

The standard translation of ∀x(Px ∨ Qx), computed by st: quantifiers relativized to the individual sort, predicates world-relativized to the current-world variable Sum.inr 0.

Equations

• AloniVanOrmondt2023.stUnivPxOrQx = FirstOrder.Language.ModalFormula.st 0 AloniVanOrmondt2023.univPxOrQxModal

theorem AloniVanOrmondt2023.stUnivPxOrQx_closed : FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.stClose 0 stUnivPxOrQx) = ∅

The closure is a genuine sentence: the compiler computes the free-variable finset.

def AloniVanOrmondt2023.stUnivPxOrQxSentence : (FirstOrder.Language.monadicWithConstants BSML.FCAtom Predicate).correspondence.Sentence

The sort-guarded closed standard translation of ∀x(Px ∨ Qx), as a sentence.

Equations

• AloniVanOrmondt2023.stUnivPxOrQxSentence = (FirstOrder.Language.stClose 0 AloniVanOrmondt2023.stUnivPxOrQx).toSentence AloniVanOrmondt2023.stUnivPxOrQx_closed

@[instance_reducible]

def AloniVanOrmondt2023.instStructureCorrespondenceMonadicWithConstantsFCAtomPredicateSumTwoAtomWorld : (FirstOrder.Language.monadicWithConstants BSML.FCAtom Predicate).correspondence.Structure (BSML.TwoAtomWorld ⊕ BSML.FCAtom)

Equations

• AloniVanOrmondt2023.instStructureCorrespondenceMonadicWithConstantsFCAtomPredicateSumTwoAtomWorld = FirstOrder.Language.ModalStructure.correspondence AloniVanOrmondt2023.univAccessModel

theorem AloniVanOrmondt2023.models_stUnivPxOrQxSentence_iff : (BSML.TwoAtomWorld ⊕ BSML.FCAtom) ⊨ stUnivPxOrQxSentence ↔ ∃ (i : QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom) (v : BSML.QVar → BSML.FCAtom), (∀ (y : BSML.QVar), i.assign y = some (v y)) ∧ QBSML.support univAccessModel univPxOrQx {i}

Truth of the standard-translation sentence in univAccessModel.correspondence is support of ∀x(Px ∨ Qx) at some singleton with a total assignment — the compactness-ready form of Proposition 4.1, every translation step (toModal?, st, the free-variable check) computed by the compiler.

Frame conditions

theorem AloniVanOrmondt2023.univAccessModel_indisputable (s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)) : FirstOrder.Language.ModalStructure.IsIndisputable univAccessModel s

univAccessModel's universal accessibility makes R indisputable on every state (every world sees the same Finset.univ). Mirrors Aloni2022.deonticModel_indisputable_on_team for the QBSML carrier.

Indisputability vs state-basedness (paper §4.1.1, Definition 4.10):

• Indisputable: all worlds in s↓ see the same accessible set (R constant).
• State-based: every w ∈ s↓ sees exactly s↓ (R(w) = s↓).

theorem AloniVanOrmondt2023.univAccessModel_stateBased_of_full {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} (hfull : QBSML.State.worldProj s = Finset.univ) : FirstOrder.Language.ModalStructure.IsStateBased univAccessModel s

State-basedness is strictly stronger than indisputability; universal access delivers it exactly on states whose world projection exhausts TwoAtomWorld. The precondition for the epistemic Facts 3 and 6.

def AloniVanOrmondt2023.fullState : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)

A state with full world projection: every world, paired with the empty assignment. Witnesses that the epistemic hypothesis of fact3_ignorance and fact6_distributionEpi is satisfiable.

Equations

• AloniVanOrmondt2023.fullState = Finset.image (fun (w : BSML.TwoAtomWorld) => (w, fun (x : BSML.QVar) => none)) Finset.univ

The §5 facts

theorem AloniVanOrmondt2023.fact3_ignorance {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} (hfull : QBSML.State.worldProj s = Finset.univ) (h : QBSML.support univAccessModel (Pa.disj Pb).enrich s) : QBSML.support univAccessModel Pa.poss s ∧ QBSML.support univAccessModel Pb.poss s

Fact 3 (ignorance), on states of full world projection.

theorem AloniVanOrmondt2023.fact5_distribution {i : QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom} (h : QBSML.support univAccessModel univPxOrQx.enrich {i}) : QBSML.support univAccessModel (QBSML.Formula.exi BSML.QVar.x Px) {i} ∧ QBSML.support univAccessModel (QBSML.Formula.exi BSML.QVar.x Qx) {i}

Fact 5 (distribution at maximal information).

theorem AloniVanOrmondt2023.fact6_distributionEpi {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} (hfull : QBSML.State.worldProj s = Finset.univ) (h : QBSML.support univAccessModel univPxOrQx.enrich s) : QBSML.support univAccessModel (QBSML.Formula.exi BSML.QVar.x Px.poss) s ∧ QBSML.support univAccessModel (QBSML.Formula.exi BSML.QVar.x Qx.poss) s

Fact 6 (distribution◇), on states of full world projection.

theorem AloniVanOrmondt2023.fact7_boxFC {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} (h : QBSML.support univAccessModel (Pa.disj Pb).nec.enrich s) : QBSML.support univAccessModel Pa.poss s ∧ QBSML.support univAccessModel Pb.poss s

Fact 7 (□-free choice; □ derived, Formula.nec).

theorem AloniVanOrmondt2023.fact8_narrowScopeFC {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} (h : QBSML.support univAccessModel (Pa.disj Pb).poss.enrich s) : QBSML.support univAccessModel Pa.poss s ∧ QBSML.support univAccessModel Pb.poss s

Fact 8 (◇-free choice); cf. Aloni2022.aloni2022_fact4_NS_FC.

theorem AloniVanOrmondt2023.fact9_universalFC {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} (h : QBSML.support univAccessModel univPossPxOrQx.enrich s) : QBSML.support univAccessModel (QBSML.Formula.univ BSML.QVar.x Px.poss) s ∧ QBSML.support univAccessModel (QBSML.Formula.univ BSML.QVar.x Qx.poss) s

Fact 9 (universal free choice), attested experimentally by [Che09b].

theorem AloniVanOrmondt2023.fact10_negation {s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar BSML.FCAtom)} (h : QBSML.support univAccessModel (Pa.disj Pb).neg.enrich s) : QBSML.support univAccessModel Pa.neg s ∧ QBSML.support univAccessModel Pb.neg s

Fact 10 (negation behaviour); cf. Aloni2022.aloni2022_fact11_dual_prohibition.

Fact 4 (obviation): the Fig. 14 countermodel

The paper's Fig. 14: a single index at the world both with the empty assignment, every world seeing exactly {both}.

inductive AloniVanOrmondt2023.Fig14Atom : Type

The Fig. 14 domain: exactly the paper's two objects. (The third FCAtom atom would give the universal extension an x/c index supporting neither disjunct, breaking the premise — the paper notes the split works "because the domain contains two objects".)

• a : Fig14Atom
• b : Fig14Atom

@[instance_reducible]

instance AloniVanOrmondt2023.instDecidableEqFig14Atom : DecidableEq Fig14Atom

Equations

• AloniVanOrmondt2023.instDecidableEqFig14Atom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AloniVanOrmondt2023.instReprFig14Atom : Repr Fig14Atom

Equations

• AloniVanOrmondt2023.instReprFig14Atom = { reprPrec := AloniVanOrmondt2023.instReprFig14Atom.repr }

def AloniVanOrmondt2023.instReprFig14Atom.repr : Fig14Atom → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AloniVanOrmondt2023.instFintypeFig14Atom : Fintype Fig14Atom

Equations

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

def AloniVanOrmondt2023.fig14V (w : BSML.TwoAtomWorld) : Predicate → Fig14Atom → Prop

Fig. 14 valuation: P holds exactly of a and Q exactly of b — divergent extensions, unlike univAccessModel's.

Equations

• AloniVanOrmondt2023.fig14V w AloniVanOrmondt2023.Predicate.P x✝ = (x✝ = AloniVanOrmondt2023.Fig14Atom.a ∧ w.holds BSML.FCAtom.a = true)
• AloniVanOrmondt2023.fig14V w AloniVanOrmondt2023.Predicate.Q x✝ = (x✝ = AloniVanOrmondt2023.Fig14Atom.b ∧ w.holds BSML.FCAtom.b = true)

def AloniVanOrmondt2023.fig14Model : QBSML.Model BSML.TwoAtomWorld Fig14Atom Fig14Atom Predicate

Equations

• AloniVanOrmondt2023.fig14Model = QBSML.Model.ofMonadic (fun (x : BSML.TwoAtomWorld) => {BSML.TwoAtomWorld.both}) (fun (x : BSML.TwoAtomWorld) => id) AloniVanOrmondt2023.fig14V

def AloniVanOrmondt2023.fig14Index : QBSML.Index BSML.TwoAtomWorld BSML.QVar Fig14Atom

Equations

• AloniVanOrmondt2023.fig14Index = (BSML.TwoAtomWorld.both, fun (x : BSML.QVar) => none)

def AloniVanOrmondt2023.fig14State : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar Fig14Atom)

Equations

• AloniVanOrmondt2023.fig14State = {AloniVanOrmondt2023.fig14Index}

theorem AloniVanOrmondt2023.fig14_stateBased : FirstOrder.Language.ModalStructure.IsStateBased fig14Model fig14State

The countermodel's R is state-based on its state — the epistemic reading Fact 4 assumes, so obviation is not an artifact of dropping the frame condition behind ignorance.

theorem AloniVanOrmondt2023.fig14_premise : QBSML.support fig14Model univPxOrQx.enrich fig14State

The universal extension splits into the x/a half supporting [Px]⁺ and the x/b half supporting [Qx]⁺ (paper Fig. 15).

theorem AloniVanOrmondt2023.fig14_conclusion_fails : ¬QBSML.support fig14Model (QBSML.Formula.univ BSML.QVar.x (Px.poss.conj Qx.poss)) fig14State

At the x/b index the only accessible world is both, where P holds of a alone (paper Fig. 16's failing substate).

theorem AloniVanOrmondt2023.fact4_obviation : ∃ (M : QBSML.Model BSML.TwoAtomWorld Fig14Atom Fig14Atom Predicate) (s : Finset (QBSML.Index BSML.TwoAtomWorld BSML.QVar Fig14Atom)), QBSML.support M univPxOrQx.enrich s ∧ ¬QBSML.support M (QBSML.Formula.univ BSML.QVar.x (Px.poss.conj Qx.poss)) s

Fact 4 (obviation): [∀x(Px ∨ Qx)]⁺ ⊭ ∀x(◇Px ∧ ◇Qx) — the universal quantifier obviates the free-choice/ignorance effect.