Scontras and Pearl (2021): When Pragmatics Matters More for Truth-Value Judgments

Scontras and Pearl model the truth-value judgment task for the scopally ambiguous sentences every horse didn't jump and two horses didn't jump. A world is the number of horses that jumped. A speaker who knows the world, a scope interpretation and a question under discussion chooses between the sentence and silence, aiming to convey the answer to the question (S1). A pragmatic listener inverts that speaker jointly over worlds, interpretations and questions (L1). The endorsing speaker, who sees only the world, chooses between the sentence and silence by the listener's beliefs about the world (S2), so that a truth-value judgment is a production decision.

Main results

• one_half_lt_S2_real_amb_iff: the sentence is endorsed more often than not exactly when it is produced at the observed world more often than on average.
• S2_real_amb_all: once the question is whether all the horses jumped, the two interpretations of every horse didn't jump produce alike and the scope prior does not affect endorsement.
• S2_real_amb_mono_baseRate: production falls with the number of jumpers, so a higher success base rate in the binomial world prior raises endorsement.
• share_twoAtLeast_le_share_twoExact, share_twoExact_lt_share_twoAtLeast: with four horses and two jumpers the surface speaker favors the exact reading whatever the question, while the inverse speaker asked whether all jumped favors the at-least reading.

Implementation notes

• The rationality of S1 and the priors on worlds, interpretations and questions are parameters.
• A determiner is a quantifier on van Benthem's tree of numbers, a relation between the number of restrictor members outside its scope and the number inside it. Every is NumberTree.all, a numeral is the cardinal quantifier of the interval of a Degree.Comparison, and a scope interpretation is a negation of the determiner (Scope.negation), inner for surface scope and outer for inverse scope. The paper tabulates the truth conditions at two and at four horses, and here they follow for any number.
• Both models share the paper's five questions. The every-not model is the case of a question prior carried by the first three.
• Utterances are costless and the literal listener carries no world prior, following Qing and Franke. The speaker addresses the question as in the hyperbole model of Kao and colleagues.

TODO

• The numerical predictions of the paper's figures, at unit rationality and its grid of priors, are not stated.
• The base-rate result is proved at two horses, the paper's scenario. For any number of horses it would follow from production being antitone and the binomial family being stochastically increasing in its success probability.

References

• [SP21]
• [ML03]
• [KWBG14]
• [QF15]
• [GF16]
• [vB84]

inductive ScontrasPearl2021.Utt : Type

The utterances of (2) are the null utterance, which says nothing, and the scopally ambiguous test sentence.

• null : Utt
• amb : Utt

@[instance_reducible]

instance ScontrasPearl2021.instDecidableEqUtt : DecidableEq Utt

Equations

• ScontrasPearl2021.instDecidableEqUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ScontrasPearl2021.instFintypeUtt : Fintype Utt

Equations

• ScontrasPearl2021.instFintypeUtt = { elems := { val := ↑ScontrasPearl2021.Utt.enumList, nodup := ScontrasPearl2021.Utt.enumList_nodup }, complete := ScontrasPearl2021.instFintypeUtt._proof_1 }

@[instance_reducible]

instance ScontrasPearl2021.instMeasurableSpaceUtt : MeasurableSpace Utt

Equations

• ScontrasPearl2021.instMeasurableSpaceUtt = ⊤

instance ScontrasPearl2021.instDiscreteMeasurableSpaceUtt : DiscreteMeasurableSpace Utt

inductive ScontrasPearl2021.Scope : Type

The scope interpretations of the test sentence put the determiner over negation, or negation over the determiner.

• surface : Scope
• inverse : Scope

@[instance_reducible]

instance ScontrasPearl2021.instDecidableEqScope : DecidableEq Scope

Equations

• ScontrasPearl2021.instDecidableEqScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ScontrasPearl2021.instFintypeScope : Fintype Scope

Equations

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

@[instance_reducible]

instance ScontrasPearl2021.instMeasurableSpaceScope : MeasurableSpace Scope

Equations

• ScontrasPearl2021.instMeasurableSpaceScope = ⊤

instance ScontrasPearl2021.instDiscreteMeasurableSpaceScope : DiscreteMeasurableSpace Scope

instance ScontrasPearl2021.instNonemptyScope : Nonempty Scope

inductive ScontrasPearl2021.QUD : Type

The questions under discussion of (3) and (7) ask how many horses jumped, and whether all, none, exactly two or at least two did.

• howMany : QUD
• all : QUD
• none : QUD
• exactlyTwo : QUD
• atLeastTwo : QUD

@[instance_reducible]

instance ScontrasPearl2021.instDecidableEqQUD : DecidableEq QUD

Equations

• ScontrasPearl2021.instDecidableEqQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ScontrasPearl2021.instFintypeQUD : Fintype QUD

Equations

• ScontrasPearl2021.instFintypeQUD = { elems := { val := ↑ScontrasPearl2021.QUD.enumList, nodup := ScontrasPearl2021.QUD.enumList_nodup }, complete := ScontrasPearl2021.instFintypeQUD._proof_1 }

@[instance_reducible]

instance ScontrasPearl2021.instMeasurableSpaceQUD : MeasurableSpace QUD

Equations

• ScontrasPearl2021.instMeasurableSpaceQUD = ⊤

instance ScontrasPearl2021.instDiscreteMeasurableSpaceQUD : DiscreteMeasurableSpace QUD

instance ScontrasPearl2021.instNonemptyQUD : Nonempty QUD

@[reducible, inline]

abbrev ScontrasPearl2021.World (n : ℕ) : Type

A world is the number of horses, out of n, that jumped.

Equations

• ScontrasPearl2021.World n = Fin (n + 1)

Semantics

def ScontrasPearl2021.Scope.negation : Scope → Quantifier.NumberTree → Quantifier.NumberTree

A scope interpretation negates the determiner on the tree of numbers. The surface interpretation, the determiner over negation, is its inner negation, and the inverse interpretation, negation over the determiner, is its outer negation.

Equations

• ScontrasPearl2021.Scope.surface.negation x✝ = x✝.innerNeg
• ScontrasPearl2021.Scope.inverse.negation x✝ = x✝ᶜ

@[instance_reducible]

instance ScontrasPearl2021.instDecidableRelNatNegation (i : Scope) (D : Quantifier.NumberTree) [DecidableRel D] : DecidableRel (i.negation D)

Equations

• ScontrasPearl2021.instDecidableRelNatNegation ScontrasPearl2021.Scope.surface D = ScontrasPearl2021.instDecidableRelNatNegation._aux_1 D
• ScontrasPearl2021.instDecidableRelNatNegation ScontrasPearl2021.Scope.inverse D = ScontrasPearl2021.instDecidableRelNatNegation._aux_3 D

theorem ScontrasPearl2021.negation_surface_all : Scope.surface.negation Quantifier.NumberTree.all = Quantifier.NumberTree.no

On its surface interpretation every horse didn't jump is no horse jumped, the paper's "none" reading.

theorem ScontrasPearl2021.negation_inverse_all : Scope.inverse.negation Quantifier.NumberTree.all = Quantifier.NumberTree.notAll

On its inverse interpretation every horse didn't jump is not all horses jumped, the paper's "not-all" reading.

def ScontrasPearl2021.numeral (c : Degree.Comparison) (k : ℕ) : Quantifier.NumberTree

A numeral is the cardinal quantifier of the interval that the comparison c selects at k. The comparison .eq gives the exact reading and .ge the at-least reading.

Equations

• ScontrasPearl2021.numeral c k = Quantifier.NumberTree.cardinal (c.interval k)

@[instance_reducible]

instance ScontrasPearl2021.instDecidableRelNatNumeral (c : Degree.Comparison) (k : ℕ) : DecidableRel (numeral c k)

Equations

• ScontrasPearl2021.instDecidableRelNatNumeral c k = ScontrasPearl2021.instDecidableRelNatNumeral._aux_1 c k

@[reducible, inline]

abbrev ScontrasPearl2021.twoExact : Quantifier.NumberTree

The numeral two on its exact reading.

Equations

• ScontrasPearl2021.twoExact = ScontrasPearl2021.numeral Degree.Comparison.eq 2

@[reducible, inline]

abbrev ScontrasPearl2021.twoAtLeast : Quantifier.NumberTree

The numeral two on its at-least reading.

Equations

• ScontrasPearl2021.twoAtLeast = ScontrasPearl2021.numeral Degree.Comparison.ge 2

def ScontrasPearl2021.ext (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) : Scope → Utt → Finset (World n)

The extension of an utterance under a scope interpretation ((2), (6)) among n horses. The null utterance is true everywhere. With w jumpers, n - w horses lie outside the scope jump and w inside it, and D horses didn't jump is true when the interpretation's negation of D holds of those two counts.

Equations

• ScontrasPearl2021.ext D n x✝ ScontrasPearl2021.Utt.null = Finset.univ
• ScontrasPearl2021.ext D n x✝ ScontrasPearl2021.Utt.amb = (x✝.negation D).row n

theorem ScontrasPearl2021.mem_ext {D : Quantifier.NumberTree} [DecidableRel D] {n : ℕ} {w : World n} {i : Scope} : w ∈ ext D n i Utt.amb ↔ i.negation D (n - ↑w) ↑w

theorem ScontrasPearl2021.mem_ext_surface {D : Quantifier.NumberTree} [DecidableRel D] {n : ℕ} {w : World n} : w ∈ ext D n Scope.surface Utt.amb ↔ D (↑w) (n - ↑w)

theorem ScontrasPearl2021.mem_ext_inverse {D : Quantifier.NumberTree} [DecidableRel D] {n : ℕ} {w : World n} : w ∈ ext D n Scope.inverse Utt.amb ↔ ¬D (n - ↑w) ↑w

theorem ScontrasPearl2021.mem_ext_every_surface {n : ℕ} {w : World n} : w ∈ ext Quantifier.NumberTree.all n Scope.surface Utt.amb ↔ w = 0

On its surface interpretation every horse didn't jump is true where none jumped (2).

theorem ScontrasPearl2021.mem_ext_every_inverse {n : ℕ} {w : World n} : w ∈ ext Quantifier.NumberTree.all n Scope.inverse Utt.amb ↔ w ≠ Fin.last n

On its inverse interpretation every horse didn't jump is true where not all jumped (2).

theorem ScontrasPearl2021.mem_ext_numeral_surface {c : Degree.Comparison} {k n : ℕ} {w : World n} : w ∈ ext (numeral c k) n Scope.surface Utt.amb ↔ c.Rel (n - ↑w) k

On its surface interpretation a numeral sentence is true where the number of non-jumpers stands in the numeral's comparison to its value (6).

theorem ScontrasPearl2021.mem_ext_numeral_inverse {c : Degree.Comparison} {k n : ℕ} {w : World n} : w ∈ ext (numeral c k) n Scope.inverse Utt.amb ↔ ¬c.Rel (↑w) k

On its inverse interpretation a numeral sentence is true where the number of jumpers does not stand in the numeral's comparison to its value (6).

theorem ScontrasPearl2021.ext_congr {D : Quantifier.NumberTree} [DecidableRel D] {n : ℕ} {D' : Quantifier.NumberTree} [DecidableRel D'] (h : ∀ (a b : ℕ), a + b = n → (D a b ↔ D' a b)) (i : Scope) (u : Utt) : ext D n i u = ext D' n i u

The extension sees a determiner only at counts that sum to the number of horses, a row of the tree of numbers, so determiners that agree there have the same extensions.

theorem ScontrasPearl2021.numeral_eq_iff_all {n a b : ℕ} (h : a + b = n) : numeral Degree.Comparison.eq n a b ↔ Quantifier.NumberTree.all a b

Among n restrictor members, exactly n lie inside the scope just in case none lies outside.

theorem ScontrasPearl2021.numeral_ge_iff_all {n a b : ℕ} (h : a + b = n) : numeral Degree.Comparison.ge n a b ↔ Quantifier.NumberTree.all a b

Among n restrictor members, at least n lie inside the scope just in case none lies outside.

theorem ScontrasPearl2021.ext_numeral_eq_self (n : ℕ) : ext (numeral Degree.Comparison.eq n) n = ext Quantifier.NumberTree.all n

With as many horses as the numeral counts, the numeral sentence on the exact reading is true exactly where every horse didn't jump is, on both interpretations (§4.2.1).

theorem ScontrasPearl2021.ext_numeral_ge_self (n : ℕ) : ext (numeral Degree.Comparison.ge n) n = ext Quantifier.NumberTree.all n

With as many horses as the numeral counts, the numeral sentence on the at-least reading is true exactly where every horse didn't jump is, on both interpretations (§4.2.1).

theorem ScontrasPearl2021.ext_twoExact_surface : ext twoExact 4 Scope.surface Utt.amb = {2}

With four horses, two horses didn't jump on the exact reading of the numeral is true on its surface interpretation only where exactly two jumped ((6), Figure 5).

theorem ScontrasPearl2021.ext_twoExact_inverse : ext twoExact 4 Scope.inverse Utt.amb = {0, 1, 3, 4}

With four horses, two horses didn't jump on the exact reading is true on its inverse interpretation wherever the number of jumpers is not two (6).

theorem ScontrasPearl2021.ext_twoAtLeast_surface : ext twoAtLeast 4 Scope.surface Utt.amb = {0, 1, 2}

With four horses, two horses didn't jump on the at-least reading is true on its surface interpretation where fewer than three jumped (6).

theorem ScontrasPearl2021.ext_twoAtLeast_inverse : ext twoAtLeast 4 Scope.inverse Utt.amb = {0, 1}

With four horses, two horses didn't jump on the at-least reading is true on its inverse interpretation where fewer than two jumped (6).

def ScontrasPearl2021.project (n : ℕ) : QUD → World n → World n ⊕ Bool

The projection of a question ((3), (7)) sends a world to its answer, the number of jumpers for how many?, and for the polar questions whether all, none, exactly two or at least two jumped.

Equations

• ScontrasPearl2021.project n ScontrasPearl2021.QUD.howMany x✝ = Sum.inl x✝
• ScontrasPearl2021.project n ScontrasPearl2021.QUD.all x✝ = Sum.inr (decide (x✝ = Fin.last n))
• ScontrasPearl2021.project n ScontrasPearl2021.QUD.none x✝ = Sum.inr (decide (x✝ = 0))
• ScontrasPearl2021.project n ScontrasPearl2021.QUD.exactlyTwo x✝ = Sum.inr (decide (↑x✝ = 2))
• ScontrasPearl2021.project n ScontrasPearl2021.QUD.atLeastTwo x✝ = Sum.inr (decide (2 ≤ ↑x✝))

def ScontrasPearl2021.cell (n : ℕ) (q : QUD) (w : World n) : Finset (World n)

The cell of a world under a question is the set of worlds sharing its answer.

Equations

• ScontrasPearl2021.cell n q w = {w' : ScontrasPearl2021.World n | ScontrasPearl2021.project n q w' = ScontrasPearl2021.project n q w}

theorem ScontrasPearl2021.mem_cell {n : ℕ} {q : QUD} {w w' : World n} : w' ∈ cell n q w ↔ project n q w' = project n q w

theorem ScontrasPearl2021.mem_cell_self {n : ℕ} (q : QUD) (w : World n) : w ∈ cell n q w

theorem ScontrasPearl2021.mem_cell_all {n : ℕ} {w w' : World n} : w' ∈ cell n QUD.all w ↔ (w' = Fin.last n ↔ w = Fin.last n)

theorem ScontrasPearl2021.cell_exactlyTwo_two (w : World 2) : cell 2 QUD.exactlyTwo w = cell 2 QUD.all w

With two horses, exactly two? asks whether all jumped.

theorem ScontrasPearl2021.cell_atLeastTwo_two (w : World 2) : cell 2 QUD.atLeastTwo w = cell 2 QUD.all w

With two horses, at least two? asks whether all jumped.

The model

noncomputable def ScontrasPearl2021.L0 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (i : Scope) : ProbabilityTheory.Kernel Utt (World n)

The literal listener is uniform on the extension of the utterance under the scope interpretation, with no world prior (fn. 6).

Equations

• ScontrasPearl2021.L0 D n i = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (u : ScontrasPearl2021.Utt) => ↑(ScontrasPearl2021.ext D n i u))

instance ScontrasPearl2021.instIsFiniteKernelUttWorldL0 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (i : Scope) : ProbabilityTheory.IsFiniteKernel (L0 D n i)

theorem ScontrasPearl2021.map_L0_apply (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (i : Scope) (q : QUD) (u : Utt) (w : World n) : (((L0 D n i).map (project n q)) u) {project n q w} = (ProbabilityTheory.uniformOn ↑(ext D n i u)) ↑(cell n q w)

The literal listener of a scope interpretation gives a world's answer to a question the fraction of the extension lying in the world's cell.

noncomputable def ScontrasPearl2021.S1 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) : ProbabilityTheory.Kernel (World n × Scope × QUD) Utt

The speaker of §3.1, at a world, a scope interpretation and a question, knows the world's answer to the question and is informative at rationality α about the belief of the interpretation's literal listener about it. The utterances are costless (fn. 8).

Equations

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

theorem ScontrasPearl2021.S1_apply (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (w : World n) (l : Scope × QUD) : (S1 D n α) (w, l) = (RSA.speaker α 0 (⇑((L0 D n l.1).map (project n l.2))) MeasureTheory.Measure.dirac) (project n l.2 w)

instance ScontrasPearl2021.instIsFiniteKernelProdWorldScopeQUDUttS1 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) : ProbabilityTheory.IsFiniteKernel (S1 D n α)

theorem ScontrasPearl2021.isMarkovKernel_S1 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (hα : 0 ≤ α) : ProbabilityTheory.IsMarkovKernel (S1 D n α)

noncomputable def ScontrasPearl2021.L1 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) : ProbabilityTheory.Kernel Utt (World n × Scope × QUD)

The pragmatic listener of §3.1 inverts the speaker over worlds, interpretations and questions, against the product of the world prior and a prior on interpretations and questions (the paper's P(i) P(q)).

Equations

• ScontrasPearl2021.L1 D n α μ ν = RSA.listener (μ.prod ν) ⇑(ScontrasPearl2021.S1 D n α)

instance ScontrasPearl2021.instIsFiniteKernelUttProdWorldScopeQUDL1 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) : ProbabilityTheory.IsFiniteKernel (L1 D n α μ ν)

noncomputable def ScontrasPearl2021.S2 (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) : ProbabilityTheory.Kernel (World n) Utt

The endorsing speaker of §3.1 is, at the observed world, the best response at unit rationality to the world marginal of the pragmatic listener.

Equations

• ScontrasPearl2021.S2 D n α μ ν = RSA.speaker 1 0 (⇑(ScontrasPearl2021.L1 D n α μ ν).fst) MeasureTheory.Measure.dirac

theorem ScontrasPearl2021.S2_numeral_eq_self (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) : S2 (numeral Degree.Comparison.eq n) n α μ ν = S2 Quantifier.NumberTree.all n α μ ν

With as many horses as the numeral counts, the numeral model on the exact reading is the every-not model (§4.2.1).

theorem ScontrasPearl2021.S2_numeral_ge_self (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) : S2 (numeral Degree.Comparison.ge n) n α μ ν = S2 Quantifier.NumberTree.all n α μ ν

With as many horses as the numeral counts, the numeral model on the at-least reading is the every-not model (§4.2.1).

Production shares

noncomputable def ScontrasPearl2021.cellMass (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (l : Scope × QUD) (u : Utt) (w : World n) : ℝ

The cell mass is the fraction of the extension of an utterance under a scope interpretation that lies in the cell of a world under a question, which is the literal listener's mass on the world's answer.

Equations

• ScontrasPearl2021.cellMass D n l u w = (((ScontrasPearl2021.L0 D n l.1).map (ScontrasPearl2021.project n l.2)) u).real {ScontrasPearl2021.project n l.2 w}

theorem ScontrasPearl2021.cellMass_eq (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (l : Scope × QUD) (u : Utt) (w : World n) : cellMass D n l u w = ↑(ext D n l.1 u ∩ cell n l.2 w).card / ↑(ext D n l.1 u).card

theorem ScontrasPearl2021.cellMass_nonneg (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (l : Scope × QUD) (u : Utt) (w : World n) : 0 ≤ cellMass D n l u w

theorem ScontrasPearl2021.cellMass_null_pos (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (l : Scope × QUD) (w : World n) : 0 < cellMass D n l Utt.null w

noncomputable def ScontrasPearl2021.share (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (l : Scope × QUD) (w : World n) : ℝ

The share is the probability that the speaker produces the test sentence at a world under a scope interpretation and a question.

Equations

• ScontrasPearl2021.share D n α l w = ((ScontrasPearl2021.S1 D n α) (w, l)).real {ScontrasPearl2021.Utt.amb}

theorem ScontrasPearl2021.share_eq (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (hα : 0 ≤ α) (l : Scope × QUD) (w : World n) : share D n α l w = cellMass D n l Utt.amb w ^ α / (cellMass D n l Utt.amb w ^ α + cellMass D n l Utt.null w ^ α)

theorem ScontrasPearl2021.share_nonneg (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (l : Scope × QUD) (w : World n) : 0 ≤ share D n α l w

theorem ScontrasPearl2021.share_le_one (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (l : Scope × QUD) (w : World n) : share D n α l w ≤ 1

theorem ScontrasPearl2021.share_lt_one (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (hα : 0 ≤ α) (l : Scope × QUD) (w : World n) : share D n α l w < 1

theorem ScontrasPearl2021.share_pos (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (hα : 0 ≤ α) {l : Scope × QUD} {w : World n} (h : w ∈ ext D n l.1 Utt.amb) : 0 < share D n α l w

The test sentence is produced at a world at which it is true.

theorem ScontrasPearl2021.S1_real_null (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (hα : 0 ≤ α) (l : Scope × QUD) (w : World n) : ((S1 D n α) (w, l)).real {Utt.null} = 1 - share D n α l w

The null utterance takes the rest of the speaker's mass.

def ScontrasPearl2021.cellCount (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (l : Scope × QUD) (u : Utt) (w : World n) : ℕ

The cell count is the number of worlds in the cell of w under the question of l at which u is true under the interpretation of l.

Equations

• ScontrasPearl2021.cellCount D n l u w = (ScontrasPearl2021.ext D n l.1 u ∩ ScontrasPearl2021.cell n l.2 w).card

theorem ScontrasPearl2021.share_le_share_iff (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (hα : 0 < α) {D' : Quantifier.NumberTree} [DecidableRel D'] {l l' : Scope × QUD} {w w' : World n} (hS : 0 < (ext D n l.1 Utt.amb).card) (hS' : 0 < (ext D' n l'.1 Utt.amb).card) : share D n α l w ≤ share D' n α l' w' ↔ cellCount D n l Utt.amb w * cellCount D' n l' Utt.null w' * (ext D' n l'.1 Utt.amb).card ≤ cellCount D' n l' Utt.amb w' * cellCount D n l Utt.null w * (ext D n l.1 Utt.amb).card

In comparing production probabilities across worlds, interpretations, questions and determiners, the rationality cancels, leaving a comparison of the odds of the test sentence against silence, each the fraction of the sentence's extension in the world's cell over the fraction of all worlds in it.

theorem ScontrasPearl2021.share_lt_share_iff (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (hα : 0 < α) {D' : Quantifier.NumberTree} [DecidableRel D'] {l l' : Scope × QUD} {w w' : World n} (hS : 0 < (ext D n l.1 Utt.amb).card) (hS' : 0 < (ext D' n l'.1 Utt.amb).card) : share D n α l w < share D' n α l' w' ↔ cellCount D n l Utt.amb w * cellCount D' n l' Utt.null w' * (ext D' n l'.1 Utt.amb).card < cellCount D' n l' Utt.amb w' * cellCount D n l Utt.null w * (ext D n l.1 Utt.amb).card

Endorsement

noncomputable def ScontrasPearl2021.production (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (ν : MeasureTheory.Measure (Scope × QUD)) (w : World n) : ℝ

The production at a world is the probability that the test sentence is produced there, the interpretation and the question drawn from ν.

Equations

• ScontrasPearl2021.production D n α ν w = ∑ l : ScontrasPearl2021.Scope × ScontrasPearl2021.QUD, ν.real {l} * ScontrasPearl2021.share D n α l w

noncomputable def ScontrasPearl2021.expectedProduction (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) : ℝ

The expected production is the prior probability that the test sentence is produced, the observation marginal of the speaker.

Equations

• ScontrasPearl2021.expectedProduction D n α μ ν = ((μ.prod ν).bind ⇑(ScontrasPearl2021.S1 D n α)).real {ScontrasPearl2021.Utt.amb}

theorem ScontrasPearl2021.production_nonneg (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (ν : MeasureTheory.Measure (Scope × QUD)) (w : World n) : 0 ≤ production D n α ν w

theorem ScontrasPearl2021.expectedProduction_eq_sum (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : expectedProduction D n α μ ν = ∑ w : World n, μ.real {w} * production D n α ν w

theorem ScontrasPearl2021.production_le_one (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure ν] (w : World n) : production D n α ν w ≤ 1

theorem ScontrasPearl2021.production_lt_one (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 ≤ α) (w : World n) : production D n α ν w < 1

theorem ScontrasPearl2021.production_pos (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 ≤ α) {w : World n} (h : ∀ (l : Scope × QUD), w ∈ ext D n l.1 Utt.amb) : 0 < production D n α ν w

The test sentence is produced with positive probability at a world at which it is true on both interpretations.

theorem ScontrasPearl2021.expectedProduction_lt_one (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 ≤ α) : expectedProduction D n α μ ν < 1

theorem ScontrasPearl2021.expectedProduction_pos (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 ≤ α) {w : World n} (hμ : μ {w} ≠ 0) (h : ∀ (l : Scope × QUD), w ∈ ext D n l.1 Utt.amb) : 0 < expectedProduction D n α μ ν

noncomputable def ScontrasPearl2021.endorse (m z : ℝ) : ℝ

endorse m z is the endorsement probability as a function of the production probability m at the observed world and its expectation z under the world prior.

Equations

• ScontrasPearl2021.endorse m z = m * (1 - z) / (m * (1 - z) + z * (1 - m))

theorem ScontrasPearl2021.endorse_denom_pos {m z : ℝ} (hm0 : 0 ≤ m) (hm1 : m ≤ 1) (hz0 : 0 < z) (hz1 : z < 1) : 0 < m * (1 - z) + z * (1 - m)

theorem ScontrasPearl2021.endorse_le_endorse {m m' z : ℝ} (hm0 : 0 ≤ m) (hm1 : m' ≤ 1) (hz0 : 0 < z) (hz1 : z < 1) (h : m ≤ m') : endorse m z ≤ endorse m' z

Endorsement rises with the production probability at the observed world.

theorem ScontrasPearl2021.endorse_antitone {m z z' : ℝ} (hm0 : 0 ≤ m) (hm1 : m ≤ 1) (hz0 : 0 < z) (hz1 : z' < 1) (h : z ≤ z') : endorse m z' ≤ endorse m z

Endorsement falls with the expected production probability.

theorem ScontrasPearl2021.one_half_lt_endorse_iff {m z : ℝ} (hm0 : 0 ≤ m) (hm1 : m ≤ 1) (hz0 : 0 < z) (hz1 : z < 1) : 1 / 2 < endorse m z ↔ z < m

The sentence is endorsed more often than not exactly when it is produced at the observed world more often than on average.

theorem ScontrasPearl2021.S2_real_amb (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 < α) {w : World n} (hμ : μ {w} ≠ 0) (hz0 : 0 < expectedProduction D n α μ ν) (hz1 : expectedProduction D n α μ ν < 1) : ((S2 D n α μ ν) w).real {Utt.amb} = endorse (production D n α ν w) (expectedProduction D n α μ ν)

The endorsement probability at a world of positive prior is the production probability at the world played against its expectation under the world prior (§3.1).

theorem ScontrasPearl2021.one_half_lt_S2_real_amb_iff (D : Quantifier.NumberTree) [DecidableRel D] (n : ℕ) (α : ℝ) (μ : MeasureTheory.Measure (World n)) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 < α) {w : World n} (hμ : μ {w} ≠ 0) (hz0 : 0 < expectedProduction D n α μ ν) (hz1 : expectedProduction D n α μ ν < 1) : 1 / 2 < ((S2 D n α μ ν) w).real {Utt.amb} ↔ expectedProduction D n α μ ν < production D n α ν w

The sentence is endorsed more often than not exactly when it is produced at the observed world more often than on average under the world prior (§5.1).

The every-not model (§3)

theorem ScontrasPearl2021.zero_mem_ext_every {n : ℕ} (hn : 0 < n) (i : Scope) : 0 ∈ ext Quantifier.NumberTree.all n i Utt.amb

The sentence every horse didn't jump is true at the no-success world on both interpretations.

theorem ScontrasPearl2021.ext_every_amb_card_pos {n : ℕ} (hn : 0 < n) (i : Scope) : 0 < (ext Quantifier.NumberTree.all n i Utt.amb).card

theorem ScontrasPearl2021.map_L0_every_all {n : ℕ} (hn : 0 < n) (i : Scope) (w : World n) : (((L0 Quantifier.NumberTree.all n i).map (project n QUD.all)) Utt.amb) {project n QUD.all w} = if w = Fin.last n then 0 else 1

Under the question all? the sentence every horse didn't jump fully resolves the question in the negative on either interpretation, as its literal listener is certain of the answer at every world short of total success.

theorem ScontrasPearl2021.S1_all_scope (α : ℝ) {n : ℕ} (hn : 0 < n) (w : World n) : (S1 Quantifier.NumberTree.all n α) (w, Scope.surface, QUD.all) = (S1 Quantifier.NumberTree.all n α) (w, Scope.inverse, QUD.all)

Under the question all? the two scope interpretations of every horse didn't jump produce alike at every world, since the sentence answers the question in the negative on either reading (§3.2, §5.1).

theorem ScontrasPearl2021.share_all_scope (α : ℝ) {n : ℕ} (hn : 0 < n) (w : World n) : share Quantifier.NumberTree.all n α (Scope.surface, QUD.all) w = share Quantifier.NumberTree.all n α (Scope.inverse, QUD.all) w

theorem ScontrasPearl2021.production_all (α : ℝ) {n : ℕ} (ρ : MeasureTheory.Measure Scope) [MeasureTheory.IsProbabilityMeasure ρ] (hn : 0 < n) (w : World n) : production Quantifier.NumberTree.all n α (ρ.prod (MeasureTheory.Measure.dirac QUD.all)) w = share Quantifier.NumberTree.all n α (Scope.surface, QUD.all) w

With the question settled as all?, the production of the sentence at a world does not depend on the scope prior.

theorem ScontrasPearl2021.expectedProduction_all (α : ℝ) {n : ℕ} (ρ : MeasureTheory.Measure Scope) [MeasureTheory.IsProbabilityMeasure ρ] (hn : 0 < n) (μ : MeasureTheory.Measure (World n)) [MeasureTheory.IsProbabilityMeasure μ] : expectedProduction Quantifier.NumberTree.all n α μ (ρ.prod (MeasureTheory.Measure.dirac QUD.all)) = ∑ w : World n, μ.real {w} * share Quantifier.NumberTree.all n α (Scope.surface, QUD.all) w

theorem ScontrasPearl2021.S2_real_amb_all (α : ℝ) {n : ℕ} (ρ : MeasureTheory.Measure Scope) [MeasureTheory.IsProbabilityMeasure ρ] (hα : 0 < α) (hn : 0 < n) (μ : MeasureTheory.Measure (World n)) [MeasureTheory.IsProbabilityMeasure μ] (ρ' : MeasureTheory.Measure Scope) [MeasureTheory.IsProbabilityMeasure ρ'] {w : World n} (hμ : μ {w} ≠ 0) (hz0 : 0 < expectedProduction Quantifier.NumberTree.all n α μ (ρ.prod (MeasureTheory.Measure.dirac QUD.all))) (hz1 : expectedProduction Quantifier.NumberTree.all n α μ (ρ.prod (MeasureTheory.Measure.dirac QUD.all)) < 1) : ((S2 Quantifier.NumberTree.all n α μ (ρ.prod (MeasureTheory.Measure.dirac QUD.all))) w).real {Utt.amb} = ((S2 Quantifier.NumberTree.all n α μ (ρ'.prod (MeasureTheory.Measure.dirac QUD.all))) w).real {Utt.amb}

With the question settled as all?, endorsement does not depend on the scope prior, which matters only through questions the two interpretations answer differently (§3.2, Figure 3).

Two horses (§3.2)

theorem ScontrasPearl2021.share_le_share_all (α : ℝ) (hα : 0 < α) (i : Scope) (q : QUD) : share Quantifier.NumberTree.all 2 α (i, q) 1 ≤ share Quantifier.NumberTree.all 2 α (i, QUD.all) 1

At the not-all world of the two-horse scenario, the question all? maximizes the production of the sentence under either interpretation, since the sentence answers it fully on either reading (§3.2, Figure 2).

theorem ScontrasPearl2021.share_none_le_share (α : ℝ) (hα : 0 < α) (i : Scope) (q : QUD) : share Quantifier.NumberTree.all 2 α (i, QUD.none) 1 ≤ share Quantifier.NumberTree.all 2 α (i, q) 1

At the not-all world, the question none? minimizes the production of the sentence under either interpretation (§3.2, Figure 2).

theorem ScontrasPearl2021.share_howMany_lt_share_all (α : ℝ) (hα : 0 < α) : share Quantifier.NumberTree.all 2 α (Scope.surface, QUD.howMany) 1 < share Quantifier.NumberTree.all 2 α (Scope.surface, QUD.all) 1

On the surface interpretation the sentence is false at the not-all world, so how many? has it produced less often than all?, under which it is nonetheless a full answer.

theorem ScontrasPearl2021.share_none_lt_share_howMany (α : ℝ) (hα : 0 < α) : share Quantifier.NumberTree.all 2 α (Scope.inverse, QUD.none) 1 < share Quantifier.NumberTree.all 2 α (Scope.inverse, QUD.howMany) 1

On the inverse interpretation, none? has the sentence produced less often than how many?, since the sentence, not all jumped, leaves none? open.

theorem ScontrasPearl2021.share_antitone (α : ℝ) (hα : 0 < α) (l : Scope × QUD) : Antitone (share Quantifier.NumberTree.all 2 α l)

Production of the sentence falls with the number of jumpers, under every interpretation and question.

theorem ScontrasPearl2021.production_antitone (α : ℝ) (hα : 0 < α) (ν : MeasureTheory.Measure (Scope × QUD)) : Antitone (production Quantifier.NumberTree.all 2 α ν)

theorem ScontrasPearl2021.S2_real_amb_mono_baseRate (α : ℝ) (ν : MeasureTheory.Measure (Scope × QUD)) [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 < α) {p p' : ↑unitInterval} (hp : 0 < ↑p) (hpp' : ↑p ≤ ↑p') (hp' : ↑p' < 1) (w : World 2) : ((S2 Quantifier.NumberTree.all 2 α (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial 2 p)) ν) w).real {Utt.amb} ≤ ((S2 Quantifier.NumberTree.all 2 α (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial 2 p')) ν) w).real {Utt.amb}

Raising the success base rate of the binomial world prior raises endorsement at every world (§3.2, Figure 2), since the more success is expected, the more the sentence rules out on either reading.

The two-not model (§4)

theorem ScontrasPearl2021.share_twoAtLeast_le_share_twoExact (α : ℝ) (hα : 0 < α) (q : QUD) : share twoAtLeast 4 α (Scope.surface, q) 2 ≤ share twoExact 4 α (Scope.surface, q) 2

With four horses and two jumpers, the surface interpretation of the sentence is produced at least as often on the exact reading of the numeral as on the at-least reading, whatever the question, since the exact reading makes the sentence true at that world alone (§4.2.2, Figure 7).

theorem ScontrasPearl2021.share_twoAtLeast_lt_share_twoExact (α : ℝ) (hα : 0 < α) {q : QUD} (hq : q ≠ QUD.all) : share twoAtLeast 4 α (Scope.surface, q) 2 < share twoExact 4 α (Scope.surface, q) 2

The advantage of the exact reading is strict under every question but all?, which the surface interpretation answers fully on either reading.

theorem ScontrasPearl2021.share_twoExact_lt_share_twoAtLeast (α : ℝ) (hα : 0 < α) : share twoExact 4 α (Scope.inverse, QUD.all) 2 < share twoAtLeast 4 α (Scope.inverse, QUD.all) 2

Under the inverse interpretation and the question all? the at-least reading is produced more often at that world. Not exactly two jumped is compatible with all four having jumped and so leaves all? open, while not at least two jumped settles it. This is why the paper's 2-of-4 fit needs a low prior on inverse scope (§4.2.2, Figure 7).