Putting oughts together

@cite{boylan-2023}

Semantics and Pragmatics 16, Article 5: 1–53.

Core Proposal

Consistent Agglomeration — when φ and ψ are consistent, ⌜ought φ⌝ and ⌜ought ψ⌝ entail ⌜ought (φ ∧ ψ)⌝ — is valid for deontic but not epistemic ought. Boylan gives a unified semantics that derives this asymmetry from three independently motivated components:

1. Existential semantics: ought is an existential quantifier over the propositionally best partial answers to a relevance question (PBEST), not a universal quantifier over best worlds.

2. Question-sensitivity: The ordering only ranks partial answers to a contextually supplied relevance question Q, following @cite{karttunen-1977}'s partition semantics.

3. Pairwise consistency definedness: ought is defined only when all pairs in PBEST are consistent with the background information.

The deontic/epistemic split arises from a structural difference in orderings: deontic orderings satisfy an averaging constraint (a disjunction cannot be worse than ALL its disjuncts), while epistemic orderings can violate it (a disjunction can be more probable than any disjunct).

Structure

The file is organized top-down: abstract framework first, concrete applications second.

§§1–6 establish the formal machinery — proposition-level orderings, partitions (partial/complete answers), PBEST, pairwise consistency, ought, and ordering assumptions (Assumptions 1–6 from the appendix).

§7 derives the general structural properties from those assumptions:

• Fact 1 (fact1_partial_complete): Partition disjunction — a partial answer and complete answer are either nested or disjoint.
• Fact 2 (fact2_unique_deontic_complete): Under deontic orderings, PBEST contains exactly one complete answer.
• Fact 3 (fact3_deontic_boxy): Singleton PBEST reduces Boylan's ought to Kratzer necessity.
• Fact 4 (fact4_no_agglomeration): Singleton PBEST validates Agglomeration.
• Inheritance (inheritance): φ ⊨ ψ → ⌜ought φ⌝ ⊨ ⌜ought ψ⌝.
• No dilemma (no_dilemma): Pairwise consistency prevents ⌜ought φ⌝ ∧ ⌜ought ¬φ⌝.

§§8–14 instantiate the framework for concrete scenarios (The Office, Dessert) and comparisons (conflict account, Kratzer bridge).

Connection to Existing Infrastructure

• Builds on Kratzer.Ordering (bestWorlds, atLeastAsGoodAs, accessibleWorlds, ModalBase, OrderingSource).
• Bridges to Kratzer.Background (isConsistent ↔ pairConsistent).
• Connects to Kratzer.Flavor (EpistemicFlavor, DeonticFlavor).
• Contrasts with the universal-quantifier accounts in Directive.lean (@cite{von-fintel-iatridou-2008}) and Rubinstein2014.lean (@cite{rubinstein-2014}), which model weak necessity as ∀ over refined best-world sets. Boylan's operator is existential over propositions.

@[reducible, inline]

abbrev Boylan2023.World : Type

Equations

• Boylan2023.World = Fin 4

def Boylan2023.allWorlds : List World

Equations

• Boylan2023.allWorlds = [0, 1, 2, 3]

def Boylan2023.accessibleWorldsList (_f : Core.Logic.Intensional.ModalBase World) (_w : World) : List World

Computable list of accessible worlds for use in the Boylan framework. accessibleWorlds is now Set-valued (noncomputable); for the decide- driven machinery here we ignore the (always empty) modal base and return allWorlds. The Office and Dessert scenarios both use empty bases.

Equations

• Boylan2023.accessibleWorldsList _f _w = Boylan2023.allWorlds

Lifting world ordering to propositions

Kratzer's ordering ranks worlds. Boylan needs ordering over propositions (subsets of the modal base). We lift the world ordering: a proposition p is at least as good as q iff every world satisfying q is at-least-as-good-as some world satisfying p. In practice, Boylan's ordering over partial answers is supplied by context (probability for epistemics, value for deontics), so we parameterize directly over a proposition-level ordering.

@[reducible, inline]

abbrev Boylan2023.PropOrdering : Type

A proposition-level ordering: ranks propositions relative to an evaluation world. This abstracts over the source of the ordering (probability, normality, deontic value, etc.).

Equations

• Boylan2023.PropOrdering = (Boylan2023.World → (Boylan2023.World → Bool) → (Boylan2023.World → Bool) → Bool)

Questions as partitions

The relevance question Q restricted to the modal base f(w) partitions the accessible worlds into cells. Complete answers are individual cells; partial answers are unions of cells. This is the mathematical foundation for Boylan's semantics — ought quantifies over the best partial answers.

The partition framework corresponds to Assumptions 4 (question-sensitivity), 5 (partition invariance), and 6 (comparability) from the appendix.

structure Boylan2023.BoylanPartition (accessible : List World) : Type

A partition of accessible worlds into non-empty pairwise-disjoint cells. Models Q|f(w) — the relevance question restricted to the modal base.

• cells : List (World → Bool)
• cover (w : World) : w ∈ accessible → ∃ c ∈ self.cells, c w = true

  Every accessible world belongs to some cell.

• disjoint (c₁ : World → Bool) : c₁ ∈ self.cells → ∀ c₂ ∈ self.cells, c₁ ≠ c₂ → ∀ w ∈ accessible, ¬(c₁ w = true ∧ c₂ w = true)

  Distinct cells share no accessible world.

• inhabited (c : World → Bool) : c ∈ self.cells → ∃ w ∈ accessible, c w = true

  Every cell contains at least one accessible world.

def Boylan2023.BoylanPartition.isPartialAnswer {acc : List World} (Q : BoylanPartition acc) (p : World → Bool) : Prop

A partial answer is a union of cells: if p intersects a cell on the accessible worlds, it contains the entire cell.

Equations

• Q.isPartialAnswer p = ∀ c ∈ Q.cells, (∃ w ∈ acc, c w = true ∧ p w = true) → ∀ w ∈ acc, c w = true → p w = true

def Boylan2023.BoylanPartition.isCompleteAnswer {acc : List World} (Q : BoylanPartition acc) (q : World → Bool) : Prop

A complete answer is a single cell of the partition.

Equations

• Q.isCompleteAnswer q = (q ∈ Q.cells)

theorem Boylan2023.BoylanPartition.partial_contains_cell {acc : List World} (Q : BoylanPartition acc) {p : World → Bool} (hp : Q.isPartialAnswer p) (hne : ∃ w ∈ acc, p w = true) : ∃ c ∈ Q.cells, ∀ w ∈ acc, c w = true → p w = true

Every non-empty partial answer contains at least one complete cell. Since p is a union of cells and is non-empty, some cell's accessible worlds are entirely within p.

PBEST

PBEST(w, f, g, Q) = {p ⊆ f(w) : p ≠ ∅ and ¬∃q ⊆ f(w) : q ≺ p}

The set of undominated (best) propositions among the partial answers to Q that are subsets of the modal base information f(w). We take a list of candidate propositions (the partial answers to Q restricted to f(w)) and filter to those that are undominated under the ordering.

def Boylan2023.StrictlyBetter (ord : PropOrdering) (w : World) (p q : World → Bool) : Prop

Strict betterness between propositions: p is strictly better than q.

Equations

• Boylan2023.StrictlyBetter ord w p q = (ord w p q = true ∧ ¬ord w q p = true)

def Boylan2023.PBEST (ord : PropOrdering) (w : World) (candidates : List (World → Bool)) (acc : List World) : List (World → Bool)

PBEST: the propositionally best partial answers.

Given a list of candidate propositions (partial answers to Q restricted to f(w)), returns those that are non-empty on the accessible worlds and undominated under the ordering.

Equations

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

PBEST bridge lemmas

theorem Boylan2023.PBEST_subset {ord : PropOrdering} {w : World} {candidates : List (World → Bool)} {acc : List World} {p : World → Bool} (h : p ∈ PBEST ord w candidates acc) : p ∈ candidates

theorem Boylan2023.PBEST_nonempty {ord : PropOrdering} {w : World} {candidates : List (World → Bool)} {acc : List World} {p : World → Bool} (h : p ∈ PBEST ord w candidates acc) : ∃ v ∈ acc, p v = true

theorem Boylan2023.PBEST_undom {ord : PropOrdering} {w : World} {candidates : List (World → Bool)} {acc : List World} {p : World → Bool} (h : p ∈ PBEST ord w candidates acc) (r : World → Bool) : r ∈ candidates → ¬StrictlyBetter ord w r p

theorem Boylan2023.mem_PBEST {ord : PropOrdering} {w : World} {candidates : List (World → Bool)} {acc : List World} {p : World → Bool} (hmem : p ∈ candidates) (hne : ∃ v ∈ acc, p v = true) (hund : ∀ r ∈ candidates, ¬StrictlyBetter ord w r p) : p ∈ PBEST ord w candidates acc

Consistency definedness condition

⟦ought φ⟧ is defined only if for all p and q in PBEST(w,f,g,Q), (p ∩ q) ∩ f(w) ≠ ∅. This is pairwise, not global, consistency.

The key insight: {Alice is in, Bob is in, ..., Not everyone is in} is pairwise consistent (any two people can both be in) but globally inconsistent (not everyone can be in while someone is absent).

def Boylan2023.pairConsistent (p q : World → Bool) (accessible : List World) : Bool

Two propositions are consistent with respect to background information: there exists a world satisfying both p, q, and the modal base.

Equations

• Boylan2023.pairConsistent p q accessible = accessible.any fun (w : Boylan2023.World) => p w && q w

def Boylan2023.pairwiseConsistent (props : List (World → Bool)) (accessible : List World) : Bool

All pairs in a list of propositions are consistent.

Equations

• Boylan2023.pairwiseConsistent props accessible = props.all fun (p : Boylan2023.World → Bool) => props.all fun (q : Boylan2023.World → Bool) => Boylan2023.pairConsistent p q accessible

def Boylan2023.oughtDefined (ord : PropOrdering) (w : World) (candidates : List (World → Bool)) (accessible : List World) : Bool

Definedness condition for ought: PBEST is pairwise consistent.

Equations

• Boylan2023.oughtDefined ord w candidates accessible = Boylan2023.pairwiseConsistent (Boylan2023.PBEST ord w candidates accessible) accessible

Boylan's ought

(a) ⟦ought φ⟧^{w,f,g,Q} is defined only if for all p and q in PBEST(w,f,g,Q), p ∩ q is consistent with f(w).

(b) If defined, ⟦ought φ⟧^{w,f,g,Q} iff ∃p ∈ PBEST(w,f,g,Q): ∀w' ∈ p: ⟦φ⟧^{w'} = 1

def Boylan2023.ought (ord : PropOrdering) (f : Core.Logic.Intensional.ModalBase World) (candidates : List (World → Bool)) (φ : World → Bool) (w : World) : Option Bool

Boylan's ought: existential quantifier over PBEST. Returns none when the definedness condition fails.

Equations

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

Ordering constraints

The deontic/epistemic asymmetry arises from structural differences in orderings. Deontic orderings satisfy an averaging constraint: a disjunction's value lies between its best and worst disjuncts. Epistemic orderings violate this: P(A ∨ B) can exceed max(P(A), P(B)).

These correspond to Assumptions 1 (Limit) and 2 (Deontic orderings) from the appendix.

def Boylan2023.isDeontic (ord : PropOrdering) (w : World) (completeAnswers : List (World → Bool)) (acc : List World) : Prop

The deontic constraint on a proposition-level ordering (Assumption 2).

For every proposition p that contains a complete answer (cell) q ⊆ p on the accessible worlds, some complete answer q' ⊆ p is at least as good as p. This ensures a complete answer makes it into PBEST under deontic orderings.

Epistemics violate this: a disjunction can be more probable than any disjunct (P(A∨B) > max(P(A), P(B)) when A,B overlap).

Equations

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

def Boylan2023.orderingTransitive (ord : PropOrdering) (w : World) : Prop

Transitivity of the ordering (implicit in Kratzer's framework).

Equations

• Boylan2023.orderingTransitive ord w = ∀ (a b c : Boylan2023.World → Bool), ord w a b = true → ord w b c = true → ord w a c = true

Structural properties of Boylan's ought

The general properties derived from the framework above. These hold for all orderings, modal bases, and candidate sets — they are not finite data checks but structured proofs from the assumptions.

From the appendix: Facts 1–4 establish that deontic ought reduces to Kratzer necessity (Facts 2–3) and validates Agglomeration (Fact 4), while epistemic ought can fail Agglomeration (Fact 5, §8 below).

From §10–11: Inheritance and No-dilemma hold for all flavors.

theorem Boylan2023.fact1_partial_complete {acc : List World} (Q : BoylanPartition acc) {p q : World → Bool} (hp : Q.isPartialAnswer p) (hq : Q.isCompleteAnswer q) : (∀ w ∈ acc, q w = true → p w = true) ∨ ∀ w ∈ acc, ¬(p w = true ∧ q w = true)

Fact 1: For any partial answer p and complete answer q (cell), either q ⊆ p or p ∩ q = ∅ on the accessible worlds.

Proof: q is a cell. If q and p share an accessible world v, then since p is a union of cells, all of q's accessible worlds must be in p (by isPartialAnswer applied to cell q). Otherwise disjoint.

theorem Boylan2023.BoylanPartition.cells_pairInconsistent {acc : List World} (Q : BoylanPartition acc) {q₁ q₂ : World → Bool} (hq₁ : q₁ ∈ Q.cells) (hq₂ : q₂ ∈ Q.cells) (hne : q₁ ≠ q₂) : pairConsistent q₁ q₂ acc = false

Distinct cells of a partition are pairwise inconsistent — they share no accessible world. This is the key to uniqueness in Fact 2.

theorem Boylan2023.undominated_of_geq {ord : PropOrdering} {w : World} {candidates : List (World → Bool)} (htrans : orderingTransitive ord w) {p q : World → Bool} (hp_undom : ∀ r ∈ candidates, ¬StrictlyBetter ord w r p) (hq_geq_p : ord w q p = true) (r : World → Bool) : r ∈ candidates → ¬StrictlyBetter ord w r q

Key lemma: If p is undominated among candidates and q ≽ p (at least as good), then q is also undominated — given transitivity.

Proof: Suppose r ≻ q (r strictly better). By transitivity r ≽ p (from r ≽ q ≽ p). If also p ≽ r, then by transitivity q ≽ r (from q ≽ p ≽ r), contradicting r ≻ q. So ¬(p ≽ r), hence r ≻ p, contradicting p's undominatedness.

Fact 2 — Unique Deontic Complete Answer

Proof sketch (Boylan, p. 46):

Existence. PBEST is non-empty (Assumption 1); take p ∈ PBEST. Since p is a partial answer, some cell q ⊆ p (partial_contains_cell). By the deontic constraint (Assumption 2 / isDeontic), some cell q' ⊆ p is at least as good as p (q' ≽ p). By undominated_of_geq, q' is also undominated. Since q' is non-empty (a cell) and in the candidates, q' ∈ PBEST.

Uniqueness. Suppose q₁ ≠ q₂ are both cells in PBEST. By cells_pairInconsistent, pairConsistent q₁ q₂ acc = false. But pairwiseConsistent requires all PBEST pairs to be consistent — contradiction.

theorem Boylan2023.fact2_unique_deontic_complete {acc : List World} (Q : BoylanPartition acc) {ord : PropOrdering} {w : World} {candidates : List (World → Bool)} (htrans : orderingTransitive ord w) (hcands_pa : ∀ p ∈ candidates, Q.isPartialAnswer p) (hcells_in_cands : ∀ c ∈ Q.cells, c ∈ candidates) (hdeontic : isDeontic ord w Q.cells acc) (hp_exists : ∃ (p : World → Bool), p ∈ PBEST ord w candidates acc) (hpw : pairwiseConsistent (PBEST ord w candidates acc) acc = true) : ∃ (q : World → Bool), Q.isCompleteAnswer q ∧ q ∈ PBEST ord w candidates acc ∧ ∀ (q' : World → Bool), Q.isCompleteAnswer q' → q' ∈ PBEST ord w candidates acc → q' = q

Fact 2: Under a deontic, transitive ordering with pairwise consistency, PBEST contains exactly one complete answer.

Fact 3 — Deontic Ought Is Boxy (General)

When PBEST = [q] (a singleton containing one complete answer), Boylan's existential ought reduces to universal quantification over q — exactly Kratzer necessity relativized to the unique best complete answer.

theorem Boylan2023.fact3_deontic_boxy {ord : PropOrdering} {f : Core.Logic.Intensional.ModalBase World} {w : World} {candidates : List (World → Bool)} {q : World → Bool} (hpbest : PBEST ord w candidates (accessibleWorldsList f w) = [q]) (hpw : pairwiseConsistent [q] (accessibleWorldsList f w) = true) (φ : World → Bool) : ought ord f candidates φ w = some ((List.filter q (accessibleWorldsList f w)).all φ)

Fact 3: When PBEST is a singleton {q}, ⌜ought φ⌝ = true iff all accessible q-worlds satisfy φ.

theorem Boylan2023.fact4_no_agglomeration {ord : PropOrdering} {f : Core.Logic.Intensional.ModalBase World} {w : World} {candidates : List (World → Bool)} {q φ ψ : World → Bool} (hpbest : PBEST ord w candidates (accessibleWorldsList f w) = [q]) (hpw : pairwiseConsistent [q] (accessibleWorldsList f w) = true) (hφ : ought ord f candidates φ w = some true) (hψ : ought ord f candidates ψ w = some true) : ought ord f candidates (fun (v : World) => φ v && ψ v) w = some true

Fact 4: Under the hypotheses of Fact 3 (PBEST = [q]), Agglomeration holds: ⌜ought φ⌝ ∧ ⌜ought ψ⌝ → ⌜ought (φ ∧ ψ)⌝.

Inheritance and No-Dilemma

theorem Boylan2023.inheritance {ord : PropOrdering} {f : Core.Logic.Intensional.ModalBase World} {cands : List (World → Bool)} {φ ψ : World → Bool} {w : World} (hent : ∀ (v : World), φ v = true → ψ v = true) (hoφ : ought ord f cands φ w = some true) : ought ord f cands ψ w = some true

Inheritance: If φ entails ψ, then ⌜ought φ⌝ entails ⌜ought ψ⌝. This is a general result — not a finite data check — that holds for all orderings, modal bases, and candidate sets. Contrastivist accounts generally invalidate this (§10).

theorem Boylan2023.no_dilemma {ord : PropOrdering} {f : Core.Logic.Intensional.ModalBase World} {cands : List (World → Bool)} {φ : World → Bool} {w : World} (h1 : ought ord f cands φ w = some true) (h2 : ought ord f cands (fun (v : World) => !φ v) w = some true) : False

No dilemma when defined: Boylan's ought never simultaneously yields ⌜ought φ⌝ = true and ⌜ought ¬φ⌝ = true. If p₁ ∈ PBEST witnesses φ and p₂ ∈ PBEST witnesses ¬φ, pairwise consistency gives a world in p₁ ∩ p₂ that would satisfy both φ and ¬φ. This is the key structural advantage over the conflict account, which predicts dilemmas in The Office.

The Office

26 workers (Alice, Bob, ..., Zadie) work on separate floors. On average they each take a sick day once a month, so statistically it is rare that all 26 are present on any given day.

For each worker x: "x should be in the office today" is true. But "Everyone should be in the office today" is false.

We model this with 4 worlds (the minimum needed to demonstrate the structure): 3 workers, where exactly one is absent in each non-ideal world.

• w0: all present (low probability)
• w1: Alice absent
• w2: Bob absent
• w3: Carol absent

def Boylan2023.aliceIn : World → Bool

Who is present at work in each world.

Equations

• Boylan2023.aliceIn w = (w != 1)

def Boylan2023.bobIn : World → Bool

Equations

• Boylan2023.bobIn w = (w != 2)

def Boylan2023.carolIn : World → Bool

Equations

• Boylan2023.carolIn w = (w != 3)

def Boylan2023.everyoneIn : World → Bool

Everyone is in the office.

Equations

• Boylan2023.everyoneIn w = (Boylan2023.aliceIn w && Boylan2023.bobIn w && Boylan2023.carolIn w)

def Boylan2023.officeBase : Core.Logic.Intensional.ModalBase World

Epistemic modal base: all worlds epistemically accessible.

Equations

• Boylan2023.officeBase x✝ = []

def Boylan2023.officeOrdering : PropOrdering

Epistemic ordering for The Office: probability-based. Propositions true in more worlds are ranked higher. w1, w2, w3 are each roughly equally likely; w0 (all present) is rare.

Here we model this with a simple ordering: p is at least as good as q iff p is true in at least as many worlds as q.

Equations

• Boylan2023.officeOrdering x✝ p q = decide ((List.filter p Boylan2023.allWorlds).length ≥ (List.filter q Boylan2023.allWorlds).length)

def Boylan2023.officeCandidates : List (World → Bool)

The partial answers to the relevance question include each individual-in proposition and the not-everyone-in proposition. These are the propositions whose truth depends only on which workers are present.

In the full 26-worker model, the best propositions are {Alice is in, Bob is in, ..., Zadie is in, Not everyone is in}. In our 4-world model:

Equations

• Boylan2023.officeCandidates = [Boylan2023.aliceIn, Boylan2023.bobIn, Boylan2023.carolIn, Boylan2023.everyoneIn, fun (w : Boylan2023.World) => !Boylan2023.everyoneIn w]

theorem Boylan2023.office_pbest_length : (PBEST officeOrdering 0 officeCandidates (accessibleWorldsList officeBase 0)).length = 4

PBEST contains exactly 4 propositions (the 3 individual-in props and not-everyone-in; everyoneIn is dominated).

theorem Boylan2023.office_pairwise_consistent : pairwiseConsistent (PBEST officeOrdering 0 officeCandidates (accessibleWorldsList officeBase 0)) (accessibleWorldsList officeBase 0) = true

The best propositions are pairwise consistent: any two workers can both be in (pairwise but not globally).

theorem Boylan2023.office_ought_defined : oughtDefined officeOrdering 0 officeCandidates (accessibleWorldsList officeBase 0) = true

ought is defined in The Office (pairwise consistency holds).

theorem Boylan2023.alice_should_be_in : ought officeOrdering officeBase officeCandidates aliceIn 0 = some true

"Alice should be in the office" is true: there is a best proposition (namely aliceIn) such that Alice is in at every world in it.

theorem Boylan2023.bob_should_be_in : ought officeOrdering officeBase officeCandidates bobIn 0 = some true

"Bob should be in the office" is true.

theorem Boylan2023.not_everyone_should_be_in : ought officeOrdering officeBase officeCandidates everyoneIn 0 = some false

"Everyone should be in the office" is FALSE: no best proposition entails that everyone is in. This is Agglomeration failure.

theorem Boylan2023.epistemic_agglomeration_failure : ∃ (ord : PropOrdering) (f : Core.Logic.Intensional.ModalBase World) (cands : List (World → Bool)) (φ : World → Bool) (ψ : World → Bool) (w : World), ought ord f cands φ w = some true ∧ ought ord f cands ψ w = some true ∧ ought ord f cands (fun (v : World) => φ v && ψ v) w = some false

Fact 5 (Epistemic Agglomeration Failure): There exist parameters such that ⟦ought φ⟧ = 1 and ⟦ought ψ⟧ = 1 but ⟦ought (φ ∧ ψ)⟧ = 0, witnessed by The Office.

Dessert

Three dessert options: cannoli, cheesecake, and apple pie. Pie and cannoli are tastiest. One can order as many as one likes, but having more than one causes illness.

The relevance question how good will the action I perform be? lumps equally-good options together. With this question, "I ought to have pie or cannoli" is true, but "I ought to have pie" and "I ought to have cannoli" are each false — Boylan's Indifference prediction.

We model this with 4 worlds:

• w0: just pie
• w1: just cannoli
• w2: just cheesecake (less tasty)
• w3: nothing / more than one (illness)

def Boylan2023.justPie : World → Bool

Propositions for each dessert outcome.

Equations

• Boylan2023.justPie w = (w == 0)

def Boylan2023.justCannoli : World → Bool

Equations

• Boylan2023.justCannoli w = (w == 1)

def Boylan2023.justCake : World → Bool

Equations

• Boylan2023.justCake w = (w == 2)

def Boylan2023.noGood : World → Bool

Equations

• Boylan2023.noGood w = (w == 3)

def Boylan2023.pieOrCannoli : World → Bool

"I have pie or cannoli" — the disjunctive ought.

Equations

• Boylan2023.pieOrCannoli w = (Boylan2023.justPie w || Boylan2023.justCannoli w)

def Boylan2023.dessertValue : World → ℕ

Deontic ordering: tracks preferences. pie ≈ cannoli > cheesecake > nothing.

A proposition is at least as good as another iff its worst outcome is at least as good as the other's worst. We implement this as: value = minimum world index among satisfying worlds (lower = better).

Equations

• Boylan2023.dessertValue 0 = 3
• Boylan2023.dessertValue 1 = 3
• Boylan2023.dessertValue 2 = 2
• Boylan2023.dessertValue 3 = 0

def Boylan2023.worstValue (p : World → Bool) : ℕ

Worst value among worlds satisfying a proposition.

Equations

• Boylan2023.worstValue p = List.foldl min 100 (List.map Boylan2023.dessertValue (List.filter p Boylan2023.allWorlds))

def Boylan2023.dessertOrdering : PropOrdering

Deontic ordering based on worst-case value (conservative).

Equations

• Boylan2023.dessertOrdering x✝ p q = decide (Boylan2023.worstValue p ≥ Boylan2023.worstValue q)

def Boylan2023.dessertBase : Core.Logic.Intensional.ModalBase World

Deontic modal base: all worlds accessible.

Equations

• Boylan2023.dessertBase x✝ = []

def Boylan2023.dessertCandidatesHowGood : List (World → Bool)

Candidates for the how good? relevance question: actions of equal quality are lumped together.

• {pie or cannoli} (best tier)
• {cheesecake} (second tier)
• {nothing/illness} (worst tier)

Equations

• Boylan2023.dessertCandidatesHowGood = [Boylan2023.pieOrCannoli, Boylan2023.justCake, Boylan2023.noGood]

theorem Boylan2023.ought_pie_or_cannoli : ought dessertOrdering dessertBase dessertCandidatesHowGood pieOrCannoli 0 = some true

"I ought to have pie or cannoli" is true under how good?.

theorem Boylan2023.not_ought_just_pie : ought dessertOrdering dessertBase dessertCandidatesHowGood justPie 0 = some false

"I ought to have (just) pie" is FALSE: no single best proposition in the how good? partition entails just pie.

theorem Boylan2023.not_ought_just_cannoli : ought dessertOrdering dessertBase dessertCandidatesHowGood justCannoli 0 = some false

"I ought to have (just) cannoli" is FALSE.

theorem Boylan2023.dessert_indifference : ought dessertOrdering dessertBase dessertCandidatesHowGood pieOrCannoli 0 = some true ∧ ought dessertOrdering dessertBase dessertCandidatesHowGood justPie 0 = some false ∧ ought dessertOrdering dessertBase dessertCandidatesHowGood justCannoli 0 = some false

Indifference: When multiple incompatible options are equally best, the strongest true ought-claim is disjunctive.

Deontic ought reduces to Kratzer necessity

When the ordering is deontic and PBEST is pairwise consistent, there is a unique best complete answer to the relevance question. Ought φ is then true iff φ holds throughout that unique best complete answer — exactly the truth conditions of classical Kratzer necessity.

We demonstrate this for the Dessert scenario: with the fine-grained what will I do? question, the deontic ordering yields a single best proposition, and ought agrees with Kratzer necessity.

def Boylan2023.dessertCandidatesWhat : List (World → Bool)

Candidates for the what will I do? question: each action is its own complete answer.

Equations

• Boylan2023.dessertCandidatesWhat = [Boylan2023.justPie, Boylan2023.justCannoli, Boylan2023.justCake, Boylan2023.noGood]

theorem Boylan2023.dessert_what_pbest_length : (PBEST dessertOrdering 0 dessertCandidatesWhat (accessibleWorldsList dessertBase 0)).length = 2

Under what will I do? with deontic ordering, PBEST contains two equally-best options (pie and cannoli are tied).

theorem Boylan2023.dessert_what_undefined : ought dessertOrdering dessertBase dessertCandidatesWhat justPie 0 = none

But these are inconsistent (no world has both just-pie and just-cannoli), so ought is UNDEFINED with the what will I do? question. This is why the deontic case forces the coarser how good? question.

def Boylan2023.dessertValueStrict : World → ℕ

Modified dessert values where pie is uniquely best. Used to show Boylan's ought agrees with Kratzer necessity when there is a unique best option (§7, Fact 3).

Equations

• Boylan2023.dessertValueStrict 0 = 4
• Boylan2023.dessertValueStrict 1 = 3
• Boylan2023.dessertValueStrict 2 = 2
• Boylan2023.dessertValueStrict 3 = 0

def Boylan2023.worstValueStrict (p : World → Bool) : ℕ

Equations

• Boylan2023.worstValueStrict p = List.foldl min 100 (List.map Boylan2023.dessertValueStrict (List.filter p Boylan2023.allWorlds))

def Boylan2023.dessertStrictOrd : PropOrdering

Equations

• Boylan2023.dessertStrictOrd x✝ p q = decide (Boylan2023.worstValueStrict p ≥ Boylan2023.worstValueStrict q)

def Boylan2023.dessertStrictCandidates : List (World → Bool)

Equations

• Boylan2023.dessertStrictCandidates = [Boylan2023.justPie, Boylan2023.justCannoli, Boylan2023.justCake, Boylan2023.noGood]

theorem Boylan2023.strict_pbest_singleton : (PBEST dessertStrictOrd 0 dessertStrictCandidates (accessibleWorldsList dessertBase 0)).length = 1

With a unique best option, PBEST is a singleton.

theorem Boylan2023.deontic_ought_is_box : ought dessertStrictOrd dessertBase dessertStrictCandidates justPie 0 = some true ∧ ought dessertStrictOrd dessertBase dessertStrictCandidates (fun (w : World) => !justPie w) 0 = some false

Fact 3 (concrete): When PBEST is a singleton {p}, ought φ = true iff ∀w' ∈ p. φ(w') — matching Kratzer necessity relativized to the unique best proposition.

Deontic Agglomeration holds

When PBEST is a singleton (the deontic case with a unique best complete answer), Agglomeration holds trivially: if the unique best proposition entails both φ and ψ, it entails φ ∧ ψ.

We verify this for the strict dessert scenario.

def Boylan2023.notCannoli : World → Bool

"I ought to have pie" and "I ought not to have cannoli" — both true.

Equations

• Boylan2023.notCannoli w = !Boylan2023.justCannoli w

theorem Boylan2023.strict_ought_pie : ought dessertStrictOrd dessertBase dessertStrictCandidates justPie 0 = some true

theorem Boylan2023.strict_ought_not_cannoli : ought dessertStrictOrd dessertBase dessertStrictCandidates notCannoli 0 = some true

theorem Boylan2023.no_deontic_agglomeration_failure : ought dessertStrictOrd dessertBase dessertStrictCandidates (fun (w : World) => justPie w && notCannoli w) 0 = some true

Fact 4 (concrete): The conjunction of two true deontic ought-claims is also true.

Connecting Boylan to Kratzer

When Boylan's ought is defined and the ordering is deontic (unique best complete answer), it agrees with Kratzer's necessity operator for the same modal base and ordering source. This is the structural connection that justifies calling deontic ought "a box after all" (§7).

def Boylan2023.classicOught (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (φ : World → Bool) (w : World) : Prop

The classic Kratzer semantics: ought is a universal quantifier over best worlds. Boylan argues this is correct for deontics but not epistemics.

Equations

• Boylan2023.classicOught f g φ w = Semantics.Modality.Kratzer.necessity f g (fun (w' : Boylan2023.World) => φ w' = true) w

theorem Boylan2023.kratzer_agglomerates (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (w : World) : Semantics.Modality.Kratzer.necessity f g (fun (w' : World) => aliceIn w' = true) w → Semantics.Modality.Kratzer.necessity f g (fun (w' : World) => bobIn w' = true) w → Semantics.Modality.Kratzer.necessity f g (fun (w' : World) => carolIn w' = true) w → Semantics.Modality.Kratzer.necessity f g (fun (w' : World) => everyoneIn w' = true) w

The classic semantics cannot distinguish the epistemic pattern.

Kratzer necessity is Agglomeration-valid by construction: if □φ and □ψ then □(φ∧ψ). So any ordering that makes "Alice should be in" true also makes "Everyone should be in" true. The classic semantics cannot get {Alice-true, Bob-true, Carol-true, Everyone-false} for ANY choice of modal base and ordering.

theorem Boylan2023.boylan_correct_office : ought officeOrdering officeBase officeCandidates aliceIn 0 = some true ∧ ought officeOrdering officeBase officeCandidates bobIn 0 = some true ∧ ought officeOrdering officeBase officeCandidates carolIn 0 = some true ∧ ought officeOrdering officeBase officeCandidates everyoneIn 0 = some false

Boylan gets the right pattern: all three individual oughts true, conjunction false.

The conflict account wrongly predicts dilemmas

The conflict account (@cite{von-fintel-2012}, @cite{horty-2012}) says ⟦ought φ⟧ = 1 iff some maximally consistent subset of the best propositions entails φ. In The Office, this predicts epistemic dilemmas: for each worker, there is an MCS entailing their absence. Boylan argues this is wrong — The Office does not involve dilemmas.

We formalize the conflict account's prediction and show it diverges from Boylan's.

def Boylan2023.subsetWorlds (props : List (World → Bool)) (mask : List Bool) (accessible : List World) : List World

A subset of propositions: represented as a Boolean mask on the list.

Equations

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

def Boylan2023.maskConsistent (props : List (World → Bool)) (mask : List Bool) (accessible : List World) : Bool

Whether a mask selects a consistent subset (non-empty intersection).

Equations

• Boylan2023.maskConsistent props mask accessible = !(Boylan2023.subsetWorlds props mask accessible).isEmpty

def Boylan2023.maskMaximal (props : List (World → Bool)) (mask : List Bool) (accessible : List World) : Bool

Whether a consistent subset is maximal: no strictly larger consistent subset exists (adding any excluded proposition breaks consistency).

Equations

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

def Boylan2023.allMasks : ℕ → List (List Bool)

Generate all Boolean masks of a given length.

Equations

• Boylan2023.allMasks 0 = [[]]
• Boylan2023.allMasks n.succ = List.flatMap (fun (m : List Bool) => [true :: m, false :: m]) (Boylan2023.allMasks n)

def Boylan2023.conflictOught (bestProps : List (World → Bool)) (accessible : List World) (φ : World → Bool) : Bool

The conflict account (eq. 61): ⟦ought φ⟧ = 1 iff for some maximally consistent subset S of g(w), ∀w' ∈ ∩S ∩ f(w): φ(w').

Equations

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

def Boylan2023.officeBestConflict : List (World → Bool)

In The Office, the conflict account yields epistemic dilemmas. The best propositions are {Alice in, Bob in, Carol in, ¬everyone in}. MCS {Bob in, Carol in, ¬everyone in} entails Alice is absent — so the conflict account predicts "Alice should NOT be in" is true.

Boylan's semantics avoids this: ought never produces dilemmas when PBEST is pairwise consistent.

Equations

• Boylan2023.officeBestConflict = [Boylan2023.aliceIn, Boylan2023.bobIn, Boylan2023.carolIn, fun (w : Boylan2023.World) => !Boylan2023.everyoneIn w]

theorem Boylan2023.conflict_predicts_alice_absent : (conflictOught officeBestConflict (accessibleWorldsList officeBase 0) fun (w : World) => !aliceIn w) = true

theorem Boylan2023.boylan_no_alice_absent : ought officeOrdering officeBase officeCandidates (fun (w : World) => !aliceIn w) 0 = some false

theorem Boylan2023.conflict_dilemma : conflictOught officeBestConflict (accessibleWorldsList officeBase 0) aliceIn = true ∧ (conflictOught officeBestConflict (accessibleWorldsList officeBase 0) fun (w : World) => !aliceIn w) = true

The conflict account also predicts a full dilemma: both "Alice should be in" AND "Alice should not be in" come out true simultaneously. Boylan's semantics avoids this entirely (see no_dilemma above).

Connecting to Kratzer's framework

Boylan's apparatus extends Kratzer with proposition-level ordering and pairwise consistency. We bridge back by showing:

1. pairConsistent agrees with Kratzer's isConsistent (Background.lean)
2. The Office and Dessert scenarios can be typed via EpistemicFlavor and DeonticFlavor (Flavor.lean)

theorem Boylan2023.pairConsistent_iff_isConsistent (p q : World → Bool) : pairConsistent p q allWorlds = true ↔ Core.Logic.Intensional.Premise.isConsistent [fun (w : World) => p w = true, fun (w : World) => q w = true]

Boylan's pairwise consistency agrees with Kratzer's proposition consistency when all worlds are accessible (Background.lean, p. 31).

def Boylan2023.officeEpistemic : Semantics.Modality.Kratzer.EpistemicFlavor World

The Office as an epistemic scenario via Kratzer.Flavor.

Equations

• Boylan2023.officeEpistemic = { evidence := Boylan2023.officeBase }

def Boylan2023.dessertDeontic : Semantics.Modality.Kratzer.DeonticFlavor World

Dessert as a deontic scenario via Kratzer.Flavor.

Equations

• Boylan2023.dessertDeontic = { circumstances := Boylan2023.dessertBase, norms := fun (x : Boylan2023.World) => [] }

theorem Boylan2023.office_base_from_flavor : officeEpistemic.toKratzerParams.base = officeBase

The epistemic flavor's modal base matches The Office.

theorem Boylan2023.dessert_base_from_flavor : dessertDeontic.toKratzerParams.base = dessertBase

The deontic flavor's modal base matches Dessert.