Coppock and Brochhagen (2013): Raising and resolving issues with scalar modifiers

Coppock and Brochhagen analyse at least and at most as quantifying over a scale of answers to the question under discussion: at least p is what only p presupposes, that some true answer is at least as strong as p, and at most p is what only p asserts, that no true answer is stronger. These are Focus.Particles.atLeast and Focus.Particles.atMost, modifiers of propositions. On the question of how many, with answers ranked by number, they give the truth conditions of the modified numerals whether the bare numeral is read two-sidedly or one-sidedly, and on a scale of mutually exclusive answers, such as academic ranks, at least widens its prejacent.

To explain why superlative modifiers carry ignorance implicatures and no scalar implicatures, the authors move to unrestricted inquisitive semantics, where at least p raises every answer at least as strong as p as a possibility. A speaker who knows the answer cannot sincerely raise several possibilities, while the comparative more than raises one, and exhaustifying the raised possibilities does not exclude the stronger answers.

Main statements

• atLeast_fragment, atMost_fragment: on the question of how many, at least and at most are the Fragment's readings of the modified numerals, pulled back along the count.
• sUnion_atLeastInq, sUnion_atMostInq: the inquisitive entries keep the truth conditions.
• restrict_atLeastInq_eq_singleton: a speaker who knows the answer cannot raise the possibilities of at least, the ignorance implicature.

Implementation notes

• A state is a relation on propositions, and the question of a measure μ has the answers μ ⁻¹' {i} (two-sided) or μ ⁻¹' Ici i (one-sided), ranked by i; the paper's assumption of one world for each number is surjectivity of μ.
• The choice-function entries (53), (54) and (60) are modelled by the sets of possibilities they denote, which is what applying them pointwise yields (range_choice_apply).
• The informational content of inquisitive at most is max within the common ground of the state, the union of its answers.

TODO

The interaction with modals is not formalized: the authoritative and speaker-insecurity readings of at least under deontic modals (§3.5) and the missing readings of at most under may, which the paper derives with Hackl's -many (§3.6).

References

• E. Coppock and T. Brochhagen, Raising and resolving issues with scalar modifiers (2013)
• E. Coppock and D. Beaver, Principles of the exclusive muddle (2014)
• I. Ciardelli, J. Groenendijk and F. Roelofsen, Attention! 'Might' in Inquisitive Semantics (2009)

Truth conditions (§2.6)

@[reducible, inline]

abbrev CoppockBrochhagen2013.ranking {W : Type u_1} {α : Type u_2} [Preorder α] (P : α → Set W) : Set W → Set W → Prop

The ranking of the answers of an indexed question by their index.

Equations

• CoppockBrochhagen2013.ranking P = Relation.Map (fun (x1 x2 : α) => x1 ≥ x2) P P

theorem CoppockBrochhagen2013.atLeast_map {W : Type u_1} {α : Type u_2} [Preorder α] {P : α → Set W} (hP : Function.Injective P) (a : α) : Focus.Particles.atLeast (ranking P) (Set.range P) (P a) = ⋃ i ∈ Set.Ici a, P i

At least the answer for a is the union of the answers from a up (30).

theorem CoppockBrochhagen2013.atMost_map {W : Type u_1} {α : Type u_2} [Preorder α] {P : α → Set W} (hP : Function.Injective P) (a : α) : Focus.Particles.atMost (ranking P) (Set.range P) (P a) = (⋃ i ∈ (Set.Iic a)ᶜ, P i)ᶜ

At most the answer for a excludes every answer not below a (31).

@[reducible, inline]

abbrev CoppockBrochhagen2013.twoSided {W : Type u_1} {α : Type u_2} (μ : W → α) (i : α) : Set W

The two-sided answers to the question of how many, by the measure μ.

Equations

• CoppockBrochhagen2013.twoSided μ i = μ ⁻¹' {i}

@[reducible, inline]

abbrev CoppockBrochhagen2013.oneSided {W : Type u_1} {α : Type u_2} [LinearOrder α] (μ : W → α) (i : α) : Set W

The one-sided answers to the question of how many, by the measure μ.

Equations

• CoppockBrochhagen2013.oneSided μ i = μ ⁻¹' Set.Ici i

theorem CoppockBrochhagen2013.twoSided_injective {W : Type u_1} {α : Type u_2} {μ : W → α} (hμ : Function.Surjective μ) : Function.Injective (twoSided μ)

theorem CoppockBrochhagen2013.oneSided_injective {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) : Function.Injective (oneSided μ)

theorem CoppockBrochhagen2013.atLeast_twoSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) (a : α) : Focus.Particles.atLeast (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ a) = μ ⁻¹' Set.Ici a

theorem CoppockBrochhagen2013.atLeast_oneSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) (a : α) : Focus.Particles.atLeast (ranking (oneSided μ)) (Set.range (oneSided μ)) (oneSided μ a) = μ ⁻¹' Set.Ici a

theorem CoppockBrochhagen2013.atMost_twoSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) (a : α) : Focus.Particles.atMost (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ a) = μ ⁻¹' Set.Iic a

theorem CoppockBrochhagen2013.atMost_oneSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) (a : α) : Focus.Particles.atMost (ranking (oneSided μ)) (Set.range (oneSided μ)) (oneSided μ a) = μ ⁻¹' Set.Iic a

theorem CoppockBrochhagen2013.atMost_twoSided_mono {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) {a b : α} (hab : a ≤ b) : Focus.Particles.atMost (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ a) ⊆ Focus.Particles.atMost (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ b)

At most weakens as the number grows, so at most two entails at most three (32).

theorem CoppockBrochhagen2013.twoSided_ssubset_atLeast {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) {a b : α} (hab : a < b) : twoSided μ a ⊂ Focus.Particles.atLeast (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ a)

On mutually exclusive answers at least widens its prejacent, as at least an assistant professor is true of a full professor (59).

theorem CoppockBrochhagen2013.atLeast_oneSided_eq {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) (a : α) : Focus.Particles.atLeast (ranking (oneSided μ)) (Set.range (oneSided μ)) (oneSided μ a) = oneSided μ a

On answers ranked by entailment at least leaves its prejacent as it is.

theorem CoppockBrochhagen2013.atLeast_fragment {W : Type u_1} {μ : W → ℕ} (hμ : Function.Surjective μ) (n : ℕ) (m : Modifier (Set ℕ)) : m ∈ Semantics.Denotes.denote English.NumeralModifiers.atLeast → Focus.Particles.atLeast (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ n) = μ ⁻¹' m {n}

On the question of how many, at least is the Fragment's reading of the numeral it modifies, pulled back along the count.

theorem CoppockBrochhagen2013.atMost_fragment {W : Type u_1} {μ : W → ℕ} (hμ : Function.Surjective μ) (n : ℕ) (m : Modifier (Set ℕ)) : m ∈ Semantics.Denotes.denote English.NumeralModifiers.atMost → Focus.Particles.atMost (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ n) = μ ⁻¹' m {n}

On the question of how many, at most is the Fragment's reading of the numeral it modifies, pulled back along the count.

The inquisitive entries (§3.3)

def CoppockBrochhagen2013.atLeastInq {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : Set (Set W)

At least p raises every answer at least as strong as p (52).

Equations

• CoppockBrochhagen2013.atLeastInq S C p = {q : Set W | q ∈ C ∧ S q p}

def CoppockBrochhagen2013.atMostInq {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : Set (Set W)

At most p raises every answer at most as strong as p, cut down to the worlds where no stronger answer is true (60).

Equations

• CoppockBrochhagen2013.atMostInq S C p = (fun (x : Set W) => x ∩ Focus.Particles.atMost S C p) '' {q : Set W | q ∈ C ∧ S p q}

theorem CoppockBrochhagen2013.sUnion_atLeastInq {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : ⋃₀ atLeastInq S C p = Focus.Particles.atLeast S C p

The informational content of inquisitive at least is min (§3.7).

theorem CoppockBrochhagen2013.sUnion_atMostInq {W : Type u_1} (S : Set W → Set W → Prop) (C : Set (Set W)) (p : Set W) : ⋃₀ atMostInq S C p = Focus.Particles.atMost S C p ∩ ⋃₀ C

The informational content of inquisitive at most is max, within the common ground (§3.7).

theorem CoppockBrochhagen2013.range_choice_apply {W : Type u_1} {T : Set (Set W)} (hT : T.Nonempty) : (Set.range fun (f : { f : Set (Set W) → Set W // ∀ (U : Set (Set W)), U.Nonempty → f U ∈ U }) => ↑f T) = T

Applying the choice-function entry (53) pointwise to a nonempty set of answers returns that set: every member is the value of some choice function.

theorem CoppockBrochhagen2013.isAttentive_atLeastInq_oneSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) {a b : α} (hab : a < b) : Inquisitive.Unrestricted.IsAttentive (atLeastInq (ranking (oneSided μ)) (Set.range (oneSided μ)) (oneSided μ a))

On nested answers at least is attentive, raising a stronger answer inside its prejacent (58).

theorem CoppockBrochhagen2013.isInquisitive_atLeastInq_twoSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) {a b : α} (hab : a < b) : Inquisitive.Unrestricted.IsInquisitive (atLeastInq (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ a))

On mutually exclusive answers at least is inquisitive, raising two maximal possibilities (59b).

theorem CoppockBrochhagen2013.atMostInq_oneSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) (a : α) : atMostInq (ranking (oneSided μ)) (Set.range (oneSided μ)) (oneSided μ a) = (fun (i : α) => μ ⁻¹' Set.Icc i a) '' Set.Iic a

On one-sided answers at most a raises the preimage of [i, a] for each i ≤ a (64).

theorem CoppockBrochhagen2013.atMostInq_twoSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} (hμ : Function.Surjective μ) (a : α) : atMostInq (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ a) = twoSided μ '' Set.Iic a

On two-sided answers at most a raises each answer up to a unchanged (63).

theorem CoppockBrochhagen2013.atMostInq_oneSided_id (a : ℕ) : atMostInq (ranking (oneSided id)) (Set.range (oneSided id)) (oneSided id a) = (fun (x : ℕ) => Set.Icc x a) '' Set.Iic a

On counts at most a raises [i, a] for each i ≤ a (64).

Ignorance (§3.4.1)

def CoppockBrochhagen2013.InteractiveSincerity {W : Type u_1} (P : Set (Set W)) (k : Set W) : Prop

The Maxim of Interactive Sincerity (68) requires a proposition that raises several possibilities to raise several within the speaker's information set k.

Equations

• CoppockBrochhagen2013.InteractiveSincerity P k = (P.Nontrivial → (Inquisitive.Unrestricted.restrict P k).Nontrivial)

theorem CoppockBrochhagen2013.restrict_atLeastInq_eq_singleton {W : Type u_1} {α : Type u_2} [Preorder α] {P : α → Set W} (hP : Function.Injective P) {a b : α} (hab : a ≤ b) {k : Set W} (hk : k ≠ ∅) (hkb : k ⊆ P b) (hsplit : ∀ (i : α), a ≤ i → k ∩ P i = k ∨ k ∩ P i = ∅) : Inquisitive.Unrestricted.restrict (atLeastInq (ranking P) (Set.range P) (P a)) k = {k}

A speaker whose information set lies in one answer P b at or above a, and meets each answer from a up wholly or not at all, restricts at least a to a single possibility (71).

theorem CoppockBrochhagen2013.split_twoSided {W : Type u_1} {α : Type u_2} {μ : W → α} {b : α} {k : Set W} (hkb : k ⊆ μ ⁻¹' {b}) (i : α) : k ∩ μ ⁻¹' {i} = k ∨ k ∩ μ ⁻¹' {i} = ∅

An information set inside one two-sided answer meets each two-sided answer wholly or not at all.

theorem CoppockBrochhagen2013.split_oneSided {W : Type u_1} {α : Type u_2} [LinearOrder α] {μ : W → α} {b : α} {k : Set W} (hkb : k ⊆ μ ⁻¹' {b}) (i : α) : k ∩ μ ⁻¹' Set.Ici i = k ∨ k ∩ μ ⁻¹' Set.Ici i = ∅

An information set inside one two-sided answer meets each one-sided answer wholly or not at all.

theorem CoppockBrochhagen2013.not_interactiveSincerity_hexagon {W : Type u_1} {μ : W → ℕ} (hμ : Function.Surjective μ) {k : Set W} (hk : k ≠ ∅) (hk6 : k ⊆ μ ⁻¹' {6}) : ¬InteractiveSincerity (atLeastInq (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ 5)) k ∧ ¬InteractiveSincerity (atLeastInq (ranking (oneSided μ)) (Set.range (oneSided μ)) (oneSided μ 5)) k

A speaker who knows that hexagons have six sides violates Interactive Sincerity with at least five, on either analysis of the bare numeral, since the sentence raises several possibilities (70a).

theorem CoppockBrochhagen2013.moreThan_interactiveSincerity {W : Type u_1} {μ : W → ℕ} (hμ : Function.Surjective μ) (k : Set W) : InteractiveSincerity {μ ⁻¹' Set.Ioi 4} k ∧ ⋃₀ {μ ⁻¹' Set.Ioi 4} = ⋃₀ atLeastInq (ranking (twoSided μ)) (Set.range (twoSided μ)) (twoSided μ 5)

The comparative raises its one possibility, so it never violates Interactive Sincerity, and on counts more than four has the content of at least five (72), (73).

Exhaustivity (§3.4.2)

@[reducible, inline]

abbrev CoppockBrochhagen2013.World : Type

The worlds of the four-world model of Figure 3, by whether Ann and whether Bill snores.

Equations

• CoppockBrochhagen2013.World = (Bool × Bool)

def CoppockBrochhagen2013.ann : Set World

Ann snores, Bill snores, and the question who snores.

Equations

• CoppockBrochhagen2013.ann = {w : CoppockBrochhagen2013.World | w.1 = true}

def CoppockBrochhagen2013.bill : Set World

Equations

• CoppockBrochhagen2013.bill = {w : CoppockBrochhagen2013.World | w.2 = true}

def CoppockBrochhagen2013.whoSnores : Set (Set World)

Equations

• CoppockBrochhagen2013.whoSnores = {CoppockBrochhagen2013.ann, CoppockBrochhagen2013.bill, CoppockBrochhagen2013.ann ∩ CoppockBrochhagen2013.bill}

theorem CoppockBrochhagen2013.exh_contrast : ⋃₀ Inquisitive.Unrestricted.exh {ann} whoSnores ⊆ billᶜ ∧ (true, true) ∈ ⋃₀ Inquisitive.Unrestricted.exh (atLeastInq (fun (x1 x2 : Set World) => x1 ⊆ x2) whoSnores ann) whoSnores

Exhaustifying Ann snores excludes that Bill snores, and exhaustifying at least Ann snores, on the entailment scale, does not (Figure 4).