Chierchia (2006): Broaden your views

Chierchia treats every polarity-sensitive item as an existential that activates domain alternatives, Kadmon and Landman's domain widening. An enrichment operation factors the alternatives into meaning, and an implicature-freezing operator σ locks the result in place. The items differ in two respects, (94): the size of their alternatives, large subdomains (MAX) enriched by the even-like evenEnrich or every subdomain that stands a chance (MIN) enriched by the antiexhaustive oMinus, and whether σ presupposes proper strengthening. Pure negative-polarity items (mai, ever) are MAX; any is MIN with the plain σ; Italian qualsiasi is MIN with the presuppositional σ; the existential free-choice items (irgendein, uno N qualsiasi) add the uniqueness implicature of their indefinite morphology, after Kratzer and Shimoyama.

Main definitions

• evenEnrich, oMinus: the even-like enrichment E, (108b), and the antiexhaustive enrichment O⁻ of a domain-dependent proposition, (108c).
• exactlyOne, atLeastTwo: the exhaustified indefinite, (81b), and its scalar alternative.
• Profile, Freezer: the parameters of (94), with the plain and the strong σ of (72).
• Profile.Felicitous: a logical form is felicitous when σ admits its output and the sentence is consistent.
• Available, Excluded: some admissible model makes a reading felicitous, or none does.

Main results

• evenEnrich_eq_or_eq_empty, evenEnrich_disj_eq_empty, evenEnrich_image_antitone_eq: E is vacuous or contradictory; it is contradictory at the existential and vacuous under negation, (47)–(53).
• oMinus_biUnion, oMinus_biUnion_eq_inter_sInter: O⁻ gives an existential universal force over its domain, (63), and there agrees with the simpler (62).
• oMinus_antitone_eq, not_oMinus_ssubset_of_antitone: under negation the free-choice implicature vanishes, so qualunque has no negative-polarity construal, (65)–(72).
• oMinus_biUnion_eq_empty_of_isActualist: an episodic universal over a widened domain is never true, (67).
• exh_atLeastTwo_eq_exactlyOne, oMinus_exactlyOne_eq_empty: O against the scalar alternative yields uniqueness, (81), and an existential free-choice item is then contradictory in an episodic sentence, (82).
• oMinus_core_biUnion_subset, oMinus_core_exactlyOne_subset, card_le_one_of_forall_mem_core_exactlyOne: under a necessity modal O⁻ yields free choice, (93d) and (117), while letting the whole domain be an antecedent would leave room for a single doctor only, (118).
• judgedReadings_predicted, judgedSentences_predicted: every judgment in the paper's rows follows from the item's profile.

Implementation notes

Propositions are sets of worlds, and "stronger relative to the common ground" in (50a) is entailment. A domain is a finite set of possible witnesses, the widened domain of (57b), so (61b)'s alternatives are those over its nonempty subdomains; large alternatives are taken to be the proper ones. As in (95), a formula is a function from domains to propositions. oMinus follows (108c) rather than (62): relating only alternatives over disjoint subdomains keeps the whole domain from being an antecedent, which the appendix requires to avoid (118). A scalar item's uniqueness implicature is added where it strengthens, by the selection of the strongest enriched meaning in (110), which yields the some_D of (91) under negation.

σ and the recursion of appendix A3 are not represented; a reading is a logical form placing σ among the environment's operators, as in (64)–(65), (91) and (93). The future and the imperative are treated as necessity modals and the generic as a positive context without an actuality condition, since the paper computes none of them beyond (55), (71) and §2. Subtrigging enters as a domain anchored to the actual individuals, (68c). A reading marked ?? or worse is predicted excluded and one marked at most ? available, so the dispreferences of (10e), (10g) and (93b) are not derived. Rows rescued by a covert modal, (4), (8a) and (89), or by intervention, (86)–(87), carry a device feature and are set aside.

TODO

• The intervention effect (86)–(87), a DP between σ and the item, is a syntactic stipulation in the paper and is not formalized.
• The paper excludes the scoped-out logical form (74b) without subtrigging only "by whatever rules out I read any book"; an actualist scope that presupposes rather than entails actuality would derive it.

References

• [Chi06]
• [KL93]
• [KS17]
• [Has97]

The lexicon of polarity-sensitive items, (94)

inductive Chierchia2006.DomainAlternatives : Type

An item activates as alternatives either the large subdomains, (46), or every subdomain that stands a chance, (56) and (61b).

• max : DomainAlternatives
• min : DomainAlternatives

@[instance_reducible]

instance Chierchia2006.instDecidableEqDomainAlternatives : DecidableEq DomainAlternatives

Equations

• Chierchia2006.instDecidableEqDomainAlternatives x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Chierchia2006.instReprDomainAlternatives.repr : DomainAlternatives → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Chierchia2006.instReprDomainAlternatives : Repr DomainAlternatives

Equations

• Chierchia2006.instReprDomainAlternatives = { reprPrec := Chierchia2006.instReprDomainAlternatives.repr }

inductive Chierchia2006.Freezer : Type

The implicature-freezing operator σ comes plain or strong; the strong one presupposes that the enrichment properly strengthens what it freezes, (72).

• plain : Freezer
• strong : Freezer

@[instance_reducible]

instance Chierchia2006.instDecidableEqFreezer : DecidableEq Freezer

Equations

• Chierchia2006.instDecidableEqFreezer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Chierchia2006.instReprFreezer : Repr Freezer

Equations

• Chierchia2006.instReprFreezer = { reprPrec := Chierchia2006.instReprFreezer.repr }

def Chierchia2006.instReprFreezer.repr : Freezer → ℕ → Std.Format

Equations

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

structure Chierchia2006.Profile : Type

A polarity-sensitive item in (94) is fixed by the size of its domain alternatives, whether indefinite morphology adds scalar alternatives, (78), and the freezing operator it selects.

• alternatives : DomainAlternatives
• scalar : Bool
• freezer : Freezer

@[instance_reducible]

instance Chierchia2006.instDecidableEqProfile : DecidableEq Profile

Equations

• Chierchia2006.instDecidableEqProfile = Chierchia2006.instDecidableEqProfile.decEq

def Chierchia2006.instDecidableEqProfile.decEq (x✝ x✝¹ : Profile) : Decidable (x✝ = x✝¹)

Equations

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

def Chierchia2006.instReprProfile.repr : Profile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Chierchia2006.instReprProfile : Repr Profile

Equations

• Chierchia2006.instReprProfile = { reprPrec := Chierchia2006.instReprProfile.repr }

def Chierchia2006.pureNPI : Profile

The pure negative-polarity items mai, ever and alcuno are σ[D-MAX].

Equations

• Chierchia2006.pureNPI = { alternatives := Chierchia2006.DomainAlternatives.max, scalar := false, freezer := Chierchia2006.Freezer.plain }

def Chierchia2006.npiFci : Profile

Any is σ[D-MIN], a negative-polarity item under negation and a universal free-choice item elsewhere.

Equations

• Chierchia2006.npiFci = { alternatives := Chierchia2006.DomainAlternatives.min, scalar := false, freezer := Chierchia2006.Freezer.plain }

def Chierchia2006.pureFci : Profile

The pure universal free-choice items qualsiasi and qualunque select the strong σ over MIN alternatives.

Equations

• Chierchia2006.pureFci = { alternatives := Chierchia2006.DomainAlternatives.min, scalar := false, freezer := Chierchia2006.Freezer.strong }

def Chierchia2006.existentialNpiFci : Profile

German irgendein is σ[MIN, SCAL], an existential free-choice item with negative-polarity uses.

Equations

• Chierchia2006.existentialNpiFci = { alternatives := Chierchia2006.DomainAlternatives.min, scalar := true, freezer := Chierchia2006.Freezer.plain }

def Chierchia2006.existentialPureFci : Profile

Italian uno N qualsiasi selects the strong σ over MIN alternatives and carries scalar alternatives.

Equations

• Chierchia2006.existentialPureFci = { alternatives := Chierchia2006.DomainAlternatives.min, scalar := true, freezer := Chierchia2006.Freezer.strong }

Even-like enrichment of large alternatives, §4

def Chierchia2006.evenEnrich {W : Type u_1} (C : Set (Set W)) (p : Set W) : Set W

Even-like enrichment E, (50a) and (108b), keeps the prejacent where it is at least as strong as every alternative.

Equations

• Chierchia2006.evenEnrich C p = {w : W | w ∈ p ∧ ∀ q ∈ C, p ⊆ q}

theorem Chierchia2006.evenEnrich_subset {W : Type u_1} (C : Set (Set W)) (p : Set W) : evenEnrich C p ⊆ p

theorem Chierchia2006.evenEnrich_eq_or_eq_empty {W : Type u_1} (C : Set (Set W)) (p : Set W) : evenEnrich C p = p ∨ evenEnrich C p = ∅

The even-like implicature is a condition on the alternatives, not on the world: enrichment is vacuous or a contradiction.

theorem Chierchia2006.evenEnrich_eq_empty_of_not_subset {W : Type u_1} {C : Set (Set W)} {p q : Set W} (hq : q ∈ C) (h : ¬p ⊆ q) : evenEnrich C p = ∅

An alternative the prejacent does not entail makes even-like enrichment a contradiction.

theorem Chierchia2006.evenEnrich_disj_eq_empty {W : Type u_1} {E : Type u_2} {D S : Finset E} {P : E → Set W} {C : Set (Set W)} (hS : ⋃ x ∈ S, P x ∈ C) {a : E} {w : W} (ha : a ∈ D) (hPa : w ∈ P a) (hSw : ∀ x ∈ S, w ∉ P x) : evenEnrich C (⋃ x ∈ D, P x) = ∅

A pure negative-polarity item at its existential is deviant, (47)–(48): a world where some member of the domain is a witness but no member of the subdomain S is shows that the statement does not entail the alternative over S, so even-like enrichment is a contradiction.

theorem Chierchia2006.evenEnrich_image_antitone_eq {W : Type u_1} {C : Set W → Set W} (hC : Antitone C) {A : Set (Set W)} {p : Set W} (hA : ∀ q ∈ A, q ⊆ p) : evenEnrich (C '' A) (C p) = C p

Under an antitone embedding, alternatives that each entail the prejacent are entailed by the embedded prejacent, so even-like enrichment is vacuous: domain widening comes to fruition in a downward-entailing context, (49) and (53).

theorem Chierchia2006.eq_empty_of_evenEnrich_ssubset {W : Type u_1} {C : Set (Set W)} {p : Set W} (h : evenEnrich C p ⊂ p) : evenEnrich C p = ∅

An item triggering the even-like implicature can meet the presupposition of the strong σ only by a contradiction, so pure negative-polarity items select the plain σ, footnote 33.

Existential free-choice items, §6 and appendix A4

def Chierchia2006.exactlyOne {W : Type u_1} {E : Type u_2} (P : E → Set W) (S : Finset E) : Set W

The exhaustified indefinite exactlyOne P S of (81b) holds where exactly one member of S is a witness.

Equations

• Chierchia2006.exactlyOne P S = {w : W | ∃! x : E, x ∈ S ∧ w ∈ P x}

def Chierchia2006.atLeastTwo {W : Type u_1} {E : Type u_2} (P : E → Set W) (S : Finset E) : Set W

atLeastTwo P S holds where two members of S are witnesses, the next row of the scale in (79c).

Equations

• Chierchia2006.atLeastTwo P S = {w : W | ∃ x ∈ S, ∃ y ∈ S, x ≠ y ∧ w ∈ P x ∧ w ∈ P y}

theorem Chierchia2006.exh_atLeastTwo_eq_exactlyOne {W : Type u_1} {E : Type u_2} (P : E → Set W) {S : Finset E} (h : ¬⋃ x ∈ S, P x ⊆ atLeastTwo P S) : Exhaustification.exh {atLeastTwo P S} (⋃ x ∈ S, P x) = exactlyOne P S

Exhaustifying the existential against its scalar alternative yields the exhaustified indefinite, (81a)–(81b), provided some world has a witness but not two.

theorem Chierchia2006.oMinus_exactlyOne_eq_empty {W : Type u_1} {E : Type u_2} (P : E → Set W) {D : Finset E} (hD : 1 < D.card) : Exhaustification.oMinus (exactlyOne P) D = ∅

With two possible witnesses the uniqueness and free-choice implicatures clash, (82). The unique witness of the domain is the unique witness of its singleton, which forces every other singleton to have a witness too, so an existential free-choice item in an episodic sentence is contradictory.

theorem Chierchia2006.notMem_core_exactlyOne {W : Type u_1} {E : Type u_2} (P : E → Set W) {D S : Finset E} {R : SetRel W W} {w : W} (hw : w ∈ R.dom) (h : w ∈ Exhaustification.oMinus (fun (S : Finset E) => R.core (exactlyOne P S)) D) (hS : S ⊂ D) (hS' : S.Nonempty) : w ∉ R.core (exactlyOne P S)

Under a necessity modal the uniqueness and free-choice implicatures together rule out any proper subdomain being necessary, (117c): a necessary subdomain would make its complement necessary too, and an accessible world would have two witnesses.

theorem Chierchia2006.oMinus_core_exactlyOne_subset {W : Type u_1} {E : Type u_2} (P : E → Set W) {D : Finset E} {R : SetRel W W} (hD : 1 < D.card) : Exhaustification.oMinus (fun (S : Finset E) => R.core (exactlyOne P S)) D ∩ R.dom ⊆ ⋂ a ∈ D, R.preimage (P a)

Under a necessity modal every member of a domain with two members is a witness in some accessible world, the free choice of (117d) and (93d).

theorem Chierchia2006.card_le_one_of_forall_mem_core_exactlyOne {W : Type u_1} {E : Type u_2} (P : E → Set W) {D : Finset E} {R : SetRel W W} {w : W} (hw : w ∈ R.dom) (h : ∀ T ⊆ D, T.Nonempty → w ∈ R.core (exactlyOne P T)) : D.card ≤ 1

If every nonempty subdomain is necessarily witnessed by exactly one member, the domain has at most one member, which is why the whole domain must not be an antecedent, (118).

def Chierchia2006.accessible : SetRel (Fin 3) (Fin 3)

In the model of (85) the evaluation world 0 accesses the two other worlds.

Equations

• Chierchia2006.accessible = {p : Fin 3 × Fin 3 | p.1 = 0 ∧ p.2 ≠ 0}

def Chierchia2006.married (d : Fin 2) : Set (Fin 3)

Doctor d is married exactly in world d + 1, the distribution of (85).

Equations

• Chierchia2006.married d = {d.succ}

theorem Chierchia2006.zero_mem_oMinus_preimage_exactlyOne_married : 0 ∈ Exhaustification.oMinus (fun (S : Finset (Fin 2)) => accessible.preimage (exactlyOne married S)) Finset.univ

Two doctors, each married in one accessible world, satisfy the enriched statement under a possibility modal, the rescue of (84)–(85).

theorem Chierchia2006.zero_mem_oMinus_core_exactlyOne_married : 0 ∈ Exhaustification.oMinus (fun (S : Finset (Fin 2)) => accessible.core (exactlyOne married S)) Finset.univ

The same distribution satisfies the enriched statement under a necessity modal, (115)–(117): no single doctor is necessary, so the free-choice implicature holds vacuously.

theorem Chierchia2006.not_forall_zero_mem_core_exactlyOne_married : ¬∀ T ⊆ Finset.univ, T.Nonempty → 0 ∈ accessible.core (exactlyOne married T)

On the same model, asserting every alternative under the necessity modal fails, (118).

The distribution of the items, (94)

def Chierchia2006.Freezer.Admits {W : Type u_1} : Freezer → Set W → Set W → Prop

The plain σ admits every enrichment, and the strong σ one that properly strengthens the statement it freezes, (72).

Equations

• Chierchia2006.Freezer.plain.Admits x✝¹ x✝ = True
• Chierchia2006.Freezer.strong.Admits x✝¹ x✝ = (x✝¹ ⊂ x✝)

theorem Chierchia2006.Freezer.admits_of_strong {W : Type u_1} (f : Freezer) {s q : Set W} (h : strong.Admits s q) : f.Admits s q

def Chierchia2006.DomainAlternatives.enrich {W : Type u_1} {E : Type u_2} : DomainAlternatives → (Finset E → Set W) → Finset E → Set W

Large alternatives trigger even-like enrichment, (108b), and alternatives that stand a chance trigger antiexhaustive enrichment, (108c).

Equations

• Chierchia2006.DomainAlternatives.max.enrich x✝¹ x✝ = Chierchia2006.evenEnrich (x✝¹ '' {S : Finset E | S ⊂ x✝ ∧ S.Nonempty}) (x✝¹ x✝)
• Chierchia2006.DomainAlternatives.min.enrich x✝¹ x✝ = Exhaustification.oMinus x✝¹ x✝

theorem Chierchia2006.exactlyOne_subset_biUnion {W : Type u_1} {E : Type u_2} {P : E → Set W} (S : Finset E) : exactlyOne P S ⊆ ⋃ x ∈ S, P x

noncomputable def Chierchia2006.Profile.statement {W : Type u_1} {E : Type u_2} (p : Profile) (C : Set W → Set W) (P : E → Set W) : Finset E → Set W

Under the operator C an item says that some member of the domain is a witness, and a scalar item adds the uniqueness implicature, (81b), where that makes its statement under C stronger, since (110) selects the strongest enriched meaning.

Equations

• p.statement C P = if p.scalar = true ∧ ∀ (S : Finset E), C (Chierchia2006.exactlyOne P S) ⊆ C (⋃ x ∈ S, P x) then Chierchia2006.exactlyOne P else fun (S : Finset E) => ⋃ x ∈ S, P x

theorem Chierchia2006.Profile.statement_of_scalar {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} {C : Set W → Set W} (hs : p.scalar = true) (hC : Monotone C) : p.statement C P = exactlyOne P

theorem Chierchia2006.Profile.statement_of_not_scalar {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} {C : Set W → Set W} (hs : p.scalar = false) : p.statement C P = fun (S : Finset E) => ⋃ x ∈ S, P x

theorem Chierchia2006.Profile.statement_antitone {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} {C : Set W → Set W} (hC : Antitone C) (S : Finset E) : C (p.statement C P S) = C (⋃ x ∈ S, P x)

Under an antitone operator a scalar item's statement is the plain existential, the some_D of (91).

inductive Chierchia2006.LF (W : Type u_3) : Type u_3

A logical form places σ among the operators of an item's environment. freeze outer inner freezes the implicature between the operator outer above σ and inner below it, and scopedOut C freezes it over the item scoped out of C, (74b).

• freeze {W : Type u_3} (outer inner : Set W → Set W) : LF W
• scopedOut {W : Type u_3} (C : Set W → Set W) : LF W

noncomputable def Chierchia2006.Profile.prejacent {W : Type u_1} {E : Type u_2} (p : Profile) (P : E → Set W) : LF W → Finset E → Set W

p.prejacent P lf is the proposition σ freezes in lf, as a function of the domain.

Equations

• p.prejacent P (Chierchia2006.LF.freeze outer inner) x✝ = inner (p.statement inner P x✝)
• p.prejacent P (Chierchia2006.LF.scopedOut C) x✝ = p.statement id (fun (a : E) => C (P a)) x✝

@[simp]

theorem Chierchia2006.Profile.prejacent_freeze {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} (outer inner : Set W → Set W) : p.prejacent P (LF.freeze outer inner) = fun (S : Finset E) => inner (p.statement inner P S)

@[simp]

theorem Chierchia2006.Profile.prejacent_scopedOut {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} (C : Set W → Set W) : p.prejacent P (LF.scopedOut C) = p.statement id fun (a : E) => C (P a)

noncomputable def Chierchia2006.Profile.frozen {W : Type u_1} {E : Type u_2} (p : Profile) (P : E → Set W) (D : Finset E) (lf : LF W) : Set W

σ's output enriches the prejacent with the item's domain alternatives.

Equations

• p.frozen P D lf = p.alternatives.enrich (p.prejacent P lf) D

noncomputable def Chierchia2006.Profile.sentence {W : Type u_1} {E : Type u_2} (p : Profile) (P : E → Set W) (D : Finset E) : LF W → Set W

The sentence applies the operator above σ to its output.

Equations

• p.sentence P D (Chierchia2006.LF.freeze outer inner) = outer (p.frozen P D (Chierchia2006.LF.freeze outer inner))
• p.sentence P D (Chierchia2006.LF.scopedOut C) = p.frozen P D (Chierchia2006.LF.scopedOut C)

def Chierchia2006.Profile.Felicitous {W : Type u_1} {E : Type u_2} (p : Profile) (P : E → Set W) (D : Finset E) (lf : LF W) : Prop

A logical form is felicitous when σ admits its output and the sentence is consistent.

Equations

• p.Felicitous P D lf = (p.freezer.Admits (p.frozen P D lf) (p.prejacent P lf D) ∧ (p.sentence P D lf).Nonempty)

theorem Chierchia2006.not_felicitous_freeze_of_antitone {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} {D : Finset E} {outer inner : Set W → Set W} (hmin : p.alternatives = DomainAlternatives.min) (hstrong : p.freezer = Freezer.strong) (hC : Antitone inner) : ¬p.Felicitous P D (LF.freeze outer inner)

Under an antitone operator below σ the enrichment is vacuous, so the strong σ cannot freeze there: no negative-polarity construal for qualunque or uno N qualsiasi, (70)–(72), (90b).

theorem Chierchia2006.not_felicitous_freeze_id_of_scalar {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} {D : Finset E} {outer : Set W → Set W} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = true) (hD : 1 < D.card) (hout : outer ∅ = ∅) : ¬p.Felicitous P D (LF.freeze outer id)

σ frozen directly over a scalar item's statement yields the clash of (82), which stays a contradiction under any operator that preserves it: no universal reading for irgendwas under könnte, footnote 42.

theorem Chierchia2006.not_felicitous_freeze_id_id_of_isActualist {W : Type u_1} {E : Type u_2} {p : Profile} {P : E → Set W} {D : Finset E} {actual : W → Set E} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) (hP : Exhaustification.IsActualist actual P) (hD : D.Nonempty) (hwide : ∀ (w : W), ∃ a ∈ D, a ∉ actual w) : ¬p.Felicitous P D (LF.freeze id id)

In an episodic sentence with an actualist scope and a widened domain the universal reading of a non-scalar item is never true, (67).

structure Chierchia2006.Model (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

A model of an item's context supplies an accessibility relation, the scope, the domain of possible witnesses, and the individuals that exist at each world.

• R : SetRel W W
• P : E → Set W
• D : Finset E
• actual : W → Set E

inductive Chierchia2006.Reading : Type

The paper distinguishes universal and existential readings, (10) and (93), and the rhetorical and negative-polarity construals under negation, (64)–(65).

• universal : Reading
• existential : Reading
• rhetorical : Reading
• negativePolarity : Reading

@[instance_reducible]

instance Chierchia2006.instDecidableEqReading : DecidableEq Reading

Equations

• Chierchia2006.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Chierchia2006.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Chierchia2006.instReprReading : Repr Reading

Equations

• Chierchia2006.instReprReading = { reprPrec := Chierchia2006.instReprReading.repr }

inductive Chierchia2006.Environment : Type

An environment is the context an item occurs in in one of the paper's examples.

• episodic : Environment
• episodicSubtrigged : Environment
• negation : Environment
• negationSubtrigged : Environment
• future : Environment
• imperative : Environment
• possibility : Environment
• necessity : Environment
• generic : Environment
• negationNecessity : Environment

@[instance_reducible]

instance Chierchia2006.instDecidableEqEnvironment : DecidableEq Environment

Equations

• Chierchia2006.instDecidableEqEnvironment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Chierchia2006.instReprEnvironment : Repr Environment

Equations

• Chierchia2006.instReprEnvironment = { reprPrec := Chierchia2006.instReprEnvironment.repr }

def Chierchia2006.instReprEnvironment.repr : Environment → ℕ → Std.Format

Equations

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

def Chierchia2006.Environment.lfs {W : Type u_1} {E : Type u_2} (m : Model W E) : Environment → Reading → List (LF W)

env.lfs m r lists the logical forms that yield the reading r. Negation over σ is the rhetorical reading, (64b), (69b), (91a), and σ over negation the negative-polarity one, (65a), (70a), (91c), as is σ over an item scoped out of negation, (75b). A modal over σ gives the universal reading, (93a), and σ over the modal the existential one, (84a), (93c). In a positive context σ gives the universal, (63) and (71).

Equations

• One or more equations did not get rendered due to their size.
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.episodic Chierchia2006.Reading.universal = [Chierchia2006.LF.freeze id id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.episodicSubtrigged Chierchia2006.Reading.universal = [Chierchia2006.LF.freeze id id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.generic Chierchia2006.Reading.universal = [Chierchia2006.LF.freeze id id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.negation Chierchia2006.Reading.rhetorical = [Chierchia2006.LF.freeze (fun (x : Set W) => xᶜ) id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.negationSubtrigged Chierchia2006.Reading.rhetorical = [Chierchia2006.LF.freeze (fun (x : Set W) => xᶜ) id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.negation Chierchia2006.Reading.negativePolarity = [Chierchia2006.LF.freeze id fun (x : Set W) => xᶜ]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.possibility Chierchia2006.Reading.universal = [Chierchia2006.LF.freeze m.R.preimage id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.possibility Chierchia2006.Reading.existential = [Chierchia2006.LF.freeze id m.R.preimage]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.future Chierchia2006.Reading.universal = [Chierchia2006.LF.freeze m.R.core id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.imperative Chierchia2006.Reading.universal = [Chierchia2006.LF.freeze m.R.core id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.necessity Chierchia2006.Reading.universal = [Chierchia2006.LF.freeze m.R.core id]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.future Chierchia2006.Reading.existential = [Chierchia2006.LF.freeze id m.R.core]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.imperative Chierchia2006.Reading.existential = [Chierchia2006.LF.freeze id m.R.core]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.necessity Chierchia2006.Reading.existential = [Chierchia2006.LF.freeze id m.R.core]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.negationNecessity Chierchia2006.Reading.rhetorical = [Chierchia2006.LF.freeze (fun (x : Set W) => xᶜ) m.R.core]
• Chierchia2006.Environment.lfs m Chierchia2006.Environment.negationNecessity Chierchia2006.Reading.negativePolarity = [Chierchia2006.LF.freeze id fun (q : Set W) => (m.R.core q)ᶜ]
• Chierchia2006.Environment.lfs m x✝¹ x✝ = []

def Chierchia2006.Environment.Admissible {W : Type u_1} {E : Type u_2} (m : Model W E) : Environment → Prop

A model is admissible for an environment when it meets the paper's standing assumptions: two possible witnesses, (82); a serial accessibility relation under a modal; and in an episodic sentence an actualist scope over a domain widened beyond the actual individuals, (67b), unless subtrigging anchors it to them, (68c).

Equations

• Chierchia2006.Environment.Admissible m Chierchia2006.Environment.episodic = (1 < m.D.card ∧ Exhaustification.IsActualist m.actual m.P ∧ ∀ (w : W), ∃ a ∈ m.D, a ∉ m.actual w)
• Chierchia2006.Environment.Admissible m Chierchia2006.Environment.negation = (1 < m.D.card ∧ Exhaustification.IsActualist m.actual m.P ∧ ∀ (w : W), ∃ a ∈ m.D, a ∉ m.actual w)
• Chierchia2006.Environment.Admissible m Chierchia2006.Environment.episodicSubtrigged = (1 < m.D.card ∧ Exhaustification.IsActualist m.actual m.P ∧ ∃ (w : W), ∀ a ∈ m.D, a ∈ m.actual w)
• Chierchia2006.Environment.Admissible m Chierchia2006.Environment.negationSubtrigged = (1 < m.D.card ∧ Exhaustification.IsActualist m.actual m.P ∧ ∃ (w : W), ∀ a ∈ m.D, a ∈ m.actual w)
• Chierchia2006.Environment.Admissible m Chierchia2006.Environment.generic = (1 < m.D.card)
• Chierchia2006.Environment.Admissible m x✝ = (1 < m.D.card ∧ ∀ (w : W), w ∈ m.R.dom)

def Chierchia2006.Available (p : Profile) (env : Environment) (r : Reading) : Prop

A reading is available to an item when some admissible model makes one of its logical forms felicitous.

Equations

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

def Chierchia2006.Excluded (p : Profile) (env : Environment) (r : Reading) : Prop

A reading is excluded for an item when no admissible model makes any of its logical forms felicitous.

Equations

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

theorem Chierchia2006.excluded_negation_negativePolarity {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hstrong : p.freezer = Freezer.strong) : Excluded p Environment.negation Reading.negativePolarity

theorem Chierchia2006.excluded_negationNecessity_negativePolarity {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hstrong : p.freezer = Freezer.strong) : Excluded p Environment.negationNecessity Reading.negativePolarity

theorem Chierchia2006.excluded_possibility_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = true) : Excluded p Environment.possibility Reading.universal

theorem Chierchia2006.excluded_episodic_of_scalar {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = true) (r : Reading) : Excluded p Environment.episodic r

theorem Chierchia2006.excluded_episodicSubtrigged_of_scalar {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = true) (r : Reading) : Excluded p Environment.episodicSubtrigged r

theorem Chierchia2006.excluded_episodic_of_not_scalar {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) (r : Reading) : Excluded p Environment.episodic r

Models of the available readings

def Chierchia2006.modalModel : Model (Fin 7) (Fin 2)

modalModel is a serial frame for the modal environments. From world 0 the two doctors are married in different accessible worlds, the distribution of (85); world 3 sees only a world where doctor 0 is married, world 5 only world 4, where both are, and world 6 only itself, where neither is.

Equations

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

def Chierchia2006.widenedModel : Model Bool (Fin 2)

widenedModel is an episodic model with a widened domain: doctor 1 exists at no world, and doctor 0 is a witness at world true only.

Equations

• Chierchia2006.widenedModel = { R := ∅, P := fun (d : Fin 2) => {w : Bool | d = 0 ∧ w = true}, D := Finset.univ, actual := fun (x : Bool) => {0} }

def Chierchia2006.anchoredModel : Model (Fin 3) (Fin 2)

anchoredModel is an episodic model anchored by subtrigging: both doctors exist at every world, both are witnesses at world 0, only doctor 0 at world 1, and neither at world 2.

Equations

• Chierchia2006.anchoredModel = { R := ∅, P := fun (d : Fin 2) => {w : Fin 3 | (d, w) ∈ {(0, 0), (0, 1), (1, 0)}}, D := Finset.univ, actual := fun (x : Fin 3) => Set.univ }

theorem Chierchia2006.Profile.statement_id {W : Type u_3} {E : Type u_4} {p : Profile} {P : E → Set W} (hs : p.scalar = true) : p.statement id P = exactlyOne P

theorem Chierchia2006.Profile.statement_core {W : Type u_3} {E : Type u_4} {p : Profile} {P : E → Set W} {R : SetRel W W} (hs : p.scalar = true) : p.statement R.core P = exactlyOne P

theorem Chierchia2006.Profile.statement_preimage {W : Type u_3} {E : Type u_4} {p : Profile} {P : E → Set W} {R : SetRel W W} (hs : p.scalar = true) : p.statement R.preimage P = exactlyOne P

theorem Chierchia2006.Profile.compl_statement_compl {W : Type u_3} {E : Type u_4} {p : Profile} {P : E → Set W} (S : Finset E) : (p.statement (fun (x : Set W) => xᶜ) P S)ᶜ = (⋃ x ∈ S, P x)ᶜ

theorem Chierchia2006.Profile.compl_core_statement {W : Type u_3} {E : Type u_4} {p : Profile} {P : E → Set W} {R : SetRel W W} (S : Finset E) : (R.core (p.statement (fun (q : Set W) => (R.core q)ᶜ) P S))ᶜ = (R.core (⋃ x ∈ S, P x))ᶜ

theorem Chierchia2006.Profile.felicitous_freeze {W : Type u_3} {E : Type u_4} {p : Profile} {P : E → Set W} {D : Finset E} {outer inner : Set W → Set W} {v w : W} (hmin : p.alternatives = DomainAlternatives.min) (hv : v ∈ inner (p.statement inner P D)) (hv' : v ∉ Exhaustification.oMinus (fun (S : Finset E) => inner (p.statement inner P S)) D) (hw : w ∈ outer (Exhaustification.oMinus (fun (S : Finset E) => inner (p.statement inner P S)) D)) : p.Felicitous P D (LF.freeze outer inner)

A logical form freeze outer inner is felicitous for any freezer once σ's output properly strengthens its input at one world and the sentence holds at another.

theorem Chierchia2006.Profile.felicitous_scopedOut {W : Type u_3} {E : Type u_4} {p : Profile} {P : E → Set W} {D : Finset E} {C : Set W → Set W} {v w : W} (hmin : p.alternatives = DomainAlternatives.min) (hv : v ∈ p.statement id (fun (a : E) => C (P a)) D) (hv' : v ∉ Exhaustification.oMinus (p.statement id fun (a : E) => C (P a)) D) (hw : w ∈ Exhaustification.oMinus (p.statement id fun (a : E) => C (P a)) D) : p.Felicitous P D (LF.scopedOut C)

A logical form scopedOut C is felicitous for any freezer under the same two conditions.

theorem Chierchia2006.available_possibility_existential {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) : Available p Environment.possibility Reading.existential

theorem Chierchia2006.available_possibility_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.possibility Reading.universal

theorem Chierchia2006.felicitous_core_existential {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) : p.Felicitous modalModel.P modalModel.D (LF.freeze id modalModel.R.core)

theorem Chierchia2006.felicitous_core_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : p.Felicitous modalModel.P modalModel.D (LF.freeze modalModel.R.core id)

theorem Chierchia2006.available_future_existential {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) : Available p Environment.future Reading.existential

theorem Chierchia2006.available_imperative_existential {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) : Available p Environment.imperative Reading.existential

theorem Chierchia2006.available_necessity_existential {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) : Available p Environment.necessity Reading.existential

theorem Chierchia2006.available_future_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.future Reading.universal

theorem Chierchia2006.available_imperative_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.imperative Reading.universal

theorem Chierchia2006.available_necessity_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.necessity Reading.universal

theorem Chierchia2006.available_negation_rhetorical {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) : Available p Environment.negation Reading.rhetorical

theorem Chierchia2006.available_negation_negativePolarity {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hplain : p.freezer = Freezer.plain) : Available p Environment.negation Reading.negativePolarity

theorem Chierchia2006.available_negationNecessity_rhetorical {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) : Available p Environment.negationNecessity Reading.rhetorical

theorem Chierchia2006.available_negationNecessity_negativePolarity {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hplain : p.freezer = Freezer.plain) : Available p Environment.negationNecessity Reading.negativePolarity

theorem Chierchia2006.available_negationSubtrigged_rhetorical {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.negationSubtrigged Reading.rhetorical

theorem Chierchia2006.available_negationSubtrigged_negativePolarity {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.negationSubtrigged Reading.negativePolarity

theorem Chierchia2006.felicitous_anchored_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : p.Felicitous anchoredModel.P anchoredModel.D (LF.freeze id id)

theorem Chierchia2006.available_episodicSubtrigged_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.episodicSubtrigged Reading.universal

theorem Chierchia2006.available_generic_universal {p : Profile} (hmin : p.alternatives = DomainAlternatives.min) (hs : p.scalar = false) : Available p Environment.generic Reading.universal

The rows

def Chierchia2006.Profile.ofKey : String → Option Profile

Profile.ofKey s is the profile that the row key s names.

Equations

• Chierchia2006.Profile.ofKey "npiFci" = some Chierchia2006.npiFci
• Chierchia2006.Profile.ofKey "pureFci" = some Chierchia2006.pureFci
• Chierchia2006.Profile.ofKey "existentialNpiFci" = some Chierchia2006.existentialNpiFci
• Chierchia2006.Profile.ofKey "existentialPureFci" = some Chierchia2006.existentialPureFci
• Chierchia2006.Profile.ofKey x✝ = none

def Chierchia2006.Environment.ofKey : String → Option Environment

Environment.ofKey s is the environment that the row key s names.

Equations

• Chierchia2006.Environment.ofKey "episodic" = some Chierchia2006.Environment.episodic
• Chierchia2006.Environment.ofKey "episodicSubtrigged" = some Chierchia2006.Environment.episodicSubtrigged
• Chierchia2006.Environment.ofKey "negation" = some Chierchia2006.Environment.negation
• Chierchia2006.Environment.ofKey "negationSubtrigged" = some Chierchia2006.Environment.negationSubtrigged
• Chierchia2006.Environment.ofKey "future" = some Chierchia2006.Environment.future
• Chierchia2006.Environment.ofKey "imperative" = some Chierchia2006.Environment.imperative
• Chierchia2006.Environment.ofKey "possibility" = some Chierchia2006.Environment.possibility
• Chierchia2006.Environment.ofKey "necessity" = some Chierchia2006.Environment.necessity
• Chierchia2006.Environment.ofKey "generic" = some Chierchia2006.Environment.generic
• Chierchia2006.Environment.ofKey "negationNecessity" = some Chierchia2006.Environment.negationNecessity
• Chierchia2006.Environment.ofKey x✝ = none

def Chierchia2006.Reading.ofKey : String → Option Reading

Reading.ofKey s is the reading that the row key s names.

Equations

• Chierchia2006.Reading.ofKey "universal" = some Chierchia2006.Reading.universal
• Chierchia2006.Reading.ofKey "existential" = some Chierchia2006.Reading.existential
• Chierchia2006.Reading.ofKey "rhetorical" = some Chierchia2006.Reading.rhetorical
• Chierchia2006.Reading.ofKey "negativePolarity" = some Chierchia2006.Reading.negativePolarity
• Chierchia2006.Reading.ofKey x✝ = none

def Chierchia2006.judgedReadings : List (Profile × Environment × Reading × Judgment)

judgedReadings parses each judged reading of a row that needs no covert device into the item's profile, the environment, the reading and its judgment.

Equations

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

def Chierchia2006.judgedSentences : List (Profile × Environment × Judgment)

judgedSentences parses each row that needs no covert device and judges the sentence as a whole.

Equations

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

theorem Chierchia2006.judgedReadings_predicted (x : Profile × Environment × Reading × Judgment) : x ∈ judgedReadings → (x.2.2.2 ≤ Judgment.questionable → Excluded x.1 x.2.1 x.2.2.1) ∧ (Judgment.marginal ≤ x.2.2.2 → Available x.1 x.2.1 x.2.2.1)

Every judged reading is predicted: a reading the paper marks ?? or worse is excluded, and one it marks at most ? is available.

theorem Chierchia2006.judgedSentences_predicted (x : Profile × Environment × Judgment) : x ∈ judgedSentences → (x.2.2 ≤ Judgment.questionable → ∀ (r : Reading), Excluded x.1 x.2.1 r) ∧ (Judgment.marginal ≤ x.2.2 → ∃ (r : Reading), Available x.1 x.2.1 r)

Every sentence judged as a whole is predicted: one the paper marks ?? or worse has every reading excluded, and one it marks at most ? has a reading available.

theorem Chierchia2006.Profile.alternatives_of_ofKey {s : String} {p : Profile} (h : p ∈ ofKey s) : p.alternatives = DomainAlternatives.min

theorem Chierchia2006.covertModal_available (e : Datum) : e ∈ Examples.all → e.feature? "device" = some "covertModal" → ∀ p ∈ (e.feature? "item").bind Profile.ofKey, Available p Environment.necessity Reading.existential

Under a necessity modal the existential reading is available to the items of the rows the paper rescues with a covert epistemic modal, (4), (8a) and (89).

Double duty on the implicational map

theorem Chierchia2006.any_double_duty : ∃ e ∈ Haspelmath1997.english, Indefinite.HaspelmathFunction.directNeg ∈ e.functions ∧ Indefinite.HaspelmathFunction.freeChoice ∈ e.functions

Roughly half of the languages in [Has97]'s survey use one series for negative polarity and free choice, English among them: the any-series covers direct negation and free choice.

theorem Chierchia2006.italian_separates_uses (e : Haspelmath1997.Series) : e ∈ Haspelmath1997.italian → (Indefinite.HaspelmathFunction.directNeg ∈ e.functions → Indefinite.HaspelmathFunction.freeChoice ∉ e.functions) ∧ (Indefinite.HaspelmathFunction.freeChoice ∈ e.functions → Indefinite.HaspelmathFunction.directNeg ∉ e.functions ∧ Indefinite.HaspelmathFunction.indirectNeg ∉ e.functions)

The other half separate the two, as Romance does: no Italian series covering direct negation covers free choice, and the free-choice series -unque covers no negation function.