Cariani (2013): 'Ought' and resolution semantics

This file formalizes [Car13]'s resolution semantics for ought. Reading ought as a universal quantifier over the best worlds validates INHERITANCE, closure of ought under entailment of the prejacent, and the paper takes the classical counterexamples at face value: Joan ought to attend her classes does not entail Joan ought to either attend her classes or burn down the philosophy department ([Ros44]), and Procrastinate ought to accept and write the review does not entail Procrastinate ought to accept ([JP86]). The account keeps COARSENESS, on which an ought-sentence can be true although some way of making its prejacent true is impermissible, by relativizing ought to a resolution: a partition of the modal base into the agent's options (Setoid W), an ordering of the options, and a benchmark below which an option is impermissible (ResolutionContext). Ought p holds when the resolution decides p, every best option entails p, and every option entailing p meets the benchmark (Ought), so that one impermissible option compatible with the prejacent falsifies the sentence, the paper's COARSE FALSEMAKING (not_ought_of_not_meetsBenchmark), while impermissible ways of p that no option distinguishes leave it true.

Both puzzles refute INHERITANCE (not_inheritance_ross, not_inheritance_proc). Permission has two candidate entries, some option at the benchmark entails p or some best option does (Permitted₁, Permitted₂); ought entails both, both are closed under entailment, and since that closure together with the duality of ought and permission would restore INHERITANCE (inheritance_of_dual), ought is the dual of neither. A boxing semantics is the special case of the finest resolution with a benchmark every option meets (ought_bot_iff).

Implementation notes

• The ordering on options is a valuation of worlds in a preordered scale that the resolution decides, so that it ranks options, with the benchmark a threshold of the scale; this is neutral between the ranking and quantitative scales the paper allows, and the best options are the MaximalFor elements of the valuation. The paper's examples value an option at the rank of its best world (ofRanking).
• The resolution partitions the modal base itself, so the modal base is not a separate parameter and the ordering does not vary with it. The paper's third puzzle, conditional oughts under the restrictor analysis of conditionals, needs the modal base and is not formalized.
• Visibility is Setoid.Decides, the resolution settling the prejacent.

References

• [Car13]
• [Ros44]
• [JP86]
• [Kra81b]

structure Cariani2013.ResolutionContext (W : Type u_3) (V : Type u_4) : Type (max u_3 u_4)

A resolution context: the resolution, a partition of the modal base into the agent's options; the ordering, a valuation of worlds that the resolution decides, so that it ranks options; and the benchmark, the threshold of the scale below which an option is impermissible.

• resolution : Setoid W

  The resolution: worlds in one cell realize the same option.

• value : W → V

  The ordering: the value of a world's option in the scale.

• value_decided : self.resolution ≤ Setoid.ker self.value

  The valuation is constant on options.

• benchmark : V

  The benchmark: the least permissible value.

def Cariani2013.ResolutionContext.ofRanking {W : Type u_1} {V : Type u_2} [Fintype W] [SemilatticeSup V] [OrderBot V] (s : Setoid W) [DecidableRel ⇑s] (rank : W → V) (benchmark : V) : ResolutionContext W V

The context of a ranked action space: an option is valued at the rank of its best world.

Equations

• Cariani2013.ResolutionContext.ofRanking s rank benchmark = { resolution := s, value := fun (w : W) => {x : W | s x w}.sup rank, value_decided := ⋯, benchmark := benchmark }

The clauses

@[reducible, inline]

abbrev Cariani2013.ResolutionContext.IsVisible {W : Type u_1} {V : Type u_2} (rc : ResolutionContext W V) (p : Set W) : Prop

p is visible when the resolution decides it: each option entails p or its negation.

Equations

• rc.IsVisible p = rc.resolution.Decides p

def Cariani2013.ResolutionContext.MeetsBenchmark {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (w : W) : Prop

An option meets the benchmark when its value is at least the benchmark.

Equations

• rc.MeetsBenchmark w = (rc.benchmark ≤ rc.value w)

def Cariani2013.ResolutionContext.IsBest {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (w : W) : Prop

An option is best when no option is strictly better.

Equations

• rc.IsBest w = MaximalFor (fun (x : W) => True) rc.value w

def Cariani2013.ResolutionContext.IsOptimal {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) : Prop

p is optimal when every best option entails it.

Equations

• rc.IsOptimal p = ∀ (w : W), rc.IsBest w → rc.resolution.cell w ⊆ p

def Cariani2013.ResolutionContext.IsStronglyPermissible {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) : Prop

p is strongly permissible when every option that entails it meets the benchmark.

Equations

• rc.IsStronglyPermissible p = ∀ (w : W), rc.resolution.cell w ⊆ p → rc.MeetsBenchmark w

The operators

def Cariani2013.ResolutionContext.Ought {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) : Prop

Ought p: p is visible, optimal, and strongly permissible.

Equations

• rc.Ought p = (rc.IsVisible p ∧ rc.IsOptimal p ∧ rc.IsStronglyPermissible p)

def Cariani2013.ResolutionContext.Permitted₁ {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) : Prop

Permitted p, first entry: some option that entails p meets the benchmark.

Equations

• rc.Permitted₁ p = ∃ (w : W), rc.resolution.cell w ⊆ p ∧ rc.MeetsBenchmark w

def Cariani2013.ResolutionContext.Permitted₂ {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) : Prop

Permitted p, second entry: some best option entails p.

Equations

• rc.Permitted₂ p = ∃ (w : W), rc.IsBest w ∧ rc.resolution.cell w ⊆ p

def Cariani2013.ResolutionContext.Inheritance {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) : Prop

INHERITANCE: ought is closed under entailment of the prejacent.

Equations

• rc.Inheritance = ∀ (p q : Set W), p ⊆ q → rc.Ought p → rc.Ought q

@[instance_reducible]

instance Cariani2013.ResolutionContext.instDecidableMeetsBenchmark {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) [DecidableRel fun (x1 x2 : V) => x1 ≤ x2] (w : W) : Decidable (rc.MeetsBenchmark w)

Equations

• rc.instDecidableMeetsBenchmark w = Cariani2013.ResolutionContext.instDecidableMeetsBenchmark._aux_1 rc w

@[instance_reducible]

instance Cariani2013.ResolutionContext.instDecidableIsBest {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) [Fintype W] [DecidableRel fun (x1 x2 : V) => x1 ≤ x2] (w : W) : Decidable (rc.IsBest w)

Equations

• rc.instDecidableIsBest w = { decide := decide True && decide (∀ (x : W), True → rc.value w ≤ rc.value x → rc.value x ≤ rc.value w), reflects_decide := ⋯ }

@[instance_reducible]

instance Cariani2013.ResolutionContext.instDecidableIsOptimal {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) [Fintype W] [DecidableRel ⇑rc.resolution] [DecidableRel fun (x1 x2 : V) => x1 ≤ x2] [DecidablePred fun (x : W) => x ∈ p] : Decidable (rc.IsOptimal p)

Equations

• rc.instDecidableIsOptimal p = { decide := decide (∀ a ∈ Finset.univ, (fun (x : W) => rc.IsBest x → rc.resolution.cell x ⊆ p) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Cariani2013.ResolutionContext.instDecidableIsStronglyPermissible {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) [Fintype W] [DecidableRel ⇑rc.resolution] [DecidableRel fun (x1 x2 : V) => x1 ≤ x2] [DecidablePred fun (x : W) => x ∈ p] : Decidable (rc.IsStronglyPermissible p)

Equations

• rc.instDecidableIsStronglyPermissible p = { decide := decide (∀ a ∈ Finset.univ, (fun (x : W) => rc.resolution.cell x ⊆ p → rc.MeetsBenchmark x) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Cariani2013.ResolutionContext.instDecidableOught {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) [Fintype W] [DecidableRel ⇑rc.resolution] [DecidableRel fun (x1 x2 : V) => x1 ≤ x2] [DecidablePred fun (x : W) => x ∈ p] : Decidable (rc.Ought p)

Equations

• rc.instDecidableOught p = { decide := decide (rc.IsVisible p) && decide (rc.IsOptimal p ∧ rc.IsStronglyPermissible p), reflects_decide := ⋯ }

@[instance_reducible]

instance Cariani2013.ResolutionContext.instDecidablePermitted₁ {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) [Fintype W] [DecidableRel ⇑rc.resolution] [DecidableRel fun (x1 x2 : V) => x1 ≤ x2] [DecidablePred fun (x : W) => x ∈ p] : Decidable (rc.Permitted₁ p)

Equations

• rc.instDecidablePermitted₁ p = { decide := decide (∃ a ∈ Finset.univ, (fun (x : W) => rc.resolution.cell x ⊆ p ∧ rc.MeetsBenchmark x) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Cariani2013.ResolutionContext.instDecidablePermitted₂ {W : Type u_1} {V : Type u_2} [Preorder V] (rc : ResolutionContext W V) (p : Set W) [Fintype W] [DecidableRel ⇑rc.resolution] [DecidableRel fun (x1 x2 : V) => x1 ≤ x2] [DecidablePred fun (x : W) => x ∈ p] : Decidable (rc.Permitted₂ p)

Equations

• rc.instDecidablePermitted₂ p = { decide := decide (∃ a ∈ Finset.univ, (fun (x : W) => rc.IsBest x ∧ rc.resolution.cell x ⊆ p) a), reflects_decide := ⋯ }

Coarse falsemaking and permission

theorem Cariani2013.ResolutionContext.not_ought_of_not_meetsBenchmark {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} {p : Set W} {w : W} (hp : rc.resolution.cell w ⊆ p) (h : ¬rc.MeetsBenchmark w) : ¬rc.Ought p

COARSE FALSEMAKING: one option below the benchmark that entails p falsifies ought p, however good the other options are.

theorem Cariani2013.ResolutionContext.exists_isBest {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} [Finite W] [Nonempty W] : ∃ (w : W), rc.IsBest w

Some option is best as soon as there are options.

theorem Cariani2013.ResolutionContext.Ought.permitted₂ {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} {p : Set W} [Finite W] [Nonempty W] (ho : rc.Ought p) : rc.Permitted₂ p

What one ought to do some best option does.

theorem Cariani2013.ResolutionContext.Ought.permitted₁ {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} {p : Set W} [Finite W] [Nonempty W] (ho : rc.Ought p) : rc.Permitted₁ p

What one ought to do is permitted: a best option does it by optimality and meets the benchmark by strong permissibility.

theorem Cariani2013.ResolutionContext.Permitted₁.mono {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} {p q : Set W} (hpq : p ⊆ q) : rc.Permitted₁ p → rc.Permitted₁ q

PI: permission is closed under entailment of the prejacent, on either entry.

theorem Cariani2013.ResolutionContext.Permitted₂.mono {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} {p q : Set W} (hpq : p ⊆ q) : rc.Permitted₂ p → rc.Permitted₂ q

The boxing special case

theorem Cariani2013.ResolutionContext.ought_bot_iff {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} {p : Set W} (h : rc.resolution = ⊥) (hb : ∀ (w : W), rc.MeetsBenchmark w) : rc.Ought p ↔ ∀ (w : W), rc.IsBest w → w ∈ p

On the finest resolution with every option at the benchmark, ought p is quantification over the best worlds: the boxing semantics is a resolution semantics.

Duality

theorem Cariani2013.inheritance_of_dual {W : Type u_1} {O P : Set W → Prop} (hd : ∀ (p : Set W), O p ↔ ¬P pᶜ) (hP : ∀ (p q : Set W), p ⊆ q → P p → P q) {p q : Set W} (hpq : p ⊆ q) (hp : O p) : O q

DUALITY of an operator with a permission closed under entailment yields INHERITANCE.

theorem Cariani2013.ResolutionContext.not_dual₁ {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} (h : ¬rc.Inheritance) : ¬∀ (p : Set W), rc.Ought p ↔ ¬rc.Permitted₁ pᶜ

Where INHERITANCE fails, ought is not the dual of benchmark permission.

theorem Cariani2013.ResolutionContext.not_dual₂ {W : Type u_1} {V : Type u_2} [Preorder V] {rc : ResolutionContext W V} (h : ¬rc.Inheritance) : ¬∀ (p : Set W), rc.Ought p ↔ ¬rc.Permitted₂ pᶜ

Where INHERITANCE fails, ought is not the dual of best-option permission.

Ross's paradox

inductive Cariani2013.RossW : Type

Joan's three courses of action.

• attend : RossW
• stayHome : RossW
• burn : RossW

@[instance_reducible]

instance Cariani2013.instDecidableEqRossW : DecidableEq RossW

Equations

• Cariani2013.instDecidableEqRossW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cariani2013.instFintypeRossW : Fintype RossW

Equations

• Cariani2013.instFintypeRossW = { elems := { val := ↑Cariani2013.RossW.enumList, nodup := Cariani2013.RossW.enumList_nodup }, complete := Cariani2013.instFintypeRossW._proof_1 }

def Cariani2013.rossRank : RossW → ℕ

Attending is best, staying home next, burning down the department worst.

Equations

• Cariani2013.rossRank Cariani2013.RossW.attend = 3
• Cariani2013.rossRank Cariani2013.RossW.stayHome = 2
• Cariani2013.rossRank Cariani2013.RossW.burn = 1

def Cariani2013.rossContext : ResolutionContext RossW ℕ

Joan's context: each action its own option, the benchmark at staying home, so that burning down the department is the one impermissible option.

Equations

• Cariani2013.rossContext = Cariani2013.ResolutionContext.ofRanking ⊥ Cariani2013.rossRank 2

@[instance_reducible]

instance Cariani2013.instDecidableRelRossWR : DecidableRel ⇑rossContext.resolution

Equations

• Cariani2013.instDecidableRelRossWR a b = Setoid.instDecidableRelROfDecidableEq_linglib a b

theorem Cariani2013.ross_ought_attend : rossContext.Ought {RossW.attend}

Joan ought to attend her classes is true.

theorem Cariani2013.ross_disjunction_visible_not_permissible : rossContext.IsVisible {RossW.attend, RossW.burn} ∧ ¬rossContext.IsStronglyPermissible {RossW.attend, RossW.burn}

The disjunction is visible, so only the permissibility clause rejects it: burning down the department entails attend or burn and is below the benchmark.

theorem Cariani2013.ross_not_ought_disjunction : ¬rossContext.Ought {RossW.attend, RossW.burn}

Joan ought to either attend her classes or burn down the philosophy department is false.

theorem Cariani2013.ross_stayHome_permitted_not_ought : rossContext.Permitted₁ {RossW.stayHome} ∧ ¬rossContext.Ought {RossW.stayHome}

Staying home is permitted but not obligatory: it is at the benchmark and not best.

theorem Cariani2013.not_inheritance_ross : ¬rossContext.Inheritance

Ross's paradox refutes INHERITANCE.

theorem Cariani2013.not_dual_ross : (¬∀ (p : Set RossW), rossContext.Ought p ↔ ¬rossContext.Permitted₁ pᶜ) ∧ ¬∀ (p : Set RossW), rossContext.Ought p ↔ ¬rossContext.Permitted₂ pᶜ

And so ought is the dual of neither permission.

Procrastinate

inductive Cariani2013.ProcW : Type

Procrastinate's three courses of action ([JP86]): accepting the review and writing it, declining it, and accepting without writing.

• acceptWrite : ProcW
• decline : ProcW
• acceptNoWrite : ProcW

@[instance_reducible]

instance Cariani2013.instDecidableEqProcW : DecidableEq ProcW

Equations

• Cariani2013.instDecidableEqProcW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cariani2013.instFintypeProcW : Fintype ProcW

Equations

• Cariani2013.instFintypeProcW = { elems := { val := ↑Cariani2013.ProcW.enumList, nodup := Cariani2013.ProcW.enumList_nodup }, complete := Cariani2013.instFintypeProcW._proof_1 }

def Cariani2013.procRank : ProcW → ℕ

Accepting and writing is best; declining is better than accepting and not writing, which is what Procrastinate would in fact do.

Equations

• Cariani2013.procRank Cariani2013.ProcW.acceptWrite = 3
• Cariani2013.procRank Cariani2013.ProcW.decline = 2
• Cariani2013.procRank Cariani2013.ProcW.acceptNoWrite = 1

def Cariani2013.procContext : ResolutionContext ProcW ℕ

Procrastinate's context, with the benchmark at declining.

Equations

• Cariani2013.procContext = Cariani2013.ResolutionContext.ofRanking ⊥ Cariani2013.procRank 2

@[instance_reducible]

instance Cariani2013.instDecidableRelProcWR : DecidableRel ⇑procContext.resolution

Equations

• Cariani2013.instDecidableRelProcWR a b = Setoid.instDecidableRelROfDecidableEq_linglib a b

theorem Cariani2013.proc_ought_acceptWrite : procContext.Ought {ProcW.acceptWrite}

Procrastinate ought to accept and write the review is true.

theorem Cariani2013.proc_not_ought_accept : ¬procContext.Ought {ProcW.acceptWrite, ProcW.acceptNoWrite}

Procrastinate ought to accept is false: accepting without writing is a way of accepting and is below the benchmark.

theorem Cariani2013.not_inheritance_proc : ¬procContext.Inheritance

Procrastinate refutes INHERITANCE too, on a prejacent weakened by an impermissible option rather than by a disjunct.

Jenny's ways to school

inductive Cariani2013.Mode : Type

Jenny's ways to school.

• running : Mode
• walking : Mode
• swimming : Mode
• driving : Mode

@[instance_reducible]

instance Cariani2013.instDecidableEqMode : DecidableEq Mode

Equations

• Cariani2013.instDecidableEqMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cariani2013.instFintypeMode : Fintype Mode

Equations

• Cariani2013.instFintypeMode = { elems := { val := ↑Cariani2013.Mode.enumList, nodup := Cariani2013.Mode.enumList_nodup }, complete := Cariani2013.instFintypeMode._proof_1 }

def Cariani2013.jennyRank : Mode → ℕ

Running is best, walking and swimming tie, driving is worst.

Equations

• Cariani2013.jennyRank Cariani2013.Mode.running = 3
• Cariani2013.jennyRank Cariani2013.Mode.walking = 2
• Cariani2013.jennyRank Cariani2013.Mode.swimming = 2
• Cariani2013.jennyRank Cariani2013.Mode.driving = 1

@[reducible, inline]

abbrev Cariani2013.mode (m : Mode) : Set (Mode × Bool)

The proposition that Jenny goes to school by m; a world also records whether she has a cup of coffee, which the resolution ignores.

Equations

• Cariani2013.mode m = {w : Cariani2013.Mode × Bool | w.1 = m}

def Cariani2013.jennyContext : ResolutionContext (Mode × Bool) ℕ

Jenny's context: the ways to school as options, coffee below the resolution, and the benchmark between walking and driving, so that driving is the one impermissible option.

Equations

• Cariani2013.jennyContext = Cariani2013.ResolutionContext.ofRanking (Setoid.ker Prod.fst) (fun (x : Cariani2013.Mode × Bool) => Cariani2013.jennyRank x.1) 2

@[instance_reducible]

instance Cariani2013.instDecidableRelProdModeBoolR : DecidableRel ⇑jennyContext.resolution

Equations

• Cariani2013.instDecidableRelProdModeBoolR = Cariani2013.instDecidableRelProdModeBoolR._aux_1

theorem Cariani2013.jenny_ought_running : jennyContext.Ought (mode Mode.running)

Running is permissible, optimal, and strongly permissible, so Jenny ought to run.

theorem Cariani2013.jenny_running_or_driving : jennyContext.Permitted₁ (mode Mode.running ∪ mode Mode.driving) ∧ jennyContext.IsOptimal (mode Mode.running ∪ mode Mode.driving) ∧ ¬jennyContext.IsStronglyPermissible (mode Mode.running ∪ mode Mode.driving)

Running or driving is permissible and optimal but not strongly permissible.

theorem Cariani2013.jenny_swimming_or_driving : jennyContext.Permitted₁ (mode Mode.swimming ∪ mode Mode.driving) ∧ ¬jennyContext.IsOptimal (mode Mode.swimming ∪ mode Mode.driving) ∧ ¬jennyContext.IsStronglyPermissible (mode Mode.swimming ∪ mode Mode.driving)

Swimming or driving is permissible but neither strongly permissible nor optimal.

theorem Cariani2013.jenny_visible : jennyContext.IsVisible (mode Mode.running ∪ mode Mode.walking) ∧ ¬jennyContext.IsVisible {w : Mode × Bool | w.2 = true}

Running or walking is visible in Jenny's resolution; having a cup of coffee is not.