Documentation

Linglib.Semantics.Mood.Verbal

Verbal mood as component selection #

Verbal mood — the indicative/subjunctive contrast in the complement clauses of attitude verbs — reduces, on [Por18]'s account (Ch. 2), to which component of the embedding attitude's state the mood operator quantifies over. His unification: the Truth intuition ([Far85], [Por97]) and the Comparison intuition ([GP97]) are both correct because they target different components — universal quantification over the information component underwrites Truth-style selection (boxCs), and quantification over the best-ranked subset underwrites Comparison-style selection (boxLe). A third operator for question-embedding predicates (wonder, ask) selects for clauses settled by the open question (boxAns) — this library's extension; Portner's unification proper is restricted to declarative complementation.

Main declarations #

VerbalOp — the three operators, with HasTarget sending each to its component.
VerbalOp.interp — interpretation as boxOn ∘ target.
Selector.toVerbalOp — the bridge from predicate-class selection.

Main statements #

indicative_ne_subjunctive, interrogative_ne_indicative — the operators are pairwise distinguishable.
target_injective — mood selection and component selection are in bijection at this layer.

inductive Mood.VerbalOp :

The three verbal-mood operators; .indicative and .subjunctive are [Por18]'s, .interrogative this library's extension.

indicative : VerbalOp
Universal quantification over the informational component — the Truth intuition.
subjunctive : VerbalOp
Quantification over the preferential component's best-ranked subset — the Comparison intuition.
interrogative : VerbalOp
Answerhood with respect to the inquiry component ([GS84]); selected by question-embedding predicates.

Instances For

@[implicit_reducible]

instance Mood.instDecidableEqVerbalOp :

DecidableEq VerbalOp

Equations

Mood.instDecidableEqVerbalOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mood.instReprVerbalOp :

Equations

Mood.instReprVerbalOp = { reprPrec := Mood.instReprVerbalOp.repr }

def Mood.instReprVerbalOp.repr :

VerbalOp → ℕ → Std.Format

Equations

Mood.instReprVerbalOp.repr Mood.VerbalOp.indicative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.VerbalOp.indicative")).group prec✝
Mood.instReprVerbalOp.repr Mood.VerbalOp.subjunctive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.VerbalOp.subjunctive")).group prec✝
Mood.instReprVerbalOp.repr Mood.VerbalOp.interrogative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.VerbalOp.interrogative")).group prec✝

Instances For

@[implicit_reducible]

instance Mood.instHasTargetVerbalOp :

HasTarget VerbalOp

Verbal-mood targets ([Por18], Ch. 2).

Equations

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

@[simp]

theorem Mood.target_indicative :

HasTarget.target VerbalOp.indicative = Component.informational

@[simp]

theorem Mood.target_subjunctive :

HasTarget.target VerbalOp.subjunctive = Component.preferential

@[simp]

theorem Mood.target_interrogative :

HasTarget.target VerbalOp.interrogative = Component.inquisitive

def Mood.VerbalOp.interp {W : Type u_1} (m : VerbalOp) :

State W → (W → Prop) → Prop

Interpretation of a verbal-mood operator against an embedding state and an embedded proposition: the necessity modal of the operator's target.

Equations

m.interp = (Mood.HasTarget.target m).boxOn

Instances For

Definitional equalities #

@[simp]

theorem Mood.interp_indicative {W : Type u_1} (c : State W) (p : W → Prop) :

VerbalOp.indicative.interp c p = c.boxCs p

@[simp]

theorem Mood.interp_subjunctive {W : Type u_1} (c : State W) (p : W → Prop) :

VerbalOp.subjunctive.interp c p = c.boxLe p

@[simp]

theorem Mood.interp_interrogative {W : Type u_1} (c : State W) (p : W → Prop) :

VerbalOp.interrogative.interp c p = c.boxAns p

Distinctness witnesses #

def Mood.sepState :

UpdateSemantics.Default.ExpState Bool

Total information over Bool, ordered so that false — the unique sepProp-world — is the unique optimal world.

Equations

Mood.sepState = { info := Set.univ, order := Core.Order.Normality.crit Mood.State.sepProp }

Instances For

def Mood.sepStateTriv :

State Bool

sepState with trivial inquiry.

Equations

Mood.sepStateTriv = Mood.State.ofExpState Mood.sepState

Instances For

theorem Mood.subjunctive_accepts_separation :

VerbalOp.subjunctive.interp sepStateTriv State.sepProp

theorem Mood.indicative_rejects_separation :

¬VerbalOp.indicative.interp sepStateTriv State.sepProp

theorem Mood.indicative_ne_subjunctive :

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

The Truth/Comparison split is genuine: the two operators disagree on some state and proposition.

theorem Mood.interrogative_ne_indicative :

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

The interrogative operator is not the indicative one (State.boxAns_not_reducible_to_boxCs).

theorem Mood.target_injective :

Function.Injective HasTarget.target

Verbal-mood targeting is injective: mood selection and component selection are in bijection at this layer. [Por18] states his Indicative and Subjunctive principles one-way ("if a clause is operated on by the informational modal, its form is indicative"), with update-based variants via his (11) fixpoints; the bijection here reflects only this three-element enum.

Bridge to `Selector` #

def Mood.Selector.toVerbalOp :

Selector → Option VerbalOp

The verbal-mood operator a predicate class selects, when the class is committed to a single mood cross-linguistically; variable and mood-neutral classes project to none. Selector covers declarative-complement embedders only, so .interrogative is not in its image.

Equations

Instances For