Brasoveanu (2010): Decomposing Modal Quantification

[Bra10] interprets discourse relative to plural information states, sets of variable assignments that store both the values of discourse referents and the dependencies between them, in a Dynamic Ty2 reformulation of [Mus96]'s CDRT. Generalized determiners store their restrictor and nuclear scope sets together with the dependencies inside them, and singular pronouns require the dref they retrieve to have one value. The modal half of the paper adds drefs for possible worlds and analyses modal verbs as the modal counterparts of determiners.

This file formalizes the system for individuals of §2. The indefinite, pronoun and proper name translations (36), (37), (42) compose the wolf discourse (27), whose truth at the dummy state (35) is derived for any model: A wolf came in. It ate Harvey. is true exactly when some wolf came in and ate Harvey (wolfDiscourse_true_iff), while a pronoun out of the blue is false there. On the matrix (64), value inclusion (65) scrambles the dependency between conventions and women and structured inclusion (66) keeps it.

Implementation notes

• A row is an assignment Dref → Flat E, CDRT's canonical register structure at Flat E, and the dummy individual ★ is ⊥.
• Predication is interpreted distributively over the rows where its drefs have values ((30), (34)); this is PCDRT.atom and PCDRT.atom₂.

TODO

• Dynamic generalized quantifiers (74)–(77), quantificational subordination and donkey anaphora (§2.5–§2.7).
• Intensional PCDRT (§3): world drefs, modal quantifiers and modal subordination.
• The entailment particles of §4.

References

• [Bra10]
• [Mus96]
• [vdB96]

Indefinites, pronouns and proper names (§2.2)

inductive Brasoveanu2010.Dref : Type

The drefs of the wolf discourse (27): the wolf u and Harvey u'.

• u : Dref
• u' : Dref

@[instance_reducible]

instance Brasoveanu2010.instDecidableEqDref : DecidableEq Dref

Equations

• Brasoveanu2010.instDecidableEqDref x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Brasoveanu2010.Row (E : Type u_2) : Type u_2

A row of a plural info state: an individual or ★ for each dref.

Equations

• Brasoveanu2010.Row E = (Brasoveanu2010.Dref → Flat E)

@[reducible, inline]

abbrev Brasoveanu2010.Pred (E : Type u_2) : Type u_2

A property, type et: a dref to an update.

Equations

• Brasoveanu2010.Pred E = (Brasoveanu2010.Dref → DynamicSemantics.Update (Set (Brasoveanu2010.Row E)))

def Brasoveanu2010.iStar {E : Type u_1} : Row E

The dummy assignment i★, which assigns ★ to every dref; {i★} is the dummy info state (28), which holds no anaphoric information.

Equations

• Brasoveanu2010.iStar = ⊥

def Brasoveanu2010.noun {E : Type u_1} (P : E → Prop) : Pred E

(26), (30): a noun or intransitive verb is a test that its argument satisfies it.

Equations

• Brasoveanu2010.noun P v = DynamicSemantics.Update.test (PCDRT.atom P v)

def Brasoveanu2010.indef {E : Type u_1} (d : Dref) (P P' : Pred E) : DynamicSemantics.Update (Set (Row E))

(36): the singular indefinite introduces u, makes it singular, and predicates its restrictor and its scope of it.

Equations

• Brasoveanu2010.indef d P P' = ((SetRel.comp (PCDRT.intro d) (DynamicSemantics.Update.test (PCDRT.sing d))).comp (P d)).comp (P' d)

def Brasoveanu2010.pron {E : Type u_1} (d : Dref) (P : Pred E) : DynamicSemantics.Update (Set (Row E))

(37): the singular pronoun requires its dref to be singular and passes it to the predicate.

Equations

• Brasoveanu2010.pron d P = SetRel.comp (DynamicSemantics.Update.test (PCDRT.sing d)) (P d)

def Brasoveanu2010.name {E : Type u_1} (x : E) (d : Dref) (P : Pred E) : DynamicSemantics.Update (Set (Row E))

(42), (43): a proper name introduces a dref whose only value is its bearer.

Equations

• Brasoveanu2010.name x d P = (SetRel.comp (PCDRT.intro d) (DynamicSemantics.Update.test {I : Set (Brasoveanu2010.Row E) | PCDRT.value d I = {x}})).comp (P d)

def Brasoveanu2010.transVerb {E : Type u_1} (R : E → E → Prop) (Q : Pred E → DynamicSemantics.Update (Set (Row E))) : Pred E

(45a): a transitive verb applies its object's quantifier to the relation.

Equations

• Brasoveanu2010.transVerb R Q v = Q fun (v' : Brasoveanu2010.Dref) => DynamicSemantics.Update.test (PCDRT.atom₂ R v v')

def Brasoveanu2010.wolfDiscourse {E : Type u_1} (wolf comeIn : E → Prop) (eat : E → E → Prop) (harvey : E) : DynamicSemantics.Update (Set (Row E))

The wolf discourse (27), (46): A^u wolf came in. It_u ate Harvey^{u'}.

Equations

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

theorem Brasoveanu2010.wolfDiscourse_true_iff {E : Type u_1} (wolf comeIn : E → Prop) (eat : E → E → Prop) (harvey : E) : {iStar} ∈ SetRel.dom (wolfDiscourse wolf comeIn eat harvey) ↔ ∃ (x : E), wolf x ∧ comeIn x ∧ eat x harvey

The truth conditions of (27) at the dummy state (35): the discourse can update {i★} exactly when some wolf came in and ate Harvey.

theorem Brasoveanu2010.pron_not_true_at_iStar {E : Type u_1} (d : Dref) (P : Pred E) : {iStar} ∉ SetRel.dom (pron d P)

A pronoun out of the blue is infelicitous (§2.2): its singular number fails at the dummy state, where its dref has no value.

Structured inclusion (63)–(66)

The matrix (64): the conventions α₁ … α₄ in u₁, the women β₁ … β₄ courted at them in u₂, and two ways of storing a subset of the conventions in u₃.

inductive Brasoveanu2010.Dref₃ : Type

The drefs of (63): conventions, women, and a subset of the conventions.

• u₁ : Dref₃
• u₂ : Dref₃
• u₃ : Dref₃

@[instance_reducible]

instance Brasoveanu2010.instDecidableEqDref₃ : DecidableEq Dref₃

Equations

• Brasoveanu2010.instDecidableEqDref₃ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Brasoveanu2010.Ind : Type

The individuals of (64).

• α₁ : Ind
• α₂ : Ind
• α₃ : Ind
• α₄ : Ind
• β₁ : Ind
• β₂ : Ind
• β₃ : Ind
• β₄ : Ind

@[instance_reducible]

instance Brasoveanu2010.instDecidableEqInd : DecidableEq Ind

Equations

• Brasoveanu2010.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Brasoveanu2010.row (a b c : Flat Ind) : Dref₃ → Flat Ind

A row of (64) from its u₁, u₂ and u₃ values.

Equations

• Brasoveanu2010.row a b c Brasoveanu2010.Dref₃.u₁ = a
• Brasoveanu2010.row a b c Brasoveanu2010.Dref₃.u₂ = b
• Brasoveanu2010.row a b c Brasoveanu2010.Dref₃.u₃ = c

def Brasoveanu2010.valueCol : Set (Dref₃ → Flat Ind)

(64) with the value-inclusion column: u₃ holds α₁, α₃, α₁, α₂.

Equations

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

def Brasoveanu2010.structCol : Set (Dref₃ → Flat Ind)

(64) with the structured column: u₃ holds α₁, α₂, ★, α₄.

Equations

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

theorem Brasoveanu2010.value_subset_valueCol : PCDRT.value Dref₃.u₃ valueCol ⊆ PCDRT.value Dref₃.u₁ valueCol

Both columns store a subset of the conventions (65).

theorem Brasoveanu2010.value_subset_structCol : PCDRT.value Dref₃.u₃ structCol ⊆ PCDRT.value Dref₃.u₁ structCol

theorem Brasoveanu2010.valueCol_scrambles_dep : ¬PCDRT.dep Dref₃.u₃ Dref₃.u₂ valueCol ⊆ PCDRT.dep Dref₃.u₁ Dref₃.u₂ valueCol

The value-inclusion column pairs α₁ with β₃, a dependency (63a) never established.

theorem Brasoveanu2010.valueCol_not_structSub : valueCol ∉ PCDRT.structSub Dref₃.u₃ Dref₃.u₁

The value-inclusion column is not a structured subset (66).

theorem Brasoveanu2010.structCol_structSubAll : structCol ∈ PCDRT.structSubAll Dref₃.u₃ Dref₃.u₁

The structured column is a fully structured subset (68).

theorem Brasoveanu2010.structCol_keeps_dep : PCDRT.dep Dref₃.u₃ Dref₃.u₂ structCol ⊆ PCDRT.dep Dref₃.u₁ Dref₃.u₂ structCol

The structured column keeps the dependency between conventions and women.