Portner and Rubinstein (2020): Desire, belief, and semantic composition: variation in mood selection with desire predicates

Spanish querer 'want' and esperar 'hope' both take the subjunctive, while French vouloir takes it and espérer the indicative, though the verbs mean the same in the two languages. Portner and Rubinstein place the variation in composition. The content of a believing situation is one modal background and that of a desiring situation a pair of an ordering source and a modal base; the indicative is simple necessity over one background and the subjunctive local necessity over a pair, and a mood whose force does not fit the content is uninterpretable. French moods first simplify the content, unifying a pair whose backgrounds are consistent at every situation. The desires behind hope are consistent with the beliefs and those behind want need not be, so French hope takes the indicative, with the truth conditions Spanish hope has with the subjunctive.

Main results

• spanish_takes, french_takes: the mood each verb takes in each language, which is the mood its fragment entry records (spanish_fragment, french_fragment).
• french_hope_eq_spanish_hope: French hope with the indicative means what Spanish hope with the subjunctive means.
• want_alice_and_want_sue, bestWorlds_want_alice_eq_neg_one: local necessity lets an agent want each of two outcomes their beliefs rule out together, which von Fintel's best-worlds want forbids.
• not_hope_both: no one hopes for each of two outcomes their beliefs rule out together.

Implementation notes

• Backgrounds are relative to worlds rather than situations, and Backgrounds holds those of one attitude holder; that the desires of want need not be consistent with the beliefs⁺ is the assumption that at some world they are not.
• The local necessity of (19) quantifies over f(s) where ⋂f(s) is meant.
• The diversity presuppositions and the similarity-semantics version of the fragment are not formalized.

References

• [PR20]
• [Por18]
• [Kra81b]
• [vF99a]
• [Fra96]

Contents and moods

inductive PortnerRubinstein2020.Content (W : Type u_2) : Type u_2

The content of an attitude situation is one modal background or a pair of an ordering source and a modal base.

• single {W : Type u_2} (f : Modality.Background W) : Content W

  One modal background.

• pair {W : Type u_2} (g f : Modality.Background W) : Content W

  An ordering source g ranking the worlds of a modal base f.

@[instance_reducible]

instance PortnerRubinstein2020.instHasTargetContent {W : Type u_1} : Mood.HasTarget (Content W)

One background targets the informational component and a pair, whose ordering source ranks worlds, the preferential one.

Equations

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

def PortnerRubinstein2020.Content.state {W : Type u_1} : Content W → W → Mood.State W

The mood state a content induces at a world.

Equations

• (PortnerRubinstein2020.Content.single f).state x✝ = Mood.State.ofExpState (Mood.stateAt f ⊥ x✝)
• (PortnerRubinstein2020.Content.pair g f).state x✝ = Mood.State.ofExpState (Mood.stateAt f g x✝)

def PortnerRubinstein2020.spanish {W : Type u_1} (m : Mood.Grammatical) (c : Content W) : Option ((W → Prop) → W → Prop)

The Spanish moods relate a clause to a world through the force of the mood applied to the content. A mood and a content that target different components do not combine.

Equations

• PortnerRubinstein2020.spanish m c = if Mood.HasTarget.target m = Mood.HasTarget.target c then some fun (p : W → Prop) (w : W) => m.interp (c.state w) p else none

@[simp]

theorem PortnerRubinstein2020.spanish_indicative_single {W : Type u_1} (f : Modality.Background W) : spanish Mood.Grammatical.indicative (Content.single f) = some (Modality.simpleNecessity f)

@[simp]

theorem PortnerRubinstein2020.spanish_subjunctive_pair {W : Type u_1} (g f : Modality.Background W) : spanish Mood.Grammatical.subjunctive (Content.pair g f) = some fun (p : W → Prop) (w : W) => Modality.goodPossibility f g p w

@[simp]

theorem PortnerRubinstein2020.spanish_subjunctive_single {W : Type u_1} (f : Modality.Background W) : spanish Mood.Grammatical.subjunctive (Content.single f) = none

@[simp]

theorem PortnerRubinstein2020.spanish_indicative_pair {W : Type u_1} (g f : Modality.Background W) : spanish Mood.Grammatical.indicative (Content.pair g f) = none

noncomputable def PortnerRubinstein2020.spl {W : Type u_1} : Content W → Content W

Simplification unifies a pair whose backgrounds are consistent at every world into one background, and leaves any other content alone.

Equations

• One or more equations did not get rendered due to their size.
• PortnerRubinstein2020.spl x✝ = x✝

noncomputable def PortnerRubinstein2020.french {W : Type u_1} (m : Mood.Grammatical) (c : Content W) : Option ((W → Prop) → W → Prop)

The French moods apply the Spanish ones to the simplified content.

Equations

• PortnerRubinstein2020.french m c = PortnerRubinstein2020.spanish m (PortnerRubinstein2020.spl c)

Believe, want and hope

structure PortnerRubinstein2020.Backgrounds (W : Type u_2) : Type u_2

The modal backgrounds of an attitude holder.

• dox : Modality.Background W

  The beliefs.

• doxPlus : Modality.Background W

  The beliefs⁺, a background compatible with the beliefs, the modal base of want.

• bul : Modality.Background W

  The desires.

• bulc : Modality.Background W

  The consistent desires, the ordering source of hope.

• consistent (w : W) : ((self.dox ⊔ self.bulc).accessibleWorlds w).Nonempty

  The consistent desires are consistent with the beliefs at every world.

• inconsistent : ¬∀ (w : W), ((self.doxPlus ⊔ self.bul).accessibleWorlds w).Nonempty

  The desires are not consistent with the beliefs⁺ at every world.

def PortnerRubinstein2020.Backgrounds.believe {W : Type u_1} (B : Backgrounds W) : Content W

A believing situation has the beliefs as content.

Equations

• B.believe = PortnerRubinstein2020.Content.single B.dox

def PortnerRubinstein2020.Backgrounds.want {W : Type u_1} (B : Backgrounds W) : Content W

A wanting situation ranks the beliefs⁺ by the desires.

Equations

• B.want = PortnerRubinstein2020.Content.pair B.bul B.doxPlus

def PortnerRubinstein2020.Backgrounds.hope {W : Type u_1} (B : Backgrounds W) : Content W

A hoping situation ranks the beliefs by the consistent desires.

Equations

• B.hope = PortnerRubinstein2020.Content.pair B.bulc B.dox

theorem PortnerRubinstein2020.Backgrounds.spl_believe {W : Type u_1} (B : Backgrounds W) : spl B.believe = B.believe

theorem PortnerRubinstein2020.Backgrounds.spl_want {W : Type u_1} (B : Backgrounds W) : spl B.want = B.want

theorem PortnerRubinstein2020.Backgrounds.spl_hope {W : Type u_1} (B : Backgrounds W) : spl B.hope = Content.single (B.dox ⊔ B.bulc)

theorem PortnerRubinstein2020.spanish_takes {W : Type u_1} (B : Backgrounds W) (m : Mood.Grammatical) : ((spanish m B.believe).isSome = true ↔ m = Mood.Grammatical.indicative) ∧ ((spanish m B.want).isSome = true ↔ m = Mood.Grammatical.subjunctive) ∧ ((spanish m B.hope).isSome = true ↔ m = Mood.Grammatical.subjunctive)

In Spanish believe takes the indicative and want and hope the subjunctive.

theorem PortnerRubinstein2020.french_takes {W : Type u_1} (B : Backgrounds W) (m : Mood.Grammatical) : ((french m B.believe).isSome = true ↔ m = Mood.Grammatical.indicative) ∧ ((french m B.want).isSome = true ↔ m = Mood.Grammatical.subjunctive) ∧ ((french m B.hope).isSome = true ↔ m = Mood.Grammatical.indicative)

In French believe and hope take the indicative and want the subjunctive.

theorem PortnerRubinstein2020.french_hope_eq_spanish_hope {W : Type u_1} (B : Backgrounds W) : french Mood.Grammatical.indicative B.hope = spanish Mood.Grammatical.subjunctive B.hope

French hope with the indicative means what Spanish hope with the subjunctive means.

The fragments

def PortnerRubinstein2020.coding : Mood.Grammatical → Complement.Coding

The coding of a finite clause in a grammatical mood.

Equations

• PortnerRubinstein2020.coding Mood.Grammatical.indicative = Complement.Coding.indicative
• PortnerRubinstein2020.coding Mood.Grammatical.subjunctive = Complement.Coding.subjunctive

def PortnerRubinstein2020.Selects (v : Verb) (m : Mood.Grammatical) : Prop

A verb selects a mood when one of its frames has a clause in that mood.

Equations

• PortnerRubinstein2020.Selects v m = ∃ fr ∈ v.valency.frames, PortnerRubinstein2020.coding m ∈ fr.codings

@[instance_reducible]

instance PortnerRubinstein2020.instDecidableSelects (v : Verb) (m : Mood.Grammatical) : Decidable (Selects v m)

Equations

• PortnerRubinstein2020.instDecidableSelects v m = PortnerRubinstein2020.instDecidableSelects._aux_1 v m

theorem PortnerRubinstein2020.spanish_fragment {W : Type u_1} (B : Backgrounds W) (m : Mood.Grammatical) : (Selects Spanish.Verbs.creer m ↔ (spanish m B.believe).isSome = true) ∧ (Selects Spanish.Verbs.querer m ↔ (spanish m B.want).isSome = true) ∧ (Selects Spanish.Verbs.esperar m ↔ (spanish m B.hope).isSome = true)

The Spanish entries record the moods the analysis predicts.

theorem PortnerRubinstein2020.french_fragment {W : Type u_1} (B : Backgrounds W) (m : Mood.Grammatical) : (Selects French.Verbs.croire m ↔ (french m B.believe).isSome = true) ∧ (Selects French.Verbs.vouloir m ↔ (french m B.want).isSome = true) ∧ (Selects French.Verbs.esperer m ↔ (french m B.hope).isSome = true)

The French entries record the moods the analysis predicts.

Conflicting desires

Desiring to marry Alice and desiring to marry Sue, where the beliefs⁺ rule out marrying both: the worlds where the speaker marries one of them are incomparable under the desires, so each marriage holds throughout a branch of the ordering and neither holds at every best world.

inductive PortnerRubinstein2020.Marriage : Type

The outcomes are marrying Alice alone, marrying Sue alone, and marrying neither.

• alice : Marriage
• sue : Marriage
• neither : Marriage

@[instance_reducible]

instance PortnerRubinstein2020.instDecidableEqMarriage : DecidableEq Marriage

Equations

• PortnerRubinstein2020.instDecidableEqMarriage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PortnerRubinstein2020.marriesAlice : Marriage → Prop

Marrying Alice.

Equations

• PortnerRubinstein2020.marriesAlice x✝ = (x✝ = PortnerRubinstein2020.Marriage.alice)

def PortnerRubinstein2020.marriesSue : Marriage → Prop

Marrying Sue.

Equations

• PortnerRubinstein2020.marriesSue x✝ = (x✝ = PortnerRubinstein2020.Marriage.sue)

def PortnerRubinstein2020.doxPlus : Modality.Background Marriage

The beliefs⁺ leave every outcome open.

Equations

• PortnerRubinstein2020.doxPlus = ⊥

def PortnerRubinstein2020.bul : Modality.Background Marriage

The desires are to marry Alice and to marry Sue.

Equations

• PortnerRubinstein2020.bul x✝ = {PortnerRubinstein2020.marriesAlice, PortnerRubinstein2020.marriesSue}

theorem PortnerRubinstein2020.want_alice_and_want_sue (w : Marriage) : Modality.goodPossibility doxPlus bul marriesAlice w ∧ Modality.goodPossibility doxPlus bul marriesSue w

The speaker wants to marry Alice and wants to marry Sue.

theorem PortnerRubinstein2020.bestWorlds_want_alice_eq_neg_one (w : Marriage) : Desire.BestWorlds.want doxPlus.accessibleWorlds bul marriesAlice w = -1

On von Fintel's best-worlds want it is false that the speaker wants to marry Alice, since the outcome is contingent on the beliefs⁺ and marrying Sue is a best outcome.

theorem PortnerRubinstein2020.not_hope_both {W : Type u_1} (B : Backgrounds W) {p q : W → Prop} {w : W} (hpq : ∀ v ∈ B.dox.accessibleWorlds w, ¬(p v ∧ q v)) : ¬(Modality.goodPossibility B.dox B.bulc p w ∧ Modality.goodPossibility B.dox B.bulc q w)

No one hopes for each of two outcomes their beliefs rule out together.