Križ and Chemla (2015): finding truth-value gaps

Križ and Chemla introduce two experimental methods for detecting truth-value gaps and use them to ask where the homogeneity gap of a plural definite survives embedding, under sentential negation, all, no and exactly 2. A display gives each of four cells, or boys, the trivalent value of the bare plural over its nine symbols, or presents, and a sentence is evaluated by its quantifier on the display resolved existentially or universally, the variants with some and with all in place of the definite. Gaps were found exactly where the two variants differ, which includes the GAP?? configuration of exactly 2 and excludes its GAP? configuration. Of the accounts the paper assesses, Spector's supervaluation over the two resolutions fits every finding; comparing the literal with the globally exhaustified meaning, after Magri, misses the gaps under negation, under no and in the GAP?? configuration; and the universal projection of a homogeneity presupposition predicts gaps where false was found.

Main results

• items_variants: every display of Table 13 realizes its condition, except the faulty A2 and B2 no items (faulty_items) and the GAP? item 5599 (misprinted_gapQQ).
• found_iff: Table 2 finds a gap exactly outside GAP?, apart from the discounted no tests.
• supervaluation_eq_one_iff_condition, supervaluation_eq_zero_iff_found: the supervaluation predicts every designed value and every finding.
• globalConstrual_misfit_iff: the implicature construal misfits exactly the downward-entailing GAP items and the GAP?? items; globalConstrual_wideScope: a wide-scope definite rescues it under plain negation.
• pointwise_ne_iff: supervaluating over per-boy resolutions departs exactly on GAP?.
• situations_variants: Table 12's parses and construals follow from its six situations.
• globalExh_iff_mem_strengthened: global exhaustification is Magri's double strengthening.

Implementation notes

The stimuli and findings are the tables of Data/Experiments/KrizChemla2015. The E-neg tests reuse the E-∅ displays with the negated sentence, whose designed values swap (negationItems), and sentential negation is the outer negation notAll of the unembedded sentence. The weak and strong variants are the some- and all-substituted readings, exchanged under a downward-entailing scope, which is how §3's principle, stated for upward-entailing contexts, extends to negation and no. The A2 and B2 no tests are discounted, as footnotes 10 and 14 do. The statistics are stored as printed and not re-thresholded; the (si2) and (si4) construals are the supervaluation by Table 12's lit ≠ loc column.

TODO

• The trivalent projection theory after George that §6.3 credits with matching the supervaluation is not implemented.

References

• [KC15]
• [Spe13b]
• [Mag09]
• [Mag14]
• [CFS12]
• [Sch94]
• [Lob00]
• [Gaj05]
• [Geo08]
• [Ste12]
• [BK01]
• [vB84]

Displays and their resolutions

@[reducible, inline]

abbrev KrizChemla2015.Display : Type

A display lists, for each boy, the trivalent value of he found his presents.

Equations

• KrizChemla2015.Display = List SignType

def KrizChemla2015.cell (n : ℕ) : SignType

A cell in which n of the nine objects are found or target-colored has the value of the bare plural over the nine, true when all are, false when none are, and a gap otherwise.

Equations

• KrizChemla2015.cell n = Homogeneity.barePlural (fun (j m : ℕ) => j < m) (Finset.range 9) n

theorem KrizChemla2015.designated_k3_cell (n : ℕ) : cell n = 1 ↔ 9 ≤ n

A cell is true, designated at K3, when all nine objects are found.

theorem KrizChemla2015.designated_lp_cell (n : ℕ) : 0 ≤ cell n ↔ 1 ≤ n

A cell is non-false, designated at LP, when at least one object is found.

def KrizChemla2015.holds (q : Quantifier.NumberTree) (c : List Bool) : Prop

A number tree holds of a resolution according to how many boys it resolves out of and into the scope.

Equations

• KrizChemla2015.holds q c = q (List.count false c) (List.count true c)

@[instance_reducible]

instance KrizChemla2015.instDecidableHoldsOfDecidableRelNat (q : Quantifier.NumberTree) [DecidableRel q] (c : List Bool) : Decidable (holds q c)

Equations

• KrizChemla2015.instDecidableHoldsOfDecidableRelNat q c = KrizChemla2015.instDecidableHoldsOfDecidableRelNat._aux_1 q c

theorem KrizChemla2015.holds_map_not (q : Quantifier.NumberTree) (c : List Bool) : holds q (List.map not c) ↔ holds q.innerNeg c

Reversing every boy's resolution evaluates the inner negation.

def KrizChemla2015.resolve (δ : Trivalent.Designation) (d : Display) : List Bool

The uniform resolution of a display at a designation standard puts each boy in the scope when his value is designated.

Equations

• KrizChemla2015.resolve δ d = List.map (fun (v : SignType) => decide (δ.threshold ≤ v)) d

theorem KrizChemla2015.resolve_map_neg (δ : Trivalent.Designation) (d : Display) : resolve δ (List.map Neg.neg d) = List.map not (resolve δ.dual d)

Negating every cell resolves at the dual standard and reverses the result.

def KrizChemla2015.resolutions (d : Display) : List (List Bool)

The resolutions of a display that choose a designation standard boy by boy.

Equations

• KrizChemla2015.resolutions d = (List.map (fun (v : SignType) => [decide (0 ≤ v), decide (v = 1)]) d).sections

theorem KrizChemla2015.resolve_mem_resolutions (δ : Trivalent.Designation) (d : Display) : resolve δ d ∈ resolutions d

theorem KrizChemla2015.resolve_le_of_mem_resolutions {d : Display} {c : List Bool} (hc : c ∈ resolutions d) : List.Forall₂ (fun (x1 x2 : Bool) => x1 ≤ x2) (resolve Trivalent.Designation.k3 d) c ∧ List.Forall₂ (fun (x1 x2 : Bool) => x1 ≤ x2) c (resolve Trivalent.Designation.lp d)

The K3 resolution is least and the LP resolution greatest among the resolutions.

theorem KrizChemla2015.resolve_lp_eq_resolve_k3 {d : Display} (h : ∀ v ∈ d, v ≠ 0) : resolve Trivalent.Designation.lp d = resolve Trivalent.Designation.k3 d

A display without partial cells has a single resolution.

theorem KrizChemla2015.holds_of_forall₂_le {q : Quantifier.NumberTree} (hq : q.ScopeMonotone) {c c' : List Bool} (h : List.Forall₂ (fun (x1 x2 : Bool) => x1 ≤ x2) c c') (hc : holds q c) : holds q c'

Moving boys into the scope preserves a scope-monotone quantifier.

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.reading (q : Quantifier.NumberTree) (d : Display) (δ : Trivalent.Designation) : Prop

A reading evaluates the quantifier over the uniform resolution at δ, which at LP (non-false) is the existential resolution of the definite and at K3 (true) the universal one.

Equations

• KrizChemla2015.reading q d δ = KrizChemla2015.holds q (KrizChemla2015.resolve δ d)

@[reducible, inline]

abbrev KrizChemla2015.someReading (q : Quantifier.NumberTree) (d : Display) : Prop

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

Equations

• KrizChemla2015.someReading q d = KrizChemla2015.reading q d Trivalent.Designation.lp

@[reducible, inline]

abbrev KrizChemla2015.allReading (q : Quantifier.NumberTree) (d : Display) : Prop

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

Equations

• KrizChemla2015.allReading q d = KrizChemla2015.reading q d Trivalent.Designation.k3

@[instance_reducible]

instance KrizChemla2015.instDecidableReadingOfDecidableRelNat (q : Quantifier.NumberTree) (d : Display) [DecidableRel q] (δ : Trivalent.Designation) : Decidable (reading q d δ)

Equations

• KrizChemla2015.instDecidableReadingOfDecidableRelNat q d δ = KrizChemla2015.instDecidableReadingOfDecidableRelNat._aux_1 q d δ

theorem KrizChemla2015.reading_all {d : Display} (δ : Trivalent.Designation) : reading Quantifier.NumberTree.all d δ ↔ ∀ v ∈ d, δ.threshold ≤ v

The universal quantifier holds of a resolution when every boy is in the scope.

theorem KrizChemla2015.reading_no {d : Display} (δ : Trivalent.Designation) : reading Quantifier.NumberTree.no d δ ↔ ∀ v ∈ d, ¬δ.threshold ≤ v

The negative quantifier holds of a resolution when no boy is in the scope.

theorem KrizChemla2015.reading_map_neg {q : Quantifier.NumberTree} {d : Display} (δ : Trivalent.Designation) : reading q (List.map Neg.neg d) δ ↔ reading q.innerNeg d δ.dual

Negating the predicate in every cell evaluates the inner negation of the quantifier at the dual standard, so it exchanges the some- and all-substituted readings.

theorem KrizChemla2015.someReading_iff_allReading {q : Quantifier.NumberTree} {d : Display} (h : ∀ v ∈ d, v ≠ 0) : someReading q d ↔ allReading q d

On a display without partial cells the two resolutions coincide.

theorem KrizChemla2015.allReading_imp_someReading {q : Quantifier.NumberTree} {d : Display} (hq : q.ScopeMonotone) : allReading q d → someReading q d

Under a scope-monotone quantifier the universal variant entails the existential one.

theorem KrizChemla2015.someReading_imp_allReading {q : Quantifier.NumberTree} {d : Display} (hq : q.ScopeAntitone) : someReading q d → allReading q d

Under a scope-antitone quantifier the existential variant entails the universal one.

Two-component verdicts

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

The verdict from two meaning components is the supervaluation over the pair, clearly true when both hold, clearly false when neither does, and a truth-value gap when they conflict.

Equations

• KrizChemla2015.gapValue p q = SignType.supervaluation Finset.univ fun (b : Bool) => if b = true then p else q

@[simp]

theorem KrizChemla2015.gapValue_eq_one_iff {p q : Prop} [Decidable p] [Decidable q] : gapValue p q = 1 ↔ p ∧ q

@[simp]

theorem KrizChemla2015.gapValue_eq_neg_one_iff {p q : Prop} [Decidable p] [Decidable q] : gapValue p q = -1 ↔ ¬p ∧ ¬q

@[simp]

theorem KrizChemla2015.gapValue_eq_zero_iff {p q : Prop} [Decidable p] [Decidable q] : gapValue p q = 0 ↔ ¬(p ↔ q)

theorem KrizChemla2015.gapValue_ne_zero {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : gapValue p q ≠ 0

Two components that agree yield a bivalent verdict.

The approaches of §6

def KrizChemla2015.globalExh (q : Quantifier.NumberTree) (d : Display) : Prop

The globally double-exhaustified meaning, (30) and (39), is the conjunction of the some- and all-substituted readings, [Mag14]'s double strengthening (globalExh_iff_mem_strengthened). In a downward-entailing scope exhaustification is vacuous, and the conjunction is then the literal meaning (globalExh_iff_of_scopeAntitone).

Equations

• KrizChemla2015.globalExh q d = (KrizChemla2015.someReading q d ∧ KrizChemla2015.allReading q d)

theorem KrizChemla2015.globalExh_iff_of_scopeAntitone {q : Quantifier.NumberTree} {d : Display} (hq : q.ScopeAntitone) : globalExh q d ↔ someReading q d

Under a downward-entailing quantifier global exhaustification is vacuous.

def KrizChemla2015.supervaluation (q : Quantifier.NumberTree) [DecidableRel q] (d : Display) : SignType

The supervaluation of [Spe13b] (§6.2) makes the sentence true when it is true however the definite is resolved, existentially or universally, and false when it is false however it is resolved.

Equations

• KrizChemla2015.supervaluation q d = SignType.supervaluation Finset.univ (KrizChemla2015.reading q d)

@[instance_reducible]

instance KrizChemla2015.instDecidableGlobalExh (q : Quantifier.NumberTree) [DecidableRel q] (d : Display) : Decidable (globalExh q d)

Equations

• KrizChemla2015.instDecidableGlobalExh q d = { decide := decide (KrizChemla2015.someReading q d) && decide (KrizChemla2015.allReading q d), reflects_decide := ⋯ }

def KrizChemla2015.globalConstrual (q : Quantifier.NumberTree) [DecidableRel q] (d : Display) : SignType

The implicature construals (si1) and (si3) of §6.1.2, after [Mag09]'s oddness condition, put a gap where the literal and the globally exhaustified meaning conflict.

Equations

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

def KrizChemla2015.universalPresupposition (q : Quantifier.NumberTree) [DecidableRel q] (d : Display) : SignType

Homogeneity as a presupposition projecting universally from the quantifier's scope, after [Sch94], [Lob00] and [Gaj05] as assessed in §6.3, is the presupposition that every cell is homogeneous weakly conjoined with the universal-force assertion. The presupposition is the ∂ of [BK01], the join p ⊔ 0 with the gap.

Equations

• KrizChemla2015.universalPresupposition q d = (max (SignType.ofProp (∀ v ∈ d, v ≠ 0)) 0).meetWeak (SignType.ofProp (KrizChemla2015.allReading q d))

def KrizChemla2015.pointwise (q : Quantifier.NumberTree) [DecidableRel q] (d : Display) : SignType

Supervaluation over the resolutions that treat the partial cells one by one, a richer candidate set than the existential and universal readings, of the kind §6.2 says predicts a gap in the gap? condition; footnote 19 notes that quantified trivalent logics make the same prediction.

Equations

• KrizChemla2015.pointwise q d = SignType.supervaluation (KrizChemla2015.resolutions d).toFinset (KrizChemla2015.holds q)

theorem KrizChemla2015.supervaluation_eq_designations {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : supervaluation q d = SignType.supervaluation Finset.univ (reading q d)

The supervaluation ranges over the two designation standards.

theorem KrizChemla2015.supervaluation_eq_one_iff {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : supervaluation q d = 1 ↔ someReading q d ∧ allReading q d

The supervaluation is true when both variants are.

theorem KrizChemla2015.supervaluation_eq_neg_one_iff {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : supervaluation q d = -1 ↔ ¬someReading q d ∧ ¬allReading q d

The supervaluation is false when neither variant is true.

theorem KrizChemla2015.supervaluation_eq_zero_iff {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : supervaluation q d = 0 ↔ ¬(someReading q d ↔ allReading q d)

The supervaluation gaps when the variants differ.

theorem KrizChemla2015.supervaluation_ne_zero {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} (h : ∀ v ∈ d, v ≠ 0) : supervaluation q d ≠ 0

A display without partial cells gets a bivalent verdict, whatever the quantifier.

theorem KrizChemla2015.supervaluation_map_neg {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : supervaluation q (List.map Neg.neg d) = supervaluation q.innerNeg d

The supervaluation does not see the scope of the definite relative to a negation inside the cells, since negating every cell gives the supervaluation of the inner negation.

theorem KrizChemla2015.supervaluation_compl {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : supervaluation qᶜ d = -supervaluation q d

The outer negation of the quantifier negates the supervaluation.

theorem KrizChemla2015.globalConstrual_eq_zero_iff {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : globalConstrual q d = 0 ↔ someReading q d ∧ ¬allReading q d

The global construal gaps where the literal meaning holds and the all-substituted one fails.

theorem KrizChemla2015.globalConstrual_ne_supervaluation_iff {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : globalConstrual q d ≠ supervaluation q d ↔ ¬someReading q d ∧ allReading q d

The global construals depart from supervaluation exactly where the literal meaning is false and the locally exhaustified meaning true.

theorem KrizChemla2015.globalConstrual_eq_supervaluation_of_scopeMonotone {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} (hq : q.ScopeMonotone) : globalConstrual q d = supervaluation q d

In the scope of a scope-monotone quantifier such as every the implicature construals all align, since comparing the literal meaning with global exhaustification and with local exhaustification comes to the same thing (§6.1.3).

theorem KrizChemla2015.globalConstrual_ne_zero_of_scopeAntitone {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} (hq : q.ScopeAntitone) : globalConstrual q d ≠ 0

Without local exhaustification no gap can arise in the scope of a downward-entailing quantifier such as no, since exhaustification is vacuous there and the literal and globally exhaustified meanings never conflict.

theorem KrizChemla2015.universalPresupposition_eq_zero_iff {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : universalPresupposition q d = 0 ↔ 0 ∈ d

Universal projection fails exactly on the displays with a partial cell.

Negation and the wide-scope parse (§6.1.3)

theorem KrizChemla2015.supervaluation_all_singleton (v : SignType) : supervaluation Quantifier.NumberTree.all [v] = v

Over one cell the unembedded sentence takes the cell's value.

theorem KrizChemla2015.globalConstrual_notAll_ne_zero (v : SignType) : globalConstrual Quantifier.NumberTree.notAll [v] ≠ 0

The literal-against-global construal never gaps under plain negation, which is downward entailing.

theorem KrizChemla2015.globalConstrual_wideScope (v : SignType) : globalConstrual Quantifier.NumberTree.all [-v] = supervaluation Quantifier.NumberTree.notAll [v]

On the parse (35) where the definite takes scope over negation, the literal-against-global construal of the shapes are not green is the supervaluation of its narrow-scope negation, so it gaps exactly on the mixed cell. No such parse is available under no, whose definite contains a variable the quantifier binds.

Global exhaustification is double strengthening

def KrizChemla2015.weakPole (q : Quantifier.NumberTree) [DecidableRel q] (n : ℕ) : Finset (Fin n → SignType)

The displays of n boys on which the some-substituted reading holds, the weak pole.

Equations

• KrizChemla2015.weakPole q n = {w : Fin n → SignType | KrizChemla2015.someReading q (List.ofFn w)}

def KrizChemla2015.strongPole (q : Quantifier.NumberTree) [DecidableRel q] (n : ℕ) : Finset (Fin n → SignType)

The displays of n boys on which the all-substituted reading holds, the strong pole.

Equations

• KrizChemla2015.strongPole q n = {w : Fin n → SignType | KrizChemla2015.allReading q (List.ofFn w)}

theorem KrizChemla2015.globalExh_iff_mem_strengthened {q : Quantifier.NumberTree} [DecidableRel q] {n : ℕ} (h : weakPole q n ⊆ strongPole q n ∨ (weakPole q n ∩ strongPole q n).Nonempty) (w : Fin n → SignType) : globalExh q (List.ofFn w) ↔ w ∈ Magri2014.strengthened Magri2014.primalMates (Magri2014.primal (weakPole q n) (strongPole q n)) Magri2014.Item.mystery

Exhaustifying the sentence twice over its some- and all-substituted alternatives, by [Mag14]'s double strengthening, yields globalExh, (30) and (39), provided either the strong pole is weaker, as in a downward-entailing scope, or the two poles are compatible.

Per-boy resolutions

theorem KrizChemla2015.supervaluation_eq_image {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : supervaluation q d = SignType.supervaluation (Finset.image (fun (δ : Trivalent.Designation) => resolve δ d) Finset.univ) (holds q)

The two-candidate supervaluation ranges over the uniform resolutions.

theorem KrizChemla2015.toFlat_pointwise_le {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : (pointwise q d).toFlat ≤ (supervaluation q d).toFlat

Richer candidates can only add gaps, since whatever the quantifier the per-boy supervaluation is at most as informative as the two-candidate one.

theorem KrizChemla2015.pointwise_eq_supervaluation_of_scopeMonotone {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} (hq : q.ScopeMonotone) : pointwise q d = supervaluation q d

Under a scope-monotone quantifier the per-boy resolutions add no gap, the uniform ones being their extremes.

theorem KrizChemla2015.pointwise_compl {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} : pointwise qᶜ d = -pointwise q d

The outer negation of the quantifier negates the per-boy supervaluation.

theorem KrizChemla2015.pointwise_eq_supervaluation_of_scopeAntitone {q : Quantifier.NumberTree} [DecidableRel q] {d : Display} (hq : q.ScopeAntitone) : pointwise q d = supervaluation q d

Under a scope-antitone quantifier, likewise.

The experiments

def KrizChemla2015.Embedding.tree : Embedding → Quantifier.NumberTree

The number tree of each environment; sentential negation is the outer negation of the unembedded sentence over its one cell.

Equations

• KrizChemla2015.Embedding.unembedded.tree = Quantifier.NumberTree.all
• KrizChemla2015.Embedding.negation.tree = Quantifier.NumberTree.notAll
• KrizChemla2015.Embedding.all.tree = Quantifier.NumberTree.all
• KrizChemla2015.Embedding.no.tree = Quantifier.NumberTree.no
• KrizChemla2015.Embedding.exactly.tree = Quantifier.NumberTree.cardinal {KrizChemla2015.numeral}

@[instance_reducible]

instance KrizChemla2015.instDecidableRelNatTree (e : Embedding) : DecidableRel e.tree

Equations

• KrizChemla2015.instDecidableRelNatTree KrizChemla2015.Embedding.unembedded = KrizChemla2015.instDecidableRelNatTree._aux_1
• KrizChemla2015.instDecidableRelNatTree KrizChemla2015.Embedding.all = KrizChemla2015.instDecidableRelNatTree._aux_3
• KrizChemla2015.instDecidableRelNatTree KrizChemla2015.Embedding.negation = KrizChemla2015.instDecidableRelNatTree._aux_5
• KrizChemla2015.instDecidableRelNatTree KrizChemla2015.Embedding.no = KrizChemla2015.instDecidableRelNatTree._aux_7
• KrizChemla2015.instDecidableRelNatTree KrizChemla2015.Embedding.exactly = KrizChemla2015.instDecidableRelNatTree._aux_9

@[instance_reducible]

instance KrizChemla2015.instDecidableScopeAntitoneTree (e : Embedding) : Decidable e.tree.ScopeAntitone

Negation and no are downward entailing; the other environments are not.

Equations

• KrizChemla2015.instDecidableScopeAntitoneTree KrizChemla2015.Embedding.unembedded = isFalse KrizChemla2015.instDecidableScopeAntitoneTree._proof_1
• KrizChemla2015.instDecidableScopeAntitoneTree KrizChemla2015.Embedding.all = isFalse KrizChemla2015.instDecidableScopeAntitoneTree._proof_2
• KrizChemla2015.instDecidableScopeAntitoneTree KrizChemla2015.Embedding.negation = isTrue Quantifier.NumberTree.scopeAntitone_notAll
• KrizChemla2015.instDecidableScopeAntitoneTree KrizChemla2015.Embedding.no = isTrue Quantifier.NumberTree.scopeAntitone_no
• KrizChemla2015.instDecidableScopeAntitoneTree KrizChemla2015.Embedding.exactly = isFalse ⋯

def KrizChemla2015.Item.display (i : Item) : Display

The display of an item, each cell's trivalent value.

Equations

• i.display = List.map KrizChemla2015.cell i.cells

def KrizChemla2015.Condition.neg : Condition → Condition

The designed value of the negated sentence swaps TRUE and FALSE.

Equations

• KrizChemla2015.Condition.clearlyTrue.neg = KrizChemla2015.Condition.clearlyFalse
• KrizChemla2015.Condition.clearlyFalse.neg = KrizChemla2015.Condition.clearlyTrue
• x✝.neg = x✝

def KrizChemla2015.negationItems : List Item

The E-neg items are the E-∅ displays judged with the negated sentence.

Equations

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

def KrizChemla2015.tested : List Item

The items judged in the experiments, Table 13's and the E-neg ones.

Equations

• KrizChemla2015.tested = KrizChemla2015.items ++ KrizChemla2015.negationItems

def KrizChemla2015.weak (e : Embedding) (d : Display) : Prop

The weak variant of the sentence, which the strong one entails, is the some-substituted reading, or under a downward-entailing scope the all-substituted one.

Equations

• KrizChemla2015.weak e d = if e.tree.ScopeAntitone then KrizChemla2015.allReading e.tree d else KrizChemla2015.someReading e.tree d

def KrizChemla2015.strong (e : Embedding) (d : Display) : Prop

The strong variant of the sentence.

Equations

• KrizChemla2015.strong e d = if e.tree.ScopeAntitone then KrizChemla2015.someReading e.tree d else KrizChemla2015.allReading e.tree d

@[instance_reducible]

instance KrizChemla2015.instDecidableWeak (e : Embedding) (d : Display) : Decidable (weak e d)

Equations

• KrizChemla2015.instDecidableWeak e d = id inferInstance

@[instance_reducible]

instance KrizChemla2015.instDecidableStrong (e : Embedding) (d : Display) : Decidable (strong e d)

Equations

• KrizChemla2015.instDecidableStrong e d = id inferInstance

def KrizChemla2015.misprinted : Item

The GAP? item 5599 of Table 13, whose two full cells §3.3.2's description of the GAP? items excludes.

Equations

• KrizChemla2015.misprinted = { embedding := KrizChemla2015.Embedding.exactly, condition := KrizChemla2015.Condition.gapQ, cells := [5, 5, 9, 9], status := KrizChemla2015.ItemStatus.used }

theorem KrizChemla2015.misprinted_mem : misprinted ∈ items

The item is printed in Table 13.

theorem KrizChemla2015.misprinted_gapQQ : ¬weak Embedding.exactly misprinted.display ∧ strong Embedding.exactly misprinted.display

The item realizes the GAP?? pattern, its all-variant true and its some-variant false.

theorem KrizChemla2015.items_variants (i : Item) : i ∈ tested → i.status ≠ ItemStatus.faulty → i ≠ misprinted → (weak i.embedding i.display ↔ i.condition ∈ [Condition.clearlyTrue, Condition.gap]) ∧ (strong i.embedding i.display ↔ i.condition ∈ [Condition.clearlyTrue, Condition.gapQQ])

Every tested item realizes its condition by §3's principle, read with the entailment direction of its scope, the weak variant holding in the TRUE and GAP conditions and the strong one in the TRUE and GAP?? conditions.

theorem KrizChemla2015.faulty_items (i : Item) : i ∈ items → i.status = ItemStatus.faulty → weak i.embedding i.display ∧ ¬strong i.embedding i.display

Because of the coding error of §3.2.4, the faulty E-no items, coded FALSE, realize the GAP pattern.

def KrizChemla2015.GapTest.Discounted (t : GapTest) : Prop

A test is discounted when it is one of the A2 and B2 tests of no, whose sentences lacked negative inversion (fn 10) and were plausibly read with an unbound definite (fn 14).

Equations

• t.Discounted = (t.experiment ∈ [KrizChemla2015.Experiment.a2, KrizChemla2015.Experiment.b2] ∧ t.embedding = KrizChemla2015.Embedding.no)

@[instance_reducible]

instance KrizChemla2015.instDecidableDiscounted (t : GapTest) : Decidable t.Discounted

Equations

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

theorem KrizChemla2015.found_iff (t : GapTest) : t ∈ gapTests → ((t.found = Found.yes ↔ t.condition ≠ Condition.gapQ) ↔ ¬t.Discounted)

Table 2 found a gap in every GAP and GAP?? test and in no GAP? test, except in the discounted tests.

theorem KrizChemla2015.gapTests_condition (t : GapTest) : t ∈ gapTests → t.condition ∈ [Condition.gap, Condition.gapQ, Condition.gapQQ]

Table 2 tests only the gap conditions.

theorem KrizChemla2015.supervaluation_eq_one_iff_weak (e : Embedding) (d : Display) : supervaluation e.tree d = 1 ↔ weak e d ∧ strong e d

The supervaluation is true exactly on the variants' agreement in truth.

theorem KrizChemla2015.supervaluation_eq_zero_iff_weak (e : Embedding) (d : Display) : supervaluation e.tree d = 0 ↔ ¬(weak e d ↔ strong e d)

The supervaluation gaps exactly where the variants differ.

theorem KrizChemla2015.supervaluation_eq_one_iff_condition (i : Item) : i ∈ tested → i.status ≠ ItemStatus.faulty → i ≠ misprinted → (supervaluation i.embedding.tree i.display = 1 ↔ i.condition = Condition.clearlyTrue)

The supervaluation is true exactly on the items designed true.

theorem KrizChemla2015.supervaluation_eq_zero_iff_found (i : Item) : i ∈ tested → i.status ≠ ItemStatus.faulty → i ≠ misprinted → ∀ t ∈ gapTests, ¬t.Discounted → t.embedding = i.embedding → t.condition = i.condition → (supervaluation i.embedding.tree i.display = 0 ↔ t.found = Found.yes)

The supervaluation gaps on an item exactly when its environment and condition were found to gap, outside the discounted tests.

theorem KrizChemla2015.globalConstrual_misfit_iff (i : Item) : i ∈ tested → i.status ≠ ItemStatus.faulty → i ≠ misprinted → ∀ t ∈ gapTests, ¬t.Discounted → t.embedding = i.embedding → t.condition = i.condition → (¬(globalConstrual i.embedding.tree i.display = 0 ↔ t.found = Found.yes) ↔ i.embedding.tree.ScopeAntitone ∧ i.condition = Condition.gap ∨ i.condition = Condition.gapQQ)

The literal-against-global construal misfits exactly the GAP items under a downward-entailing scope, sentential negation and no, and the GAP?? items, where the all-variant is true and the some-variant false (§6.1.3).

theorem KrizChemla2015.universalPresupposition_false_item : ∃ i ∈ items, i.embedding = Embedding.all ∧ i.condition = Condition.clearlyFalse ∧ universalPresupposition i.embedding.tree i.display = 0

Universal projection predicts a presupposition failure on a FALSE item of all, where the sentence was judged false as soon as one cell has no target symbols, the argument from (42).

theorem KrizChemla2015.pointwise_ne_iff (i : Item) : i ∈ tested → i.status ≠ ItemStatus.faulty → i ≠ misprinted → (pointwise i.embedding.tree i.display ≠ supervaluation i.embedding.tree i.display ↔ i.condition = Condition.gapQ)

The per-boy supervaluation departs from the two-candidate one on exactly the GAP? items.

def KrizChemla2015.atLeastTwo : Quantifier.NumberTree

The at-least reading of exactly 2 that §3.4 discusses.

Equations

• KrizChemla2015.atLeastTwo = Quantifier.NumberTree.cardinal {b : ℕ | 2 ≤ b}

@[instance_reducible]

instance KrizChemla2015.instDecidableRelNatAtLeastTwo : DecidableRel atLeastTwo

Equations

• KrizChemla2015.instDecidableRelNatAtLeastTwo x✝ b = { decide := Nat.ble 2 b, reflects_decide := ⋯ }

theorem KrizChemla2015.atLeastTwo_gapQ (i : Item) : i ∈ items → i.condition = Condition.gapQ → i ≠ misprinted → supervaluation atLeastTwo i.display = 0

On the at-least reading the GAP? items are gap items.

theorem KrizChemla2015.atLeastTwo_false (i : Item) : i ∈ items → i.embedding = Embedding.exactly → i.condition = Condition.clearlyFalse → (supervaluation atLeastTwo i.display = 1 ↔ 3 ≤ List.count 9 i.cells)

On the at-least reading the FALSE items of exactly with three or more full cells are true, the items with elevated true responses in Fig. 10.

def KrizChemla2015.Share.value : Share → SignType

A teacher's cell in a situation of Table 12.

Equations

• KrizChemla2015.Share.all.value = 1
• KrizChemla2015.Share.half.value = 0
• KrizChemla2015.Share.none.value = -1

def KrizChemla2015.Situation.display (s : Situation) : Display

The display of a situation of Table 12, Bill's, Mary's and Sue's cells.

Equations

• s.display = List.map KrizChemla2015.Share.value [s.bill, s.mary, s.sue]

theorem KrizChemla2015.situations_variants (s : Situation) : s ∈ situations → (someReading Embedding.exactly.tree s.display ↔ s.condition ∈ [Condition.clearlyTrue, Condition.gap]) ∧ (allReading Embedding.exactly.tree s.display ↔ s.condition ∈ [Condition.clearlyTrue, Condition.gapQQ]) ∧ (supervaluation Embedding.exactly.tree s.display = 0 ↔ s.found = Found.yes) ∧ (globalConstrual Embedding.exactly.tree s.display = 0 ↔ s.condition = Condition.gap)

Table 12 follows from its situations. The literal and locally exhaustified parses hold as its corresponding conditions require, the (si2) and (si4) construals, the supervaluation, gap exactly where a gap was found, and the (si1) and (si3) construals miss the GAP?? situation.