Križ (2016): homogeneity, non-maximality, and all

This file verifies [Kri16]'s predictions against a finite model, using the homogeneity substrate in Semantics.Homogeneity and its plural instantiation (barePlural, allPlural — both originating with this paper). A five-world model checks the predictions end-to-end, including the §4.2 sensitivity to what an exception does instead and the §4.1 unmentionability of exceptions. Closing sections connect the analysis to the typed data in Data.Examples.Kriz2015 and to [Mag14]'s rival gap derivation.

Implementation notes

QUD W is the substrate partition type, not the [Rob96] QUD-stack: §4.5 of the paper argues (examples (39)-(40)) that the current issue is an overarching, not directly manipulable, property of the discourse, so coarseQ/fineQ below are pedagogical constructions. Following §4.4, the gap is trivalent but not presuppositional (contra [Gaj05]). The §4.6 numeral puzzle (the ten professors smiled resists non-maximality) is left unaddressed, as in the paper.

References

• M. Križ, Homogeneity, Non-Maximality, and All
• M. Križ, Aspects of Homogeneity in the Semantics of Natural Language
• K. Fine, Vagueness, Truth and Logic

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 ⋯

@[instance_reducible]

instance Kriz2016.instReprProf : Repr Prof

Equations

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

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.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

def Kriz2016.coarseQ : QUD ProfWorld

Coarse QUD: "Was Sue's talk well-received?"

Equations

• Kriz2016.coarseQ = QUD.ofDecEq Kriz2016.receptionGrade

def Kriz2016.fineQ : QUD ProfWorld

Fine QUD: "Did every professor smile?"

Equations

• Kriz2016.fineQ = QUD.ofDecEq id

Trivalent values at each world

theorem Kriz2016.bare_allSmiled : Semantics.Homogeneity.barePlural smiled profs ProfWorld.allSmiled = Trivalent.true

theorem Kriz2016.bare_smithNeutral : Semantics.Homogeneity.barePlural smiled profs ProfWorld.smithNeutral = Trivalent.indet

theorem Kriz2016.bare_onlyLeeSmiled : Semantics.Homogeneity.barePlural smiled profs ProfWorld.onlyLeeSmiled = Trivalent.indet

theorem Kriz2016.bare_noneSmiled : Semantics.Homogeneity.barePlural smiled profs ProfWorld.noneSmiled = Trivalent.false

theorem Kriz2016.bare_profs_homogeneous : Semantics.Homogeneity.isHomogeneous (Semantics.Homogeneity.barePlural smiled profs)

The bare plural about the professors is homogeneous: smithNeutral is in the gap.

End-to-end predictions

theorem Kriz2016.smithNeutral_usable_coarse : Semantics.Homogeneity.usable coarseQ (Semantics.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 : ¬Semantics.Homogeneity.usable fineQ (Semantics.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 : QUD ProfWorld) (h : Semantics.Homogeneity.usable q (Semantics.Homogeneity.allPlural smiled profs) ProfWorld.smithNeutral) : False

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

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

Wherever the all-sentence is usable, Smith smiled.

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

The coarse QUD communicates the gap-world smithNeutral.

theorem Kriz2016.fine_does_not_communicate_gap : ProfWorld.smithNeutral ∉ Semantics.Homogeneity.communicatedContent fineQ (Semantics.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 : Trivalent.Prop3 ProfWorld

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

Equations

• Kriz2016.smithDidntSmile w = if Kriz2016.smiled Kriz2016.Prof.smith w then Trivalent.false else Trivalent.true

theorem Kriz2016.smith_exception_unaddressable : ¬Semantics.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 : Semantics.Homogeneity.barePlural smiled profs ProfWorld.smithAngry = Trivalent.indet

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

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

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

The §4.2 contrast: same sentence, same QUD, opposite usability at the two gap-worlds.

The typed switches data

The switches items of Data.Examples.Kriz2015 show the model's pattern in the wild: "Oh no, the switches are on!" is acceptable under the existential issue and unacceptable under the universal one (cf. smithNeutral_usable_coarse vs smithNeutral_not_usable_fine), and the all variant is unacceptable even in the permissive context (cf. all_not_usable_smithNeutral). The gap rows lift to .indet observations in the pooled Generalizations.HomogeneityGap data.

theorem Kriz2016.switches_gap_observed_indet : Option.map (fun (x : Generalizations.HomogeneityGap.GapDatum) => x.observed) (Generalizations.HomogeneityGap.fromExample Kriz2015.Examples.switches_pos_gap) = some Trivalent.indet ∧ Option.map (fun (x : Generalizations.HomogeneityGap.GapDatum) => x.observed) (Generalizations.HomogeneityGap.fromExample Kriz2015.Examples.switches_neg_gap) = some Trivalent.indet

Both switches gap rows (positive and negated) observe .indet: the gap is symmetric under negation.

theorem Kriz2016.model_matches_gap_row : Option.map (fun (x : Generalizations.HomogeneityGap.GapDatum) => x.observed) (Generalizations.HomogeneityGap.fromExample Kriz2015.Examples.switches_pos_gap) = some (Semantics.Homogeneity.barePlural smiled profs ProfWorld.smithNeutral)

The model matches the data: the bare plural's value at the gap-world is the value the positive gap row observes.

Conjunction overgeneration (§6.2)

Conjunctions of proper names are homogeneous (Szabolcsi & Haddican 2004, [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 ⋯

@[instance_reducible]

instance Kriz2016.instReprConjWorld : Repr ConjWorld

Equations

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

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.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

def Kriz2016.coarseConjQ : QUD ConjWorld

Equations

• Kriz2016.coarseConjQ = QUD.ofDecEq Kriz2016.someWentPartition

theorem Kriz2016.conj_dorasMissing_gap : Semantics.Homogeneity.barePlural wentThere threeCoworkers ConjWorld.dorasMissing = Trivalent.indet

theorem Kriz2016.conj_modeled_as_plural_predicts_nonmax : Semantics.Homogeneity.usable coarseConjQ (Semantics.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.

Križ vs Magri on the gap's value

[Mag14] derives homogeneity from double exhaustification over alternative geometry: on a gap scenario, doubleExh .mystery is bivalent-false (Magri2014.gap_positive_false) — the gap collapses inside the semantics. For Križ the same input is .indet, and the gap is pragmatically recoverable under a coarse issue (gap_enables_nonmax). A false sentence is unutterable on standard Gricean terms, so Magri's account needs additional pragmatic machinery to license the non-maximal uses the finite model exhibits. Magri2014.fromPredicate translates the model's (smiled, profs, smithNeutral) into Magri's count abstraction, so both operators run on the same input.

def Kriz2016.magriGapScenario : Magri2014.Scenario

A 3-atom Magri scenario where 2 of 3 atoms satisfy the predicate.

Equations

• Kriz2016.magriGapScenario = { total := 3, satisfying := 2, valid := Kriz2016.magriGapScenario._proof_2 }

theorem Kriz2016.fromPredicate_smithNeutral : Magri2014.fromPredicate smiled profs ProfWorld.smithNeutral = magriGapScenario

Counting satisfiers of smiled at smithNeutral yields the 2-of-3 scenario: the divergence below is a same-input comparison.

theorem Kriz2016.magriGapScenario_isGap : Magri2014.isGap magriGapScenario = true

theorem Kriz2016.magri_2of3_gap_is_bivalent_false : Magri2014.doubleExh Magri2014.Role.mystery magriGapScenario = false

Magri's doubleExh .mystery is false on a 2-of-3 gap.

theorem Kriz2016.kriz_vs_magri_alternative_geometry : Magri2014.doubleExh Magri2014.Role.mystery (Magri2014.fromPredicate smiled profs ProfWorld.smithNeutral) = false ∧ Semantics.Homogeneity.barePlural smiled profs ProfWorld.smithNeutral = Trivalent.indet ∧ Semantics.Homogeneity.usable coarseQ (Semantics.Homogeneity.barePlural smiled profs) ProfWorld.smithNeutral

On the same input, Magri's operator returns false while Križ's returns .indet and the sentence is usable under the coarse issue: the two accounts assign the gap incompatible statuses.