Lassiter (2017): Graded Modality

This file formalizes chapters 4 to 8 of Lassiter.

Chapters 4 to 6 place the epistemic adjectives and auxiliaries on one scale. Likely and probable measure a proposition by its probability, on a scale bounded below by the likelihood of a contradiction and above by that of a tautology (likelihood_univ, ofOrder_probability), and they are relative adjectives on it. Certain takes the scale's maximum as its standard and possible its minimum, so the three are Kennedy's three positive forms on one closed scale (mem_likely_iff_relativePos, mem_certain_iff_maxStandardPos, mem_possible_iff_minStandardPos). A relative adjective on a closed scale is what Kennedy's Interpretive Economy excludes, Degree.Boundedness.Admits, and what the book's own typology (4.58) allows: likely is the counter-example of p. 82 (coherent_and_not_admits_contextual_probability). The distribution of completely and slightly, which Kennedy reads off the scale, the book reads off the positive form (§4.2.9); Kennedy's licensing is the book's quantified over the standards Interpretive Economy admits (licenses_iff_exists_admits), so the two disagree exactly on adjectives like likely, which license neither (not_licensesPos_contextual).

The auxiliaries are thresholds on the same scale (6.29), Lassiter 2015's probMust and probMight, and at threshold one they are the adjectives certain and possible (mem_possible_iff_not_mem_certain_compl). The ordering of the five thresholds of p. 152 makes every item entail every weaker one (antitone_pos), and the strong theory, a must at probability one, conflicts with that ordering (not_strictMono_of_strong), as does a might at probability zero (not_strictMono_of_might_zero); with a positive threshold might is strictly stronger than possible (exists_mem_possible_not_mem_might).

Chapters 7 and 8 give the scalar semantics of good and ought. Goodness is expected value, the probability-weighted average of world values over a proposition (Desire.ExpectedValue.expectedValue); it is an interval scale and intermediate on disjoint unions. Ought is constrained rather than defined (Constraints): Sloman's Principle relates it to goodness (an obligatory proposition is strictly better than each of its alternatives, after Sloman), the Smith Principle restricts agglomeration to exhaustive pairs, and Weakening closes obligation under disjunction. Sloman's Principle alone excludes conflicting oughts, ought φ together with ought ¬φ (Constraints.not_compl), and the Smith Principle carries the Smith argument from ought (M ∨ S) and ought ¬M to ought S (Smith.ought_S), on a sample model that meets the Sloman requirements of all three. On Cariani's four-world counter-model to Weakening, where A and B each beat their negations in expected value but A ∨ B ties with its negation, Sloman's Principle and Weakening together make ought A and ought B incompatible (Cariani.not_ought_and). The scalar reading of ought as a threshold on an intermediate scale derives Weakening and, given ought-exclusivity, the Smith Principle; both derivations live with the expected-value substrate.

Implementation notes

Probabilities are probability measures read on their real values, as in Lassiter 2015, and the probability scale is the closed real unit interval. The p. 82 claim that the likelihood scale, if connected, is isomorphic to a finitely additive probability holds of these measures by construction; its measurement-theoretic direction, from the axioms listed on p. 97 to a measure, is not formalized, and the tower's own representation theorem uses Scott's cancellation condition rather than those axioms. The book states the threshold ordering twice: strictly on p. 152, θ_possible < θ_might < θ_likely < θ_must < θ_certain, which StrictMono records, and on p. 156 with θ_possible = θ_might. That the Disjunctive Inference fails on the probability scale, and that more likely than does not entail might, are Lassiter 2015's Lassiter2015.prob_refutes_rightUnion and Lassiter2015.weak_refutes_moreLikely_might.

For chapters 7 and 8, the goodness scale and the alternative sets of the constraint set are parameters; the consequences take the needed alternative memberships as hypotheses, the polar sets {φ, ¬φ} being the book's weakest choice. The counter-model instantiates the scale by expected value over an equiprobable domain of four worlds indexed by the truth values of A and B.

TODO

• The measurement-theoretic representation of p. 82 and p. 97, and its generalization to sets of measures when connectedness fails.
• The certainty scales of Analyses 2 and 3 (§5.1.6, §5.1.7), the first a half-open interval (Degree.Boundedness.ofOrder_Ioc) or a log transform.
• The experiment of §6.5 as Data/Experiments, and the modifier judgments of §4.2 as examples.

References

• [Las17a]
• [Ken07b]
• [Las15]
• [Sco64]
• [Car16]
• [Slo70]

Chapter 4: the likelihood scale

@[reducible, inline]

abbrev Lassiter2017.Probability : Type

The probability scale, the closed unit interval, on which likely and probable measure propositions (§4.1).

Equations

• Lassiter2017.Probability = ↑(Set.Icc 0 1)

noncomputable def Lassiter2017.likelihood {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] (A : Set W) : Probability

A proposition's degree of likelihood is its probability.

Equations

• Lassiter2017.likelihood P A = ⟨P.real A, ⋯⟩

@[simp]

theorem Lassiter2017.coe_likelihood {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] (A : Set W) : ↑(likelihood P A) = P.real A

@[simp]

theorem Lassiter2017.likelihood_univ {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] : likelihood P Set.univ = ⊤

Nothing is likelier than a tautology (p. 84).

@[simp]

theorem Lassiter2017.likelihood_empty {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure P] : likelihood P ∅ = ⊥

Nothing is less likely than a contradiction (p. 84).

theorem Lassiter2017.ofOrder_probability : Degree.Boundedness.ofOrder Probability = Degree.Boundedness.closed

The probability scale is totally closed (p. 82, p. 97).

Two typologies of standards (§4.2.4–§4.2.6)

def Lassiter2017.Coherent (b : Degree.Boundedness) (s : Degree.PositiveStandard) : Prop

A positive standard admits a scale as in (4.58), where a minimum or maximum standard needs its endpoint and a contextual standard fits any scale. Interpretive Economy, Boundedness.Admits, is (4.59), which confines the contextual standard to open scales.

Equations

• Lassiter2017.Coherent b s = (s = Degree.PositiveStandard.contextual ∨ b.Admits s)

theorem Lassiter2017.coherent_of_admits {b : Degree.Boundedness} {s : Degree.PositiveStandard} (h : b.Admits s) : Coherent b s

What Interpretive Economy admits is coherent.

theorem Lassiter2017.coherent_and_not_admits_contextual {b : Degree.Boundedness} (hb : b ≠ Degree.Boundedness.open_) : Coherent b Degree.PositiveStandard.contextual ∧ ¬b.Admits Degree.PositiveStandard.contextual

The two typologies part exactly at a contextual standard on a scale with an endpoint.

theorem Lassiter2017.coherent_and_not_admits_contextual_probability : Coherent (Degree.Boundedness.ofOrder Probability) Degree.PositiveStandard.contextual ∧ ¬(Degree.Boundedness.ofOrder Probability).Admits Degree.PositiveStandard.contextual

On the probability scale a contextual standard is coherent and Interpretive Economy excludes it, so a relative likely is the counter-example of p. 82.

theorem Lassiter2017.ofOrder_Ioo_zero_one : Degree.Boundedness.ofOrder ↑(Set.Ioo 0 1) = Degree.Boundedness.open_ ∧ 1 ∉ Set.Ioo 0 1

The open-interval alternative of §4.2.6 keeps Interpretive Economy by making the scale (0, 1), which is open, at the cost of a degree for the tautology.

def Lassiter2017.LicensesPos : Kennedy2007.DegreeModifier → Degree.PositiveStandard → Prop

As the book licenses maximizers and minimizers (§4.2.9), completely takes the positive form of a maximum adjective and slightly that of a minimum adjective, whatever the scale.

Equations

• Lassiter2017.LicensesPos Kennedy2007.DegreeModifier.maximizer x✝ = (x✝ = Degree.PositiveStandard.maxEndpoint)
• Lassiter2017.LicensesPos Kennedy2007.DegreeModifier.minimizer x✝ = (x✝ = Degree.PositiveStandard.minEndpoint)

theorem Lassiter2017.licenses_iff_exists_admits (m : Kennedy2007.DegreeModifier) (b : Degree.Boundedness) : Kennedy2007.Licenses m b ↔ ∃ (s : Degree.PositiveStandard), b.Admits s ∧ LicensesPos m s

[Ken07b]'s licensing by the scale is the book's licensing by the positive form, quantified over the standards Interpretive Economy admits on the scale.

theorem Lassiter2017.not_licensesPos_contextual (m : Kennedy2007.DegreeModifier) : ¬LicensesPos m Degree.PositiveStandard.contextual

A relative adjective licenses neither modifier, whatever its scale, which is why completely likely and slightly likely lack a degree reading on a closed scale ((4.62), (4.63)), where Kennedy's licensing predicts one.

The epistemic adjectives on one scale (§4.2.2, §5.1.5, §5.2.5)

def Lassiter2017.likely {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : ℝ) : Set (Set W)

Likely and probable are relative adjectives, true above a contextual threshold.

Equations

• Lassiter2017.likely P θ = P.real ⁻¹' Set.Ioi θ

def Lassiter2017.certain {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) : Set (Set W)

Certain and sure take the maximum standard of the probability scale (§5.1.5).

Equations

• Lassiter2017.certain P = P.real ⁻¹' Set.Ici 1

def Lassiter2017.possible {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) : Set (Set W)

Possible takes the minimum standard of the probability scale (§5.2.5).

Equations

• Lassiter2017.possible P = P.real ⁻¹' Set.Ioi 0

theorem Lassiter2017.mem_possible_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} : A ∈ possible P ↔ 0 < P.real A

theorem Lassiter2017.certain_subset_likely {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {θ : ℝ} (hθ : θ < 1) : certain P ⊆ likely P θ

Certainty entails likelihood (§5.1.4).

theorem Lassiter2017.likely_subset_possible {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {θ : ℝ} (hθ : 0 ≤ θ) : likely P θ ⊆ possible P

Likelihood entails possibility (§5.2.3).

theorem Lassiter2017.mem_certain_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [MeasureTheory.IsProbabilityMeasure P] : A ∈ certain P ↔ P.real A = 1

theorem Lassiter2017.mem_likely_iff_relativePos {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [MeasureTheory.IsProbabilityMeasure P] (θ : Probability) : A ∈ likely P ↑θ ↔ Kennedy2007.RelativePos (likelihood P) θ A

Likely is [Ken07b]'s relative positive form on the probability scale.

theorem Lassiter2017.mem_certain_iff_maxStandardPos {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [MeasureTheory.IsProbabilityMeasure P] : A ∈ certain P ↔ Kennedy2007.MaxStandardPos (likelihood P) A

Certain is Kennedy's maximum-standard positive form on the probability scale.

theorem Lassiter2017.mem_possible_iff_minStandardPos {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [MeasureTheory.IsProbabilityMeasure P] : A ∈ possible P ↔ Kennedy2007.MinStandardPos (likelihood P) A

Possible is Kennedy's minimum-standard positive form on the probability scale.

theorem Lassiter2017.mem_possible_iff_not_mem_certain_compl {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [MeasureTheory.IsProbabilityMeasure P] [DiscreteMeasurableSpace W] : A ∈ possible P ↔ Aᶜ ∉ certain P

Certain and possible are [Las15]'s must and might at threshold one, the strong auxiliaries (p. 156), and so duals, A being possible iff its negation is not certain.

def Lassiter2017.percent {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (n : ℝ) : Set (Set W)

n percent A compares the degree with the scale's maximum (4.51b).

Equations

• Lassiter2017.percent P n = {A : Set W | P.real A / P.real Set.univ = n / 100}

theorem Lassiter2017.mem_percent_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [MeasureTheory.IsProbabilityMeasure P] (n : ℝ) : A ∈ percent P n ↔ P.real A = n / 100

n percent likely is interpretable because the maximum is a degree of the scale (p. 121–122).

theorem Lassiter2017.mem_percent_fifty_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [MeasureTheory.IsProbabilityMeasure P] [DiscreteMeasurableSpace W] : A ∈ percent P 50 ↔ P.real A = P.real Aᶜ

Fifty percent likely is "exactly as likely as not" (p. 103).

Chapter 6: the thresholds

inductive Lassiter2017.EpistemicItem : Type

The five epistemic items of the ordering on p. 152, weakest first.

• possible : EpistemicItem
• might : EpistemicItem
• likely : EpistemicItem
• must : EpistemicItem
• certain : EpistemicItem

@[instance_reducible]

instance Lassiter2017.instDecidableEqEpistemicItem : DecidableEq EpistemicItem

Equations

• Lassiter2017.instDecidableEqEpistemicItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lassiter2017.EpistemicItem.rank : EpistemicItem → Fin 5

The rank of an item in the strength ordering.

Equations

• Lassiter2017.EpistemicItem.possible.rank = 0
• Lassiter2017.EpistemicItem.might.rank = 1
• Lassiter2017.EpistemicItem.likely.rank = 2
• Lassiter2017.EpistemicItem.must.rank = 3
• Lassiter2017.EpistemicItem.certain.rank = 4

theorem Lassiter2017.EpistemicItem.rank_injective : Function.Injective rank

@[instance_reducible]

instance Lassiter2017.EpistemicItem.instLinearOrder : LinearOrder EpistemicItem

Equations

• Lassiter2017.EpistemicItem.instLinearOrder = LinearOrder.lift' Lassiter2017.EpistemicItem.rank Lassiter2017.EpistemicItem.rank_injective

def Lassiter2017.EpistemicItem.comparison : EpistemicItem → Degree.Comparison

Must and certain compare the probability weakly with their thresholds, might, likely and possible strictly (6.29).

Equations

• Lassiter2017.EpistemicItem.must.comparison = Degree.Comparison.ge
• Lassiter2017.EpistemicItem.certain.comparison = Degree.Comparison.ge
• Lassiter2017.EpistemicItem.possible.comparison = Degree.Comparison.gt
• Lassiter2017.EpistemicItem.might.comparison = Degree.Comparison.gt
• Lassiter2017.EpistemicItem.likely.comparison = Degree.Comparison.gt

def Lassiter2017.pos {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : EpistemicItem → ℝ) (i : EpistemicItem) : Set (Set W)

The positive form of an item under a profile of thresholds.

Equations

• Lassiter2017.pos P θ i = P.real ⁻¹' i.comparison.interval (θ i)

theorem Lassiter2017.mem_pos_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : EpistemicItem → ℝ) {A : Set W} (i : EpistemicItem) : A ∈ pos P θ i ↔ i.comparison.Rel (P.real A) (θ i)

theorem Lassiter2017.mem_pos_must_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : EpistemicItem → ℝ) {A : Set W} : A ∈ pos P θ EpistemicItem.must ↔ Lassiter2015.probMust P (θ EpistemicItem.must) A

(6.29a) is [Las15]'s must.

theorem Lassiter2017.mem_pos_might_iff {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : EpistemicItem → ℝ) {A : Set W} [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] (hdual : θ EpistemicItem.might = 1 - θ EpistemicItem.must) : A ∈ pos P θ EpistemicItem.might ↔ Aᶜ ∉ pos P θ EpistemicItem.must

(6.29b) with the duality θ_might = 1 − θ_must of p. 156 is [Las15]'s might, so might A holds iff must ¬A fails.

theorem Lassiter2017.pos_certain {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : EpistemicItem → ℝ) (h : θ EpistemicItem.certain = 1) : pos P θ EpistemicItem.certain = certain P

At threshold one certain is its positive form.

theorem Lassiter2017.pos_possible {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : EpistemicItem → ℝ) (h : θ EpistemicItem.possible = 0) : pos P θ EpistemicItem.possible = possible P

At threshold zero possible is its positive form.

theorem Lassiter2017.antitone_pos {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) (θ : EpistemicItem → ℝ) (hθ : StrictMono θ) : Antitone (pos P θ)

The ordering of p. 152 makes the positive forms antitone in strength, so certain entails must (§6.1), must entails likely (6.14), likely entails might (6.18), and might entails possible (§6.5).

theorem Lassiter2017.compl_lt_of_mem_must {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] {θ' : ℝ} (hθ : 1 / 2 < θ') (h : A ∈ P.real ⁻¹' Set.Ici θ') : P.real Aᶜ < P.real A

Must A leaves ¬A at most 1 − θ_must likely, so above one half A is more likely than its negation (6.16).

theorem Lassiter2017.mem_might_of_compl_lt {W : Type u_1} [MeasurableSpace W] (P : MeasureTheory.Measure W) {A : Set W} [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure P] {θ' : ℝ} (hθ : θ' ≤ 1 / 2) (h : P.real Aᶜ < P.real A) : A ∈ P.real ⁻¹' Set.Ioi θ'

What is more likely than not is a might, given θ_might ≤ 1/2 (6.19).

theorem Lassiter2017.must_lt_certain_iff_possible_lt_might (θ : EpistemicItem → ℝ) (hmm : θ EpistemicItem.might = 1 - θ EpistemicItem.must) (hcp : θ EpistemicItem.possible = 1 - θ EpistemicItem.certain) : θ EpistemicItem.must < θ EpistemicItem.certain ↔ θ EpistemicItem.possible < θ EpistemicItem.might

Under the dualities of must and might and of certain and possible, certain is stronger than must iff might is stronger than possible (p. 164).

theorem Lassiter2017.not_strictMono_of_strong (θ : EpistemicItem → ℝ) (h : θ EpistemicItem.must = 1) (hc : θ EpistemicItem.certain ≤ 1) : ¬StrictMono θ

The strong theory, a must at probability one, conflicts with the ordering of p. 152 when no threshold exceeds the tautology's degree, since must cannot then be weaker than certain (§6.1).

theorem Lassiter2017.not_strictMono_of_might_zero (θ : EpistemicItem → ℝ) (h : θ EpistemicItem.might = 0) (hp : 0 ≤ θ EpistemicItem.possible) : ¬StrictMono θ

Likewise a might at probability zero cannot be stronger than possible (p. 152).

theorem Lassiter2017.exists_mem_possible_not_mem_might {θ : ℝ} (h0 : 0 < θ) (h1 : θ ≤ 1) : ∃ (P : MeasureTheory.Measure (Fin 2)), MeasureTheory.IsProbabilityMeasure P ∧ ∃ A ∈ possible P, A ∉ P.real ⁻¹' Set.Ioi θ

With a positive threshold, might is strictly stronger than possible (§6.5), since a proposition of probability exactly θ is possible and not a might.

structure Lassiter2017.Constraints {W : Type u_1} (μ : Set W → ℝ) (ought : Set W → Prop) (alt : Set W → Set (Set W)) : Prop

The constraints on ought relative to a goodness scale μ and alternative sets alt are Sloman's Principle, the Smith Principle, and Weakening.

• sloman ⦃φ : Set W⦄ : ought φ → ∀ ψ ∈ alt φ, ψ ≠ φ → μ ψ < μ φ
• smith ⦃φ ψ : Set W⦄ : φ ∪ ψ = Set.univ → ought φ → ought ψ → ought (φ ∩ ψ)
• weakening ⦃φ ψ : Set W⦄ : ought φ → ought ψ → ought (φ ∪ ψ)

theorem Lassiter2017.Constraints.not_compl {W : Type u_1} {μ : Set W → ℝ} {ought : Set W → Prop} {alt : Set W → Set (Set W)} [Nonempty W] (h : Constraints μ ought alt) {φ : Set W} (hφ : φᶜ ∈ alt φ) (hφ' : φ ∈ alt φᶜ) (h₁ : ought φ) : ¬ought φᶜ

A proposition and its negation, each an alternative to the other, cannot both be obligatory.

theorem Lassiter2017.Constraints.not_and_of_le {W : Type u_1} {μ : Set W → ℝ} {ought : Set W → Prop} {alt : Set W → Set (Set W)} [Nonempty W] (h : Constraints μ ought alt) {φ ψ : Set W} (hne : (φ ∪ ψ)ᶜ ∈ alt (φ ∪ ψ)) (hle : μ (φ ∪ ψ) ≤ μ (φ ∪ ψ)ᶜ) : ¬(ought φ ∧ ought ψ)

Weakening carries a failure of Sloman's Principle at a disjunction, one no better than its negation, back to the disjuncts.

noncomputable def Lassiter2017.goodness {W : Type u_1} [MeasurableSpace W] (pr : MeasureTheory.Measure W) (V : W → ℝ) (φ : Set W) : ℝ

Goodness as expected value over the whole domain, the book's default prob(D) = 1.

Equations

• Lassiter2017.goodness pr V φ = Desire.ExpectedValue.expectedValue pr V Set.univ φ

The Smith scenario

inductive Lassiter2017.Smith : Type

Smith can do military service, alternative service, or neither.

• military : Smith
• service : Smith
• neither : Smith

@[instance_reducible]

instance Lassiter2017.instDecidableEqSmith : DecidableEq Smith

Equations

• Lassiter2017.instDecidableEqSmith x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lassiter2017.Smith.instFintype : Fintype Smith

Equations

• Lassiter2017.Smith.instFintype = { elems := {Lassiter2017.Smith.military, Lassiter2017.Smith.service, Lassiter2017.Smith.neither}, complete := ⋯ }

@[instance_reducible]

instance Lassiter2017.Smith.instMeasurableSpace : MeasurableSpace Smith

Equations

• Lassiter2017.Smith.instMeasurableSpace = ⊤

instance Lassiter2017.Smith.instMeasurableSingletonClass : MeasurableSingletonClass Smith

def Lassiter2017.Smith.M : Set Smith

Smith serves in the military.

Equations

• Lassiter2017.Smith.M = {Lassiter2017.Smith.military}

def Lassiter2017.Smith.S : Set Smith

Smith performs alternative service.

Equations

• Lassiter2017.Smith.S = {Lassiter2017.Smith.service}

@[reducible, inline]

noncomputable abbrev Lassiter2017.Smith.prior : MeasureTheory.Measure Smith

The sample model's prior makes the three options equiprobable.

Equations

• Lassiter2017.Smith.prior = ProbabilityTheory.uniformOn Set.univ

def Lassiter2017.Smith.value : Smith → ℝ

In the sample model only alternative service is worth anything.

Equations

• w.value = if w = Lassiter2017.Smith.service then 1 else 0

theorem Lassiter2017.Smith.sloman : goodness prior value (M ∪ S)ᶜ < goodness prior value (M ∪ S) ∧ goodness prior value M < goodness prior value Mᶜ ∧ goodness prior value Sᶜ < goodness prior value S

The sample model meets the Sloman requirements of the premises ought (M ∨ S) and ought ¬M and of the conclusion ought S.

theorem Lassiter2017.Smith.ought_S {μ : Set Smith → ℝ} {ought : Set Smith → Prop} {alt : Set Smith → Set (Set Smith)} (h : Constraints μ ought alt) (h₁ : ought (M ∪ S)) (h₂ : ought Mᶜ) : ought S

In the Smith argument, the Smith Principle agglomerates the exhaustive premises to ought S.

Cariani's counter-model to Weakening

@[reducible, inline]

abbrev Lassiter2017.Cariani.World : Type

Four equiprobable worlds, indexed by the truth values of A and B.

Equations

• Lassiter2017.Cariani.World = (Bool × Bool)

@[reducible, inline]

noncomputable abbrev Lassiter2017.Cariani.prior : MeasureTheory.Measure World

The uniform prior.

Equations

• Lassiter2017.Cariani.prior = ProbabilityTheory.uniformOn Set.univ

def Lassiter2017.Cariani.value : World → ℝ

A world is worth 100 at A ∧ B, -50 at A ∧ ¬B and ¬A ∧ B, and 0 at ¬A ∧ ¬B.

Equations

• Lassiter2017.Cariani.value (true, true) = 100
• Lassiter2017.Cariani.value (true, false) = -50
• Lassiter2017.Cariani.value (false, true) = -50
• Lassiter2017.Cariani.value (false, false) = 0

def Lassiter2017.Cariani.A : Set World

The proposition A.

Equations

• Lassiter2017.Cariani.A = {w : Lassiter2017.Cariani.World | w.1 = true}

def Lassiter2017.Cariani.B : Set World

The proposition B.

Equations

• Lassiter2017.Cariani.B = {w : Lassiter2017.Cariani.World | w.2 = true}

theorem Lassiter2017.Cariani.goodness_A : goodness prior value A = 25

theorem Lassiter2017.Cariani.goodness_compl_A : goodness prior value Aᶜ = -25

theorem Lassiter2017.Cariani.goodness_B : goodness prior value B = 25

theorem Lassiter2017.Cariani.goodness_compl_B : goodness prior value Bᶜ = -25

theorem Lassiter2017.Cariani.goodness_union : goodness prior value (A ∪ B) = 0

theorem Lassiter2017.Cariani.goodness_compl_union : goodness prior value (A ∪ B)ᶜ = 0

theorem Lassiter2017.Cariani.sloman : goodness prior value Aᶜ < goodness prior value A ∧ goodness prior value Bᶜ < goodness prior value B

A and B each satisfy Sloman's Principle against their negations.

theorem Lassiter2017.Cariani.not_ought_and {ought : Set World → Prop} {alt : Set World → Set (Set World)} (h : Constraints (goodness prior value) ought alt) (halt : (A ∪ B)ᶜ ∈ alt (A ∪ B)) : ¬(ought A ∧ ought B)

Sloman's Principle and Weakening make ought A and ought B incompatible, since the disjunction ties with its negation.