@cite{aloni-2022}: BSML applied to permission disjunction #
@cite{aloni-2022}
Computational instantiation of NS FC, WS FC, Dual Prohibition, Double Negation
FC, and Modal Disjunction (Facts 3, 4, 5, 11, 12) in BSML+ on a 4-world deontic
model. Each result is a named theorem invoking the universal substrate theorem
in Theories/Semantics/BSML/FreeChoice.lean, applied to the concrete model
constructed below.
Out of scope #
- Negative FC (Fact 14)
- Universal FC, ALL-OTHERS-FC, ALL-OTHERS-DUAL-PROHIBITION (Aloni §6.2 first-order)
- BSML* (Fact 13–14, §6.3.1) and BSML◇ / BSML∅ (§7) interpretation strategies
- §6.1 epistemic vs deontic contrast (this file is purely deontic)
The universal results live in Theories/Semantics/BSML/FreeChoice.lean:
narrowScopeFC, wideScopeFC, modalDisjunction, dualProhibition,
doubleNegationFC, negativeFC_poss_fails_bsmlPlus. The Negative FC failure
(Fact 14) on a single Unit world is proved there.
Atoms and worlds #
This file uses typed atoms FCAtom.{a, b} (from Phenomena.FreeChoice.Atoms)
rather than String identifiers. The valuation routes directly through
PowerSet2World.holds, eliminating the silent typo trap of the earlier
String-based pattern (match p with | "coffee" => ... | _ => false).
Worlds are PowerSet2World (nothing/onlyA/onlyB/both), matching
Aloni 2022 Figure 1's w_∅/w_a/w_b/w_ab. We label FCAtom.a as
"coffee" and FCAtom.b as "tea" in prose only — the formal types are
the typed atoms throughout.
The free-choice team: {both, onlyA, onlyB} = {w_ab, w_a, w_b}.
Excludes nothing (= w_∅), the world that would supply a zero-witness
substate for the disjunction enrichment.
Equations
Instances For
The prohibition team: just nothing (= w_∅). With restrictiveModel,
R[nothing] = {nothing} so the prohibition ¬◇(a ∨ b) is supported.
Equations
Instances For
Deontic model: universal accessibility from every world. Indisputable on
every non-empty team (R[w] = R[v] = univ trivially), but not state-based
on freeChoiceTeam since R[w] = univ ⊋ freeChoiceTeam.
Valuation: val a w = w.holds a — direct routing through the typed
atom. No String fallthrough, no silent typos.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restrictive deontic model: from nothing, only nothing is accessible;
from any other world, all worlds. Used for Dual Prohibition on the
prohibition team {nothing}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
State-based deontic model: R[w] = freeChoiceTeam for every world. Strictly stronger than indisputability; required for Modal Disjunction (Fact 3).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A deontic model where indisputability fails on freeChoiceTeam —
onlyA and onlyB see different accessible sets. Demonstrates that the
indisputable-R precondition of wideScopeFC (Fact 5) is necessary, not
incidental: WS FC's conclusion may fail on this model even when its
enriched premise is supported. (Aloni 2022 Figure 5(b) shape — non-indisputable R.
Figure 5(a) shows the dual case where R is indisputable but enrichment fails.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
◇(a ∨ b) — narrow-scope premise (Fact 4).
Equations
- One or more equations did not get rendered due to their size.
Instances For
¬◇(a ∨ b) — Dual Prohibition premise (Fact 11).
Equations
- One or more equations did not get rendered due to their size.
Instances For
◇a ∨ ◇b — wide-scope disjunction premise (Fact 5).
Equations
- One or more equations did not get rendered due to their size.
Instances For
¬¬◇(a ∨ b) — double-negation premise (Fact 12).
Equations
- One or more equations did not get rendered due to their size.
Instances For
a ∨ b — plain disjunction (Modal Disjunction premise, Fact 3).
Equations
Instances For
Fact 4 instantiated at the deontic model + free-choice team:
enriched ◇(a ∨ b) entails ◇a ∧ ◇b.
Proved by invoking the universal substrate theorem narrowScopeFC.
The premise of Fact 4 holds on this model + team.
Fact 11 instantiated at the restrictive model + prohibition team: enriched ¬◇(a ∨ b) entails ¬◇a ∧ ¬◇b.
Fact 5 instantiated at the deontic model + free-choice team:
enriched (◇a ∨ ◇b) entails ◇a ∧ ◇b, given indisputability.
Indisputability holds trivially on this model (universal access), so this
is a consequence-direction test — see aloni2022_fact5_WS_FC_fails_loose
for the discriminating failure direction.
The WS FC enriched premise IS supported on looseDeonticModel for
freeChoiceTeam — even though indisputability fails. This pairs with
aloni2022_fact5_WS_FC_fails_loose to demonstrate that the implication
of WS FC genuinely fails (premise holds, conclusion does not) on this
model — not a vacuous failure.
Necessity of indisputability: on looseDeonticModel (where indisputability
fails on freeChoiceTeam), the WS FC conclusion mayCoffee is not
supported on the team — even though the enriched premise IS supported
(aloni2022_fact5_premise_supported_loose). The substrate's wideScopeFC
cannot apply (its indisputability hypothesis fails), and the implication
genuinely breaks: premise holds, conclusion does not.
Fact 12 instantiated at the deontic model + free-choice team: enriched ¬¬◇(a ∨ b) entails ◇a ∧ ◇b (FC re-emerges under double negation). The earlier instantiation of this file (lines 117–118 in the pre-refactor version) duplicated the NS FC test rather than exhibiting the entailment from the double-negation premise; this is the correct form.
Fact 3 instantiated at the state-based model + free-choice team: enriched (a ∨ b) entails ◇a ∧ ◇b — without ◇ in the premise, by virtue of state-basedness.