Verbal mood as component selection

import Linglib.Semantics.Mood.Verbal · namespace Mood.Grammatical

Verbal mood is the contrast between indicative and subjunctive in complement clauses. On the comparison-based theory the subjunctive marks a clause whose embedding attitude ranks worlds by an ordering. Portner states it as two principles (p. 235): a clause operated on by the informational modal is indicative, and a clause operated on by the preference modal is subjunctive. Portner and Rubinstein refine the subjunctive's force to local necessity, truth throughout a branch of the ordering, which lets an agent want incompatible things and agrees with the preference modal when the context set has a most normal world. Here the indicative is simple necessity over the context set, the Truth intuition of Farkas and of Portner's earlier work, and the subjunctive local necessity under the ordering, the Comparison intuition of Giorgi and Pianesi.

Portner leaves question-embedding predicates open (p. 237): Italian chiedere takes the indicative when it means 'ask' and the subjunctive when it means 'wonder'.

Main definitions

Mood.Grammatical.target: the component a grammatical mood relates to.
Mood.Grammatical.interp: a grammatical mood interpreted as the force of its component.

Main statements

Mood.Grammatical.interp_iff_boxOn: with a most normal world in the context set, each mood is the necessity modal of its component.
Mood.Grammatical.indicative_ne_subjunctive: the two moods disagree on some state.

References

Portner 2018, Mood
Portner & Rubinstein 2020, Desire, Belief, and Semantic Composition: Variation in Mood Selection with Desire Predicates formalized
Farkas 1985, Intensional Descriptions and the Romance Subjunctive Mood
Portner 1997, The semantics of mood, complementation, and conversational force
Giorgi & Pianesi 1997, Tense and Aspect: From Semantics to Morphosyntax

Declarations

The indicative targets the informational component and the subjunctive the preferential one.

def target L58–62

Grammatical → Component

Used by target_indicative, target_subjunctive, interp_iff_boxOn, target_injective

Used in PortnerRubinstein2020

L64

L66

The indicative is simple necessity over the context set and the subjunctive is local necessity under the ordering.

def interp L68–72

{W : Type u_1} :

Grammatical → State W → (W → Prop) → Prop

indicative.interp x✝¹ x✝ = x✝¹.boxCs x✝
subjunctive.interp x✝¹ x✝ = x✝¹.localNecessity x✝

Used by interp_indicative, interp_subjunctive, interp_iff_boxOn, indicative_ne_subjunctive

Used in PortnerRubinstein2020

L74–75

L77–78

When the context set has a world at least as normal as all of its worlds, each mood is the necessity modal of the component it targets.

theorem interp_iff_boxOn L80–87

{W : Type u_1} {c : State W} {b : W} (hb : b ∈ c.info) (hleast : ∀ v ∈ c.info, b ≤ v) (m : Grammatical) (p : W → Prop) :

m.interp c p ↔ m.target.boxOn c p

Built from ,

L89–92

The indicative and the subjunctive disagree on some state and proposition.

theorem indicative_ne_subjunctive L94–98

∃ (c : State Bool) (p : Bool → Prop), subjunctive.interp c p ∧ ¬indicative.interp c p

Built from

L100