Purver and Ginzburg (2004): Clarifying Noun Phrase Semantics

A reprise question repeats a phrase of the previous utterance to query it, as Turkey? does after We'll get the turkey out of the oven. Purver and Ginzburg read what a noun phrase denotes off the readings its reprises have. In the grammar of Ginzburg and Cooper a sign lists its contextual parameters, the objects a hearer must identify in context, and a reprise can query only these. The Reprise Content Hypothesis says that a reprise queries part of the content of the reprised phrase, and in its strong version exactly that content. The paper takes a quantified noun phrase to denote a witness set, a subset of the noun's extension that its quantifier holds of, and its Definiteness Principle makes that content a contextual parameter in a definite use and a member of the store of existentially quantified objects in an indefinite one.

Main statements

• rows_predicted: every corpus reading the paper judges possible queries a contextual parameter of the sign for that use of a noun phrase, and no reading it marks impossible does.
• strong_np, not_strong_gq: a definite noun phrase that denotes a witness set holds the strong hypothesis, and one that denotes a generalized quantifier never does, although both make the same parameters available.
• Sign.strong_word_iff: a word holds the strong hypothesis exactly when it stores none of its content.
• pair_apply_iff: a quantifier holds of a predicate exactly when some witness set lies inside the predicate and the rest of the noun's extension lies outside it, which is the paper's reading of a monotone decreasing noun phrase as a reference set with its complement.

Implementation notes

• A sign records which kinds of object it contributes, not their values, since the argument turns on what kind of object a reprise queries. A content is the set of its components, so that both members of a reference set and complement pair can be abstracted.
• Sign.phrase takes the parameters that the Definiteness Principle distributes as an optional argument, by default the content. It is set for attributive definites, where the paper asks for "a slightly different version" of the principle, and for the generalized-quantifier alternative.
• The rows carry the paper's classification of each use as a feature, and a referential use of an indefinite or a universal counts as definite, as in the paper. Every noun phrase gets the sign of a determiner with a noun, pronouns and bare wh-words included. Marginal readings make no claim.
• Quantifier scope, anaphora, the retrieval of stored objects and the corpus counts are not formalized.

References

• [PG04]
• [GC04]
• [BC81]

Signs and the Definiteness Principle

inductive PurverGinzburg2004.Kind : Type

The kinds of semantic object a nominal sign contributes or abstracts. They are an individual or witness set, a property, a determiner relation, a function to witness sets with its situational argument, a generalized quantifier, and the complement set of a monotone decreasing phrase.

• individual : Kind
• property : Kind
• relation : Kind
• function : Kind
• situation : Kind
• quantifier : Kind
• complement : Kind

@[instance_reducible]

instance PurverGinzburg2004.instDecidableEqKind : DecidableEq Kind

Equations

• PurverGinzburg2004.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PurverGinzburg2004.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PurverGinzburg2004.instReprKind : Repr Kind

Equations

• PurverGinzburg2004.instReprKind = { reprPrec := PurverGinzburg2004.instReprKind.repr }

structure PurverGinzburg2004.Sign : Type

A nominal sign carries the components of its content, the contextual parameters a reprise can query, and the parameters stored for existential closure.

• content : Finset Kind
• cparams : Finset Kind
• store : Finset Kind

@[instance_reducible]

instance PurverGinzburg2004.instDecidableEqSign : DecidableEq Sign

Equations

• PurverGinzburg2004.instDecidableEqSign = PurverGinzburg2004.instDecidableEqSign.decEq

def PurverGinzburg2004.instDecidableEqSign.decEq (x✝ x✝¹ : Sign) : Decidable (x✝ = x✝¹)

Equations

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

def PurverGinzburg2004.Sign.word (content store : Finset Kind) : Sign

Sign.word content store is the sign of a word, whose contextual parameters are the content it does not store (74).

Equations

• PurverGinzburg2004.Sign.word content store = { content := content, cparams := content \ store, store := store }

def PurverGinzburg2004.Sign.phrase (content store : Finset Kind) (head : Sign) (nonHead : Finset Sign) (params : Finset Kind := content) : Sign

Sign.phrase content store head nonHead is the sign of a phrase (75). Its contextual parameters are those of every daughter (73) with the parameters it does not store, and its store adds that of the head daughter. The parameters are the content unless params is given.

Equations

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

def PurverGinzburg2004.Sign.DefinitenessPrinciple (s : Sign) : Prop

The Definiteness Principle requires each component of the content to be a contextual parameter or stored.

Equations

• s.DefinitenessPrinciple = (s.content ⊆ s.cparams ∪ s.store)

@[instance_reducible]

instance PurverGinzburg2004.Sign.instDecidableDefinitenessPrinciple (s : Sign) : Decidable s.DefinitenessPrinciple

Equations

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

def PurverGinzburg2004.Sign.Strong (s : Sign) : Prop

A sign holds the strong Reprise Content Hypothesis when a reprise can query its whole content, every component being a contextual parameter.

Equations

• s.Strong = (s.content ⊆ s.cparams)

@[instance_reducible]

instance PurverGinzburg2004.Sign.instDecidableStrong (s : Sign) : Decidable s.Strong

Equations

• s.instDecidableStrong = { decide := decide (∀ a ∈ s.content.val.attach, (fun (x : PurverGinzburg2004.Kind) (a : x ∈ s.content) => x ∈ s.cparams) ↑a ⋯), reflects_decide := ⋯ }

theorem PurverGinzburg2004.Sign.definitenessPrinciple_word {c s : Finset Kind} : (word c s).DefinitenessPrinciple

theorem PurverGinzburg2004.Sign.definitenessPrinciple_phrase {c s : Finset Kind} {head : Sign} {nonHead : Finset Sign} : (phrase c s head nonHead).DefinitenessPrinciple

theorem PurverGinzburg2004.Sign.strong_word_iff {c s : Finset Kind} : (word c s).Strong ↔ Disjoint c s

A word holds the strong hypothesis exactly when it stores none of its content (§4.5).

theorem PurverGinzburg2004.Sign.strong_phrase {c s : Finset Kind} {head : Sign} {nonHead : Finset Sign} (h : Disjoint c s) : (phrase c s head nonHead).Strong

A phrase that stores none of its content holds the strong hypothesis (§4.5).

theorem PurverGinzburg2004.Sign.cparams_subset_cparams_phrase {c s : Finset Kind} {head : Sign} {nonHead : Finset Sign} {d : Sign} {params : Finset Kind} (hd : d ∈ insert head nonHead) : d.cparams ⊆ (phrase c s head nonHead params).cparams

A phrase inherits the contextual parameters of each daughter (73), which gives its reprises their sub-constituent readings.

The signs of nouns and noun phrases

def PurverGinzburg2004.cn : Sign

A common noun contributes a property, which it abstracts (28).

Equations

• PurverGinzburg2004.cn = PurverGinzburg2004.Sign.word {PurverGinzburg2004.Kind.property} ∅

def PurverGinzburg2004.det : Sign

A determiner contributes a relation between sets, which it abstracts.

Equations

• PurverGinzburg2004.det = PurverGinzburg2004.Sign.word {PurverGinzburg2004.Kind.relation} ∅

def PurverGinzburg2004.np : Reference.Definiteness → Sign

A quantified noun phrase contributes the witness set its determiner picks out of the noun's property (72). A definite use abstracts it and an indefinite use stores it.

Equations

• One or more equations did not get rendered due to their size.
• PurverGinzburg2004.np Reference.Definiteness.definite = PurverGinzburg2004.Sign.phrase {PurverGinzburg2004.Kind.individual} ∅ PurverGinzburg2004.cn {PurverGinzburg2004.det}

def PurverGinzburg2004.attributive : Sign

An attributive definite contributes the value of a function at a situation, and abstracts the function and the situation in place of that value (48).

Equations

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

def PurverGinzburg2004.gq : Reference.Definiteness → Sign

On the generalized-quantifier alternative the content is a quantifier, and a definite use abstracts a witness set of it (66).

Equations

• One or more equations did not get rendered due to their size.
• PurverGinzburg2004.gq Reference.Definiteness.indefinite = PurverGinzburg2004.Sign.phrase {PurverGinzburg2004.Kind.quantifier} ∅ PurverGinzburg2004.cn {PurverGinzburg2004.det} ∅

def PurverGinzburg2004.pair (store : Finset Kind) : Sign

A monotone decreasing noun phrase contributes a reference set with its complement and stores store. It stores both when existentially quantified (92) and neither when referential (93), and the variant (94) stores the complement set alone.

Equations

• PurverGinzburg2004.pair store = PurverGinzburg2004.Sign.phrase {PurverGinzburg2004.Kind.individual, PurverGinzburg2004.Kind.complement} store PurverGinzburg2004.cn {PurverGinzburg2004.det}

theorem PurverGinzburg2004.strong_cn : cn.Strong

Common nouns hold the strong hypothesis (§3.3).

theorem PurverGinzburg2004.strong_np : (np Reference.Definiteness.definite).Strong

Definite noun phrases hold the strong hypothesis (§4.4.2).

theorem PurverGinzburg2004.indefinite_no_referent : Kind.individual ∉ (np Reference.Definiteness.indefinite).cparams

An indefinite stores its witness set, so no reprise of it queries a referent (§4.2).

theorem PurverGinzburg2004.cparams_gq (d : Reference.Definiteness) : (gq d).cparams = (np d).cparams

The generalized-quantifier alternative makes the same parameters available as the witness-set account (§4.4.1).

theorem PurverGinzburg2004.not_strong_gq (d : Reference.Definiteness) : ¬(gq d).Strong

The generalized-quantifier alternative never lets a reprise query its content, so it holds only the weak hypothesis (§4.4.1).

theorem PurverGinzburg2004.not_strong_attributive : ¬attributive.Strong

The functional analysis of attributive definites holds only the weak hypothesis (§4.1.3).

theorem PurverGinzburg2004.attributive_not_definitenessPrinciple : ¬attributive.DefinitenessPrinciple

An attributive definite neither abstracts nor stores its content, only the function and the situation (§4.5).

theorem PurverGinzburg2004.strong_pair : (pair ∅).Strong

The referential pair holds the strong hypothesis (93).

The corpus readings

def PurverGinzburg2004.signOfNP : List (String × Sign)

The sign of each use of a noun phrase the rows distinguish. Referential uses of indefinites and universals have the sign of a definite, since the paper distinguishes definite uses by their content being a contextual parameter (§4.2.2, §4.3).

Equations

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

def PurverGinzburg2004.kindOfReading : List (String × Kind)

The kind of object each paraphrase reading queries.

Equations

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

def PurverGinzburg2004.Sign.Predicts (s : Sign) (r : Datum) : Prop

A sign predicts the readings of a row when each reading the paper judges possible queries one of its contextual parameters and no reading the paper marks impossible does.

Equations

• s.Predicts r = ∀ p ∈ r.readings, ∃ k ∈ List.lookup p.1 PurverGinzburg2004.kindOfReading, (p.2 = Judgment.acceptable → k ∈ s.cparams) ∧ (p.2 = Judgment.unacceptable → k ∉ s.cparams)

@[instance_reducible]

instance PurverGinzburg2004.Sign.instDecidablePredicts (s : Sign) (r : Datum) : Decidable (s.Predicts r)

Equations

• s.instDecidablePredicts r = PurverGinzburg2004.Sign.instDecidablePredicts._aux_1 s r

theorem PurverGinzburg2004.rows_predicted (r : Datum) : r ∈ Examples.all → ∃ s ∈ r.parse? "np" signOfNP, s.Predicts r

The sign of each use of a noun phrase predicts the readings of its reprises, (25) to (90).

theorem PurverGinzburg2004.not_predicts_ex90 : ¬(pair {Kind.complement}).Predicts Examples.ex90

The complement-set reading the paper gives its constructed (90) is not predicted when the complement set is stored (94), so that reading calls for abstracting both members (93).

Witness sets and truth conditions

theorem PurverGinzburg2004.witness_subset_of_empty {α : Type u_1} {Q : Quantifier.NP α} {A : α → Prop} (hQ : Q fun (x : α) => False) (X : α → Prop) : ∃ (w : α → Prop), Q.Witness A w ∧ ∀ (x : α), w x → X x

A quantifier that holds of the empty set has a witness set inside every predicate, so the plain witness representation (85) says nothing of few or no (§5.5).

theorem PurverGinzburg2004.not_witness_iff_of_empty {α : Type u_1} {Q : Quantifier.NP α} {A X : α → Prop} (hQ : Q fun (x : α) => False) (hX : ¬Q X) : ¬∀ (Y : α → Prop), Q Y ↔ ∃ (w : α → Prop), Q.Witness A w ∧ ∀ (x : α), w x → Y x

The equivalence (24) of increasing quantifiers fails of a quantifier that holds of the empty set and not of every predicate.

theorem PurverGinzburg2004.pair_apply_iff {α : Type u_1} {Q : Quantifier.NP α} {A X : α → Prop} (h : Q.LivesOn A) : Q X ↔ ∃ (R : α → Prop), Q.Witness A R ∧ (∀ (x : α), R x → X x) ∧ ∀ (x : α), A x → ¬R x → ¬X x

A quantifier living on A holds of X exactly when some witness set R lies inside X while the rest of A lies outside it, the pair representation (91). This needs no monotonicity, the two conditions leaving A ∩ X as the only candidate.