Križ (2016): Homogeneity, Non-Maximality, and All

Križ accounts for the non-maximal readings of definite plurals. The professors smiled is neither true nor false when some but not all of them smiled, and the sentence is nonetheless usable there whenever the current issue does not distinguish that situation from one in which all smiled; all removes the gap and with it the non-maximal reading. A five-world model of three professors runs the account end to end on the library's homogeneity substrate (barePlural, allPlural, both originating with this paper): the non-maximal use under a coarse issue and its absence under a fine one, the unusability of the all-sentence at any gap world, the unmentionability of exceptions (smith_exception_unaddressable), and the paper's prediction that what an exception does instead matters, since a visibly angry Smith falls into a different cell of the coarse issue than a neutral one (bare_usable_neutral_not_angry). Conjunctions of names, modelled as plurals over their conjuncts, are predicted to allow non-maximal readings they rarely have (conj_modeled_as_plural_predicts_nonmax), which the paper answers with an accommodated finer issue. For collective predicates §5.1 generalises the gap by overlap: a predicate is undefined of a plurality that fails it but overlaps one that satisfies it, which on a distributive predicate is supervaluation over the atoms (generalisedTruthValue_distributive).

Implementation notes

• Setoid W is the substrate partition type, not Roberts's question stack: the paper's §4.5 argues that the current issue is an overarching property of the discourse that is not directly manipulable, so coarseQ and fineQ are constructions for the model.
• Following §4.4, the gap is trivalent but not presuppositional, contra Gajewski.
• The §4.5 puzzle of numerals (the ten professors smiled resists non-maximality) is left open, as in the paper, and so is the accommodation step of §6.2.

References

• [Kri16]
• [Kri15b] — the dissertation the account develops
• [Las99], [Kro74] — pragmatic halos and the unmentionability of exceptions
• [SH04], [Mag14] — the homogeneity of conjunctions
• [Rob96]
• [Gaj05]

Finite model

Three professors attend Sue's talk; the predicate is "smiled".

World	Smith	Jones	Lee	Bare plural	All
allSmiled	✓	✓	✓	TRUE	true
smithNeutral	✗	✓	✓	GAP	false
smithAngry	✗	✓	✓	GAP	false
onlyLeeSmiled	✗	✗	✓	GAP	false
noneSmiled	✗	✗	✗	FALSE	false

smithNeutral and smithAngry agree on who smiled but differ in what Smith does instead, which the coarse QUD ("Was the talk well-received?") is sensitive to (§4.2); the fine QUD ("Did every professor smile?") separates all worlds.

inductive Kriz2016.ProfWorld : Type

Worlds of the five-world model. In both smithNeutral and smithAngry Smith fails to smile; the worlds differ in whether his demeanour is relevant to the coarse issue (§4.2).

• allSmiled : ProfWorld
• smithNeutral : ProfWorld
• smithAngry : ProfWorld
• onlyLeeSmiled : ProfWorld
• noneSmiled : ProfWorld

@[instance_reducible]

instance Kriz2016.instDecidableEqProfWorld : DecidableEq ProfWorld

Equations

• Kriz2016.instDecidableEqProfWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Kriz2016.instReprProfWorld : Repr ProfWorld

Equations

• Kriz2016.instReprProfWorld = { reprPrec := Kriz2016.instReprProfWorld.repr }

def Kriz2016.instReprProfWorld.repr : ProfWorld → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Kriz2016.instFintypeProfWorld : Fintype ProfWorld

Equations

• Kriz2016.instFintypeProfWorld = { elems := { val := ↑Kriz2016.ProfWorld.enumList, nodup := Kriz2016.ProfWorld.enumList_nodup }, complete := Kriz2016.instFintypeProfWorld._proof_1 }

inductive Kriz2016.Prof : Type

• smith : Prof
• jones : Prof
• lee : Prof

@[instance_reducible]

instance Kriz2016.instDecidableEqProf : DecidableEq Prof

Equations

• Kriz2016.instDecidableEqProf x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kriz2016.instReprProf.repr : Prof → ℕ → Std.Format

Equations

• Kriz2016.instReprProf.repr Kriz2016.Prof.smith prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.Prof.smith")).group prec✝
• Kriz2016.instReprProf.repr Kriz2016.Prof.jones prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.Prof.jones")).group prec✝
• Kriz2016.instReprProf.repr Kriz2016.Prof.lee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.Prof.lee")).group prec✝

@[instance_reducible]

instance Kriz2016.instReprProf : Repr Prof

Equations

• Kriz2016.instReprProf = { reprPrec := Kriz2016.instReprProf.repr }

@[instance_reducible]

instance Kriz2016.instFintypeProf : Fintype Prof

Equations

• Kriz2016.instFintypeProf = { elems := { val := ↑Kriz2016.Prof.enumList, nodup := Kriz2016.Prof.enumList_nodup }, complete := Kriz2016.instFintypeProf._proof_1 }

def Kriz2016.smiled : Prof → ProfWorld → Prop

Which professor smiled in which world.

Equations

• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.allSmiled = True
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.smithNeutral = False
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.smithAngry = False
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.onlyLeeSmiled = False
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.noneSmiled = False
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.allSmiled = True
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.smithNeutral = True
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.smithAngry = True
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.onlyLeeSmiled = False
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.noneSmiled = False
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.allSmiled = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.smithNeutral = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.smithAngry = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.onlyLeeSmiled = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.noneSmiled = False

@[instance_reducible]

instance Kriz2016.smiled.instDecidable (p : Prof) (w : ProfWorld) : Decidable (smiled p w)

Equations

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

def Kriz2016.profs : Finset Prof

All three professors.

Equations

• Kriz2016.profs = Finset.univ

inductive Kriz2016.Reception : Type

Reception grades for the coarse QUD — Smith's anger pulls reception down to mixed, his neutrality leaves it positive (§4.2).

• positive : Reception
• mixed : Reception
• negative : Reception

@[instance_reducible]

instance Kriz2016.instDecidableEqReception : DecidableEq Reception

Equations

• Kriz2016.instDecidableEqReception x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kriz2016.receptionGrade : ProfWorld → Reception

Equations

• Kriz2016.receptionGrade Kriz2016.ProfWorld.allSmiled = Kriz2016.Reception.positive
• Kriz2016.receptionGrade Kriz2016.ProfWorld.smithNeutral = Kriz2016.Reception.positive
• Kriz2016.receptionGrade Kriz2016.ProfWorld.smithAngry = Kriz2016.Reception.mixed
• Kriz2016.receptionGrade Kriz2016.ProfWorld.onlyLeeSmiled = Kriz2016.Reception.mixed
• Kriz2016.receptionGrade Kriz2016.ProfWorld.noneSmiled = Kriz2016.Reception.negative

@[reducible, inline]

abbrev Kriz2016.coarseQ : Setoid ProfWorld

The coarse QUD asks "Was Sue's talk well-received?".

Equations

• Kriz2016.coarseQ = Setoid.ker Kriz2016.receptionGrade

@[reducible, inline]

abbrev Kriz2016.fineQ : Setoid ProfWorld

The fine QUD asks "Did every professor smile?".

Equations

• Kriz2016.fineQ = ⊥

Trivalent values at each world

theorem Kriz2016.bare_allSmiled : Homogeneity.barePlural smiled profs ProfWorld.allSmiled = 1

theorem Kriz2016.bare_smithNeutral : Homogeneity.barePlural smiled profs ProfWorld.smithNeutral = 0

theorem Kriz2016.bare_onlyLeeSmiled : Homogeneity.barePlural smiled profs ProfWorld.onlyLeeSmiled = 0

theorem Kriz2016.bare_noneSmiled : Homogeneity.barePlural smiled profs ProfWorld.noneSmiled = -1

End-to-end predictions

theorem Kriz2016.smithNeutral_usable_coarse : Homogeneity.usable coarseQ (Homogeneity.barePlural smiled profs) ProfWorld.smithNeutral

The bare plural is usable at smithNeutral under the coarse QUD, the non-maximal reading.

theorem Kriz2016.smithNeutral_not_usable_fine : ¬Homogeneity.usable fineQ (Homogeneity.barePlural smiled profs) ProfWorld.smithNeutral

The bare plural is not usable at smithNeutral under the fine QUD.

theorem Kriz2016.all_not_usable_smithNeutral (q : Setoid ProfWorld) (h : Homogeneity.usable q (Homogeneity.allPlural smiled profs) ProfWorld.smithNeutral) : False

The all-sentence is not usable at smithNeutral under any QUD.

theorem Kriz2016.smith_exception_unmentionable (q : Setoid ProfWorld) (w : ProfWorld) (h : Homogeneity.usable q (Homogeneity.allPlural smiled profs) w) : smiled Prof.smith w

Wherever the all-sentence is usable, Smith smiled.

theorem Kriz2016.coarse_communicates_gap : ProfWorld.smithNeutral ∈ Homogeneity.communicatedContent coarseQ (Homogeneity.barePlural smiled profs)

The coarse QUD communicates the gap-world smithNeutral.

theorem Kriz2016.fine_does_not_communicate_gap : ProfWorld.smithNeutral ∉ Homogeneity.communicatedContent fineQ (Homogeneity.barePlural smiled profs)

The fine QUD does not communicate smithNeutral.

Unmentionability of exceptions (§4.1)

"#The professors smiled, but one of them didn't" is infelicitous even where the non-maximal reading is licensed — the paper's (25a-b), with the although diagnostic traced to [Kro74] via [Las99]. The derivation is pure Addressing (the substrate's exception_unaddressable): non-maximal use requires a cell containing both a true-world and the gap-world, and the exception-mentioning continuation straddles it.

def Kriz2016.smithDidntSmile : ProfWorld → SignType

"Smith didn't smile", the exception-mentioning continuation.

Equations

• Kriz2016.smithDidntSmile w = if Kriz2016.smiled Kriz2016.Prof.smith w then -1 else 1

theorem Kriz2016.smith_exception_unaddressable : ¬Homogeneity.addressesIssue coarseQ smithDidntSmile

Under the coarse issue licensing the non-maximal use at smithNeutral, "…but Smith didn't" cannot address the issue (§4.1).

What exceptions do (§4.2)

Whether an exception is tolerated depends on what it does instead: Smith looking neutral is irrelevant to reception, Smith looking angry is not. The model places smithNeutral and smithAngry in different coarseQ cells, so the same sentence under the same QUD is usable at one gap-world and not the other — a contrast unavailable to accounts without an issue parameter (restricted reference, alternative geometry).

theorem Kriz2016.bare_smithAngry : Homogeneity.barePlural smiled profs ProfWorld.smithAngry = 0

theorem Kriz2016.bare_smithAngry_not_usable_coarse : ¬Homogeneity.usable coarseQ (Homogeneity.barePlural smiled profs) ProfWorld.smithAngry

The bare plural is not usable at smithAngry under the coarse QUD, since smithAngry shares its cell with onlyLeeSmiled and neither is in the positive extension.

theorem Kriz2016.bare_usable_neutral_not_angry : Homogeneity.usable coarseQ (Homogeneity.barePlural smiled profs) ProfWorld.smithNeutral ∧ ¬Homogeneity.usable coarseQ (Homogeneity.barePlural smiled profs) ProfWorld.smithAngry

The same sentence under the same QUD is usable at one gap-world and not at the other, the contrast of §4.2.

Conjunction overgeneration (§6.2)

Conjunctions of proper names are homogeneous ([SH04], [Mag14]) yet generally resist non-maximal readings. Modelled as a plural over its conjunct atoms, the machinery predicts non-maximal use at a gap-world (conj_modeled_as_plural_predicts_nonmax); the paper's informal response is that mentioning an individual prompts accommodation of a finer issue on which no non-maximal reading survives, an accommodation step not formalized here or in the paper.

inductive Kriz2016.ConjAtom : Type

• bert : ConjAtom
• claire : ConjAtom
• dora : ConjAtom

@[instance_reducible]

instance Kriz2016.instDecidableEqConjAtom : DecidableEq ConjAtom

Equations

• Kriz2016.instDecidableEqConjAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Kriz2016.instReprConjAtom : Repr ConjAtom

Equations

• Kriz2016.instReprConjAtom = { reprPrec := Kriz2016.instReprConjAtom.repr }

def Kriz2016.instReprConjAtom.repr : ConjAtom → ℕ → Std.Format

Equations

• Kriz2016.instReprConjAtom.repr Kriz2016.ConjAtom.bert prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjAtom.bert")).group prec✝
• Kriz2016.instReprConjAtom.repr Kriz2016.ConjAtom.claire prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjAtom.claire")).group prec✝
• Kriz2016.instReprConjAtom.repr Kriz2016.ConjAtom.dora prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjAtom.dora")).group prec✝

@[instance_reducible]

instance Kriz2016.instFintypeConjAtom : Fintype ConjAtom

Equations

• Kriz2016.instFintypeConjAtom = { elems := { val := ↑Kriz2016.ConjAtom.enumList, nodup := Kriz2016.ConjAtom.enumList_nodup }, complete := Kriz2016.instFintypeConjAtom._proof_1 }

inductive Kriz2016.ConjWorld : Type

• allWent : ConjWorld
• dorasMissing : ConjWorld
• onlyBert : ConjWorld
• noneWent : ConjWorld

@[instance_reducible]

instance Kriz2016.instDecidableEqConjWorld : DecidableEq ConjWorld

Equations

• Kriz2016.instDecidableEqConjWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kriz2016.instReprConjWorld.repr : ConjWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Kriz2016.instReprConjWorld.repr Kriz2016.ConjWorld.allWent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjWorld.allWent")).group prec✝

@[instance_reducible]

instance Kriz2016.instReprConjWorld : Repr ConjWorld

Equations

• Kriz2016.instReprConjWorld = { reprPrec := Kriz2016.instReprConjWorld.repr }

@[instance_reducible]

instance Kriz2016.instFintypeConjWorld : Fintype ConjWorld

Equations

• Kriz2016.instFintypeConjWorld = { elems := { val := ↑Kriz2016.ConjWorld.enumList, nodup := Kriz2016.ConjWorld.enumList_nodup }, complete := Kriz2016.instFintypeConjWorld._proof_1 }

def Kriz2016.wentThere : ConjAtom → ConjWorld → Prop

Equations

• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.allWent = True
• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.dorasMissing = True
• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.onlyBert = True
• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.noneWent = False
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.allWent = True
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.dorasMissing = True
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.onlyBert = False
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.noneWent = False
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.allWent = True
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.dorasMissing = False
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.onlyBert = False
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.noneWent = False

@[instance_reducible]

instance Kriz2016.wentThere.instDecidable (a : ConjAtom) (w : ConjWorld) : Decidable (wentThere a w)

Equations

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

def Kriz2016.threeCoworkers : Finset ConjAtom

Equations

• Kriz2016.threeCoworkers = Finset.univ

inductive Kriz2016.ConjPartition : Type

Cells of the coarse "did anyone go?" issue.

• someWent : ConjPartition
• noneWent : ConjPartition

@[instance_reducible]

instance Kriz2016.instDecidableEqConjPartition : DecidableEq ConjPartition

Equations

• Kriz2016.instDecidableEqConjPartition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kriz2016.someWentPartition : ConjWorld → ConjPartition

Equations

• Kriz2016.someWentPartition Kriz2016.ConjWorld.allWent = Kriz2016.ConjPartition.someWent
• Kriz2016.someWentPartition Kriz2016.ConjWorld.dorasMissing = Kriz2016.ConjPartition.someWent
• Kriz2016.someWentPartition Kriz2016.ConjWorld.onlyBert = Kriz2016.ConjPartition.someWent
• Kriz2016.someWentPartition Kriz2016.ConjWorld.noneWent = Kriz2016.ConjPartition.noneWent

@[reducible, inline]

abbrev Kriz2016.coarseConjQ : Setoid ConjWorld

Equations

• Kriz2016.coarseConjQ = Setoid.ker Kriz2016.someWentPartition

theorem Kriz2016.conj_dorasMissing_gap : Homogeneity.barePlural wentThere threeCoworkers ConjWorld.dorasMissing = 0

theorem Kriz2016.conj_modeled_as_plural_predicts_nonmax : Homogeneity.usable coarseConjQ (Homogeneity.barePlural wentThere threeCoworkers) ConjWorld.dorasMissing

Modelled as a plural over {Bert, Claire, Dora}, the conjunction is predicted usable at the gap-world dorasMissing under the coarse issue — the overgenerated non-maximal reading.

Generalised homogeneity (§5.1)

def Kriz2016.generalisedTruthValue {Atom : Type u_1} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (a : Finset Atom) : SignType

The generalised truth value of §5.1 is true where P holds of a, undefined where a fails P but overlaps a plurality of domain that satisfies it, and false otherwise.

Equations

• Kriz2016.generalisedTruthValue P domain a = if P a then 1 else if ∃ b ∈ domain, ¬Disjoint a b ∧ P b then 0 else -1

theorem Kriz2016.generalisedTruthValue_distributive {Atom : Type u_1} [DecidableEq Atom] (pred : Atom → Prop) [DecidablePred pred] {a : Finset Atom} (hne : a.Nonempty) {domain : Finset (Finset Atom)} (hdomain : ∀ x ∈ a, {x} ∈ domain) : generalisedTruthValue (fun (s : Finset Atom) => ∀ x ∈ s, pred x) domain a = SignType.supervaluation a pred

On a distributive predicate the generalised value is supervaluation over the atoms, given a domain that contains every atom.