[KC15]: Two methods to find truth-value gaps

[KC15] introduce two experimental methods for detecting truth-value gaps — separate completely-true and completely-false tasks (Exps. A0-A3) and one-shot ternary judgments (Exps. B1-B3, C2-C4) — and apply them to the projection of plural-definite homogeneity from the scope of sentential negation, every/all, no, and exactly 2. The gap projects in every tested environment except the gap? configuration (where the some- and all-substituted variants of the sentence are both false); under no it emerges only with the grammatical restimulation of Exp. C2, small but robust (fn. 14).

The stimulus rows live in the generated Data.Examples.KrizChemla2015 module and are pooled by [[Generalizations.HomogeneityProjection]] (embedded cells) and [[Generalizations.HomogeneityGap]] (unembedded and negated cells). This file implements §6's assessment of the three theoretical approaches to homogeneity against those pools.

Main declarations

• Cell, Display — the experimental displays: arrays of nine objects, each array classified by whether it is fully, partially, or not at all target-satisfying.
• someReading, allReading — the paper's guiding principle (§3): the sentence variants with the definite plural replaced by an existential or a universal quantifier.
• supervaluation — two-candidate supervaluation ([Spe13a]): true iff true on both resolutions of the definite, false iff false on both. As §6.2 notes, this coincides with the local-exhaustification implicature construals (si2)/(si4) of §6.1.2 on the projection data.
• globalConstrual — implicature construals (si1)/(si3) ([Mag09], [Mag14]): gap iff the literal and globally exhaustified meanings conflict.
• universalPresupposition — homogeneity as a presupposition projecting universally from the quantifier's scope ([Sch94], [Lob00], [Gaj05]).
• display — a representative Table 13 display for each tested C-series cell.

Main results

• supervaluation_matches_pool — the supervaluation/local-exhaustification prediction reproduces every pooled projection judgment: §6.4's bottom line, at the price of either local exhaustification in downward-entailing contexts (contra [CFS12]) or a restricted candidate set.
• globalConstrual_divergence — construals comparing the literal meaning with global exhaustification fail on exactly the C2 no gap and the C4 gap?? gap, the paper's two problem cells for (si1)/(si3).
• universalPresupposition_divergence — universal projection fails on exactly the bivalently-judged conditions containing non-homogeneous cells (argument (42) of §6.3) plus the gap? condition.
• globalConstrual_every, globalConstrual_no_never_gap — §6.1.3's structural observations: all implicature construals align in the scope of every, and without local exhaustification no gap can arise in the scope of no.
• supervaluationGap_matches_pool, bareLiteral_misses_negation_gap, wideScopeParse_matches_pool — the unembedded grid: supervaluation predicts the polarity × scenario judgments; the bare existential literal meaning predicts no gap under negation (the downward-entailing problem of §6.1.3); the wide-scope parse of the definite (fn. 18) restores the fit.

Todo

• [Geo08]-style trivalent presupposition projection — the variant §6.3 endorses as matching the supervaluation predictions — is not implemented, nor are the richer-candidate supervaluation variants of fn. 19, which over-predict a gap in the gap? condition.

Displays

inductive KrizChemla2015.Cell : Type

One array of a display — one boy's presents (C series) or one cell of shapes (A/B series) — classified by how much of it is target-satisfying: all of it, some but not all (mixed), or none.

• full : Cell
• mixed : Cell
• empty : Cell

@[instance_reducible]

instance KrizChemla2015.instDecidableEqCell : DecidableEq Cell

Equations

• KrizChemla2015.instDecidableEqCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KrizChemla2015.instReprCell.repr : Cell → ℕ → Std.Format

Equations

• KrizChemla2015.instReprCell.repr KrizChemla2015.Cell.full prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KrizChemla2015.Cell.full")).group prec✝
• KrizChemla2015.instReprCell.repr KrizChemla2015.Cell.mixed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KrizChemla2015.Cell.mixed")).group prec✝
• KrizChemla2015.instReprCell.repr KrizChemla2015.Cell.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KrizChemla2015.Cell.empty")).group prec✝

@[instance_reducible]

instance KrizChemla2015.instReprCell : Repr Cell

Equations

• KrizChemla2015.instReprCell = { reprPrec := KrizChemla2015.instReprCell.repr }

@[reducible, inline]

abbrev KrizChemla2015.Display : Type

A display: one Cell per boy.

Equations

• KrizChemla2015.Display = List KrizChemla2015.Cell

def KrizChemla2015.Cell.homogeneous (c : Cell) : Prop

A cell is homogeneous when the target property holds of all of it or none of it — the presupposition [Sch94]-style accounts attach to plural predication.

Equations

• c.homogeneous = (c ≠ KrizChemla2015.Cell.mixed)

@[instance_reducible]

instance KrizChemla2015.instDecidablePredCellHomogeneous : DecidablePred Cell.homogeneous

Equations

• KrizChemla2015.instDecidablePredCellHomogeneous c = KrizChemla2015.instDecidablePredCellHomogeneous._aux_1 c

def KrizChemla2015.occupied (d : Display) : ℕ

Number of cells whose boy found at least some of his presents.

Equations

• KrizChemla2015.occupied d = List.countP (fun (x : KrizChemla2015.Cell) => x != KrizChemla2015.Cell.empty) d

def KrizChemla2015.filled (d : Display) : ℕ

Number of cells whose boy found all of his presents.

Equations

• KrizChemla2015.filled d = List.count KrizChemla2015.Cell.full d

The some- and all-substituted readings

§3's guiding principle: a sentence with a definite plural has a gap in a situation where the variant with an existential in place of the definite is true while the variant with a universal is false.

def KrizChemla2015.someReading : Generalizations.HomogeneityProjection.EmbeddingOperator → Display → Prop

The some-substituted reading: some (of his) presents in place of the definite. This is the literal meaning on [Mag14]'s analysis and the existential resolution of the definite on [Spe13a]'s.

Equations

• KrizChemla2015.someReading Generalizations.HomogeneityProjection.EmbeddingOperator.every x✝ = ∀ c ∈ x✝, c ≠ KrizChemla2015.Cell.empty
• KrizChemla2015.someReading Generalizations.HomogeneityProjection.EmbeddingOperator.no x✝ = ∀ c ∈ x✝, c = KrizChemla2015.Cell.empty
• KrizChemla2015.someReading Generalizations.HomogeneityProjection.EmbeddingOperator.exactlyTwo x✝ = (KrizChemla2015.occupied x✝ = 2)
• KrizChemla2015.someReading Generalizations.HomogeneityProjection.EmbeddingOperator.notEvery x✝ = ¬∀ c ∈ x✝, c ≠ KrizChemla2015.Cell.empty

def KrizChemla2015.allReading : Generalizations.HomogeneityProjection.EmbeddingOperator → Display → Prop

The all-substituted reading: all of his presents in place of the definite. This is the locally exhaustified parse on [Mag14]'s analysis and the universal resolution on [Spe13a]'s.

Equations

• KrizChemla2015.allReading Generalizations.HomogeneityProjection.EmbeddingOperator.every x✝ = ∀ c ∈ x✝, c = KrizChemla2015.Cell.full
• KrizChemla2015.allReading Generalizations.HomogeneityProjection.EmbeddingOperator.no x✝ = ∀ c ∈ x✝, c ≠ KrizChemla2015.Cell.full
• KrizChemla2015.allReading Generalizations.HomogeneityProjection.EmbeddingOperator.exactlyTwo x✝ = (KrizChemla2015.filled x✝ = 2)
• KrizChemla2015.allReading Generalizations.HomogeneityProjection.EmbeddingOperator.notEvery x✝ = ¬∀ c ∈ x✝, c = KrizChemla2015.Cell.full

@[instance_reducible]

instance KrizChemla2015.instDecidableSomeReading (op : Generalizations.HomogeneityProjection.EmbeddingOperator) (d : Display) : Decidable (someReading op d)

Equations

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

@[instance_reducible]

instance KrizChemla2015.instDecidableAllReading (op : Generalizations.HomogeneityProjection.EmbeddingOperator) (d : Display) : Decidable (allReading op d)

Equations

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

def KrizChemla2015.globalExh : Generalizations.HomogeneityProjection.EmbeddingOperator → Display → Prop

The globally double-exhaustified meaning, (30) in [KC15]: exhaustification is vacuous in the downward-entailing scope of no and conjoins the some- and all-substituted readings elsewhere. (notEvery postdates the paper's grid — [ABB+23] — and takes the general clause; no theorem below exercises it.)

Equations

• KrizChemla2015.globalExh Generalizations.HomogeneityProjection.EmbeddingOperator.no x✝ = KrizChemla2015.someReading Generalizations.HomogeneityProjection.EmbeddingOperator.no x✝
• KrizChemla2015.globalExh x✝¹ x✝ = (KrizChemla2015.someReading x✝¹ x✝ ∧ KrizChemla2015.allReading x✝¹ x✝)

@[instance_reducible]

instance KrizChemla2015.instDecidableGlobalExh (op : Generalizations.HomogeneityProjection.EmbeddingOperator) (d : Display) : Decidable (globalExh op d)

Equations

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

The three approaches

def KrizChemla2015.gapValue (p q : Prop) [Decidable p] [Decidable q] : Trivalent

Trivalent verdict from two meaning components: clearly true when both hold, clearly false when neither does, a truth-value gap when they conflict. Each §6 construal instantiates this with a different pair of components.

Equations

• KrizChemla2015.gapValue p q = if p ∧ q then Trivalent.true else if ¬p ∧ ¬q then Trivalent.false else Trivalent.indet

def KrizChemla2015.supervaluation (op : Generalizations.HomogeneityProjection.EmbeddingOperator) (d : Display) : Trivalent

Two-candidate supervaluation ([Spe13a]; §6.2): supervaluate over the existential and universal resolutions of the definite. Extensionally this is also the (si2)/(si4) implicature construal of §6.1.2 — gap iff the literal and locally exhaustified meanings conflict — which is how §6.2 argues the two approaches make the same projection predictions.

Equations

• KrizChemla2015.supervaluation op d = KrizChemla2015.gapValue (KrizChemla2015.someReading op d) (KrizChemla2015.allReading op d)

def KrizChemla2015.globalConstrual (op : Generalizations.HomogeneityProjection.EmbeddingOperator) (d : Display) : Trivalent

Implicature construals (si1)/(si3) of §6.1.2 ([Mag09]'s oddness condition): gap iff the literal meaning and the globally exhaustified meaning conflict.

Equations

• KrizChemla2015.globalConstrual op d = KrizChemla2015.gapValue (KrizChemla2015.someReading op d) (KrizChemla2015.globalExh op d)

def KrizChemla2015.universalPresupposition (op : Generalizations.HomogeneityProjection.EmbeddingOperator) (d : Display) : Trivalent

Homogeneity as a presupposition projecting universally from the quantifier's scope ([Sch94], [Lob00], [Gaj05], as assessed in §6.3): presupposition failure unless every cell is homogeneous, in which case the universal-force assertion decides the sentence.

Equations

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

The tested grid

def KrizChemla2015.display : Generalizations.HomogeneityProjection.EmbeddingOperator → Generalizations.HomogeneityProjection.GapScenario → Option Display

A representative Table 13 display for each condition of Exps. C2-C4 (none for cells the paper did not test). Read [cell₁, ..., cell₄] for the four boys; e.g. the (every, gap) display 9929 — three boys found all nine of their presents, one found two — is [full, full, mixed, full].

Equations

• One or more equations did not get rendered due to their size.
• KrizChemla2015.display x✝¹ x✝ = none

def KrizChemla2015.predictOn (account : Generalizations.HomogeneityProjection.EmbeddingOperator → Display → Trivalent) (op : Generalizations.HomogeneityProjection.EmbeddingOperator) (sc : Generalizations.HomogeneityProjection.GapScenario) : Option Trivalent

Restrict a display-level account to the paper's tested grid, none marking cells the paper did not test.

Equations

• KrizChemla2015.predictOn account op sc = Option.map (account op) (KrizChemla2015.display op sc)

Predictions against the projection pool

theorem KrizChemla2015.supervaluation_matches_pool (d : Generalizations.HomogeneityProjection.ProjectionDatum) : d ∈ Generalizations.HomogeneityProjection.allData → d.source.bibkey = "kriz-chemla-2015" → predictOn supervaluation d.operator d.scenario = some d.observed

The supervaluation (equivalently, local-exhaustification) prediction reproduces every pooled projection judgment — §6.4's bottom line. The fit is bought either by allowing local exhaustification in downward-entailing contexts, contra [CFS12], or by restricting the supervaluation candidates to the existential and universal resolutions.

theorem KrizChemla2015.globalConstrual_divergence (d : Generalizations.HomogeneityProjection.ProjectionDatum) : d ∈ Generalizations.HomogeneityProjection.allData → d.source.bibkey = "kriz-chemla-2015" → (predictOn globalConstrual d.operator d.scenario ≠ some d.observed ↔ (d.operator, d.scenario) ∈ [(Generalizations.HomogeneityProjection.EmbeddingOperator.no, Generalizations.HomogeneityProjection.GapScenario.gap), (Generalizations.HomogeneityProjection.EmbeddingOperator.exactlyTwo, Generalizations.HomogeneityProjection.GapScenario.gapQQ)])

Construals locating the gap in a literal-vs-global-exhaustification conflict fail on exactly two cells: the small-but-robust no gap of Exp. C2 (no implicature arises in a downward-entailing context, §6.1.3) and the gap?? gap of Exp. C4 (Table 12's s6, where the literal meaning and the implicature are false and true respectively, so their conjunction is simply false). Both cells are predicted clearly false but observed gappy.

theorem KrizChemla2015.universalPresupposition_divergence (d : Generalizations.HomogeneityProjection.ProjectionDatum) : d ∈ Generalizations.HomogeneityProjection.allData → d.source.bibkey = "kriz-chemla-2015" → (predictOn universalPresupposition d.operator d.scenario ≠ some d.observed ↔ (d.operator, d.scenario) ∈ [(Generalizations.HomogeneityProjection.EmbeddingOperator.every, Generalizations.HomogeneityProjection.GapScenario.falseScenario), (Generalizations.HomogeneityProjection.EmbeddingOperator.no, Generalizations.HomogeneityProjection.GapScenario.falseScenario), (Generalizations.HomogeneityProjection.EmbeddingOperator.exactlyTwo, Generalizations.HomogeneityProjection.GapScenario.falseScenario), (Generalizations.HomogeneityProjection.EmbeddingOperator.exactlyTwo, Generalizations.HomogeneityProjection.GapScenario.gapQ)])

Universal projection of the homogeneity presupposition fails on exactly the bivalently-judged conditions whose displays contain non-homogeneous cells — the false conditions of Exps. C2/C3, argument (42) of §6.3 — plus the gap? condition, where a presupposition failure is predicted but falsity observed.

Structural observations (§6.1.3)

theorem KrizChemla2015.globalConstrual_every (d : Display) : globalConstrual Generalizations.HomogeneityProjection.EmbeddingOperator.every d = supervaluation Generalizations.HomogeneityProjection.EmbeddingOperator.every d

In the scope of every the implicature construals all align: comparing the literal meaning with global exhaustification and with local exhaustification comes to the same thing, on any display.

theorem KrizChemla2015.globalConstrual_no_never_gap (d : Display) : globalConstrual Generalizations.HomogeneityProjection.EmbeddingOperator.no d ≠ Trivalent.indet

Without local exhaustification, no gap can arise in the scope of no: exhaustification is vacuous there, so the literal and globally exhaustified meanings never conflict. The observed C2 gap therefore forces either local exhaustification or the supervaluation/presupposition alternatives.

The unembedded grid

The polarity × scenario cells of Exps. A0/A1/B1 live in the [[Generalizations.HomogeneityGap]] pool. An unembedded display is a single cell: nine shapes, of which all, some, or none are target-colored.

def KrizChemla2015.scenarioCell : Generalizations.HomogeneityGap.GapScenario → Cell

The display cell realizing each unembedded scenario.

Equations

• KrizChemla2015.scenarioCell Generalizations.HomogeneityGap.GapScenario.all = KrizChemla2015.Cell.full
• KrizChemla2015.scenarioCell Generalizations.HomogeneityGap.GapScenario.none = KrizChemla2015.Cell.empty
• KrizChemla2015.scenarioCell Generalizations.HomogeneityGap.GapScenario.gap = KrizChemla2015.Cell.mixed

def KrizChemla2015.supervaluationGap (pol : Features.Polarity) (sc : Generalizations.HomogeneityGap.GapScenario) : Trivalent

Supervaluation over the unembedded grid: resolve the definite existentially and universally, under negation for negative polarity.

Equations

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

theorem KrizChemla2015.supervaluationGap_matches_pool (d : Generalizations.HomogeneityGap.GapDatum) : d ∈ Generalizations.HomogeneityGap.allData → d.source.bibkey = "kriz-chemla-2015" → supervaluationGap d.polarity d.scenario = d.observed

The supervaluation account reproduces the paper's unembedded and negated judgments: truth on uniform displays, the gap on mixed ones, projected through negation (Exps. A1/B1).

def KrizChemla2015.bareLiteralNegative (sc : Generalizations.HomogeneityGap.GapScenario) : Trivalent

The bare implicature construal assigns a negated sentence its existential literal meaning outright — negation is downward-entailing, so no implicature arises and no gap is predicted (§6.1.3).

Equations

• KrizChemla2015.bareLiteralNegative sc = if KrizChemla2015.scenarioCell sc = KrizChemla2015.Cell.empty then Trivalent.true else Trivalent.false

theorem KrizChemla2015.bareLiteral_misses_negation_gap : ∃ d ∈ Generalizations.HomogeneityGap.allData, d.source.bibkey = "kriz-chemla-2015" ∧ d.polarity = Features.Polarity.negative ∧ d.scenario = Generalizations.HomogeneityGap.GapScenario.gap ∧ bareLiteralNegative d.scenario ≠ d.observed

The E-neg gap of Exps. A1/B1 refutes the bare implicature construal: the negated mixed-display cell is observed gappy but predicted clearly false. This is §6.1.3's downward-entailing problem, which for plain negation the wide-scope parse solves (wideScopeParse_matches_pool) but for no — whose definite contains a variable bound by the quantifier ([steedman-2012]) — nothing does.

def KrizChemla2015.wideScopeParse (sc : Generalizations.HomogeneityGap.GapScenario) : Trivalent

The negated sentence with the definite parsed above negation (fn. 18): the existential and universal resolutions now scope over the negated predicate.

Equations

• KrizChemla2015.wideScopeParse sc = KrizChemla2015.gapValue (KrizChemla2015.scenarioCell sc ≠ KrizChemla2015.Cell.full) (KrizChemla2015.scenarioCell sc = KrizChemla2015.Cell.empty)

theorem KrizChemla2015.wideScopeParse_matches_pool (d : Generalizations.HomogeneityGap.GapDatum) : d ∈ Generalizations.HomogeneityGap.allData → d.source.bibkey = "kriz-chemla-2015" → d.polarity = Features.Polarity.negative → wideScopeParse d.scenario = d.observed

With the wide-scope parse, the implicature construal again reproduces the negated judgments — the paper's rescue for plain negation.