Denić (2023): Probabilities and logic in implicature computation

This file formalizes the two puzzles with embedded disjunction of [Den23] and their resolution. All 20 of Mary's friends are French or Spanish preferably triggers the distributive inferences that at least one is French and at least one is Spanish, while Both of Mary's friends are French or Spanish preferably triggers ignorance about them, (6) and (7), and fewer disjuncts likewise favour the distributive reading, (8) and (9). Under the exhaustification of [Fox07], the distributive reading arises when only the disjunction activates its alternatives, ALT-or, all of which are innocently excludable, and the ignorance reading when the quantifier does too, ALT-all-or, none of whose alternatives is, (26); since the alternatives stand in the same entailment relations for any domain size, §3.2, no theory on which implicatures are a function of entailment can distinguish the two sentences, and the pruning constraints of [FK11] do not either, §3.3. The proposal, (30), is that an alternative is pruned the more likely it is given the utterance: with each individual one of the m properties at random, the probability that some of n individuals is A given that all are one of the m is 1 − ((m − 1)/m)^n, increasing in n and decreasing in m, and larger than that of the universal alternative once n > 1, the assumptions of §4; a threshold on it prunes the existential alternatives of (6) and (8) but not of (7) and (9). The deviance puzzle, §5, is that #Each of those three girls is Mary, Susan, or Jane is degraded where is called is not: the identity predicate is singleton-denoting, so given common knowledge the three names are borne by the three girls one each, every existential alternative is settled, and the ignorance inferences the sentence triggers contradict common knowledge, (40), the blindness of [Mag09] extended from scalar to ignorance inferences. Informativeness must then be computed blindly too, §7.3: given common knowledge the existential alternatives of the deviant sentence are certain and would be pruned, whereas blind to it their probability lies below every threshold that resolves the inference puzzle.

Implementation notes

Worlds assign each of the n individuals exactly one of the m properties, the uniform prior of §4's assumptions; the prejacent all are one of them is then every world, and the conjunctive alternatives of the chapter's footnote 8, which it sets aside, are unsatisfiable. The exhaustification results are the substrate's innocent exclusion over sets of worlds, stated for every n ≥ 2 and m ≥ 2, the distributive reading itself for two disjuncts. Probabilities are the uniform measure uniformOn on reals. The mapping from conditional probability to pruning, which the chapter leaves open between a linear and a threshold form, is taken as a threshold. Ignorance inferences are the pragmatic ones of §3.1, about every alternative the exhaustified utterance leaves open, so the grammatical parse of §7.1 is not modelled. The modified-numeral cases of [BH19], (43), and the symmetry, modal and downward-entailing challenges of §8 are recorded in the data only.

References

• [Den23]
• [Fox07]
• [FK11]
• [Mag09]
• [BH19]

@[reducible, inline]

abbrev Denic2023.World (n m : ℕ) : Type

In the worlds for all of n are A₁ or … or Aₘ each individual has exactly one of the m properties.

Equations

• Denic2023.World n m = (Fin n → Fin m)

def Denic2023.allAre {n m : ℕ} (i : Fin m) : Set (World n m)

All n are Aᵢ, the universal alternative.

Equations

• Denic2023.allAre i = {w : Denic2023.World n m | ∀ (x : Fin n), w x = i}

def Denic2023.someAre {n m : ℕ} (i : Fin m) : Set (World n m)

Some of the n are Aᵢ, the existential alternative.

Equations

• Denic2023.someAre i = {w : Denic2023.World n m | ∃ (x : Fin n), w x = i}

def Denic2023.altOr (n m : ℕ) : Set (Set (World n m))

Under ALT-or only the disjunction activates its alternatives, (24) and (25).

Equations

• Denic2023.altOr n m = Set.range Denic2023.allAre

def Denic2023.altAllOr (n m : ℕ) : Set (Set (World n m))

Under ALT-all-or the quantifier activates its alternatives too, (22) and (23).

Equations

• Denic2023.altAllOr n m = Set.range Denic2023.allAre ∪ Set.range Denic2023.someAre

theorem Denic2023.altAllOr_finite {n m : ℕ} : (altAllOr n m).Finite

def Denic2023.LeavesOpen {n m : ℕ} (ALT : Set (Set (World n m))) (a : Set (World n m)) : Prop

The exhaustified utterance leaves an alternative open, entailing neither it nor its negation, so that the maxim of quantity, (19), yields ignorance about it, §3.1.

Equations

• Denic2023.LeavesOpen ALT a = ((Exhaustification.exhIE ALT Set.univ ∩ a).Nonempty ∧ (Exhaustification.exhIE ALT Set.univ ∩ aᶜ).Nonempty)

Entailment cannot tell the sentences apart, §3.2

theorem Denic2023.isInnocentlyExcludable_altOr {n m : ℕ} (hn : 2 ≤ n) (hm : 2 ≤ m) (i : Fin m) : Exhaustification.IsInnocentlyExcludable (altOr n m) Set.univ (allAre i)

With ALT-or every alternative is innocently excludable, for any domain of at least two, since a world with two individuals of different properties falsifies them all.

theorem Denic2023.exhIE_altOr {n : ℕ} (hn : 2 ≤ n) : Exhaustification.exhIE (altOr n 2) Set.univ = someAre 0 ∩ someAre 1

Exhaustifying with ALT-or over two disjuncts gives the distributive reading (6a), that some are French and some are Spanish.

theorem Denic2023.exhIE_altOr_subset_someAre {n : ℕ} (hn : 2 ≤ n) (i : Fin 2) : Exhaustification.exhIE (altOr n 2) Set.univ ⊆ someAre i

With ALT-or the existential alternatives are entailed, so no ignorance arises about them, (6b).

theorem Denic2023.const_mem_exhMW {n m : ℕ} (hn : 1 ≤ n) (i : Fin m) : (fun (x : Fin n) => i) ∈ Exhaustification.exhMW (altAllOr n m) Set.univ

With ALT-all-or, the world where everyone is i is minimal, since any world verifying fewer alternatives would have to falsify all are i and some are i while verifying no other alternative, and there is no such world.

theorem Denic2023.split_mem_exhMW {n m : ℕ} (hn : 2 ≤ n) {i k : Fin m} (hik : i ≠ k) : (fun (x : Fin n) => if ↑x = 0 then i else k) ∈ Exhaustification.exhMW (altAllOr n m) Set.univ

With ALT-all-or, the world where one individual is i and the rest are k is minimal.

theorem Denic2023.not_isInnocentlyExcludable_altAllOr {n m : ℕ} (hn : 2 ≤ n) (hm : 2 ≤ m) (a : Set (World n m)) : a ∈ altAllOr n m → ¬Exhaustification.IsInnocentlyExcludable (altAllOr n m) Set.univ a

With ALT-all-or no alternative is innocently excludable (26), for any domain of at least two, each universal alternative holding at a minimal constant world and each existential one at a minimal two-property world.

theorem Denic2023.exhIE_altAllOr {n m : ℕ} (hn : 2 ≤ n) (hm : 2 ≤ m) : Exhaustification.exhIE (altAllOr n m) Set.univ = Set.univ

With ALT-all-or exhaustification is vacuous.

theorem Denic2023.leavesOpen_altAllOr {n m : ℕ} (hn : 2 ≤ n) (hm : 2 ≤ m) (a : Set (World n m)) : a ∈ altAllOr n m → LeavesOpen (altAllOr n m) a

With ALT-all-or every alternative is left open, giving ignorance about all of them (7b).

Probabilistic informativeness, §4

theorem Denic2023.ncard_someAre_compl {n m : ℕ} (i : Fin m) : (someAre i)ᶜ.ncard = (m - 1) ^ n

theorem Denic2023.ncard_someAre {n m : ℕ} (i : Fin m) : (someAre i).ncard = m ^ n - (m - 1) ^ n

theorem Denic2023.ncard_allAre {n m : ℕ} (i : Fin m) : (allAre i).ncard = 1

theorem Denic2023.uniformOn_real_someAre {n m : ℕ} (hm : 1 ≤ m) (i : Fin m) : (ProbabilityTheory.uniformOn Set.univ).real (someAre i) = 1 - ((↑m - 1) / ↑m) ^ n

Under the uniform prior of §4, the probability that some of the n individuals is Aᵢ given that all are one of the m is 1 − ((m − 1)/m)^n.

theorem Denic2023.uniformOn_real_allAre {n m : ℕ} (i : Fin m) : (ProbabilityTheory.uniformOn Set.univ).real (allAre i) = (1 / ↑m) ^ n

The probability that all n individuals are Aᵢ is (1/m)^n.

theorem Denic2023.uniformOn_real_someAre_lt {n m : ℕ} (hm : 2 ≤ m) {n' : ℕ} (h : n < n') (i : Fin m) : (ProbabilityTheory.uniformOn Set.univ).real (someAre i) < (ProbabilityTheory.uniformOn Set.univ).real (someAre i)

The more individuals, the likelier that some of them is Aᵢ, §4's assumption (i).

theorem Denic2023.uniformOn_real_allAre_lt_someAre {n m : ℕ} (hn : 2 ≤ n) (hm : 2 ≤ m) (i : Fin m) : (ProbabilityTheory.uniformOn Set.univ).real (allAre i) < (ProbabilityTheory.uniformOn Set.univ).real (someAre i)

With more than one individual, that some of them is Aᵢ is likelier than that all are, §4's assumption (ii).

theorem Denic2023.uniformOn_real_someAre_anti {n m : ℕ} (hn : 1 ≤ n) (hm : 2 ≤ m) {m' : ℕ} (h : m < m') (i : Fin m) (i' : Fin m') : (ProbabilityTheory.uniformOn Set.univ).real (someAre i') < (ProbabilityTheory.uniformOn Set.univ).real (someAre i)

The more disjuncts, the less likely that some individual is A₁, §4's assumption (iii).

def Denic2023.Pruned (θ p : ℝ) : Prop

In the threshold form of (30), an alternative is pruned when its probability given the utterance reaches the threshold.

Equations

• Denic2023.Pruned θ p = (θ ≤ p)

theorem Denic2023.threshold_separates : ∃ (θ : ℝ), Pruned θ ((ProbabilityTheory.uniformOn Set.univ).real (someAre 0)) ∧ Pruned θ ((ProbabilityTheory.uniformOn Set.univ).real (someAre 0)) ∧ ¬Pruned θ ((ProbabilityTheory.uniformOn Set.univ).real (someAre 0)) ∧ ¬Pruned θ ((ProbabilityTheory.uniformOn Set.univ).real (someAre 0))

One threshold resolves the inference puzzle. The existential alternatives of all-20-or, (6), and simple-disj, (8), are pruned, leaving ALT-or and the distributive reading, and those of all-2-or, (7), and complex-disj, (9), are kept, leaving ALT-all-or and ignorance.

The deviance puzzle, §5 to §7

def Denic2023.distinct (n : ℕ) : Set (World n n)

In the common-knowledge worlds for each of the n girls is one of the n names under the identity copula, the names are borne by different girls.

Equations

• Denic2023.distinct n = {w : Denic2023.World n n | Function.Injective w}

def Denic2023.SingletonDenoting {n m : ℕ} (CK : Set (World n m)) (P : World n m → Fin n → Prop) : Prop

A predicate of individuals is singleton-denoting given common knowledge CK (§5) when at every common-knowledge world it holds of at most one individual.

Equations

• Denic2023.SingletonDenoting CK P = ∀ w ∈ CK, ∀ (x y : Fin n), P w x → P w y → x = y

theorem Denic2023.singletonDenoting_distinct {n : ℕ} (i : Fin n) : SingletonDenoting (distinct n) fun (w : World n n) (x : Fin n) => w x = i

Is Mary is singleton-denoting given that the names are borne by different girls, (37a).

theorem Denic2023.not_singletonDenoting_univ {n m : ℕ} (hn : 2 ≤ n) (i : Fin m) : ¬SingletonDenoting Set.univ fun (w : World n m) (x : Fin n) => w x = i

Is called Mary is not singleton-denoting, since two girls may bear the name (37b).

theorem Denic2023.distinct_subset_someAre {n : ℕ} (i : Fin n) : distinct n ⊆ someAre i

Given common knowledge and the utterance, every name is borne by some girl, since an injection of the n girls into the n names is a surjection.

def Denic2023.Settled {n m : ℕ} (CK a : Set (World n m)) : Prop

Common knowledge settles an alternative when it holds or fails at every world compatible with it.

Equations

• Denic2023.Settled CK a = (CK ⊆ a ∨ CK ⊆ aᶜ)

theorem Denic2023.deviant_be {n : ℕ} (hn : 2 ≤ n) (i : Fin n) : LeavesOpen (altAllOr n n) (someAre i) ∧ Settled (distinct n) (someAre i)

Deviant-be (31) is deviant (40) because exhaustification with ALT-all-or leaves every existential alternative open, so ignorance about it is inferred, while common knowledge settles it.

theorem Denic2023.non_deviant_called {n m : ℕ} (hn : 2 ≤ n) (hm : 2 ≤ m) (i : Fin m) : LeavesOpen (altAllOr n m) (someAre i) ∧ ¬Settled Set.univ (someAre i)

For non-deviant-called (32) the same ignorance is inferred, but common knowledge settles nothing, since the girls may all be called Mary or none may be.

theorem Denic2023.uniformOn_distinct_real_someAre {n : ℕ} (i : Fin n) : (ProbabilityTheory.uniformOn (distinct n)).real (someAre i) = 1

Relative to common knowledge the existential alternatives of deviant-be are certain.

theorem Denic2023.blind_informativeness (θ : ℝ) (h : 3 / 4 < θ) (h1 : θ ≤ 1) : ¬Pruned θ ((ProbabilityTheory.uniformOn Set.univ).real (someAre 0)) ∧ Pruned θ ((ProbabilityTheory.uniformOn (distinct 3)).real (someAre 0))

Informativeness must be computed blindly to common knowledge (§7.3). Relative to it the existential alternatives of deviant-be are certain and any threshold prunes them, which would leave no ignorance inference and predict no deviance; blind to it their probability is 1 − (2/3)^3, below every threshold that keeps the alternatives of all-2-or, so they survive.