Boylan (2023): Putting oughts together

Consistent Agglomeration, from ⌜ought φ⌝ and ⌜ought ψ⌝ to ⌜ought (φ ∧ ψ)⌝ for consistent φ and ψ, is valid for deontic ought and fails for epistemic ought ([Boy23]): in The Office each worker should be in today though not everyone should be. The semantics makes ought an existential quantifier over the propositionally best partial answers to a contextual relevance question, restricted to the background information, and presupposes those best answers pairwise consistent. The split then follows from the orderings. A deontic ordering places a partial answer between the best and the worst complete answer inside it, so exactly one complete answer is best (Fact 2), ought reduces to universal quantification over it (Fact 3) and agglomerates (Fact 4); an epistemic ordering can rank a disjunction above each disjunct, as a threshold on probability does, and The Office falsifies Agglomeration (Fact 5). Inheritance holds and no choice of parameters verifies a dilemma, against the conflict account, which reads The Office as one and agglomerates its premises.

Implementation notes

The background information is a finite set of worlds and the relevance question restricted to it a Finpartition, whose partial answers are the unions of complete answers; an ordering is a relation on finite propositions at a world. Definedness and truth are separate predicates, so the presupposition of (71a) is a hypothesis of the theorems that need it. Assumption 2 enters through its lower half, that some complete answer inside a partial answer is at least as good as it, which is what Fact 2 uses. The Office has two workers absent independently with probability one third, worlds weighted by counts rather than probabilities; Dessert orders by worst outcome and asks the two questions of §8.2.

References

• [Boy23]
• [Kar77b]
• [vF12]
• [Hor12]

Questions and partial answers (§4.2)

def Boylan2023.partialAnswers {W : Type u_1} [DecidableEq W] {acc : Finset W} (Q : Finpartition acc) : Finset (Finset W)

The partial answers to the relevance question restricted to the background information, Q|f(w): the unions of nonempty sets of complete answers.

Equations

• Boylan2023.partialAnswers Q = Finset.image (fun (x : Finset (Finset W)) => x.sup id) (Finset.Ioc ∅ Q.parts)

theorem Boylan2023.mem_partialAnswers {W : Type u_1} [DecidableEq W] {acc : Finset W} {Q : Finpartition acc} {p : Finset W} : p ∈ partialAnswers Q ↔ ∃ (s : Finset (Finset W)), s ≠ ∅ ∧ s ⊆ Q.parts ∧ s.sup id = p

theorem Boylan2023.parts_subset_partialAnswers {W : Type u_1} [DecidableEq W] {acc : Finset W} {Q : Finpartition acc} : Q.parts ⊆ partialAnswers Q

A complete answer is a partial answer.

theorem Boylan2023.subset_of_mem_partialAnswers {W : Type u_1} [DecidableEq W] {acc : Finset W} {Q : Finpartition acc} {p : Finset W} (hp : p ∈ partialAnswers Q) : p ⊆ acc

A partial answer lies within the background information.

theorem Boylan2023.nonempty_of_mem_partialAnswers {W : Type u_1} [DecidableEq W] {acc : Finset W} {Q : Finpartition acc} {p : Finset W} (hp : p ∈ partialAnswers Q) : p.Nonempty

A partial answer is nonempty.

theorem Boylan2023.fact1 {W : Type u_1} [DecidableEq W] {acc : Finset W} {Q : Finpartition acc} {p q : Finset W} (hp : p ∈ partialAnswers Q) (hq : q ∈ Q.parts) : q ⊆ p ∨ Disjoint q p

Fact 1: a complete answer lies inside a partial answer or is disjoint from it.

Orderings and the best answers (§4)

@[reducible, inline]

abbrev Boylan2023.PropOrdering (W : Type u_2) : Type u_2

An ordering of propositions at a world, ord w p q for p ≾ q, p at least as good as q; context supplies it, from value for a deontic and from probability or normality for an epistemic ought.

Equations

• Boylan2023.PropOrdering W = (W → Finset W → Finset W → Prop)

def Boylan2023.Better {W : Type u_1} (ord : PropOrdering W) (w : W) (q p : Finset W) : Prop

q ≺ p: q is strictly better than p.

Equations

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

@[instance_reducible]

instance Boylan2023.instDecidableBetter {W : Type u_1} (ord : PropOrdering W) [(w : W) → DecidableRel (ord w)] (w : W) (q p : Finset W) : Decidable (Better ord w q p)

Equations

• Boylan2023.instDecidableBetter ord w q p = { decide := decide (ord w q p) && decide ¬ord w p q, reflects_decide := ⋯ }

def Boylan2023.PBEST {W : Type u_1} [DecidableEq W] (ord : PropOrdering W) [(w : W) → DecidableRel (ord w)] (w : W) {acc : Finset W} (Q : Finpartition acc) : Finset (Finset W)

(70): the propositionally best partial answers, those no partial answer strictly betters.

Equations

• Boylan2023.PBEST ord w Q = {p ∈ Boylan2023.partialAnswers Q | ∀ q ∈ Boylan2023.partialAnswers Q, ¬Boylan2023.Better ord w q p}

def Boylan2023.Defined {W : Type u_1} [DecidableEq W] (ord : PropOrdering W) [(w : W) → DecidableRel (ord w)] (w : W) {acc : Finset W} (Q : Finpartition acc) : Prop

(71a): ought is defined only if the best answers are pairwise consistent with the background information.

Equations

• Boylan2023.Defined ord w Q = ∀ p ∈ Boylan2023.PBEST ord w Q, ∀ q ∈ Boylan2023.PBEST ord w Q, (p ∩ q).Nonempty

def Boylan2023.Ought {W : Type u_1} [DecidableEq W] (ord : PropOrdering W) [(w : W) → DecidableRel (ord w)] (w : W) {acc : Finset W} (Q : Finpartition acc) (φ : W → Prop) : Prop

(71b): ⌜ought φ⌝, some best answer entails φ.

Equations

• Boylan2023.Ought ord w Q φ = ∃ p ∈ Boylan2023.PBEST ord w Q, ∀ v ∈ p, φ v

def Boylan2023.IsDeontic {W : Type u_1} [DecidableEq W] (ord : PropOrdering W) (w : W) {acc : Finset W} (Q : Finpartition acc) : Prop

Assumption 2, the half Fact 2 uses: inside every partial answer some complete answer is at least as good as it.

Equations

• Boylan2023.IsDeontic ord w Q = ∀ p ∈ Boylan2023.partialAnswers Q, ∃ q ∈ Q.parts, q ⊆ p ∧ ord w q p

@[instance_reducible]

instance Boylan2023.instDecidableDefined {W : Type u_1} [DecidableEq W] (ord : PropOrdering W) [(w : W) → DecidableRel (ord w)] (w : W) {acc : Finset W} (Q : Finpartition acc) : Decidable (Defined ord w Q)

Equations

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

@[instance_reducible]

instance Boylan2023.instDecidableOughtOfDecidablePred {W : Type u_1} [DecidableEq W] (ord : PropOrdering W) [(w : W) → DecidableRel (ord w)] (w : W) {acc : Finset W} (Q : Finpartition acc) (φ : W → Prop) [DecidablePred φ] : Decidable (Ought ord w Q φ)

Equations

• Boylan2023.instDecidableOughtOfDecidablePred ord w Q φ = { decide := decide (∃ (a : Finset W) (_ : a ∈ Boylan2023.PBEST ord w Q), (fun (p : Finset W) => ∀ v ∈ p, φ v) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Boylan2023.instDecidableIsDeontic {W : Type u_1} [DecidableEq W] (ord : PropOrdering W) [(w : W) → DecidableRel (ord w)] (w : W) {acc : Finset W} (Q : Finpartition acc) : Decidable (IsDeontic ord w Q)

Equations

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

theorem Boylan2023.mem_PBEST {W : Type u_1} [DecidableEq W] {ord : PropOrdering W} [(w : W) → DecidableRel (ord w)] {w : W} {acc : Finset W} {Q : Finpartition acc} {p : Finset W} : p ∈ PBEST ord w Q ↔ p ∈ partialAnswers Q ∧ ∀ q ∈ partialAnswers Q, ¬Better ord w q p

Inheritance and dilemmas (§3.3, §8.1, §10)

theorem Boylan2023.inheritance {W : Type u_1} [DecidableEq W] {ord : PropOrdering W} [(w : W) → DecidableRel (ord w)] {w : W} {acc : Finset W} {Q : Finpartition acc} {φ ψ : W → Prop} (h : ∀ (v : W), φ v → ψ v) (hφ : Ought ord w Q φ) : Ought ord w Q ψ

Inheritance: an ought passes to whatever its prejacent entails.

theorem Boylan2023.no_dilemma {W : Type u_1} [DecidableEq W] {ord : PropOrdering W} [(w : W) → DecidableRel (ord w)] {w : W} {acc : Finset W} {Q : Finpartition acc} {φ : W → Prop} (hdef : Defined ord w Q) (h₁ : Ought ord w Q φ) (h₂ : Ought ord w Q fun (x : W) => ¬φ x) : False

No dilemma: where ought is defined, ⌜ought φ⌝ and ⌜ought ¬φ⌝ are never both true, since their witnesses share a world.

Deontic ought is a box (Facts 2–4)

theorem Boylan2023.not_better_of_le {W : Type u_1} [DecidableEq W] {ord : PropOrdering W} {w : W} {acc : Finset W} {Q : Finpartition acc} [IsTrans (Finset W) (ord w)] {p q : Finset W} (hp : ∀ r ∈ partialAnswers Q, ¬Better ord w r p) (hqp : ord w q p) (r : Finset W) : r ∈ partialAnswers Q → ¬Better ord w r q

Anything at least as good as an undominated answer is undominated.

theorem Boylan2023.fact2 {W : Type u_1} [DecidableEq W] {ord : PropOrdering W} [(w : W) → DecidableRel (ord w)] {w : W} {acc : Finset W} {Q : Finpartition acc} [IsTrans (Finset W) (ord w)] (hdeon : IsDeontic ord w Q) (hdef : Defined ord w Q) (hne : (PBEST ord w Q).Nonempty) : ∃ q ∈ Q.parts, q ∈ PBEST ord w Q ∧ ∀ q' ∈ Q.parts, q' ∈ PBEST ord w Q → q' = q

Fact 2: under a deontic transitive ordering whose ought is defined, exactly one complete answer is best.

theorem Boylan2023.fact3 {W : Type u_1} [DecidableEq W] {ord : PropOrdering W} [(w : W) → DecidableRel (ord w)] {w : W} {acc : Finset W} {Q : Finpartition acc} {q : Finset W} (hq : q ∈ Q.parts) (hqb : q ∈ PBEST ord w Q) (hdef : Defined ord w Q) (φ : W → Prop) : Ought ord w Q φ ↔ ∀ v ∈ q, φ v

Fact 3: with a best complete answer q and ought defined, ⌜ought φ⌝ holds exactly when φ holds throughout q, the classic entry (59) relativized to q.

theorem Boylan2023.fact4 {W : Type u_1} [DecidableEq W] {ord : PropOrdering W} [(w : W) → DecidableRel (ord w)] {w : W} {acc : Finset W} {Q : Finpartition acc} [IsTrans (Finset W) (ord w)] (hdeon : IsDeontic ord w Q) (hdef : Defined ord w Q) (hne : (PBEST ord w Q).Nonempty) {φ ψ : W → Prop} (hφ : Ought ord w Q φ) (hψ : Ought ord w Q ψ) : Ought ord w Q fun (v : W) => φ v ∧ ψ v

Fact 4: deontic oughts agglomerate.

Epistemic orderings from a threshold (§8.1)

def Boylan2023.threshold {W : Type u_1} (μ : W → ℕ) (T : ℕ) : PropOrdering W

The epistemic ordering of §8.1: p ≾ q when p passes the threshold, or is at least as likely as q. Worlds carry weights and the threshold is half the information's weight.

Equations

• Boylan2023.threshold μ T x✝ p q = (T < 2 * p.sum μ ∨ q.sum μ ≤ p.sum μ)

@[instance_reducible]

instance Boylan2023.instDecidableRelFinsetThreshold {W : Type u_1} (μ : W → ℕ) (T : ℕ) (w : W) : DecidableRel (threshold μ T w)

Equations

• Boylan2023.instDecidableRelFinsetThreshold μ T w p q = { decide := decide (T < 2 * p.sum μ) || decide (q.sum μ ≤ p.sum μ), reflects_decide := ⋯ }

theorem Boylan2023.inter_nonempty_of_half_lt {W : Type u_1} [DecidableEq W] {μ : W → ℕ} {acc p q : Finset W} (hp : p ⊆ acc) (hq : q ⊆ acc) (h₁ : acc.sum μ < 2 * p.sum μ) (h₂ : acc.sum μ < 2 * q.sum μ) : (p ∩ q).Nonempty

Two propositions each likelier than not overlap: the pairwise consistency of the best answers is a consequence of probability theory.

theorem Boylan2023.mem_PBEST_threshold {W : Type u_1} [DecidableEq W] {μ : W → ℕ} {T : ℕ} {acc : Finset W} {Q : Finpartition acc} {w : W} (hex : ∃ q ∈ partialAnswers Q, T < 2 * q.sum μ) {p : Finset W} : p ∈ PBEST (threshold μ T) w Q ↔ p ∈ partialAnswers Q ∧ T < 2 * p.sum μ

Once some partial answer passes the threshold, the best answers are exactly those that do: a threshold ordering ranks every one of them above every complete answer below it.

theorem Boylan2023.defined_threshold {W : Type u_1} [DecidableEq W] {μ : W → ℕ} {T : ℕ} {acc : Finset W} {Q : Finpartition acc} {w : W} (hT : acc.sum μ = T) (hex : ∃ q ∈ partialAnswers Q, T < 2 * q.sum μ) : Defined (threshold μ T) w Q

The definedness condition holds for a threshold ordering at half the information's weight.

The conflict account (61)

def Boylan2023.MaxConsistent {W : Type u_1} [DecidableEq W] [Fintype W] (props S : Finset (Finset W)) : Prop

The maximal contextually consistent subsets of a set of propositions, D(f(w), g(w)) with the whole space as information (fn. 16).

Equations

• Boylan2023.MaxConsistent props S = (S ⊆ props ∧ (S.inf id).Nonempty ∧ ∀ S' ⊆ props, S ⊂ S' → ¬(S'.inf id).Nonempty)

@[instance_reducible]

instance Boylan2023.instDecidableMaxConsistent {W : Type u_1} [DecidableEq W] [Fintype W] (props S : Finset (Finset W)) : Decidable (MaxConsistent props S)

Equations

• Boylan2023.instDecidableMaxConsistent props S = { decide := decide (S ⊆ props) && decide ((S.inf id).Nonempty ∧ ∀ S' ⊆ props, S ⊂ S' → ¬(S'.inf id).Nonempty), reflects_decide := ⋯ }

def Boylan2023.ConflictOught {W : Type u_1} [DecidableEq W] [Fintype W] (props : Finset (Finset W)) (φ : W → Prop) : Prop

(61): the conflict account ([vF12], [Hor12]), ⌜ought φ⌝ iff some maximal consistent subset of the best propositions entails φ.

Equations

• Boylan2023.ConflictOught props φ = ∃ S ∈ props.powerset, Boylan2023.MaxConsistent props S ∧ ∀ v ∈ S.inf id, φ v

@[instance_reducible]

instance Boylan2023.instDecidableConflictOughtOfDecidablePred {W : Type u_1} [DecidableEq W] [Fintype W] (props : Finset (Finset W)) (φ : W → Prop) [DecidablePred φ] : Decidable (ConflictOught props φ)

Equations

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

The classic semantics (59)

theorem Boylan2023.classic_agglomerates {W : Type u_1} {f g : Modality.Background W} {φ ψ : W → Prop} {w : W} (hφ : Modality.necessity f g φ w) (hψ : Modality.necessity f g ψ w) : Modality.necessity f g (φ ⊓ ψ) w

The classic entry (59), Kratzer necessity over the best worlds, agglomerates unconditionally, so it cannot fit The Office for any modal base and ordering source.

The Office (§8.1)

@[reducible, inline]

abbrev Boylan2023.Office.World : Type

A world of The Office with two workers: whether Alice and whether Bob are in.

Equations

• Boylan2023.Office.World = (Bool × Bool)

def Boylan2023.Office.weight (w : World) : ℕ

Each worker is in with probability two thirds, independently: a world weighs 2 for each worker in and 1 for each out, out of 9.

Equations

• Boylan2023.Office.weight w = (if w.1 = true then 2 else 1) * if w.2 = true then 2 else 1

@[instance_reducible]

instance Boylan2023.Office.instDecidableRelWorldR : DecidableRel ⇑(Setoid.ker id)

Equations

• Boylan2023.Office.instDecidableRelWorldR a b = { decide := decide ((id a).1 = (id b).1) && decide ((id a).2 = (id b).2), reflects_decide := ⋯ }

def Boylan2023.Office.question : Finpartition Finset.univ

The relevance question which workers are in?, every world its own complete answer.

Equations

• Boylan2023.Office.question = Finpartition.ofSetoid (Setoid.ker id)

def Boylan2023.Office.ordering : PropOrdering World

The epistemic ordering: best above the threshold of one half.

Equations

• Boylan2023.Office.ordering = Boylan2023.threshold Boylan2023.Office.weight 9

@[instance_reducible]

instance Boylan2023.Office.instDecidableRelFinsetWorldOrdering (w : World) : DecidableRel (ordering w)

Equations

• Boylan2023.Office.instDecidableRelFinsetWorldOrdering w = Boylan2023.Office.instDecidableRelFinsetWorldOrdering._aux_1 w

def Boylan2023.Office.aliceIn (w : World) : Prop

Equations

• Boylan2023.Office.aliceIn w = (w.1 = true)

def Boylan2023.Office.bobIn (w : World) : Prop

Equations

• Boylan2023.Office.bobIn w = (w.2 = true)

@[instance_reducible]

instance Boylan2023.Office.instDecidablePredWorldAliceIn : DecidablePred aliceIn

Equations

• Boylan2023.Office.instDecidablePredWorldAliceIn w = Boylan2023.Office.instDecidablePredWorldAliceIn._aux_1 w

@[instance_reducible]

instance Boylan2023.Office.instDecidablePredWorldBobIn : DecidablePred bobIn

Equations

• Boylan2023.Office.instDecidablePredWorldBobIn w = Boylan2023.Office.instDecidablePredWorldBobIn._aux_1 w

theorem Boylan2023.Office.defined : Defined ordering (true, true) question

ought is defined in The Office: the best answers are pairwise consistent.

theorem Boylan2023.Office.alice_should_be_in : Ought ordering (true, true) question aliceIn

(2): Alice should be in the office today.

theorem Boylan2023.Office.bob_should_be_in : Ought ordering (true, true) question bobIn

(3): Bob should be in the office today.

theorem Boylan2023.Office.not_everyone_should_be_in : ¬Ought ordering (true, true) question fun (v : World) => aliceIn v ∧ bobIn v

(6) is false: no best answer entails that everyone is in.

theorem Boylan2023.Office.not_alice_should_be_out : ¬Ought ordering (true, true) question fun (x : World) => ¬aliceIn x

(66) is false: no best answer entails that Alice is absent.

theorem Boylan2023.Office.not_isDeontic : ¬IsDeontic ordering (true, true) question

Assumption 3: the epistemic ordering violates the deontic constraint, Alice is in outranking every complete answer inside it.

theorem Boylan2023.Office.fact5 : ∃ (ord : PropOrdering World) (x : (w : World) → DecidableRel (ord w)) (w : World) (Q : Finpartition Finset.univ) (φ : World → Prop) (ψ : World → Prop), Defined ord w Q ∧ Ought ord w Q φ ∧ Ought ord w Q ψ ∧ ¬Ought ord w Q fun (v : World) => φ v ∧ ψ v

Fact 5: parameters on which two oughts are true and their conjunction false.

def Boylan2023.Office.conflictBest : Finset (Finset World)

The conflict account's best propositions for The Office: each worker in, and not everyone in.

Equations

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

theorem Boylan2023.Office.conflict_everyone_in : ConflictOught conflictBest fun (v : World) => aliceIn v ∧ bobIn v

On the conflict account (6) comes out true: the set of everyone in is maximal consistent.

theorem Boylan2023.Office.conflict_dilemma : ConflictOught conflictBest aliceIn ∧ ConflictOught conflictBest fun (x : World) => ¬aliceIn x

(67): the conflict account makes (2) and (66) both true, a dilemma The Office does not involve.

Dessert (§8.2)

inductive Boylan2023.Dessert.World : Type

The outcomes: one of the three desserts, or illness from more than one.

• pie : World
• cannoli : World
• cake : World
• ill : World

@[instance_reducible]

instance Boylan2023.Dessert.instDecidableEqWorld : DecidableEq World

Equations

• Boylan2023.Dessert.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Boylan2023.Dessert.instFintypeWorld : Fintype World

Equations

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

@[instance_reducible]

instance Boylan2023.Dessert.instReprWorld : Repr World

Equations

• Boylan2023.Dessert.instReprWorld = { reprPrec := Boylan2023.Dessert.instReprWorld.repr }

def Boylan2023.Dessert.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

def Boylan2023.Dessert.value : World → ℕ

Pie and cannoli are tastiest, cheesecake less so, illness worst.

Equations

• Boylan2023.Dessert.value Boylan2023.Dessert.World.pie = 3
• Boylan2023.Dessert.value Boylan2023.Dessert.World.cannoli = 3
• Boylan2023.Dessert.value Boylan2023.Dessert.World.cake = 2
• Boylan2023.Dessert.value Boylan2023.Dessert.World.ill = 0

def Boylan2023.Dessert.worst (p : Finset World) : WithTop ℕ

The worst outcome a proposition allows.

Equations

• Boylan2023.Dessert.worst p = p.inf fun (v : Boylan2023.Dessert.World) => ↑(Boylan2023.Dessert.value v)

def Boylan2023.Dessert.ordering : PropOrdering World

The deontic ordering: a proposition is at least as good as another when its worst outcome is.

Equations

• Boylan2023.Dessert.ordering x✝ p q = (Boylan2023.Dessert.worst q ≤ Boylan2023.Dessert.worst p)

@[instance_reducible]

instance Boylan2023.Dessert.instDecidableRelFinsetWorldOrdering (w : World) : DecidableRel (ordering w)

Equations

• Boylan2023.Dessert.instDecidableRelFinsetWorldOrdering w p q = Boylan2023.Dessert.instDecidableRelFinsetWorldOrdering._aux_1 w p q

@[instance_reducible]

instance Boylan2023.Dessert.instDecidableRelWorldR : DecidableRel ⇑(Setoid.ker id)

Equations

• Boylan2023.Dessert.instDecidableRelWorldR a b = Boylan2023.Dessert.instDecidableEqWorld (id a) (id b)

@[instance_reducible]

instance Boylan2023.Dessert.instDecidableRelWorldR_1 : DecidableRel ⇑(Setoid.ker value)

Equations

• Boylan2023.Dessert.instDecidableRelWorldR_1 a b = { decide := (Boylan2023.Dessert.value a).beq (Boylan2023.Dessert.value b), reflects_decide := ⋯ }

def Boylan2023.Dessert.what : Finpartition Finset.univ

The relevance question what will I do?, every outcome its own complete answer.

Equations

• Boylan2023.Dessert.what = Finpartition.ofSetoid (Setoid.ker id)

def Boylan2023.Dessert.howGood : Finpartition Finset.univ

The relevance question how good will the action I perform be?, outcomes of equal value lumped together.

Equations

• Boylan2023.Dessert.howGood = Finpartition.ofSetoid (Setoid.ker Boylan2023.Dessert.value)

theorem Boylan2023.Dessert.isDeontic : IsDeontic ordering World.pie what ∧ IsDeontic ordering World.pie howGood

The ordering is deontic for either question.

theorem Boylan2023.Dessert.what_undefined : ¬Defined ordering World.pie what

Under what will I do? the best answers, pie and cannoli, are inconsistent, so ought is undefined: only the coarser question is a possible parameter.

theorem Boylan2023.Dessert.howGood_defined : Defined ordering World.pie howGood

Under how good? ought is defined.

theorem Boylan2023.Dessert.indifference : (Ought ordering World.pie howGood fun (v : World) => v = World.pie ∨ v = World.cannoli) ∧ (¬Ought ordering World.pie howGood fun (x : World) => x = World.pie) ∧ ¬Ought ordering World.pie howGood fun (x : World) => x = World.cannoli

Indifference: I ought to have pie or cannoli, and neither I ought to have pie nor I ought to have cannoli.

theorem Boylan2023.Dessert.ought_iff (φ : World → Prop) : Ought ordering World.pie howGood φ ↔ ∀ v ∈ {World.pie, World.cannoli}, φ v

Deontic ought is a box: under how good? the unique best complete answer is pie or cannoli, and ⌜ought φ⌝ holds exactly when φ does throughout it (Fact 3).