Coppock and Beaver's definiteness and determinacy

This file formalizes Coppock and Beaver's theory of definiteness: definite, indefinite and possessive descriptions are underlyingly predicates, the definite article presupposes weak uniqueness and no existence, and a description acquires existential import only through the type shifts that place it in argument position. The entries are terms of the paper's Weak Kleene logic with the presupposition operator of Beaver and Krahmer, and the definite article competes with the indefinite under an expression-level Maximize Presupposition.

Main statements

• anti_uniqueness: Scott is not the only author of Waverley is true exactly when Scott is an author and so is someone else, and presupposes only that Scott is an author (anti_uniqueness_presup); the Fregean rival entry can never make it true (no_anti_uniqueness_fregean).
• the_dominates_an, an_only_blocked: the definite article presuppositionally dominates the indefinite, so an only P is blocked in every context; blocking is derivation-sensitive, since the derivation scoping a plane crash inside the description is not blocked (Crash.an_only_survivor_not_blocked) while the high-scope one is (Crash.the_only_survivor_blocked).
• not_blocked_sentence_an_only: no sentence-level Maximize Presupposition blocks an only P, because the definite contributes nothing to an only phrase and the two sentences mean the same (sentence_the_only_eq_an_only); the principle must compare expressions.
• no_determinate_indefinites: an indefinite that survives blocking has no defined update under the iota shift, while iota and the existential shift update alike where unique existence is settled (readings_agree_of_existsUnique).
• only_answer_apply: the adjectival entry is the earlier paper's exclusive schema at the question what things are P, with answers ranked by entailment.
• Scenario.restrictor_rows, Lobner.rows: the paper's predicative judgments are decided by weak uniqueness of the restrictor.

Implementation notes

• Predicates are trivalent properties; the counting abbreviation |P| ≤ 1 and the exclusive component of only are read on the positive extension, so the entries are computable given decidability, which finite models supply; the same abbreviations as formulas of the paper's logic, with Haug's universal quantifier, are proved pointwise equal.
• Relative Presuppositional Strength (71) as printed transposes the two expressions: it would make the indefinite dominate the definite, against the paper's own derivation on the same page, so the definition used is the transposition that derivation needs. Competitorhood, clause (i) of Maximize Presupposition (75), is glossed only in the appendix and is carried here by classical equivalence.
• The rival entries of Table 1 are classical and noncomputable, since only their presupposition profiles are stated. Lowering the individual-denoting Fregean entry by Partee's ident reads the undefined individual through Option, since the paper's logic makes identity bivalent even on the undefined individual; Löbner's individual-noun row of Table 2 is not of the article's type and is not compared.
• The appendix's possessive type shift prints the possessor arguments in the opposite order from the main text's sortal-to-relational shift; the main text is followed.
• The judgments the paper reports are the rows of Data/Examples/CoppockBeaver2015.json. Not modelled: Type Simplicity and the entity-introducing bias of §3.4–3.5, whose rows carry a verb feature and readings only; the accommodation comparison of §2.2.3 beyond the inconsistency it turns on; the determinate possessor, the possessor being a parameter; salience; plurals; the syntax of IL3 and its Pronouns and Traces rule; the focus on only behind the inference that Anna gave a talk.

TODO

• The argumental Löbner rows compare iota-shifted possessives, which are classical; a computable iota over a finite type would let them join the decide ties.

References

• E. Coppock, D. Beaver, Definiteness and determinacy (2015)
• E. Coppock, D. Beaver, Principles of the exclusive muddle (2014)
• D. Beaver, E. Krahmer, A Partial Account of Presupposition Projection (2001)
• D. Haug, Partial Dynamic Semantics for Anaphora: Compositionality without Syntactic Coindexation (2014)
• Y. Winter, Flexibility Principles in Boolean Semantics: The Interpretation of Coordination, Plurality, and Scope in Natural Language (2001)
• D. G. Fara, Descriptions as Predicates (2001)
• B. Partee, Noun Phrase Interpretation and Type-shifting Principles (1987)
• I. Heim, Artikel und Definitheit (1991)
• O. Percus, Antipresuppositions (2006)
• P. Elbourne, Definite Descriptions (2013)
• C. Vikner, P. A. Jensen, A Semantic Analysis of the English Genitive: Interaction of Lexical and Formal Semantics (2002)

Weak uniqueness and the lexical entries

def CoppockBeaver2015.WeakUnique {E : Type u_1} (P : E → SignType) : Prop

A predicate is weakly unique, the paper's |P| ≤ 1, when its positive extension is a subsingleton.

Equations

• CoppockBeaver2015.WeakUnique P = (Trivalent.posExt P).Subsingleton

@[instance_reducible]

instance CoppockBeaver2015.instDecidableWeakUniqueOfFintypeOfDecidableEq {E : Type u_1} [Fintype E] [DecidableEq E] (P : E → SignType) : Decidable (WeakUnique P)

Equations

• CoppockBeaver2015.instDecidableWeakUniqueOfFintypeOfDecidableEq P = id (id inferInstance)

def CoppockBeaver2015.Exclusive {E : Type u_1} (P : E → SignType) (x : E) : Prop

Nothing other than x is a P — the exclusive component of only (57).

Equations

• CoppockBeaver2015.Exclusive P x = ∀ (y : E), y ≠ x → P y ≠ 1

@[instance_reducible]

instance CoppockBeaver2015.instDecidableRelForallSignTypeExclusiveOfFintypeOfDecidableEq {E : Type u_1} [Fintype E] [DecidableEq E] : DecidableRel Exclusive

Equations

• CoppockBeaver2015.instDecidableRelForallSignTypeExclusiveOfFintypeOfDecidableEq P x = { decide := decide (∀ a ∈ Finset.univ, (fun (y : E) => y ≠ x → P y ≠ 1) a), reflects_decide := ⋯ }

theorem CoppockBeaver2015.not_exclusive_iff {E : Type u_1} {P : E → SignType} {x : E} : ¬Exclusive P x ↔ ∃ (y : E), y ≠ x ∧ P y = 1

theorem CoppockBeaver2015.exclusive_iff_subset_singleton {E : Type u_1} {P : E → SignType} {x : E} : Exclusive P x ↔ Trivalent.posExt P ⊆ {x}

Exclusivity is containment of the positive extension in the singleton.

def CoppockBeaver2015.the {E : Type u_1} [DecidablePred WeakUnique] (P : E → SignType) : E → SignType

The Weak Fregean definite article (50) returns the restrictor, presupposing weak uniqueness and no existence.

Equations

• CoppockBeaver2015.the P x = (max (SignType.ofProp (CoppockBeaver2015.WeakUnique P)) 0).meetWeak (P x)

def CoppockBeaver2015.an {E : Type u_1} (P : E → SignType) : E → SignType

The indefinite article (65) is an identity on predicates.

Equations

• CoppockBeaver2015.an P = P

def CoppockBeaver2015.only {E : Type u_1} [DecidableRel Exclusive] (P : E → SignType) : E → SignType

Adjectival only (57) presupposes the prejacent and asserts exclusivity.

Equations

• CoppockBeaver2015.only P x = (max (P x) 0).meetWeak (SignType.ofProp (CoppockBeaver2015.Exclusive P x))

theorem CoppockBeaver2015.only_eq_one_iff {E : Type u_1} [DecidableRel Exclusive] {P : E → SignType} {x : E} : only P x = 1 ↔ P x = 1 ∧ Exclusive P x

theorem CoppockBeaver2015.only_eq_neg_one_iff {E : Type u_1} [DecidableRel Exclusive] {P : E → SignType} {x : E} : only P x = -1 ↔ P x = 1 ∧ ∃ (y : E), y ≠ x ∧ P y = 1

theorem CoppockBeaver2015.only_eq_zero_iff {E : Type u_1} [DecidableRel Exclusive] {P : E → SignType} {x : E} : only P x = 0 ↔ P x ≠ 1

Only presupposes its prejacent.

theorem CoppockBeaver2015.weakUnique_only {E : Type u_1} [DecidableRel Exclusive] (P : E → SignType) : WeakUnique (only P)

An only phrase satisfies weak uniqueness, so there is never more than one only P.

theorem CoppockBeaver2015.the_eq_of_weakUnique {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} (h : WeakUnique P) : the P = P

theorem CoppockBeaver2015.the_eq_zero_of_not_weakUnique {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} (h : ¬WeakUnique P) (x : E) : the P x = 0

theorem CoppockBeaver2015.the_eq_zero_iff {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} {x : E} : the P x = 0 ↔ ¬WeakUnique P ∨ P x = 0

theorem CoppockBeaver2015.the_ne_zero_iff {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} {x : E} : the P x ≠ 0 ↔ WeakUnique P ∧ P x ≠ 0

The definite is classical exactly on weakly unique restrictors, where the noun is.

theorem CoppockBeaver2015.neg_the_eq_zero_iff {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} {x : E} : -the P x = 0 ↔ ¬WeakUnique P ∨ P x = 0

The uniqueness presupposition projects through negation, (45)–(46), so the negated definite is undefined exactly where the definite is.

theorem CoppockBeaver2015.the_neg_one {E : Type u_1} [DecidablePred WeakUnique] (x : E) : the (fun (x : E) => -1) x = -1

The empty restrictor is weakly unique, so the definite of an empty noun is false rather than undefined — uniqueness without existence, the predicative reading of (13).

theorem CoppockBeaver2015.neg_the_neg_one {E : Type u_1} [DecidablePred WeakUnique] (x : E) : -the (fun (x : E) => -1) x = 1

Existence does not project, (45a), so that is not the heart is true when there are no hearts.

theorem CoppockBeaver2015.eq_of_the_eq_one {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} {a b : E} (ha : the P a = 1) (hb : the P b = 1) : a = b

Two subjects of a true predicative definite coincide. Weak uniqueness is what makes Löbner's negation test contradictory and his conjunction test equivalent, (114)–(115).

theorem CoppockBeaver2015.the_only {E : Type u_1} [DecidablePred WeakUnique] [DecidableRel Exclusive] (P : E → SignType) : the (only P) = only P

The uniqueness presupposition of the is trivially satisfied by an only phrase, so the only P means only P, (60).

theorem CoppockBeaver2015.anti_uniqueness {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} {x : E} [DecidableRel Exclusive] : -the (only P) x = 1 ↔ P x = 1 ∧ ∃ (y : E), y ≠ x ∧ P y = 1

x is not the only P is true exactly when x is a P and so is something else, the anti-uniqueness inference (64).

theorem CoppockBeaver2015.anti_uniqueness_presup {E : Type u_1} [DecidablePred WeakUnique] {P : E → SignType} {x : E} [DecidableRel Exclusive] : -the (only P) x = 0 ↔ P x ≠ 1

The presupposition of only projects through negation (63), so x is not the only P is undefined exactly when x is no P.

The entries as formulas of the paper's logic

The abbreviation |P| ≤ 1 of footnote 18 and the exclusive component of (57) are formulas of IL3, read with Haug's universal quantifier and the Weak Kleene conditional. On a restrictor that is somewhere defined the first is classical weak uniqueness, and where the prejacent holds the second is classical exclusivity, so the entries above are the paper's pointwise.

noncomputable def CoppockBeaver2015.atMostOneFormula {E : Type u_1} (P : E → SignType) : SignType

|P| ≤ 1 as a formula is ∀x[P(x) → ∀y[P(y) → x = y]].

Equations

• CoppockBeaver2015.atMostOneFormula P = Trivalent.forallHaug fun (x : E) => (-P x).joinWeak (Trivalent.forallHaug fun (y : E) => (-P y).joinWeak (SignType.ofProp (x = y)))

noncomputable def CoppockBeaver2015.exclusiveFormula {E : Type u_1} (P : E → SignType) (x : E) : SignType

The exclusive component of only as a formula is ∀y[x ≠ y → ¬P(y)].

Equations

• CoppockBeaver2015.exclusiveFormula P x = Trivalent.forallHaug fun (y : E) => (-SignType.ofProp (x ≠ y)).joinWeak (-P y)

theorem CoppockBeaver2015.atMostOne_eq_ofProp {E : Type u_1} {P : E → SignType} [Decidable (WeakUnique P)] (h : ∃ (x : E), P x ≠ 0) : atMostOneFormula P = SignType.ofProp (WeakUnique P)

theorem CoppockBeaver2015.the_eq_meetWeak_atMostOne {E : Type u_1} [DecidablePred WeakUnique] (P : E → SignType) (x : E) : the P x = (max (atMostOneFormula P) 0).meetWeak (P x)

The definite article is the paper's entry (50) pointwise.

theorem CoppockBeaver2015.exclusiveFormula_eq_ofProp {E : Type u_1} {P : E → SignType} {x : E} [Decidable (Exclusive P x)] (h : P x = 1) : exclusiveFormula P x = SignType.ofProp (Exclusive P x)

theorem CoppockBeaver2015.only_eq_meetWeak_exclusiveFormula {E : Type u_1} [DecidableRel Exclusive] (P : E → SignType) (x : E) : only P x = (max (P x) 0).meetWeak (exclusiveFormula P x)

Adjectival only is the paper's entry (57) pointwise.

The exclusive schema

Footnote 22: adjectival only instantiates the exclusive schema of [CB14], whose entry for the adjectival case constrains the current question to what things are P, its answers ranked by entailment and predicating cumulative sums. Read on the space of extensions of the noun, those answers are the propositions that the Ps include a given collection — upper sets, with the vacuous answer weakest and inert — and the schema's value at an extension is the entry (57).

def CoppockBeaver2015.answer {E : Type u_1} (X : Set E) : Set (Set E)

A partial answer to what things are P on the space of extensions says that the Ps include X.

Equations

• CoppockBeaver2015.answer X = Set.Ici X

theorem CoppockBeaver2015.mem_atLeast_answer {E : Type u_1} {w : Set E} {x : E} : w ∈ Focus.Particles.atLeast (fun (x1 x2 : Set (Set E)) => x1 ⊆ x2) (Set.range answer) (answer {x}) ↔ x ∈ w

Some true answer is at least as strong as the prejacent exactly when the Ps include x, so the schema's presupposition is the prejacent.

theorem CoppockBeaver2015.mem_atMost_answer {E : Type u_1} {w : Set E} {x : E} : w ∈ Focus.Particles.atMost (fun (x1 x2 : Set (Set E)) => x1 ⊆ x2) (Set.range answer) (answer {x}) ↔ w ⊆ {x}

No true answer is stronger than the prejacent exactly when the Ps are contained in {x}, so the schema's assertion is exclusivity.

theorem CoppockBeaver2015.only_answer_apply {E : Type u_1} [DecidableRel Exclusive] (w : Set E) [DecidablePred fun (x : E) => x ∈ w] (x : E) : Focus.Particles.only (fun (x1 x2 : Set (Set E)) => x1 ⊆ x2) (Set.range answer) (answer {x}) w = only (fun (y : E) => SignType.ofProp (y ∈ w)) x

Adjectival only is the exclusive schema at the question what things are P. The schema of [CB14] over the answers, on the entailment scale, evaluated at an extension, is the entry (57) of the predicate with that extension.

Presupposition profiles of the entries in Table 1

def CoppockBeaver2015.PresupposesUniqueness {E : Type u_1} (D : (E → SignType) → E → SignType) : Prop

An entry presupposes uniqueness when it is classical only on weakly unique restrictors.

Equations

• CoppockBeaver2015.PresupposesUniqueness D = ∀ (P : E → SignType) (x : E), D P x ≠ 0 → CoppockBeaver2015.WeakUnique P

def CoppockBeaver2015.PresupposesExistence {E : Type u_1} (D : (E → SignType) → E → SignType) : Prop

An entry presupposes existence when it is classical only on nonempty restrictors.

Equations

• CoppockBeaver2015.PresupposesExistence D = ∀ (P : E → SignType) (x : E), D P x ≠ 0 → (Trivalent.posExt P).Nonempty

theorem CoppockBeaver2015.not_presupposesUniqueness_of_ne_zero {E : Type u_1} [Nontrivial E] {D : (E → SignType) → E → SignType} {x : E} (h : D (fun (x : E) => 1) x ≠ 0) : ¬PresupposesUniqueness D

An entry classical on the full restrictor presupposes no uniqueness.

theorem CoppockBeaver2015.not_presupposesExistence_of_ne_zero {E : Type u_1} {D : (E → SignType) → E → SignType} {x : E} (h : D (fun (x : E) => -1) x ≠ 0) : ¬PresupposesExistence D

An entry classical on the empty restrictor presupposes no existence.

noncomputable def CoppockBeaver2015.theRussellian {E : Type u_1} (P : E → SignType) : E → SignType

The Russellian predicative entry (52a) asserts existence and uniqueness.

Equations

• CoppockBeaver2015.theRussellian P x = (SignType.ofProp (∃! y : E, P y = 1)).meetWeak (P x)

noncomputable def CoppockBeaver2015.theFregean {E : Type u_1} (P : E → SignType) : E → SignType

The Fregean predicative entry (52b) presupposes existence and uniqueness.

Equations

• CoppockBeaver2015.theFregean P x = (max (SignType.ofProp (∃! y : E, P y = 1)) 0).meetWeak (P x)

noncomputable def CoppockBeaver2015.theRussellianGQ {E : Type u_1} (P Q : E → SignType) : SignType

The Russellian quantificational entry (53a) asserts unique existence of the restrictor.

Equations

• CoppockBeaver2015.theRussellianGQ P Q = (SignType.ofProp (∃! y : E, P y = 1)).meetWeak (SignType.ofProp (Trivalent.posExt P ⊆ Trivalent.posExt Q))

noncomputable def CoppockBeaver2015.theFregeanGQ {E : Type u_1} (P Q : E → SignType) : SignType

The Fregean quantificational entry (53b) presupposes unique existence of the restrictor.

Equations

• CoppockBeaver2015.theFregeanGQ P Q = (max (SignType.ofProp (∃! y : E, P y = 1)) 0).meetWeak (SignType.ofProp (Trivalent.posExt P ⊆ Trivalent.posExt Q))

noncomputable def CoppockBeaver2015.be {E : Type u_1} (G : (E → SignType) → SignType) : E → SignType

Partee's be lowers a generalized quantifier to a predicate.

Equations

• CoppockBeaver2015.be G x = G fun (y : E) => SignType.ofProp (y = x)

noncomputable def CoppockBeaver2015.identIota {E : Type u_1} (P : E → SignType) : E → SignType

Partee's ident applied to the individual-denoting Fregean entry yields the property of being the unique P, undefined when there is none (Table 2).

Equations

• CoppockBeaver2015.identIota P x = (Reference.iota fun (x : E) => P x = 1).elim 0 fun (j : E) => SignType.ofProp (x = j)

theorem CoppockBeaver2015.presupposesUniqueness_the {E : Type u_1} [DecidablePred WeakUnique] : PresupposesUniqueness the

theorem CoppockBeaver2015.not_presupposesExistence_the {E : Type u_1} [Nonempty E] [DecidablePred WeakUnique] : ¬PresupposesExistence the

theorem CoppockBeaver2015.not_presupposesUniqueness_theRussellian {E : Type u_1} [Nontrivial E] : ¬PresupposesUniqueness theRussellian

theorem CoppockBeaver2015.not_presupposesExistence_theRussellian {E : Type u_1} [Nonempty E] : ¬PresupposesExistence theRussellian

theorem CoppockBeaver2015.theFregean_ne_zero_iff {E : Type u_1} {P : E → SignType} {x : E} : theFregean P x ≠ 0 ↔ (∃! y : E, P y = 1) ∧ P x ≠ 0

theorem CoppockBeaver2015.presupposesUniqueness_theFregean {E : Type u_1} : PresupposesUniqueness theFregean

theorem CoppockBeaver2015.presupposesExistence_theFregean {E : Type u_1} : PresupposesExistence theFregean

theorem CoppockBeaver2015.not_presupposesUniqueness_be_theRussellianGQ {E : Type u_1} [Nontrivial E] : ¬PresupposesUniqueness fun (P : E → SignType) => be (theRussellianGQ P)

Lowering the Russellian quantifier by be presupposes nothing (Table 2).

theorem CoppockBeaver2015.not_presupposesExistence_be_theRussellianGQ {E : Type u_1} [Nonempty E] : ¬PresupposesExistence fun (P : E → SignType) => be (theRussellianGQ P)

theorem CoppockBeaver2015.be_theFregeanGQ_ne_zero_iff {E : Type u_1} {P : E → SignType} {x : E} : be (theFregeanGQ P) x ≠ 0 ↔ ∃! y : E, P y = 1

theorem CoppockBeaver2015.presupposesUniqueness_be_theFregeanGQ {E : Type u_1} : PresupposesUniqueness fun (P : E → SignType) => be (theFregeanGQ P)

Lowering the Fregean quantifier by be presupposes both existence and uniqueness.

theorem CoppockBeaver2015.presupposesExistence_be_theFregeanGQ {E : Type u_1} : PresupposesExistence fun (P : E → SignType) => be (theFregeanGQ P)

theorem CoppockBeaver2015.identIota_ne_zero_iff {E : Type u_1} {P : E → SignType} {x : E} : identIota P x ≠ 0 ↔ ∃! y : E, P y = 1

theorem CoppockBeaver2015.presupposesUniqueness_identIota {E : Type u_1} : PresupposesUniqueness identIota

Lowering the individual-denoting Fregean entry by ident presupposes both existence and uniqueness (Table 2).

theorem CoppockBeaver2015.presupposesExistence_identIota {E : Type u_1} : PresupposesExistence identIota

theorem CoppockBeaver2015.no_anti_uniqueness_fregean {E : Type u_1} [DecidableRel Exclusive] (P : E → SignType) (x : E) : -theFregean (only P) x ≠ 1

Under the Fregean entry x is not the only P is never true (§2.2.3), since the presupposition that there is exactly one only P is inconsistent with the assertion that x, a P, is not one. The Weak Fregean entry has no such clash (anti_uniqueness).

Maximize Presupposition

def CoppockBeaver2015.ClassicallyEquivalent {E : Type u_1} (α β : (E → SignType) → E → SignType) : Prop

Two entries are classically equivalent (70) when, on bivalent restrictors, they agree wherever both are classical.

Equations

• CoppockBeaver2015.ClassicallyEquivalent α β = ∀ (P : E → SignType), Trivalent.IsBivalent P → ∀ (x : E), α P x ≠ 0 → β P x ≠ 0 → α P x = β P x

def CoppockBeaver2015.AtLeastAsStrong {E : Type u_1} (α β : (E → SignType) → E → SignType) : Prop

α is presuppositionally at least as strong as β when, on bivalent restrictors, wherever α is classical so is β. As printed, (71) quantifies the other way around, which with (72) would have the indefinite dominate the definite; the paper's own derivation of the opposite on the same page needs this transposition.

Equations

• CoppockBeaver2015.AtLeastAsStrong α β = ∀ (P : E → SignType), Trivalent.IsBivalent P → ∀ (x : E), α P x ≠ 0 → β P x ≠ 0

def CoppockBeaver2015.Dominates {E : Type u_1} (α β : (E → SignType) → E → SignType) : Prop

α presuppositionally dominates β (72) when the two are classically equivalent and α is strictly stronger.

Equations

• CoppockBeaver2015.Dominates α β = (CoppockBeaver2015.ClassicallyEquivalent α β ∧ CoppockBeaver2015.AtLeastAsStrong α β ∧ ¬CoppockBeaver2015.AtLeastAsStrong β α)

theorem CoppockBeaver2015.the_dominates_an {E : Type u_1} [Nontrivial E] [DecidablePred WeakUnique] : Dominates the an

The definite article dominates the indefinite.

def CoppockBeaver2015.Blocks {E : Type u_1} {W : Type u_2} (C : Set W) (D : ((E → SignType) → E → SignType) → W → SignType) (α β : (E → SignType) → E → SignType) : Prop

Under Maximize Presupposition (75), α blocks its competitor β in context C and derivation D, the sentence meaning as a function of the article's meaning, when α dominates β and the two derivations update C alike; the update of a context with a meaning (74) is the substrate's Heimian partial update CCP.Partial.ofTrivalent. Clause (i), competitorhood, is glossed in the appendix as classical equivalence with a high-frequency item and is carried by Dominates.

Equations

• CoppockBeaver2015.Blocks C D α β = (CoppockBeaver2015.Dominates α β ∧ DynamicSemantics.CCP.Partial.ofTrivalent (D α) C = DynamicSemantics.CCP.Partial.ofTrivalent (D β) C)

theorem CoppockBeaver2015.blocks_of_weakUnique {E : Type u_1} {W : Type u_2} [DecidablePred WeakUnique] {C : Set W} (F : W → (E → SignType) → SignType) (π : W → E → SignType) [Nontrivial E] (h : ∀ w ∈ C, WeakUnique (π w)) : Blocks C (fun (α : (E → SignType) → E → SignType) (w : W) => F w (α (π w))) the an

Where the restrictor is weakly unique throughout the context, the blocks a in every derivation applying the article to it.

theorem CoppockBeaver2015.not_blocks_of_not_weakUnique {E : Type u_1} {W : Type u_2} [DecidablePred WeakUnique] {C : Set W} (F : W → (E → SignType) → SignType) (π : W → E → SignType) (hF : ∀ (w : W), (F w fun (x : E) => 0) = 0) {w : W} (hw : w ∈ C) (h : ¬WeakUnique (π w)) (hdom : ∀ w ∈ C, F w (π w) ≠ 0) : ¬Blocks C (fun (α : (E → SignType) → E → SignType) (w : W) => F w (α (π w))) the an

Where weak uniqueness fails at a world of the context, the fails to block a provided the indefinite sentence is classical on the context and the material around the description is strict in its undefinedness.

theorem CoppockBeaver2015.an_only_blocked {E : Type u_1} {W : Type u_2} [DecidablePred WeakUnique] {C : Set W} (F : W → (E → SignType) → SignType) (π : W → E → SignType) [DecidableRel Exclusive] [Nontrivial E] : Blocks C (fun (α : (E → SignType) → E → SignType) (w : W) => F w (α (only (π w)))) the an

An only P is blocked in every context (66), since an only phrase meets the definite's presupposition and the two derivations coincide.

theorem CoppockBeaver2015.sentence_the_only_eq_an_only {E : Type u_1} {W : Type u_2} [DecidablePred WeakUnique] (F : W → (E → SignType) → SignType) (π : W → E → SignType) [DecidableRel Exclusive] : (fun (w : W) => F w (the (only (π w)))) = fun (w : W) => F w (an (only (π w)))

The sentence with the and the sentence with a(n) mean the same whenever the description is an only phrase, since the article contributes nothing to an inherently unique description.

theorem CoppockBeaver2015.not_blocked_sentence_an_only {E : Type u_1} {W : Type u_2} [DecidablePred WeakUnique] (F : W → (E → SignType) → SignType) (π : W → E → SignType) [DecidableRel Exclusive] : ¬Competition.Blocked (Competition.sameAssertion (fun (x : W → SignType) => {fun (w : W) => F w (the (only (π w)))}) fun (p : W → SignType) => {w : W | p w = 1}) (fun (p : W → SignType) => {w : W | p w ≠ 0}) fun (w : W) => F w (an (only (π w)))

With the the-sentence as the alternative, the an-sentence is not blocked at sentence level, although an_only_blocked blocks it at expression level, so Maximize Presupposition must compare expressions rather than sentences.

Existence in argument position

noncomputable def CoppockBeaver2015.iota {E : Type u_1} (P : E → SignType) : Option E

The iota shift (84) returns the unique satisfier, or the undefined individual.

Equations

• CoppockBeaver2015.iota P = Reference.iota fun (x : E) => P x = 1

theorem CoppockBeaver2015.iota_isSome_iff {E : Type u_1} (P : E → SignType) : (iota P).isSome = true ↔ ∃! x : E, P x = 1

theorem CoppockBeaver2015.iota_eq_none_iff {E : Type u_1} (P : E → SignType) : iota P = none ↔ ¬∃! x : E, P x = 1

theorem CoppockBeaver2015.iota_neg_one {E : Type u_1} : (iota fun (x : E) => -1) = none

On the argumental reading of (14), the empty restrictor has no referent.

theorem CoppockBeaver2015.iota_the {E : Type u_1} [DecidablePred WeakUnique] (P : E → SignType) : iota (the P) = iota P

Under iota the article's presupposition adds nothing, since iota presupposes uniqueness.

theorem CoppockBeaver2015.elim_iota_ne_zero_iff {E : Type u_1} (P f : E → SignType) (hf : ∀ (x : E), f x ≠ 0) : (iota P).elim 0 f ≠ 0 ↔ ∃! x : E, P x = 1

On the determinate reading (87), undefinedness of the individual percolates (86), so the sentence is classical exactly when the description has exactly one satisfier.

noncomputable def CoppockBeaver2015.ex {E : Type u_1} (P Q : E → SignType) : SignType

The existential shift (85) asserts a common satisfier of restrictor and scope.

Equations

• CoppockBeaver2015.ex P Q = Trivalent.existsHaug fun (x : E) => (P x).meetWeak (Q x)

theorem CoppockBeaver2015.ex_zero_left {E : Type u_1} (Q : E → SignType) : ex (fun (x : E) => 0) Q = 0

def CoppockBeaver2015.scopeInside {E : Type u_1} (T : E → E → SignType) (Q : (E → SignType) → SignType) (M : (E → SignType) → E → SignType) : E → SignType

The type shift of footnote 26 scopes an argument quantifier inside the modified description — the further existential within the nominal that intervenes between the determiner and the exclusive.

Equations

• CoppockBeaver2015.scopeInside T Q M x = Q fun (z : E) => M (fun (y : E) => T z y) x

theorem CoppockBeaver2015.not_update_dom_iota {E : Type u_1} {W : Type u_2} {C : Set W} {π : W → E → SignType} (G : W → E → SignType) {w : W} (hw : w ∈ C) (h : ¬∃! x : E, π w x = 1) : ¬(DynamicSemantics.CCP.Partial.ofTrivalent (fun (w : W) => (iota (π w)).elim 0 (G w)) C).Dom

Where some world of the context lacks a unique satisfier, the determinate reading has no defined update (§3.2–3.3).

theorem CoppockBeaver2015.readings_agree_of_existsUnique {E : Type u_1} {W : Type u_2} {C : Set W} {π Q : W → E → SignType} (hπ : ∀ w ∈ C, Trivalent.IsBivalent (π w)) (hQ : ∀ w ∈ C, Trivalent.IsBivalent (Q w)) (h : ∀ w ∈ C, ∃! x : E, π w x = 1) : DynamicSemantics.CCP.Partial.ofTrivalent (fun (w : W) => (iota (π w)).elim 0 (Q w)) C = DynamicSemantics.CCP.Partial.ofTrivalent (fun (w : W) => ex (π w) (Q w)) C

Where every world of the context has exactly one satisfier, the determinate and the indeterminate readings update the context alike (§3.4).

theorem CoppockBeaver2015.no_determinate_indefinites {E : Type u_1} {W : Type u_2} [Nontrivial E] [DecidablePred WeakUnique] (F : W → (E → SignType) → SignType) (π G : W → E → SignType) {C : Set W} (h : ¬Blocks C (fun (α : (E → SignType) → E → SignType) (w : W) => F w (α (π w))) the an) : ¬(DynamicSemantics.CCP.Partial.ofTrivalent (fun (w : W) => (iota (π w)).elim 0 (G w)) C).Dom

An indefinite the definite fails to block has, at some world of the context, a restrictor without a unique satisfier, so its reading under iota has no defined update — no determinate indefinites (§3.3).

theorem CoppockBeaver2015.neg_ex_the_only {E : Type u_1} [DecidablePred WeakUnique] [DecidableRel Exclusive] {P Q : E → SignType} (hP : Trivalent.IsBivalent P) (hQ : Trivalent.IsBivalent Q) : -ex (the (only P)) Q = (Trivalent.existsHaug fun (x : E) => max (P x) 0).meetWeak (-Trivalent.existsHaug fun (x : E) => (P x).meetWeak ((SignType.ofProp (Exclusive P x)).meetWeak (Q x)))

By Quantifier Projection (A.4.2), negated the only P under the existential shift presupposes that there is a P and denies that any sole P bears Q, the anti-uniqueness reading (89)–(94).

theorem CoppockBeaver2015.argumental_anti_uniqueness_presup {E : Type u_1} [DecidablePred WeakUnique] [DecidableRel Exclusive] {P Q : E → SignType} (hQ : Trivalent.IsBivalent Q) : -ex (the (only P)) Q = 0 ↔ ∀ (x : E), P x ≠ 1

The argumental reading presupposes a P, not an only P (§3.2), so it is undefined exactly when there is no P.

theorem CoppockBeaver2015.argumental_anti_uniqueness {E : Type u_1} [DecidablePred WeakUnique] [DecidableRel Exclusive] {P Q : E → SignType} (hQ : Trivalent.IsBivalent Q) : -ex (the (only P)) Q = 1 ↔ (∃ (x : E), P x = 1) ∧ ∀ (x : E), P x = 1 → Exclusive P x → Q x ≠ 1

The argumental anti-uniqueness reading is true exactly when there is a P and no sole P bears Q, as in (80a) with several talks, one of which Anna gave.

Possessives

def CoppockBeaver2015.toRelational {E : Type u_1} (poss : E → E → SignType) (P : E → SignType) (y : E) : E → SignType

The sortal-to-relational shift (129) sends a noun to the Ps possessed by y. The appendix's TS3 prints the possessor arguments in the opposite order; the main text's is followed.

Equations

• CoppockBeaver2015.toRelational poss P y x = (P x).meetWeak (poss x y)

theorem CoppockBeaver2015.isBivalent_toRelational {E : Type u_1} {poss : E → E → SignType} {P : E → SignType} (hP : Trivalent.IsBivalent P) (hposs : ∀ (x y : E), poss x y ≠ 0) (y : E) : Trivalent.IsBivalent (toRelational poss P y)

A possessive predicate presupposes nothing beyond its parts (§4.1, §4.3). It is classical wherever noun and possession are, so predicative possessives signal no uniqueness.

theorem CoppockBeaver2015.possessive_not_competitor {E : Type u_1} [DecidableEq E] [DecidablePred WeakUnique] {poss : E → E → SignType} {x y : E} (h : poss x y = -1) : ¬ClassicallyEquivalent (fun (P : E → SignType) => toRelational poss P y) the

Possessives do not compete with the definite article (§4). A possessive predicate is not classically equivalent to the, since a weakly unique noun true of an individual the possessor does not own separates them.

theorem CoppockBeaver2015.possessive_anti_uniqueness {E : Type u_1} [DecidableRel Exclusive] {poss : E → E → SignType} {P Q : E → SignType} (hQ : Trivalent.IsBivalent Q) (hposs : ∀ (x y : E), poss x y ≠ 0) (y : E) : -ex (toRelational poss (only P) y) Q = 1 ↔ (∃ (x : E), P x = 1) ∧ ∀ (x : E), P x = 1 → Exclusive P x → poss x y = 1 → Q x ≠ 1

On the indeterminate reading of an argumental possessive (134), he didn't make his only appearance presupposes an appearance and denies that he made any sole appearance of his.

The paper's models

Two worlds settle whether Frida wrote one book or two, the contexts of (73); two crashes with a single survivor each make only survivor of a plane crash, with the crash scoped inside the description as in (69), hold of two people.

inductive CoppockBeaver2015.Frida.Book : Type

• one : Book
• two : Book

@[instance_reducible]

instance CoppockBeaver2015.Frida.instDecidableEqBook : DecidableEq Book

Equations

• CoppockBeaver2015.Frida.instDecidableEqBook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CoppockBeaver2015.Frida.instFintypeBook : Fintype Book

Equations

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

instance CoppockBeaver2015.Frida.instNontrivialBook : Nontrivial Book

inductive CoppockBeaver2015.Frida.World : Type

• oneBook : World
• twoBooks : World

@[instance_reducible]

instance CoppockBeaver2015.Frida.instDecidableEqWorld : DecidableEq World

Equations

• CoppockBeaver2015.Frida.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CoppockBeaver2015.Frida.instFintypeWorld : Fintype World

Equations

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

def CoppockBeaver2015.Frida.wrote : World → Book → SignType

At one world Frida wrote one book; at the other, two.

Equations

• CoppockBeaver2015.Frida.wrote CoppockBeaver2015.Frida.World.oneBook CoppockBeaver2015.Frida.Book.one = 1
• CoppockBeaver2015.Frida.wrote CoppockBeaver2015.Frida.World.oneBook CoppockBeaver2015.Frida.Book.two = -1
• CoppockBeaver2015.Frida.wrote CoppockBeaver2015.Frida.World.twoBooks x✝ = 1

def CoppockBeaver2015.Frida.reading : World → Book → SignType

The speaker is reading the first book.

Equations

• CoppockBeaver2015.Frida.reading x✝ b = SignType.ofProp (b = CoppockBeaver2015.Frida.Book.one)

noncomputable def CoppockBeaver2015.Frida.sentence (α : (Book → SignType) → Book → SignType) : World → SignType

sentence α interprets I'm now reading (a/the) book she wrote with the description shifted existentially.

Equations

• CoppockBeaver2015.Frida.sentence α w = CoppockBeaver2015.ex (α (CoppockBeaver2015.Frida.wrote w)) (CoppockBeaver2015.Frida.reading w)

theorem CoppockBeaver2015.Frida.blocks_of_one : Blocks {World.oneBook} sentence the an

Once the context settles that Frida wrote exactly one book, the blocks a, (73b).

theorem CoppockBeaver2015.Frida.not_blocks_of_open : ¬Blocks Set.univ sentence the an

While the context leaves the number of books open, a is not blocked, (73a).

inductive CoppockBeaver2015.Crash.Ind : Type

• crash₁ : Ind
• crash₂ : Ind
• scott : Ind
• sam : Ind

@[instance_reducible]

instance CoppockBeaver2015.Crash.instDecidableEqInd : DecidableEq Ind

Equations

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

@[instance_reducible]

instance CoppockBeaver2015.Crash.instFintypeInd : Fintype Ind

Equations

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

instance CoppockBeaver2015.Crash.instNontrivialInd : Nontrivial Ind

def CoppockBeaver2015.Crash.crash : Ind → SignType

crash holds of the two crash individuals.

Equations

• CoppockBeaver2015.Crash.crash z = SignType.ofProp (z = CoppockBeaver2015.Crash.Ind.crash₁ ∨ z = CoppockBeaver2015.Crash.Ind.crash₂)

def CoppockBeaver2015.Crash.survived (z : Ind) : Ind → SignType

Each crash has a single survivor, Scott of the first and Sam of the second.

Equations

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

noncomputable def CoppockBeaver2015.Crash.onlySurvivor : Ind → SignType

In only survivor of a plane crash (69), the type shift of footnote 26 scopes the crash inside the description.

Equations

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

theorem CoppockBeaver2015.Crash.not_weakUnique_onlySurvivor : ¬WeakUnique onlySurvivor

The description holds of as many people as there are crashes with a single survivor.

theorem CoppockBeaver2015.Crash.an_only_survivor_not_blocked : ¬Blocks Set.univ (fun (α : (Ind → SignType) → Ind → SignType) (x : Unit) => α onlySurvivor Ind.scott) the an

An only survivor of a plane crash is not blocked on the derivation scoping the crash inside the description, (68).

noncomputable def CoppockBeaver2015.Crash.high (α : (Ind → SignType) → Ind → SignType) : Unit → SignType

The high-scope derivation places the crash above the article.

Equations

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

theorem CoppockBeaver2015.Crash.high_the_eq_low_an : high the = fun (x : Unit) => an onlySurvivor Ind.scott

The only survivor of a plane crash with the crash scoped high means what an only survivor of a plane crash means with the crash scoped low.

theorem CoppockBeaver2015.Crash.the_only_survivor_blocked : Blocks Set.univ high the an

On the high-scope derivation the blocks a. Together with an_only_survivor_not_blocked, this shows that blocking compares derivations rather than strings, so the surviving surface form owes its life to the low-scope derivation.

The paper's judgments

The rows of Data/Examples/CoppockBeaver2015.json with a restrictor feature are the predicative definites whose felicity turns on weak uniqueness alone, (10)–(12) and (44)–(46): a restrictor that holds of nothing, the scenario in which iguanas have no hearts, one that holds of both items of a two-item scenario, and an only phrase over the latter. The rows with an expression feature are Löbner's predicative tests (114)–(115), in the scenario where both subjects satisfy the noun.

inductive CoppockBeaver2015.Scenario.Item : Type

• this : Item
• that : Item

@[instance_reducible]

instance CoppockBeaver2015.Scenario.instDecidableEqItem : DecidableEq Item

Equations

• CoppockBeaver2015.Scenario.instDecidableEqItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CoppockBeaver2015.Scenario.instFintypeItem : Fintype Item

Equations

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

def CoppockBeaver2015.Scenario.restrictors : List (String × (Item → SignType))

restrictors maps a row's restrictor feature to its predicate.

Equations

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

theorem CoppockBeaver2015.Scenario.restrictor_rows (row : Datum) : row ∈ Examples.all → ∀ P ∈ row.parse? "restrictor" restrictors, row.judgment = Judgment.acceptable ↔ the P Item.this ≠ 0

A predicative-definite row is acceptable exactly when the definite of its restrictor is classical of the subject.

def CoppockBeaver2015.Lobner.expressions : List (String × (Scenario.Item → SignType))

expressions maps a row's expression, a predicative definite, indefinite, or possessive with a single possessor, to the predicate it forms from the noun in the scenario where both subjects satisfy it.

Equations

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

def CoppockBeaver2015.Lobner.verdicts : List (String × Bool)

verdicts reads a row's verdict as whether its test forces the two subjects to coincide.

Equations

• CoppockBeaver2015.Lobner.verdicts = [("contradictory", true), ("equivalent", true), ("notContradictory", false), ("notEquivalent", false)]

theorem CoppockBeaver2015.Lobner.rows (row : Datum) : row ∈ Examples.all → ∀ p ∈ row.parse? "expression" expressions, ∀ v ∈ row.parse? "verdict" verdicts, v = true ↔ ∀ (a b : Scenario.Item), (p a).meetWeak (p b) = 1 → a = b

With both subjects satisfying the noun, a row's test verdict is coincidence of the two subjects exactly for the definite (eq_of_the_eq_one), the predicative tests (114)–(115).