Magri (2009): A Theory of Individual-Level Predicates Based on Blind Mandatory Scalar Implicatures

[Mag09] explains the oddness of #Some Italians come from a warm country and of #Sometimes, John is tall by one mechanism, the blind mandatory scalar implicature. The strengthened meaning is [Fox07]'s innocent exclusion computed with logical entailment, blind to common knowledge (the Blindness Hypothesis (32)), and a sentence whose strengthened meaning contradicts common knowledge is odd (the Mismatch Hypothesis (33), Odd). Blindness is essential: with entailment given common knowledge these sentences would not be strengthened at all (exhIE_image_inter). The implicature is mandatory because relevance, constrained by (43), cannot set aside an alternative that is contextually equivalent to the utterance (disjoint_exhR), while an ordinary implicature depends on the context (exists_isRelevance). Both hypotheses carry over to presuppositions, (65) and (66) (odd_univ_iff).

Individual-level predicates differ from stage-level ones only in common knowledge: they are permanent, (70) (Permanent), hence homogeneous over any part of a lifespan (Homogeneous, (71)). The oddness of sometimes with tall, (72b), is then that of some with come from a warm country, (73) (odd_some, sometimes_odd). An existential in the scope of a universal, against its alternatives with definite descriptions (49), (94), is odd when common knowledge fixes a single witness for it (odd_narrowSome). This covers the fronted indefinite of (46a) and (54a) (winner_odd, running_odd) and the existential reading of a bare plural subject of an individual-level predicate, (84b), whose narrowest scope puts it below GEN (existential_odd). A universal over individuals rescues the existential, since distinct individuals may have distinct witnesses, (54b) and (102b) (table_not_odd, universal_not_odd). The same computation predicts the German word order facts of [Die92], (8) and (125) (word_order_rows). Overt always competes with GEN, which presupposes homogeneity, so #John is always tall is odd, (134a) (always_odd), but Firemen are always tall is not, (139b) (always_bare_not_odd).

Implementation notes

• Propositions are sets of worlds. A world of §3.3 and §4 is the extension of the one predicate at issue over individuals and an index (times, or objects and times), with lifespans, nouns and restrictors held fixed, so every extension is a logically possible world. The worlds the paper exhibits, (98), the table of (54) and the world of §4.3, are constructed.
• GEN contributes its universal assertion (137) to truth conditions; its homogeneity presupposition is used only in §4.6, as in the paper. The restrictor C̃ of (90) is arbitrary, as in the paper, and the definite alternatives (93b) restrict GEN to the part of each lifespan in C.
• The world (98) is sampled at three times of C̃, one in each fireman's stretch of tallness in the paper's picture.

TODO

• The alternatives of the episodic existential reading (92b), sketched in footnote 20, are not formalized.
• The facts of §4.4 (non-kind bare plurals, association with only, statives, locatives) are discussion only, and the contrast (133) with definite subjects is left open by the paper.

References

• [Mag09]
• [Fox07]
• [Car77a]
• [Die92]

Blind strengthening and oddness (§3.2)

def Magri2009.Odd {W : Type u_1} (Wck : Set W) (ALT : Set (Set W)) (φ : Set W) : Prop

The Mismatch Hypothesis (33): the sentence φ, with alternatives ALT, is odd when its strengthened meaning contradicts common knowledge Wck. By the Blindness Hypothesis (32) the strengthened meaning is innocent exclusion (30) with logical entailment, computed over all worlds rather than over Wck.

Equations

• Magri2009.Odd Wck ALT φ = Disjoint (Exhaustification.exhIE ALT φ) Wck

theorem Magri2009.odd_pair_iff {W : Type u_1} {Wck φ ψ : Set W} (h : (φ \ ψ).Nonempty) : Odd Wck {φ, ψ} φ ↔ φ ∩ Wck ⊆ ψ

(34), (82): against one alternative that φ can hold without, φ is odd exactly when common knowledge makes it entail the alternative.

theorem Magri2009.exhIE_insert_range {W : Type u_1} {φ : Set W} {ι : Type u_2} {ψP : ι → Set W} (h : (φ \ ⋃ (i : ι), ψP i).Nonempty) : Exhaustification.exhIE (insert φ (Set.range ψP)) φ = φ \ ⋃ (i : ι), ψP i

(53), (97), (109): against the alternatives ψP i, blind strengthening denies them all when φ can hold with all of them false.

theorem Magri2009.odd_insert_range_iff {W : Type u_1} {Wck φ : Set W} {ι : Type u_2} {ψP : ι → Set W} (h : (φ \ ⋃ (i : ι), ψP i).Nonempty) : Odd Wck (insert φ (Set.range ψP)) φ ↔ φ ∩ Wck ⊆ ⋃ (i : ι), ψP i

The Mismatch Hypothesis against a family of alternatives that φ can hold without: φ is odd exactly when common knowledge makes it entail one of them.

theorem Magri2009.exhIE_image_inter {W : Type u_1} {Wck φ : Set W} {ALT : Set (Set W)} (hφ : φ ∈ ALT) (h : ∀ a ∈ ALT, a ∩ Wck = φ ∩ Wck) : Exhaustification.exhIE ((fun (x : Set W) => x ∩ Wck) '' ALT) (φ ∩ Wck) = φ ∩ Wck

(34): the Blindness Hypothesis is essential. Strengthening with entailment given common knowledge (31b), that is innocent exclusion over the propositions restricted to Wck, leaves φ unstrengthened when its alternatives are equivalent to it given common knowledge.

Mandatoriness (§3.2.5)

structure Magri2009.IsRelevance {W : Type u_1} (Wck φ : Set W) (R : Set W → Prop) : Prop

The postulates (43) on a relevance property R in a context where φ is uttered: the utterance is relevant (43a), and propositions equivalent given common knowledge are alike in relevance (43b).

• uttered : R φ
• congr {p q : Set W} : p ∩ Wck = q ∩ Wck → (R p ↔ R q)

def Magri2009.exhR {W : Type u_1} (R : Set W → Prop) (ALT : Set (Set W)) (φ : Set W) : Set W

(42): the prejacent with every relevant innocently excludable alternative denied, the counterpart over sets of Excluder.restrict applied to innocent.

Equations

• Magri2009.exhR R ALT φ = {x : W | x ∈ φ ∧ ∀ (a : Set W), Exhaustification.IsInnocentlyExcludable ALT φ a → R a → x ∉ a}

theorem Magri2009.IsRelevance.relevant {W : Type u_1} {Wck φ ψ : Set W} {R : Set W → Prop} (hR : IsRelevance Wck φ R) (h : ψ ∩ Wck = φ ∩ Wck) : R ψ

(45): an alternative equivalent to the utterance given common knowledge is relevant.

theorem Magri2009.disjoint_exhR {W : Type u_1} {Wck φ ψ : Set W} {R : Set W → Prop} {ALT : Set (Set W)} (hR : IsRelevance Wck φ R) (hψ : Exhaustification.IsInnocentlyExcludable ALT φ ψ) (h : ψ ∩ Wck = φ ∩ Wck) : Disjoint (exhR R ALT φ) Wck

(45): a mismatching implicature is mandatory. When an excludable alternative is equivalent to the utterance given common knowledge, the strengthened meaning (42) contradicts common knowledge whatever relevance property the context supplies.

theorem Magri2009.exists_isRelevance {W : Type u_1} {Wck φ ψ : Set W} (h : ψ ∩ Wck ≠ φ ∩ Wck) : ∃ (R : Set W → Prop), IsRelevance Wck φ R ∧ ¬R ψ

(40), (44): an implicature that does not mismatch is not mandatory. Relevance of exactly the propositions equivalent to the utterance given common knowledge satisfies (43) and sets aside every other alternative.

Homogeneity (§3.4, §4.1)

def Magri2009.Homogeneous {α : Type u_2} (A B : α → Prop) : Prop

Homogeneity of the scope B with respect to the restrictor A: all As are Bs or none are. It is the presupposition YES ∪ NO of the distributivity operator (67) and of GEN (137), and (71b) takes common knowledge to entail it.

Equations

• Magri2009.Homogeneous A B = (Quantifier.GQ.every A B ∨ Quantifier.GQ.no A B)

theorem Magri2009.odd_some {W : Type u_1} {Wck : Set W} {α : Type u_2} {A B : W → α → Prop} (hck : ∀ x ∈ Wck, Homogeneous (A x) (B x)) (h : ∃ (x : W), Quantifier.GQ.some (A x) (B x) ∧ ¬Quantifier.GQ.every (A x) (B x)) : Odd Wck {{x : W | Quantifier.GQ.some (A x) (B x)}, {x : W | Quantifier.GQ.every (A x) (B x)}} {x : W | Quantifier.GQ.some (A x) (B x)}

(38), (73), (72b): a sentence with some is odd when common knowledge makes its scope homogeneous with respect to its restrictor, (71): its Horn-mate with all is logically but not contextually stronger.

theorem Magri2009.odd_univ_iff {W : Type u_1} {Wck p : Set W} (h : pᶜ.Nonempty) : Odd Wck {Set.univ, p} Set.univ ↔ Wck ⊆ p

(61), (62), (63), (142): a sentence without presupposition, (68a), is odd by the Mismatch Hypothesis for presuppositions (66) when its Horn-mate presupposes p, (68b), which common knowledge entails but logic does not: the blind strengthened presupposition (64) is pᶜ.

An existential in the scope of a universal (§3.3)

def Magri2009.narrowSome {E : Type u_1} {I : Type u_2} (N : E → Prop) (D : I → Prop) : Set (E → I → Prop)

An existential over N in the scope of a universal over the index restrictor D: (48b), (56), (91b), (105).

Equations

• Magri2009.narrowSome N D = {f : E → I → Prop | Quantifier.GQ.every D fun (i : I) => Quantifier.GQ.some N fun (x : E) => f x i}

def Magri2009.definite {E : Type u_1} {I : Type u_2} (R : E → I → Prop) (d : E) : Set (E → I → Prop)

The alternative with the N such and such, a Horn-mate of the existential by (49) and (94), denoting d, with the index restricted by R d: (50b), (57), (93b), (106b).

Equations

• Magri2009.definite R d = {f : E → I → Prop | Quantifier.GQ.every (R d) (f d)}

def Magri2009.alts {E : Type u_1} {I : Type u_2} (N : E → Prop) (D : I → Prop) (R : E → I → Prop) : Set (Set (E → I → Prop))

The scalar alternatives (25) of narrowSome N D: itself and the definite alternative for each N.

Equations

• Magri2009.alts N D R = insert (Magri2009.narrowSome N D) (Set.range fun (d : { d : E // N d }) => Magri2009.definite R ↑d)

theorem Magri2009.iUnion_definite {E : Type u_1} {I : Type u_2} {N : E → Prop} {R : E → I → Prop} : ⋃ (d : { d : E // N d }), definite R ↑d = {f : E → I → Prop | Quantifier.GQ.some N fun (d : E) => Quantifier.GQ.every (R d) (f d)}

(52), (96), (108): the definite alternatives together amount to the reading with the existential taking widest scope, (51), (95), (107).

theorem Magri2009.odd_narrowSome {E : Type u_1} {I : Type u_2} {Wck : Set (E → I → Prop)} {N : E → Prop} {D : I → Prop} {R : E → I → Prop} (hD : ∃ (i : I), D i) (hck : ∀ f ∈ Wck, ∀ (x : E), N x → ∀ (i : I), D i → f x i → ∀ (j : I), R x j → f x j) (h : (narrowSome N D \ ⋃ (d : { d : E // N d }), definite R ↑d).Nonempty) : Odd Wck (alts N D R) (narrowSome N D)

(46a), (54a), (99): an existential in the scope of a universal is odd when, at every world compatible with common knowledge, an N true at some index of D is true throughout its own restrictor, and when logically it can hold with every definite alternative false, as at (98). Blind strengthening denies the widest-scope reading, which common knowledge makes it entail.

theorem Magri2009.winner_odd {E : Type u_1} {I : Type u_2} {Wck : Set (E → I → Prop)} {N : E → Prop} {D : I → Prop} (hD : ∃ (i : I), D i) (hck : ∀ f ∈ Wck, ∃ (g : E), ∀ (x : E) (i : I), D i → (f x i ↔ x = g)) (h : (narrowSome N D \ ⋃ (d : { d : E // N d }), definite (fun (x : E) => D) ↑d).Nonempty) : Odd Wck (alts N D fun (x : E) => D) (narrowSome N D)

(46a): #On every day, a fireman won is odd when it is common knowledge that the same person was the winner on every day of D.

The context of (54)

inductive Magri2009.Competition : Type

The competitions of (54).

• swimming : Competition
• running : Competition
• jumping : Competition

@[instance_reducible]

instance Magri2009.instDecidableEqCompetition : DecidableEq Competition

Equations

• Magri2009.instDecidableEqCompetition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Magri2009.instFintypeCompetition : Fintype Competition

Equations

• Magri2009.instFintypeCompetition = { elems := { val := ↑Magri2009.Competition.enumList, nodup := Magri2009.Competition.enumList_nodup }, complete := Magri2009.instFintypeCompetition._proof_1 }

inductive Magri2009.Winner : Type

The winners in the table of (54).

• x : Winner
• y : Winner
• z : Winner

@[instance_reducible]

instance Magri2009.instDecidableEqWinner : DecidableEq Winner

Equations

• Magri2009.instDecidableEqWinner x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Magri2009.instFintypeWinner : Fintype Winner

Equations

• Magri2009.instFintypeWinner = { elems := { val := ↑Magri2009.Winner.enumList, nodup := Magri2009.Winner.enumList_nodup }, complete := Magri2009.instFintypeWinner._proof_1 }

def Magri2009.Winner.competition : Winner → Competition

The competition each person of (54) won on every day.

Equations

• Magri2009.Winner.x.competition = Magri2009.Competition.swimming
• Magri2009.Winner.y.competition = Magri2009.Competition.running
• Magri2009.Winner.z.competition = Magri2009.Competition.jumping

def Magri2009.table (g : Winner) (p : Competition × Fin 5) : Prop

The table of (54): each of x, y, z won one competition on all five days.

Equations

• Magri2009.table g p = (p.1 = g.competition)

def Magri2009.sameWinner : Set (Winner → Competition × Fin 5 → Prop)

The common knowledge of (54): the same person won each competition on all five days.

Equations

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

theorem Magri2009.running_odd : Odd sameWinner (alts (fun (x : Winner) => True) (fun (p : Competition × Fin 5) => p.1 = Competition.running) fun (x : Winner) (p : Competition × Fin 5) => p.1 = Competition.running) (narrowSome (fun (x : Winner) => True) fun (p : Competition × Fin 5) => p.1 = Competition.running)

(54a): #Every day, a fireman won the running competition is odd in the context of (54).

theorem Magri2009.table_not_odd : ¬Odd sameWinner (alts (fun (x : Winner) => True) (fun (x : Competition × Fin 5) => True) fun (x : Winner) (x_1 : Competition × Fin 5) => True) (narrowSome (fun (x : Winner) => True) fun (x : Competition × Fin 5) => True)

(54b): Every day, for every competition, a fireman won is fine in the context of (54): the table is compatible with common knowledge, verifies the sentence (56), and falsifies each definite alternative (57).

Individual-level predicates (§4)

def Magri2009.Permanent {E : Type u_1} {T : Type u_2} (live f : E → T → Prop) : Prop

(70): an extension of the predicate compatible with common knowledge about an individual-level predicate. True of an individual at some time, it is true of it throughout its lifespan live d.

Equations

• Magri2009.Permanent live f = ∀ (d : E), (∃ (t : T), f d t) → ∀ (t : T), live d t → f d t

theorem Magri2009.Permanent.homogeneous {E : Type u_1} {T : Type u_2} {live f : E → T → Prop} (hf : Permanent live f) {d : E} {A : T → Prop} (hA : ∀ (t : T), A t → live d t) : Homogeneous A (f d)

(71): a permanent predicate is homogeneous over any restrictor within a lifespan.

Existential Q-adverbs (§4.1)

def Magri2009.sometimes {E : Type u_1} {T : Type u_2} (live : E → T → Prop) (j : E) (C : T → Prop) : Set (E → T → Prop)

(79b): Sometimes, John is tall, the adverb restricted by C and, by (76) and (77), by John's lifespan.

Equations

• Magri2009.sometimes live j C = {f : E → T → Prop | Quantifier.GQ.some (fun (t : T) => live j t ∧ C t) (f j)}

def Magri2009.always {E : Type u_1} {T : Type u_2} (live : E → T → Prop) (j : E) (C : T → Prop) : Set (E → T → Prop)

(80b): its Horn-mate (81) with always.

Equations

• Magri2009.always live j C = {f : E → T → Prop | Quantifier.GQ.every (fun (t : T) => live j t ∧ C t) (f j)}

theorem Magri2009.sometimes_odd {E : Type u_1} {T : Type u_2} {live : E → T → Prop} {Wck : Set (E → T → Prop)} {j : E} {C : T → Prop} {t₁ t₂ : T} (hck : ∀ f ∈ Wck, Permanent live f) (h₁ : live j t₁ ∧ C t₁) (h₂ : live j t₂ ∧ C t₂) (hne : t₁ ≠ t₂) : Odd Wck {sometimes live j C, always live j C} (sometimes live j C)

(72b), (82): #Sometimes, John is tall is odd for every restrictor C of the adverb that meets John's lifespan at two times: its Horn-mate with always is logically stronger but equivalent given (70).

Bare plural subjects (§4.2)

theorem Magri2009.existential_odd {E : Type u_1} {T : Type u_2} {live : E → T → Prop} {Wck : Set (E → T → Prop)} {C D : T → Prop} {N : E → Prop} (hck : ∀ f ∈ Wck, Permanent live f) (hD : ∃ (t : T), D t) (h : (narrowSome N D \ ⋃ (d : { d : E // N d }), definite (fun (d : E) (t : T) => C t ∧ live d t) ↑d).Nonempty) : Odd Wck (alts N D fun (d : E) (t : T) => C t ∧ live d t) (narrowSome N D)

(84b), (99): the existential reading (91b) of the bare plural subject of Firemen are tall is odd. The existential has narrowest scope (88), below GEN over the restrictor D (the C̃ of (90)); blind strengthening denies that some fireman is tall throughout the part of his lifespan in C, (97), and given (70) a fireman tall at a time of D is tall throughout his lifespan.

The world (98)

inductive Magri2009.Fireman : Type

The three firemen of (98).

• d₁ : Fireman
• d₂ : Fireman
• d₃ : Fireman

@[instance_reducible]

instance Magri2009.instDecidableEqFireman : DecidableEq Fireman

Equations

• Magri2009.instDecidableEqFireman x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Magri2009.instFintypeFireman : Fintype Fireman

Equations

• Magri2009.instFintypeFireman = { elems := { val := ↑Magri2009.Fireman.enumList, nodup := Magri2009.Fireman.enumList_nodup }, complete := Magri2009.instFintypeFireman._proof_1 }

def Magri2009.Fireman.tallAt : Fireman → Fin 3

The time of C̃ at which each fireman of (98) is tall.

Equations

• Magri2009.Fireman.d₁.tallAt = 2
• Magri2009.Fireman.d₂.tallAt = 1
• Magri2009.Fireman.d₃.tallAt = 0

def Magri2009.lifespan : Fireman → Fin 3 → Prop

The lifespans of (98) at the three times of C̃: d₁ is born after the first, d₃ dies before the last.

Equations

• Magri2009.lifespan Magri2009.Fireman.d₁ x✝ = (x✝ ≠ 0)
• Magri2009.lifespan Magri2009.Fireman.d₂ x✝ = True
• Magri2009.lifespan Magri2009.Fireman.d₃ x✝ = (x✝ ≠ 2)

@[instance_reducible]

instance Magri2009.instDecidableRelFiremanFinOfNatNatLifespan : DecidableRel lifespan

Equations

• Magri2009.instDecidableRelFiremanFinOfNatNatLifespan Magri2009.Fireman.d₁ t = { decide := !decide (t = 0), reflects_decide := ⋯ }
• Magri2009.instDecidableRelFiremanFinOfNatNatLifespan Magri2009.Fireman.d₂ t = { decide := true, reflects_decide := ⋯ }
• Magri2009.instDecidableRelFiremanFinOfNatNatLifespan Magri2009.Fireman.d₃ t = { decide := !decide (t = 2), reflects_decide := ⋯ }

def Magri2009.world98 (d : Fireman) (t : Fin 3) : Prop

The world (98): at each time of C̃ some fireman is tall, and none is tall throughout the part of his lifespan in C̃.

Equations

• Magri2009.world98 d t = (t = d.tallAt)

@[reducible, inline]

abbrev Magri2009.alts98 : Set (Set (Fireman → Fin 3 → Prop))

The existential reading (91b) and its definite alternatives (93b) in the model of (98), with C and C̃ all three times.

Equations

• Magri2009.alts98 = Magri2009.alts (fun (x : Magri2009.Fireman) => True) (fun (x : Fin 3) => True) fun (d : Magri2009.Fireman) (t : Fin 3) => True ∧ Magri2009.lifespan d t

theorem Magri2009.world98_mem : world98 ∈ (narrowSome (fun (x : Fireman) => True) fun (x : Fin 3) => True) \ ⋃ (d : { _d : Fireman // True }), definite (fun (d : Fireman) (t : Fin 3) => True ∧ lifespan d t) ↑d

The world (98) verifies the existential reading and falsifies every definite alternative.

def Magri2009.ExistentialOdd (Wck : Set (Fireman → Fin 3 → Prop)) : Prop

The existential reading of a bare plural subject is odd against the common knowledge Wck about its predicate, in the model of (98).

Equations

• Magri2009.ExistentialOdd Wck = Magri2009.Odd Wck Magri2009.alts98 (Magri2009.narrowSome (fun (x : Magri2009.Fireman) => True) fun (x : Fin 3) => True)

theorem Magri2009.existentialOdd_permanent : ExistentialOdd {f : Fireman → Fin 3 → Prop | Permanent lifespan f}

(84b): the existential reading of Firemen are tall is odd, since common knowledge makes an individual-level predicate permanent (70).

theorem Magri2009.not_existentialOdd_univ : ¬ExistentialOdd Set.univ

(84a): the existential reading of Firemen are available is fine, since common knowledge does not constrain a stage-level predicate and the world (98) is compatible with it.

Embedding under a universal (§4.3)

inductive Magri2009.Woman : Type

The two Jewish women of the world of §4.3.

• a₁ : Woman
• a₂ : Woman

@[instance_reducible]

instance Magri2009.instDecidableEqWoman : DecidableEq Woman

Equations

• Magri2009.instDecidableEqWoman x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Magri2009.instFintypeWoman : Fintype Woman

Equations

• Magri2009.instFintypeWoman = { elems := { val := ↑Magri2009.Woman.enumList, nodup := Magri2009.Woman.enumList_nodup }, complete := Magri2009.instFintypeWoman._proof_1 }

inductive Magri2009.Man : Type

The two Jewish men of the world of §4.3.

• b₁ : Man
• b₂ : Man

@[instance_reducible]

instance Magri2009.instDecidableEqMan : DecidableEq Man

Equations

• Magri2009.instDecidableEqMan x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Magri2009.instFintypeMan : Fintype Man

Equations

• Magri2009.instFintypeMan = { elems := { val := ↑Magri2009.Man.enumList, nodup := Magri2009.Man.enumList_nodup }, complete := Magri2009.instFintypeMan._proof_1 }

def Magri2009.Woman.relative : Woman → Man

The one man each woman of §4.3 is related to.

Equations

• Magri2009.Woman.a₁.relative = Magri2009.Man.b₁
• Magri2009.Woman.a₂.relative = Magri2009.Man.b₂

def Magri2009.distributed {T : Type u_1} (a : Woman) (p : Man × T) : Prop

The world of §4.3: a₁ is related only to b₁ and a₂ only to b₂, at all times.

Equations

• Magri2009.distributed a p = (p.1 = a.relative)

theorem Magri2009.universal_not_odd {T : Type u_1} {live : Woman → T → Prop} {C D : Man → T → Prop} (h₁ : ∃ (t : T), C Man.b₂ t ∧ live Woman.a₁ t) (h₂ : ∃ (t : T), C Man.b₁ t ∧ live Woman.a₂ t) : ¬Odd {f : Woman → Man × T → Prop | ∀ (b : Man), Permanent live fun (a : Woman) (t : T) => f a (b, t)} (alts (fun (x : Woman) => True) (fun (p : Man × T) => D p.1 p.2) fun (a : Woman) (p : Man × T) => C p.1 p.2 ∧ live a p.2) (narrowSome (fun (x : Woman) => True) fun (p : Man × T) => D p.1 p.2)

(102b), (109): the existential reading (105) of the bare plural subject of Jewish women are related to every Jewish man, with the universal object scoping over GEN, is fine. Given restrictors that meet the lifespans, the world where a₁ is related only to b₁ and a₂ only to b₂ is compatible with (70) for related, verifies (105), and falsifies each definite alternative (106b). With the definite object of (102a) instead, the reading falls under existential_odd.

German word order (§4.5)

def Magri2009.commonKnowledgeOf (row : Datum) : Option (Set (Fireman → Fin 3 → Prop))

Common knowledge about the predicate of a row, by (70) from the level ([Car77a]) its predicate_level feature records: an individual-level predicate is permanent, a stage-level one unconstrained.

Equations

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

def Magri2009.PredictedOdd (row : Datum) : Prop

A row of (8) is predicted odd when its bare plural subject sits to the right of ja doch, where it has only the existential reading (§4.5.1), and that reading is odd for its predicate, (128), (129).

Equations

• Magri2009.PredictedOdd row = (row.feature? "position" = some "right" ∧ ∃ Wck ∈ Magri2009.commonKnowledgeOf row, Magri2009.ExistentialOdd Wck)

theorem Magri2009.word_order_rows (row : Datum) : row ∈ Examples.all → (row.judgment = Judgment.acceptable ↔ ¬PredictedOdd row)

(8), (125): a row is acceptable exactly when it is not predicted odd; only (8c), with the individual-level intelligent and its subject to the right of ja doch, is odd.

Overt universal Q-adverbs (§4.6)

def Magri2009.genPresup {E : Type u_1} {T : Type u_2} {α : Type u_3} (A : α → Prop) (B : (E → T → Prop) → α → Prop) : Set (E → T → Prop)

(137): the homogeneity presupposition of GEN with restrictor A, the scope being the predicate's extension read through B: (138b) for John is tall, (141b) for Firemen are tall.

Equations

• Magri2009.genPresup A B = {f : E → T → Prop | Magri2009.Homogeneous A (B f)}

theorem Magri2009.always_odd {E : Type u_1} {T : Type u_2} {live : E → T → Prop} {Wck : Set (E → T → Prop)} {j : E} {t₁ t₂ : T} (hck : ∀ f ∈ Wck, Permanent live f) (h₁ : live j t₁) (h₂ : live j t₂) (hne : t₁ ≠ t₂) : Odd Wck {Set.univ, genPresup (live j) fun (f : E → T → Prop) => f j} Set.univ

(134a), (138): #John is always tall is odd by the Mismatch Hypothesis for presuppositions. It presupposes nothing, (138a), while its Horn-mate John is tall, with GEN, presupposes that John is tall at all or at none of the times he is alive, (138b), which (70) entails.

theorem Magri2009.always_bare_not_odd {E : Type u_1} {T : Type u_2} {live : E → T → Prop} {t₁ t₂ : T} {N : E → Prop} {d₁ d₂ : E} (h₁ : N d₁ ∧ live d₁ t₁) (h₂ : N d₂ ∧ live d₂ t₂) (hne : d₁ ≠ d₂) : ¬Odd {f : E → T → Prop | Permanent live f} {Set.univ, genPresup (fun (p : E × T) => N p.1 ∧ live p.1 p.2) fun (f : E → T → Prop) (p : E × T) => f p.1 p.2} Set.univ

(139b), (141): Firemen are always tall is fine. The homogeneity presupposition of GEN is now over firemen and their times, and (70) is compatible with some firemen being tall and others not.