Condoravdi and Lauer 2016: anankastic conditionals are just conditionals

Condoravdi and Lauer argue that If you want to go to Harlem, you have to take the A train is a regular hypothetical indicative conditional: the problem Sæbø found, that the antecedent goal must enter the ordering of the modal, and the one von Fintel and Iatridou and von Stechow, Krasikova and Penka added, that conflicting actual goals must not, are both resolved by the lexical meanings involved once want reports an action-relevant preference. On that reading want says its complement is a maximal element of the agent's effective preference structure, a strict partial order on propositions that is consistent with the agent's beliefs, so hypothesizing a preference for Harlem hypothesizes the absence of every preference the agent knows to be incompatible with it. The conditional has the double-modal structure of Frank, a covert necessity over the speaker's beliefs, ordered by stereotypicality and restricted by the antecedent, with the priority modal over the historical alternatives in its scope, whose ordering source at each world is the agent's maximal effective preferences there. The same setting covers the near-anankastics of strengthened goals, teleological consequences and specializations, which differ from anankastics only in the pragmatic implication that the temporal relation of goal and prejacent invites; reading want or the modal differently gives the non-anankastic and deontic cases.

Main statements

• conditionalNecessity_orderingSource_iff: under consistent effective preferences the paraphrase (89) of (88) is exact.
• HobokenScenario.anankastic_harlem, HobokenScenario.not_possibility_path: in the Hoboken scenario the Harlem sentence (1) is true and (14) false, where Sæbø's analysis makes (1) false and (14) true, and the mere-desire construal makes (1) false.
• VladivostokScenario.haveTo_chinese_comfortFirst, VaccineScenario.should_vaccine: compatible goals enter the ordering, so the ranking of comfort and cost decides (92), and a second maximal preference makes the near-anankastic (29b) true.
• AirportScenario.should_train, AirportScenario.should_ride: the double-modal readings of (83a) and (83b) are both true, where single-modal ones cannot be.

Implementation notes

• Both modals are Kratzer's necessity, as (88) says. The priority modal's ordering source is orderingSource P a, the maximal preferences of P a v at each world v, so an anankastic is conditionalNecessity with no operator of its own, and Sæbø's rival restricts the same ordering source where the paper restricts the outer modal base.
• The effective preferences are taken consistent relative to the historical alternatives, which (66) relative to the agent's beliefs gives when those beliefs lie among them; it keeps out the atypical continuations the paper leaves to a separate mechanism.
• Each scenario is a small model with its own world type. In the Hoboken scenario the speaker is uncertain about the addressee's goal, with an empty stereotypical ordering, so the Harlem sentence is true through its antecedent worlds rather than vacuously.

TODO

• Informal in the paper and not formalized: the temporal interpretation of the internal antecedent and the prejacent, the pragmatic derivation of the means-of implication, the strong/weak modal contrast of (96) and (97), purpose constructions, informational asymmetry, the consistency of the double-modal readings of (81) and (82), and the closure condition that would validate conjunction introduction for effective preferences.

References

• C. Condoravdi and S. Lauer, Anankastic conditionals are just conditionals (2016)
• C. Condoravdi and S. Lauer, Performative verbs and performative acts (2011)
• K. J. Sæbø, Necessary conditions in a natural language (2001)
• K. von Fintel and S. Iatridou, What to do if you want to go to Harlem: Anankastic conditionals and related matters (2005)
• A. von Stechow, S. Krasikova and D. Penka, Anankastic conditionals again (2006)
• J. Huitink, Modals, conditionals and compositionality (2008)
• A. Frank, Context dependence in modal constructions (1996)
• S. Kaufmann and M. Schwager, A unified analysis of conditional imperatives (2009)
• R. M. Hare, Wanting: Some pitfalls (1971)
• D. Levinson, Probabilistic model-theoretic semantics for want (2003)
• T. E. Zimmermann, Monotonicity in opaque verbs (2006)
• A. Kratzer, The notional category of modality (1981)

The semantics of want

Want P a p w is (69): p is a maximal element of the structure P a w that a preferential background assigns to a at w, (68); the effective preference structure is the consistent and realistic one that guides action, (66) and (67), realism derivable from consistency, PreferenceStructure.Consistent.realistic, footnote 30. WantSufficient and WantNecessary are the success-oriented and Quine–Hintikka alternatives of (71), after [Zim06], downward and upward entailing, WantSufficient.anti and WantNecessary.mono. The mere-desire and effective readings that [Har71] and [Lev03] observe are two backgrounds for one predicate.

theorem CondoravdiLauer2016.not_monotone_want {W : Type u_2} {w : W} [Nontrivial W] : ¬Monotone fun (x : Set W) => Desire.Preferential.Want (fun (x : Unit) (x_1 : W) => PreferenceStructure.single {w}) () x w

Exact-match want, (71c), is not upward entailing in its complement, §5.5: the single preference {w} is not a preference for Set.univ.

theorem CondoravdiLauer2016.not_antitone_want {W : Type u_2} {w : W} [Nontrivial W] : ¬Antitone fun (x : Set W) => Desire.Preferential.Want (fun (x : Unit) (x_1 : W) => PreferenceStructure.single Set.univ) () x w

Nor is it downward entailing, since the single preference Set.univ is not a preference for {w}.

theorem CondoravdiLauer2016.want_both {W : Type u_2} {w : W} (p q : Set W) : Desire.Preferential.Want (fun (x : Unit) (x_1 : W) => PreferenceStructure.discrete {p, q}) () p w ∧ Desire.Preferential.Want (fun (x : Unit) (x_1 : W) => PreferenceStructure.discrete {p, q}) () q w

On a background that need not be consistent, wanting p and wanting q are compatible even when p and q are not, as on the mere-desire reading of (52) and (53), §2.3 and §5.4.

theorem CondoravdiLauer2016.no_third_effective {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {p q : Set W} {w : W} {B : W → Set W} {r : Set W} (hC : (P a w).Consistent (B w)) (hp : Desire.Preferential.Want P a p w) (hq : Desire.Preferential.Want P a q w) (hr : Desire.Preferential.Want P a r w) : (B w ∩ (p ∩ q ∩ r)).Nonempty

In Levinson's Paris and Rome, (56) and (58), on the effective reading, §5.2, two effective preferences leave no room for a third that is incompatible with their conjunction, since the maximal elements of a consistent structure are jointly compatible with the agent's beliefs.

def CondoravdiLauer2016.threeWay : PreferenceStructure (Fin 3)

Three unranked preferences over three worlds, pairwise compatible but jointly inconsistent.

Equations

• CondoravdiLauer2016.threeWay = PreferenceStructure.discrete {{w : Fin 3 | w ≠ 2}, {w : Fin 3 | w ≠ 0}, {w : Fin 3 | w ≠ 1}}

theorem CondoravdiLauer2016.threeWay_pairwise_not_consistent : (∀ p ∈ threeWay.prefs, ∀ q ∈ threeWay.prefs, (p ∩ q).Nonempty) ∧ ¬threeWay.Consistent Set.univ

By footnote 29, consistency (66) is stronger than pairwise compatibility, which is what the weaker version of [CL11] leaves.

Previous approaches

theorem CondoravdiLauer2016.necessity_designatedGoal_iff_haveTo {W : Type u_2} {w : W} {f : Modality.Background W} {p r : W → Prop} (h : ((f.restrict p).accessibleWorlds w).Nonempty) : Modality.necessity f (fun (x : W) => {p}) r w ↔ VonFintelIatridou2005.haveTo f p r w

[vFI05]'s have to on the reading (26), §3.2.2, is necessity under the primary ordering source g_desG(w) = {p} of the designated goal. A single proposition has the effect of adding it to the modal base, as long as the two are compatible, so this is the designated-goal have to of that study and the analysis amounts to adding the internal antecedent to the modal base; the effective-preference source of (88) instead varies from world to world, footnote 46.

Double-modal structure

theorem CondoravdiLauer2016.single_modal_strengthening {W : Type u_2} {w : W} {f g : Modality.Background W} {α β γ : W → Prop} (h₁ : Conditional.Restrictor.conditionalNecessity f g α γ w) (h₂ : Conditional.Restrictor.conditionalNecessity f g (fun (v : W) => α v ∧ β v) (fun (v : W) => ¬γ v) w) (u : W) : u ∈ Modality.bestWorlds (f.restrict α) g w → ¬β u

A single necessity modal restricted by the antecedent validates strengthening of the antecedent in the form [KS09] reject, §6.2: if A, must C and if A and B, must not C together entail that no best A-world is a B-world, a preference against B that (81) to (83) do not carry. The double-modal structure (76b) escapes, since each conditional's inner modal is evaluated in its own typical antecedent worlds.

The analysis

def CondoravdiLauer2016.orderingSource {A : Type u_1} {W : Type u_2} (P : A → W → PreferenceStructure W) (a : A) : Modality.Background W

On its teleological construal, §7.1, the priority modal is ordered at each world v by the maximal preferences of P a v, so that orderingSource EP a is the paper's g_epA.

Equations

• CondoravdiLauer2016.orderingSource P a v = (P a v).maxElts

theorem CondoravdiLauer2016.bestWorlds_orderingSource {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {f : Modality.Background W} {v : W} (hC : (P a v).Consistent (f.accessibleWorlds v)) : Modality.bestWorlds f (orderingSource P a) v = f.accessibleWorlds v ∩ ⋂₀ (P a v).maxElts

Preferences consistent relative to the modal base do not split the best worlds as the ordering source of §2.3 does: the best worlds are the accessible ones realizing every maximal preference.

theorem CondoravdiLauer2016.want_disjoint {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {p q : Set W} {B : W → Set W} (hC : ∀ (w : W), (P a w).Consistent (B w)) (h : ∀ (w : W), B w ∩ (p ∩ q) = ∅) : Disjoint {w : W | Desire.Preferential.Want P a p w} {w : W | Desire.Preferential.Want P a q w}

By (90), under consistency, an effective preference for p excludes one for any q the agent believes incompatible with p.

theorem CondoravdiLauer2016.not_want_of_mem_restricted {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {p q : Set W} {w : W} {B : W → Set W} {f : Modality.Background W} (hC : ∀ (w : W), (P a w).Consistent (B w)) (h : ∀ (w : W), B w ∩ (p ∩ q) = ∅) {v : W} (hv : v ∈ (f.restrict (Desire.Preferential.Want P a p)).accessibleWorlds w) : ¬Desire.Preferential.Want P a q v

The antecedent's restriction removes every world with a conflicting effective preference, §7.1.1, so an actual preference for Hoboken never reaches the priority modal.

theorem CondoravdiLauer2016.conditionalNecessity_orderingSource_iff {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {q : Set W} {w : W} {f₁ g₁ f₂ : Modality.Background W} {α : W → Prop} (hC : ∀ v ∈ Modality.bestWorlds (f₁.restrict α) g₁ w, (P a v).Consistent (f₂.accessibleWorlds v)) : Conditional.Restrictor.conditionalNecessity f₁ g₁ α (Modality.necessity f₂ (orderingSource P a) fun (x : W) => x ∈ q) w ↔ ∀ v ∈ Modality.bestWorlds (f₁.restrict α) g₁ w, f₂.accessibleWorlds v ∩ ⋂₀ (P a v).maxElts ⊆ q

Under consistency the paraphrase (89) is exact: the conditional (88) holds when, at every most typical belief world where the antecedent holds, the historical alternatives that realize all of the agent's maximal effective preferences are q-worlds. With want in the antecedent the hypothesized preference is among them, since want and the modal read the same background, and compatible goals such as comfort in (92) stay beside it. Consistency relative to the historical alternatives follows from (66) relative to the agent's beliefs whenever those beliefs lie among them, PreferenceStructure.Consistent.mono.

The Hoboken scenario

Von Fintel and Iatridou's stranger on the platform, §2.3 and §7.1.1: the speaker knows the facts about the trains but not the addressee's goal, which is Hoboken.

inductive CondoravdiLauer2016.HobokenScenario.Goal : Type

Where the addressee wants to go.

• harlem : Goal
• hoboken : Goal

@[instance_reducible]

instance CondoravdiLauer2016.HobokenScenario.instDecidableEqGoal : DecidableEq Goal

Equations

• CondoravdiLauer2016.HobokenScenario.instDecidableEqGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CondoravdiLauer2016.HobokenScenario.Train : Type

The two trains.

• aTrain : Train
• path : Train

@[instance_reducible]

instance CondoravdiLauer2016.HobokenScenario.instDecidableEqTrain : DecidableEq Train

Equations

• CondoravdiLauer2016.HobokenScenario.instDecidableEqTrain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure CondoravdiLauer2016.HobokenScenario.World : Type

A world records the addressee's goal, the train taken, and which train goes to Harlem, the other going to Hoboken.

• goal : Goal

  The addressee's effective goal.

• train : Train

  The train the addressee takes.

• harlemTrain : Train

  The train that goes to Harlem.

def CondoravdiLauer2016.HobokenScenario.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CondoravdiLauer2016.HobokenScenario.instDecidableEqWorld : DecidableEq World

Equations

• CondoravdiLauer2016.HobokenScenario.instDecidableEqWorld = CondoravdiLauer2016.HobokenScenario.instDecidableEqWorld.decEq

def CondoravdiLauer2016.HobokenScenario.harlem : Set World

The addressee goes to Harlem.

Equations

• CondoravdiLauer2016.HobokenScenario.harlem = {w : CondoravdiLauer2016.HobokenScenario.World | w.train = w.harlemTrain}

def CondoravdiLauer2016.HobokenScenario.hoboken : Set World

The addressee goes to Hoboken.

Equations

• CondoravdiLauer2016.HobokenScenario.hoboken = {w : CondoravdiLauer2016.HobokenScenario.World | w.train ≠ w.harlemTrain}

def CondoravdiLauer2016.HobokenScenario.aTrain : Set World

The addressee takes the A train.

Equations

• CondoravdiLauer2016.HobokenScenario.aTrain = {w : CondoravdiLauer2016.HobokenScenario.World | w.train = CondoravdiLauer2016.HobokenScenario.Train.aTrain}

def CondoravdiLauer2016.HobokenScenario.path : Set World

The addressee takes the PATH train.

Equations

• CondoravdiLauer2016.HobokenScenario.path = {w : CondoravdiLauer2016.HobokenScenario.World | w.train = CondoravdiLauer2016.HobokenScenario.Train.path}

def CondoravdiLauer2016.HobokenScenario.Goal.dest : Goal → Set World

The proposition a goal is a preference for.

Equations

• CondoravdiLauer2016.HobokenScenario.Goal.harlem.dest = CondoravdiLauer2016.HobokenScenario.harlem
• CondoravdiLauer2016.HobokenScenario.Goal.hoboken.dest = CondoravdiLauer2016.HobokenScenario.hoboken

def CondoravdiLauer2016.HobokenScenario.ep : Unit → (w : World) → PreferenceStructure World

The addressee's effective preference structure is the single preference for the goal.

Equations

• CondoravdiLauer2016.HobokenScenario.ep x✝ w = PreferenceStructure.single w.goal.dest

def CondoravdiLauer2016.HobokenScenario.desire : Unit → World → PreferenceStructure World

The addressee's mere desires are both destinations, unranked, at every world.

Equations

• CondoravdiLauer2016.HobokenScenario.desire x✝¹ x✝ = PreferenceStructure.discrete {CondoravdiLauer2016.HobokenScenario.harlem, CondoravdiLauer2016.HobokenScenario.hoboken}

def CondoravdiLauer2016.HobokenScenario.fBelS : Modality.Background World

The speaker believes that the A train goes to Harlem.

Equations

• CondoravdiLauer2016.HobokenScenario.fBelS x✝ = {fun (v : CondoravdiLauer2016.HobokenScenario.World) => v.harlemTrain = CondoravdiLauer2016.HobokenScenario.Train.aTrain}

def CondoravdiLauer2016.HobokenScenario.fHist : Modality.Background World

In the historical alternatives before boarding the goal and the routes are settled and the train is not.

Equations

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

def CondoravdiLauer2016.HobokenScenario.w₀ : World

The world where the A train goes to Harlem and the addressee, heading for Hoboken, takes the PATH train.

Equations

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

theorem CondoravdiLauer2016.HobokenScenario.consistent_ep (v : World) : (ep () v).Consistent (fHist.accessibleWorlds v)

Every goal is reachable among the historical alternatives.

theorem CondoravdiLauer2016.HobokenScenario.bestWorlds_fHist (v : World) : Modality.bestWorlds fHist (orderingSource ep ()) v = fHist.accessibleWorlds v ∩ v.goal.dest

The best continuations of a world are its historical alternatives that reach the goal.

theorem CondoravdiLauer2016.HobokenScenario.harlem_inter_hoboken : harlem ∩ hoboken = ∅

Nobody reaches both Harlem and Hoboken.

theorem CondoravdiLauer2016.HobokenScenario.w₀_excluded : w₀ ∈ fBelS.accessibleWorlds w₀ ∧ w₀ ∉ (fBelS.restrict (Desire.Preferential.Want ep () harlem)).accessibleWorlds w₀

At the Hoboken world the addressee wants Hoboken, so by (90) not Harlem; the world is in the speaker's belief state and out of the antecedent's restriction of it, §7.1.1, so the actual preference never reaches the priority modal.

theorem CondoravdiLauer2016.HobokenScenario.anankastic_harlem {w : World} : Conditional.Restrictor.conditionalNecessity fBelS ⊥ (Desire.Preferential.Want ep () harlem) (Modality.necessity fHist (orderingSource ep ()) fun (x : World) => x ∈ aTrain) w

The Harlem sentence (1) is true at every world, the Hoboken world included, §7.1.1.

theorem CondoravdiLauer2016.HobokenScenario.anankastic_hoboken {w : World} : Conditional.Restrictor.conditionalNecessity fBelS ⊥ (Desire.Preferential.Want ep () hoboken) (Modality.necessity fHist (orderingSource ep ()) fun (x : World) => x ∈ path) w

The Hoboken sentence (15) is true alongside it.

theorem CondoravdiLauer2016.HobokenScenario.not_possibility_path {w : World} : ¬Conditional.Restrictor.conditionalNecessity fBelS ⊥ (Desire.Preferential.Want ep () harlem) (Modality.possibility fHist (orderingSource ep ()) fun (x : World) => x ∈ path) w

(14), if you want to go to Harlem, you can take the PATH train, is false at every world, §2.3, since the best continuations of every antecedent world reach Harlem, which only the A train does.

theorem CondoravdiLauer2016.HobokenScenario.not_anankastic_desire : ¬Conditional.Restrictor.conditionalNecessity fBelS ⊥ (Desire.Preferential.Want desire () harlem) (Modality.necessity fHist (orderingSource ep ()) fun (x : World) => x ∈ aTrain) w₀

On the mere-desire construal of (105), with desire for want and the modal still ordered by the effective preferences, the Harlem sentence is false at the Hoboken world, §7.2.1: the addressee merely desires Harlem there too, so the antecedent does not exclude the world, and its best continuations take the PATH train. The anankastic reading needs the effective construal of both.

theorem CondoravdiLauer2016.HobokenScenario.saebo_harlem : ¬Modality.necessity fBelS ((orderingSource ep ()).restrict fun (x : World) => x ∈ harlem) (fun (x : World) => x ∈ aTrain) w₀

Sæbø's analysis, §2.3, adds the internal antecedent to the bouletic ordering source, the addressee's actual goals, on the circumstantial base that here coincides with the speaker's beliefs. At the Hoboken world the ordering then holds Harlem and Hoboken, which no world realizes together, so the best worlds split and the Harlem sentence comes out false.

theorem CondoravdiLauer2016.HobokenScenario.saebo_path : Modality.possibility fBelS ((orderingSource ep ()).restrict fun (x : World) => x ∈ harlem) (fun (x : World) => x ∈ path) w₀

On the same analysis (14) comes out true, since some best world takes the PATH train.

Compatible goals and their ranking

Von Stechow, Krasikova and Penka's two trains to Vladivostok, (92): the Chinese train is the more comfortable and here also the dearer. Going, comfort and economy are pairwise compatible but not jointly realizable, so by (66) an effective structure ranks comfort and cost, and the ranking decides whether you have to take the Chinese train is true, §7.1.1.

inductive CondoravdiLauer2016.VladivostokScenario.World : Type

What the addressee does.

• russian : World
• chinese : World
• home : World

@[instance_reducible]

instance CondoravdiLauer2016.VladivostokScenario.instDecidableEqWorld : DecidableEq World

Equations

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

def CondoravdiLauer2016.VladivostokScenario.vladivostok : Set World

The addressee goes to Vladivostok.

Equations

• CondoravdiLauer2016.VladivostokScenario.vladivostok = {w : CondoravdiLauer2016.VladivostokScenario.World | w ≠ CondoravdiLauer2016.VladivostokScenario.World.home}

def CondoravdiLauer2016.VladivostokScenario.comfort : Set World

The addressee does not ride the uncomfortable Russian train.

Equations

• CondoravdiLauer2016.VladivostokScenario.comfort = {w : CondoravdiLauer2016.VladivostokScenario.World | w ≠ CondoravdiLauer2016.VladivostokScenario.World.russian}

def CondoravdiLauer2016.VladivostokScenario.cheap : Set World

The addressee does not pay for the Chinese train.

Equations

• CondoravdiLauer2016.VladivostokScenario.cheap = {w : CondoravdiLauer2016.VladivostokScenario.World | w ≠ CondoravdiLauer2016.VladivostokScenario.World.chinese}

def CondoravdiLauer2016.VladivostokScenario.takeChinese : Set World

The addressee takes the Chinese train.

Equations

• CondoravdiLauer2016.VladivostokScenario.takeChinese = {CondoravdiLauer2016.VladivostokScenario.World.chinese}

def CondoravdiLauer2016.VladivostokScenario.takeRussian : Set World

The addressee takes the Russian train.

Equations

• CondoravdiLauer2016.VladivostokScenario.takeRussian = {CondoravdiLauer2016.VladivostokScenario.World.russian}

theorem CondoravdiLauer2016.VladivostokScenario.vladivostok_ne_comfort : vladivostok ≠ comfort

theorem CondoravdiLauer2016.VladivostokScenario.vladivostok_ne_cheap : vladivostok ≠ cheap

theorem CondoravdiLauer2016.VladivostokScenario.comfort_ne_cheap : comfort ≠ cheap

def CondoravdiLauer2016.VladivostokScenario.prefs : Set (Set World)

The addressee's preferences.

Equations

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

theorem CondoravdiLauer2016.VladivostokScenario.not_consistent_discrete : ¬(PreferenceStructure.discrete prefs).Consistent Set.univ

Unranked, the three preferences are inconsistent, so an effective structure must rank them.

def CondoravdiLauer2016.VladivostokScenario.comfortFirst : Unit → World → PreferenceStructure World

The effective preferences when comfort outranks cost.

Equations

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

def CondoravdiLauer2016.VladivostokScenario.costFirst : Unit → World → PreferenceStructure World

The effective preferences when cost outranks comfort, which is then a mere desire.

Equations

• CondoravdiLauer2016.VladivostokScenario.costFirst x✝¹ x✝ = PreferenceStructure.rankBelow CondoravdiLauer2016.VladivostokScenario.prefs CondoravdiLauer2016.VladivostokScenario.comfort_ne_cheap

theorem CondoravdiLauer2016.VladivostokScenario.haveTo_chinese_comfortFirst {w : World} : Conditional.Restrictor.conditionalNecessity ⊥ ⊥ (Desire.Preferential.Want comfortFirst () vladivostok) (Modality.necessity ⊥ (orderingSource comfortFirst ()) fun (x : World) => x ∈ takeChinese) w

With comfort ranked over cost, (92) is true: the only comfortable way to Vladivostok is the Chinese train.

theorem CondoravdiLauer2016.VladivostokScenario.haveTo_russian_costFirst {w : World} : Conditional.Restrictor.conditionalNecessity ⊥ ⊥ (Desire.Preferential.Want costFirst () vladivostok) (Modality.necessity ⊥ (orderingSource costFirst ()) fun (x : World) => x ∈ takeRussian) w

With cost ranked over comfort the addressee has to take the Russian train instead.

theorem CondoravdiLauer2016.VladivostokScenario.not_haveTo_chinese_costFirst {w : World} : ¬Conditional.Restrictor.conditionalNecessity ⊥ ⊥ (Desire.Preferential.Want costFirst () vladivostok) (Modality.necessity ⊥ (orderingSource costFirst ()) fun (x : World) => x ∈ takeChinese) w

So with cost ranked over comfort (92) is false, the judgment von Fintel and Iatridou report, §7.1.1.

Strengthened goals

The near-anankastic (29b), if you want to travel to that place, you should get a vaccine, §4.1 and §7.1.2: the vaccine is not a precondition for travelling, but with being safe a second maximal effective preference beside travelling, the analysis of (88) makes the conditional true.

inductive CondoravdiLauer2016.VaccineScenario.Trip : Type

Whether the addressee travels there.

• go : Trip
• stay : Trip

@[instance_reducible]

instance CondoravdiLauer2016.VaccineScenario.instDecidableEqTrip : DecidableEq Trip

Equations

• CondoravdiLauer2016.VaccineScenario.instDecidableEqTrip x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CondoravdiLauer2016.VaccineScenario.Shot : Type

Whether the addressee gets the vaccine.

• vaccine : Shot
• none : Shot

@[instance_reducible]

instance CondoravdiLauer2016.VaccineScenario.instDecidableEqShot : DecidableEq Shot

Equations

• CondoravdiLauer2016.VaccineScenario.instDecidableEqShot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure CondoravdiLauer2016.VaccineScenario.World : Type

A world records the trip and the shot.

• trip : Trip

  Whether the addressee travels.

• shot : Shot

  Whether the addressee is vaccinated.

@[instance_reducible]

instance CondoravdiLauer2016.VaccineScenario.instDecidableEqWorld : DecidableEq World

Equations

• CondoravdiLauer2016.VaccineScenario.instDecidableEqWorld = CondoravdiLauer2016.VaccineScenario.instDecidableEqWorld.decEq

def CondoravdiLauer2016.VaccineScenario.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

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

def CondoravdiLauer2016.VaccineScenario.travel : Set World

The addressee travels to that place.

Equations

• CondoravdiLauer2016.VaccineScenario.travel = {w : CondoravdiLauer2016.VaccineScenario.World | w.trip = CondoravdiLauer2016.VaccineScenario.Trip.go}

def CondoravdiLauer2016.VaccineScenario.safe : Set World

The addressee is safe, never travelling unvaccinated.

Equations

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

def CondoravdiLauer2016.VaccineScenario.vaccinated : Set World

The addressee gets the vaccine.

Equations

• CondoravdiLauer2016.VaccineScenario.vaccinated = {w : CondoravdiLauer2016.VaccineScenario.World | w.shot = CondoravdiLauer2016.VaccineScenario.Shot.vaccine}

def CondoravdiLauer2016.VaccineScenario.ep : Unit → World → PreferenceStructure World

The addressee effectively prefers both to travel and to be safe, unranked.

Equations

• CondoravdiLauer2016.VaccineScenario.ep x✝¹ x✝ = PreferenceStructure.discrete {CondoravdiLauer2016.VaccineScenario.travel, CondoravdiLauer2016.VaccineScenario.safe}

def CondoravdiLauer2016.VaccineScenario.strong : Unit → World → PreferenceStructure World

Travelling as the only maximal preference, the strong construal of the antecedent in [Hui08] that a singleton max would derive, footnote 31.

Equations

• CondoravdiLauer2016.VaccineScenario.strong x✝¹ x✝ = PreferenceStructure.single CondoravdiLauer2016.VaccineScenario.travel

theorem CondoravdiLauer2016.VaccineScenario.should_vaccine {w : World} : Conditional.Restrictor.conditionalNecessity ⊥ ⊥ (Desire.Preferential.Want ep () travel) (Modality.necessity ⊥ (orderingSource ep ()) fun (x : World) => x ∈ vaccinated) w

(29b) is true: every continuation realizing both preferences is vaccinated.

theorem CondoravdiLauer2016.VaccineScenario.not_should_vaccine_strong {w : World} : ¬Conditional.Restrictor.conditionalNecessity ⊥ ⊥ (Desire.Preferential.Want strong () travel) (Modality.necessity ⊥ (orderingSource strong ()) fun (x : World) => x ∈ vaccinated) w

On the strong construal (29b) is false, since some way of travelling skips the vaccine.

The double-modal structure at work

The airport sequence (83) of §6.2, where getting a ride is the preferred way and the speaker will not drive while the trains run on time. On the double-modal structure both conditionals are true, the outer modal evaluating (83a) in typical worlds without track repairs; a single modal ordered by the addressee's goals cannot make both true. The addressee's preference for a ride is left out, since the single-modal readings conflict without it.

inductive CondoravdiLauer2016.AirportScenario.Tracks : Type

Whether there is repair work on the tracks.

• clear : Tracks
• repairs : Tracks

@[instance_reducible]

instance CondoravdiLauer2016.AirportScenario.instDecidableEqTracks : DecidableEq Tracks

Equations

• CondoravdiLauer2016.AirportScenario.instDecidableEqTracks x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CondoravdiLauer2016.AirportScenario.Way : Type

How the addressee gets to the airport.

• train : Way
• ride : Way
• stay : Way

@[instance_reducible]

instance CondoravdiLauer2016.AirportScenario.instDecidableEqWay : DecidableEq Way

Equations

• CondoravdiLauer2016.AirportScenario.instDecidableEqWay x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure CondoravdiLauer2016.AirportScenario.World : Type

A world records the state of the tracks and the way the addressee goes.

• tracks : Tracks

  The state of the tracks.

• way : Way

  The way the addressee goes.

def CondoravdiLauer2016.AirportScenario.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CondoravdiLauer2016.AirportScenario.instDecidableEqWorld : DecidableEq World

Equations

• CondoravdiLauer2016.AirportScenario.instDecidableEqWorld = CondoravdiLauer2016.AirportScenario.instDecidableEqWorld.decEq

def CondoravdiLauer2016.AirportScenario.noon : Set World

The addressee gets to the airport by noon, by a ride or by train on clear tracks.

Equations

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

def CondoravdiLauer2016.AirportScenario.byTrain : Set World

The addressee takes the train.

Equations

• CondoravdiLauer2016.AirportScenario.byTrain = {w : CondoravdiLauer2016.AirportScenario.World | w.way = CondoravdiLauer2016.AirportScenario.Way.train}

def CondoravdiLauer2016.AirportScenario.byRide : Set World

The speaker gives the addressee a ride.

Equations

• CondoravdiLauer2016.AirportScenario.byRide = {w : CondoravdiLauer2016.AirportScenario.World | w.way = CondoravdiLauer2016.AirportScenario.Way.ride}

def CondoravdiLauer2016.AirportScenario.repairs : Set World

There is repair work on the tracks.

Equations

• CondoravdiLauer2016.AirportScenario.repairs = {w : CondoravdiLauer2016.AirportScenario.World | w.tracks = CondoravdiLauer2016.AirportScenario.Tracks.repairs}

def CondoravdiLauer2016.AirportScenario.ep : Unit → World → PreferenceStructure World

The addressee's effective preference is to get to the airport by noon.

Equations

• CondoravdiLauer2016.AirportScenario.ep x✝¹ x✝ = PreferenceStructure.single CondoravdiLauer2016.AirportScenario.noon

def CondoravdiLauer2016.AirportScenario.gNorm : Modality.Background World

The stereotypical ordering source, by which the trains typically run on time.

Equations

• CondoravdiLauer2016.AirportScenario.gNorm x✝ = {fun (v : CondoravdiLauer2016.AirportScenario.World) => v.tracks = CondoravdiLauer2016.AirportScenario.Tracks.clear}

def CondoravdiLauer2016.AirportScenario.fHist : Modality.Background World

In the historical alternatives the state of the tracks is settled, and the speaker gives no ride while the trains run on time.

Equations

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

theorem CondoravdiLauer2016.AirportScenario.should_train {w : World} : Conditional.Restrictor.conditionalNecessity ⊥ gNorm (Desire.Preferential.Want ep () noon) (Modality.necessity fHist (orderingSource ep ()) fun (x : World) => x ∈ byTrain) w

(83a) is true: in the typical worlds the trains run on time, and without a ride the train is the only way to be there by noon.

theorem CondoravdiLauer2016.AirportScenario.should_ride {w : World} : Conditional.Restrictor.conditionalNecessity ⊥ gNorm (fun (v : World) => Desire.Preferential.Want ep () noon v ∧ v ∈ repairs) (Modality.necessity fHist (orderingSource ep ()) fun (x : World) => x ∈ byRide) w

(83b) is true: with repairs on the tracks only a ride gets the addressee there by noon.

theorem CondoravdiLauer2016.AirportScenario.not_single_modal {w : World} : ¬(Conditional.Restrictor.conditionalNecessity ⊥ (orderingSource ep ()) (Desire.Preferential.Want ep () noon) (fun (x : World) => x ∈ byTrain) w ∧ Conditional.Restrictor.conditionalNecessity ⊥ (orderingSource ep ()) (fun (v : World) => Desire.Preferential.Want ep () noon v ∧ v ∈ repairs) (fun (x : World) => x ∈ byRide) w)

On a single modal restricted by both antecedents and ordered by the addressee's goals, (83a) and (83b) are not both true, since by single_modal_strengthening they would leave no best world with track repairs, and a ride on repaired tracks is one.

The rows

The construal rows classify the paper's conditionals by the reading of want and the construal of the modal; the other rows instantiate the theorems above.

inductive CondoravdiLauer2016.WantReading : Type

The reading of the desire predicate.

• effective : WantReading
• mere : WantReading
• weak : WantReading

@[instance_reducible]

instance CondoravdiLauer2016.instDecidableEqWantReading : DecidableEq WantReading

Equations

• CondoravdiLauer2016.instDecidableEqWantReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CondoravdiLauer2016.ModalConstrual : Type

The construal of the modal in the consequent.

• teleological : ModalConstrual
• deontic : ModalConstrual
• speakerTeleological : ModalConstrual

@[instance_reducible]

instance CondoravdiLauer2016.instDecidableEqModalConstrual : DecidableEq ModalConstrual

Equations

• CondoravdiLauer2016.instDecidableEqModalConstrual x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CondoravdiLauer2016.Interpretation : Type

The interpretation the paper assigns.

• anankastic : Interpretation
• nearAnankastic : Interpretation
• nonAnankastic : Interpretation

@[instance_reducible]

instance CondoravdiLauer2016.instDecidableEqInterpretation : DecidableEq Interpretation

Equations

• CondoravdiLauer2016.instDecidableEqInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CondoravdiLauer2016.Implication : Type

The relation the prejacent bears to the goal, §7.1.2, is a means to it, a precondition for it, a means to a strengthened goal, a consequence of it, a specialization of it, or none.

• means : Implication
• precondition : Implication
• strengthenedGoal : Implication
• consequence : Implication
• specialization : Implication
• none : Implication

@[instance_reducible]

instance CondoravdiLauer2016.instDecidableEqImplication : DecidableEq Implication

Equations

• CondoravdiLauer2016.instDecidableEqImplication x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CondoravdiLauer2016.implications : List (String × Implication)

The implications a purpose or conditional row may record.

Equations

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

structure CondoravdiLauer2016.Construal : Type

A construal row.

• want : WantReading

  The reading of want.

• modal : ModalConstrual

  The construal of the modal.

• interpretation : Interpretation

  The interpretation.

• implication : Implication

  The implication.

def CondoravdiLauer2016.Construal.ofRow (row : Datum) : Option Construal

The configuration a construal row records.

Equations

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

theorem CondoravdiLauer2016.anankastic_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "construal" → ∃ c ∈ Construal.ofRow row, c.interpretation = Interpretation.anankastic → c.want = WantReading.effective ∧ c.modal = ModalConstrual.teleological

By §7.2.1, an anankastic interpretation arises only when want targets effective preferences and the modal is construed teleologically over the same agent's effective preferences, (88); on the mere-desire construal the Harlem sentence fails, HobokenScenario.not_anankastic_desire.

theorem CondoravdiLauer2016.implication_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "construal" → ∃ c ∈ Construal.ofRow row, c.want = WantReading.effective → c.modal = ModalConstrual.teleological → (c.interpretation = Interpretation.anankastic ↔ c.implication = Implication.means ∨ c.implication = Implication.precondition)

By §7.1.2, with that setting fixed, anankastics and the near-anankastics of §4 differ only in the implication the temporal relation of goal and prejacent invites, a means or a precondition for the former, a strengthened goal, a consequence or a specialization for the latter. The truth conditions are the same, VaccineScenario.should_vaccine.

def CondoravdiLauer2016.WantReading.ofRow (row : Datum) : Option WantReading

The reading of want an incompatible-wants row records.

Equations

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

theorem CondoravdiLauer2016.incompatible_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "incompatibleWants" → ∃ r ∈ WantReading.ofRow row, row.JudgedFelicitous ↔ r = WantReading.mere

In (52) to (55), two wants the agent knows to be incompatible are coherent on the mere-desire reading, want_both, and not on the effective one, since maximal elements of a consistent structure are jointly compatible with the agent's beliefs, PreferenceStructure.Consistent.inter_inter_nonempty_of_mem_maxElts.

inductive CondoravdiLauer2016.Mood : Type

The mood of a conditional whose antecedent the speaker has just excluded.

• indicative : Mood
• subjunctive : Mood

@[instance_reducible]

instance CondoravdiLauer2016.instDecidableEqMood : DecidableEq Mood

Equations

• CondoravdiLauer2016.instDecidableEqMood x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CondoravdiLauer2016.Mood.ofRow (row : Datum) : Option Mood

The mood a row records.

Equations

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

theorem CondoravdiLauer2016.mood_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "mood" → ∃ m ∈ Mood.ofRow row, row.judgment = Judgment.acceptable ↔ m = Mood.subjunctive

In (91) and (98), when the speaker knows the agent lacks the hypothesized preference, the antecedent is epistemically impossible, the conditional vacuously true, vacuous_conditional, and the constraint on indicatives applies, for conditionals and purpose constructions alike.

def CondoravdiLauer2016.Implication.ofRow (row : Datum) : Option Implication

The implication a purpose row records.

Equations

• CondoravdiLauer2016.Implication.ofRow row = do guard (row.feature? "construction" = some "purpose") row.parse? "implication" CondoravdiLauer2016.implications

theorem CondoravdiLauer2016.purpose_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "purpose" → ∃ i ∈ Implication.ofRow row, row.judgment = Judgment.acceptable ↔ i = Implication.means ∨ i = Implication.precondition

By §7.1.3, purpose constructions admit means and preconditions; teleological consequences are excluded because the prejacent cannot be subsequent to the goal, and the infelicity with specializations is data the paper leaves open.