Franke (2011): Quantity Implicatures, Exhaustive Interpretation, and Rational Conversation

An interpretation game has as states the distinctions that the alternatives to a sentence can draw and as messages the alternatives themselves, and its receiver tries to guess the state. Franke explains quantity implicatures by iterated best response in such a game: a level-0 receiver reads a message as its denotation, a level-0 sender says something true, and a level-k + 1 player best-responds to the belief that every level-k strategy is equally likely. With flat priors this reduces to counting, since a sender picks the true messages with fewest readings, a receiver the states that send fewest messages, and a message no state sends is read literally. The probabilistic model behind the count agrees with it under flat priors and refines it by the prior under nearly flat ones; every chain of reasoning reaches a fixed point, and the fixed points are perfect Bayesian equilibria.

Main statements

• SomeAll.isNashEquilibrium_scalar_and_reversed, SomeAll.scalar_implicature: the implicature of "some" and its reversal are both equilibria, and iterated best response selects the implicature.
• TwoDisjuncts.free_choice: free choice, simplification of disjunctive antecedents and a conjunctive reading of plain disjunction are one prediction.
• SomeAllEpistemic.strong, DisjunctionEpistemic.ignorance, DisjunctionConjEpistemic.exclusivity_of_competencePrior: epistemic implicatures under each assumption about the speaker's competence.
• receiverLevel_eq_receiverChain, receiverLevel_eq_receiverChainBy: the probabilistic model is the count under flat priors and the count refined by the prior under nearly flat ones.
• exists_isFixedPt_iterate, exists_isFixedPt_receiverChain: every chain reaches a fixed point.
• exists_isPBE_of_isFixedPt: fixed points are perfect Bayesian equilibria.
• coe_receiverStep_subset_exhMW: the first sophisticated reading entails exhaustification by minimal models.
• exhIE_eq_setOf_indistinguishable: innocent exclusion keeps the worlds that no alternative distinguishes from the minimal ones.

Implementation notes

• The counting system depends only on denotations. The prior enters as a secondary criterion, which the competence assumption (67) turns into a count of undecided alternatives, so the examples are stated for every prior satisfying the assumption.
• In the probabilistic model a player type is a set of pure strategies, and the unbiased belief in it is the kernel unbiased that is uniform over its choices. The prior is a measure, the expected gain is the probability that the receiver guesses the state, and the posterior after a message of a pure sender, as in the Nash equilibria of §7, is the prior conditioned on the states that send it. The truth filter of (117) and (122) is applied by maximising over true messages and reading an unsent message literally, which agrees with the paper along every chain.
• (83) refines by the prior the literal reading of a message nobody sends; the probabilistic model and Figure 16 leave it unrefined, as here. Condition (132) is stated with the inequality its proof needs; the paper prints it reversed.
• Theorem 3 is proved for interpretation games with positive priors. The proof completes the paper's sketch by showing that the sender's choices only grow around a cycle of the chain.
• Fact 2 holds for alternatives monotonically determined by the others, as in the paper's conjunctive example, and fails for the negation of an alternative (not_ltALT_insert_compl).

TODO

• Fact 4, the condition on the alternatives under which the two exhaustivity operators agree.

References

• [Fra11]
• [vRS04]
• [Fox07]

Interpretation games

An interpretation game (§3) is a signaling game whose receiver guesses the sender's state: a meaning relation between messages and states fixes literal interpretation, a prior over the states drives inference, and both players gain 1 exactly when the guess is right.

structure Franke2011.InterpGame (T : Type u_1) (M : Type u_2) [MeasurableSpace T] : Type (max u_1 u_2)

An interpretation game is a meaning relation between messages and states together with a prior over the states.

• meaning : M → T → Prop

  meaning m t holds when message m is true at state t.

• prior : MeasureTheory.Measure T

  The prior over the states.

• meaningDecidable (m : M) : DecidablePred (self.meaning m)

def Franke2011.InterpGame.trueStates {T : Type u_1} {M : Type u_2} [MeasurableSpace T] (G : InterpGame T M) [Fintype T] (m : M) : Finset T

The extension of m is the set of states at which it is true.

Equations

• G.trueStates m = Finset.filter (G.meaning m) Finset.univ

@[simp]

theorem Franke2011.InterpGame.mem_trueStates {T : Type u_1} {M : Type u_2} [MeasurableSpace T] (G : InterpGame T M) [Fintype T] {m : M} {t : T} : t ∈ G.trueStates m ↔ G.meaning m t

def Franke2011.InterpGame.trueMessages {T : Type u_1} {M : Type u_2} [MeasurableSpace T] (G : InterpGame T M) [Fintype M] (t : T) : Finset M

trueMessages t is the set of messages true at t.

Equations

• G.trueMessages t = {x : M | G.meaning x t}

@[simp]

theorem Franke2011.InterpGame.mem_trueMessages {T : Type u_1} {M : Type u_2} [MeasurableSpace T] (G : InterpGame T M) [Fintype M] {t : T} {m : M} : m ∈ G.trueMessages t ↔ G.meaning m t

def Franke2011.InterpGame.IsNashEquilibrium {T : Type u_1} {M : Type u_2} [MeasurableSpace T] (G : InterpGame T M) [Fintype T] (σ : T → M) (ρ : M → T) : Prop

A pure profile is a Nash equilibrium (§7) when no message would get a state guessed that its own message does not, and after every message the receiver guesses a most probable state of the posterior, the prior conditioned on the states that send it.

Equations

• G.IsNashEquilibrium σ ρ = ((∀ (t : T) (m : M), ρ m = t → ρ (σ t) = t) ∧ ∀ (m : M), ρ m ∈ Finset.univ.argmax fun (t : T) => G.prior[{t} | σ ⁻¹' {m}])

theorem Franke2011.InterpGame.isNashEquilibrium_of_leftInverse {T : Type u_1} {M : Type u_2} [MeasurableSpace T] (G : InterpGame T M) [Fintype T] [MeasurableSingletonClass T] [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) {σ : T → M} {ρ : M → T} (h : Function.LeftInverse ρ σ) : G.IsNashEquilibrium σ ρ

With positive priors, a profile under which the receiver recovers every state from its message is a Nash equilibrium.

Interpretation games from belief-value tables

A base-level game distinguishes the truth-value vectors of the alternatives within the target sentence (61), an epistemic game the belief-value vectors (66), with three values: believed true, believed false and undecided. A message is true at a state when the state believes it true.

inductive Franke2011.BeliefValue : Type

The three belief values of §6.2 are believed true, believed false and undecided.

• yes : BeliefValue
• no : BeliefValue
• unc : BeliefValue

@[instance_reducible]

instance Franke2011.instDecidableEqBeliefValue : DecidableEq BeliefValue

Equations

• Franke2011.instDecidableEqBeliefValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.instFintypeBeliefValue : Fintype BeliefValue

Equations

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

def Franke2011.instReprBeliefValue.repr : BeliefValue → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.instReprBeliefValue : Repr BeliefValue

Equations

• Franke2011.instReprBeliefValue = { reprPrec := Franke2011.instReprBeliefValue.repr }

def Franke2011.ofTable {T : Type u_1} {M : Type u_2} (table : T → M → BeliefValue) [MeasurableSpace T] (prior : MeasureTheory.Measure T) : InterpGame T M

In the interpretation game of a belief-value table, m is true at t iff t believes m true.

Equations

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

def Franke2011.uncertaintyCount {T : Type u_1} {M : Type u_2} [Fintype M] (table : T → M → BeliefValue) (t : T) : ℕ

uncertaintyCount table t counts the alternatives t is undecided about.

Equations

• Franke2011.uncertaintyCount table t = {m : M | table t m = Franke2011.BeliefValue.unc}.card

def Franke2011.beliefValue {W : Type u_3} [DecidableEq W] (X A : Finset W) : BeliefValue

The belief value (65) of a proposition A in an epistemic state X is believed true when X ⊆ A, believed false when X and A are disjoint, and undecided otherwise.

Equations

• Franke2011.beliefValue X A = if X ⊆ A then Franke2011.BeliefValue.yes else if Disjoint X A then Franke2011.BeliefValue.no else Franke2011.BeliefValue.unc

def Franke2011.CompetencePrior {T : Type u_1} {M : Type u_2} [Fintype M] (table : T → M → BeliefValue) (prior : T → ℝ) : Prop

Under the competence assumption (67) the prior is a strictly decreasing function of the number of alternatives a state is undecided about.

Equations

• Franke2011.CompetencePrior table prior = ∃ (f : ℕ → ℝ), StrictAnti f ∧ prior = f ∘ Franke2011.uncertaintyCount table

def Franke2011.IncompetencePrior {T : Type u_1} {M : Type u_2} [Fintype M] (table : T → M → BeliefValue) (prior : T → ℝ) : Prop

Under the incompetence assumption (68) the prior is a strictly increasing function of the number of alternatives a state is undecided about.

Equations

• Franke2011.IncompetencePrior table prior = ∃ (f : ℕ → ℝ), StrictMono f ∧ prior = f ∘ Franke2011.uncertaintyCount table

theorem Franke2011.CompetencePrior.argmax_eq {T : Type u_1} {M : Type u_2} [Fintype M] {table : T → M → BeliefValue} {prior : T → ℝ} (h : CompetencePrior table prior) (s : Finset T) : s.argmax prior = s.argmax (⇑OrderDual.toDual ∘ uncertaintyCount table)

Under competence the most probable states of a set are the ones undecided about fewest alternatives.

theorem Franke2011.IncompetencePrior.argmax_eq {T : Type u_1} {M : Type u_2} [Fintype M] {table : T → M → BeliefValue} {prior : T → ℝ} (h : IncompetencePrior table prior) (s : Finset T) : s.argmax prior = s.argmax (uncertaintyCount table)

Under incompetence the most probable states of a set are the ones undecided about most alternatives.

The light system

A player type is a set of pure strategies, written as a correspondence: a receiver type R : M → Finset T, a sender type S : T → Finset M. Level 0 is literal meaning (73): the receiver type is the denotation and the sender type its inverse. A level-k + 1 sender in t chooses, among the messages that can induce t, those with fewest interpretations (76), the chance of being understood being one over their number (129); if no message can induce t she sends any true message. The receiver's step (77) is the same computation with the roles of states and messages exchanged, a surprise message being read literally.

def Franke2011.inverse {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] (X : α → Finset γ) (c : γ) : Finset α

The inverse X⁻¹(c) of a correspondence X : α → Finset γ at c is the set of points whose image contains c (footnote 25).

Equations

• Franke2011.inverse X c = {x : α | c ∈ X x}

@[simp]

theorem Franke2011.mem_inverse {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] {X : α → Finset γ} {c : γ} {a : α} : a ∈ inverse X c ↔ c ∈ X a

@[simp]

theorem Franke2011.inverse_inverse {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [Fintype γ] [DecidableEq α] (X : α → Finset γ) : inverse (inverse X) = X

def Franke2011.bestResponse {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [DecidableEq α] (lit : γ → Finset α) (X : α → Finset γ) (c : γ) : Finset α

The best responses to the unbiased belief in the type X at c are the points of X⁻¹(c) with fewest X-images, (76) and (77); when X⁻¹(c) is empty they are the literal choices lit c.

Equations

• Franke2011.bestResponse lit X c = if Franke2011.inverse X c = ∅ then lit c else (Franke2011.inverse X c).argmin fun (a : α) => (X a).card

def Franke2011.bestResponseBy {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [DecidableEq α] {β : Type u_3} [LinearOrder β] (key : α → β) (lit : γ → Finset α) (X : α → Finset γ) (c : γ) : Finset α

The best responses refined by a secondary criterion key, as by a nearly flat prior (83) or a nominal message cost (§9.2), keep the ones maximising key; literal choices stay unrefined.

Equations

• Franke2011.bestResponseBy key lit X c = if Franke2011.inverse X c = ∅ then lit c else ((Franke2011.inverse X c).argmin fun (a : α) => (X a).card).argmax key

theorem Franke2011.mem_bestResponse {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [DecidableEq α] {lit : γ → Finset α} {X : α → Finset γ} {c : γ} {a : α} : a ∈ bestResponse lit X c ↔ if inverse X c = ∅ then a ∈ lit c else c ∈ X a ∧ ∀ (a' : α), c ∈ X a' → (X a).card ≤ (X a').card

theorem Franke2011.bestResponseBy_subset {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [DecidableEq α] {β : Type u_3} [LinearOrder β] {lit : γ → Finset α} {X : α → Finset γ} {key : α → β} (c : γ) : bestResponseBy key lit X c ⊆ bestResponse lit X c

theorem Franke2011.bestResponseBy_of_forall_eq {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [DecidableEq α] {β : Type u_3} [LinearOrder β] {lit : γ → Finset α} {key : α → β} (h : ∀ (a b : α), key a = key b) : bestResponseBy key lit = bestResponse lit

A secondary criterion that ranks all points alike refines nothing.

theorem Franke2011.bestResponseBy_congr {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [DecidableEq α] {β : Type u_3} {β' : Type u_4} [LinearOrder β] [LinearOrder β'] {lit : γ → Finset α} {key : α → β} {key' : α → β'} (h : ∀ (s : Finset α), s.argmax key = s.argmax key') : bestResponseBy key lit = bestResponseBy key' lit

theorem Franke2011.bestResponse_subset {α : Type u_1} {γ : Type u_2} [Fintype α] [DecidableEq γ] [DecidableEq α] {lit : γ → Finset α} {X : α → Finset γ} (h : ∀ (a : α), ∀ c ∈ X a, a ∈ lit c) (c : γ) : bestResponse lit X c ⊆ lit c

Best responses respect literal meaning when the type does (Lemma 2).

def Franke2011.senderStep {T : Type u_1} {M : Type u_2} [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) : (M → Finset T) → T → Finset M

senderStep den R is the level-k + 1 sender type against the level-k receiver type R (76).

Equations

• Franke2011.senderStep den = Franke2011.bestResponse (Franke2011.inverse den)

def Franke2011.receiverStep {T : Type u_1} {M : Type u_2} [Fintype T] [DecidableEq T] [DecidableEq M] (den : M → Finset T) : (T → Finset M) → M → Finset T

receiverStep den S is the level-k + 1 receiver type against the level-k sender type S (77).

Equations

• Franke2011.receiverStep den = Franke2011.bestResponse den

def Franke2011.senderStepBy {T : Type u_1} {M : Type u_2} [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : M → β) : (M → Finset T) → T → Finset M

senderStepBy den key refines the sender step by a secondary criterion, such as nominal costs.

Equations

• Franke2011.senderStepBy den key = Franke2011.bestResponseBy key (Franke2011.inverse den)

def Franke2011.receiverStepBy {T : Type u_1} {M : Type u_2} [Fintype T] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : T → β) : (T → Finset M) → M → Finset T

receiverStepBy den key refines the receiver step by a secondary criterion, such as the prior (83).

Equations

• Franke2011.receiverStepBy den key = Franke2011.bestResponseBy key den

def Franke2011.receiverChain {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) (n : ℕ) : M → Finset T

receiverChain den n is the receiver type R₂ₙ of the chain from the literal receiver.

Equations

• Franke2011.receiverChain den n = (Franke2011.receiverStep den ∘ Franke2011.senderStep den)^[n] den

def Franke2011.senderChain {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) (n : ℕ) : T → Finset M

senderChain den n is the sender type S₂ₙ of the chain from the literal sender.

Equations

• Franke2011.senderChain den n = (Franke2011.senderStep den ∘ Franke2011.receiverStep den)^[n] (Franke2011.inverse den)

def Franke2011.receiverChainBy {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : T → β) (n : ℕ) : M → Finset T

receiverChainBy den key n is the receiver type R₂ₙ of the chain from the literal receiver when every receiver step is refined by key.

Equations

• Franke2011.receiverChainBy den key n = (Franke2011.receiverStepBy den key ∘ Franke2011.senderStep den)^[n] den

def Franke2011.senderChainBy {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : T → β) (n : ℕ) : T → Finset M

senderChainBy den key n is the sender type S₂ₙ of the chain from the literal sender when every receiver step is refined by key.

Equations

• Franke2011.senderChainBy den key n = (Franke2011.senderStep den ∘ Franke2011.receiverStepBy den key)^[n] (Franke2011.inverse den)

theorem Franke2011.receiverStepBy_congr {T : Type u_1} {M : Type u_2} [Fintype T] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] {β' : Type u_4} [LinearOrder β'] {key : T → β} {key' : T → β'} (h : ∀ (s : Finset T), s.argmax key = s.argmax key') : receiverStepBy den key = receiverStepBy den key'

theorem Franke2011.receiverChainBy_congr {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] {β' : Type u_4} [LinearOrder β'] {key : T → β} {key' : T → β'} (h : ∀ (s : Finset T), s.argmax key = s.argmax key') : receiverChainBy den key = receiverChainBy den key'

theorem Franke2011.senderChainBy_congr {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] {β' : Type u_4} [LinearOrder β'] {key : T → β} {key' : T → β'} (h : ∀ (s : Finset T), s.argmax key = s.argmax key') : senderChainBy den key = senderChainBy den key'

theorem Franke2011.senderStep_subset {T : Type u_1} {M : Type u_2} [Fintype M] [DecidableEq T] [DecidableEq M] {den R : M → Finset T} (hR : ∀ (m : M), R m ⊆ den m) (t : T) : senderStep den R t ⊆ inverse den t

A sender who believes every interpretation true only sends true messages (Lemma 2).

theorem Franke2011.receiverStep_subset {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] {den : M → Finset T} {S : T → Finset M} (hS : ∀ (t : T), S t ⊆ inverse den t) (m : M) : receiverStep den S m ⊆ den m

A receiver who believes every message sent true only assigns true interpretations (Lemma 2).

theorem Franke2011.receiverStepBy_subset {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] {den : M → Finset T} {β : Type u_3} [LinearOrder β] {key : T → β} {S : T → Finset M} (hS : ∀ (t : T), S t ⊆ inverse den t) (m : M) : receiverStepBy den key S m ⊆ den m

theorem Franke2011.receiverStep_inverse {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) (m : M) : receiverStep den (inverse den) m = (den m).argmin fun (t : T) => (inverse den t).card

The first sophisticated receiver of the chain from the literal sender reads a message as the states where it is true that make fewest messages true (107).

theorem Franke2011.receiverChain_succ {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) (n : ℕ) : receiverChain den (n + 1) = receiverStep den (senderStep den (receiverChain den n))

theorem Franke2011.senderChain_succ {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) (n : ℕ) : senderChain den (n + 1) = senderStep den (receiverStep den (senderChain den n))

theorem Franke2011.receiverChainBy_succ {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : T → β) (n : ℕ) : receiverChainBy den key (n + 1) = receiverStepBy den key (senderStep den (receiverChainBy den key n))

theorem Franke2011.senderChainBy_succ {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : T → β) (n : ℕ) : senderChainBy den key (n + 1) = senderStep den (receiverStepBy den key (senderChainBy den key n))

theorem Franke2011.receiverChain_subset {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) (n : ℕ) (m : M) : receiverChain den n m ⊆ den m

Truth is preserved along the receiver chain (Lemma 2).

theorem Franke2011.senderChain_subset {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) (n : ℕ) (t : T) : senderChain den n t ⊆ inverse den t

Truth is preserved along the sender chain (Lemma 2).

theorem Franke2011.receiverChainBy_subset {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : T → β) (n : ℕ) (m : M) : receiverChainBy den key n m ⊆ den m

theorem Franke2011.senderChainBy_subset {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) {β : Type u_3} [LinearOrder β] (key : T → β) (n : ℕ) (t : T) : senderChainBy den key n t ⊆ inverse den t

"Some" and "all" (Figure 4, §7)

Two states within the denotation of "some" (Examples.ex4): some-but-not-all, where only "some" is true, and all, where both are.

inductive Franke2011.SomeAll.State : Type

• someNotAll : State
• all : State

@[instance_reducible]

instance Franke2011.SomeAll.instDecidableEqState : DecidableEq State

Equations

• Franke2011.SomeAll.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.SomeAll.instFintypeState : Fintype State

Equations

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

@[instance_reducible]

instance Franke2011.SomeAll.instReprState : Repr State

Equations

• Franke2011.SomeAll.instReprState = { reprPrec := Franke2011.SomeAll.instReprState.repr }

def Franke2011.SomeAll.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.SomeAll.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.SomeAll.instMeasurableSpaceState = ⊤

inductive Franke2011.SomeAll.Message : Type

• some : Message
• all : Message

@[instance_reducible]

instance Franke2011.SomeAll.instDecidableEqMessage : DecidableEq Message

Equations

• Franke2011.SomeAll.instDecidableEqMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.SomeAll.instFintypeMessage : Fintype Message

Equations

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

def Franke2011.SomeAll.instReprMessage.repr : Message → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.SomeAll.instReprMessage : Repr Message

Equations

• Franke2011.SomeAll.instReprMessage = { reprPrec := Franke2011.SomeAll.instReprMessage.repr }

@[instance_reducible]

instance Franke2011.SomeAll.instMeasurableSpaceMessage : MeasurableSpace Message

Equations

• Franke2011.SomeAll.instMeasurableSpaceMessage = ⊤

noncomputable def Franke2011.SomeAll.game : InterpGame State Message

The interpretation game of Figure 4 has flat priors.

Equations

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

instance Franke2011.SomeAll.instIsFiniteMeasureStatePriorMessageGame : MeasureTheory.IsFiniteMeasure game.prior

def Franke2011.SomeAll.scalarSender : State → Message

In the attested play (69) the sender says "some" when not all.

Equations

• Franke2011.SomeAll.scalarSender Franke2011.SomeAll.State.someNotAll = Franke2011.SomeAll.Message.some
• Franke2011.SomeAll.scalarSender Franke2011.SomeAll.State.all = Franke2011.SomeAll.Message.all

def Franke2011.SomeAll.scalarReceiver : Message → State

In the attested play (69) the receiver reads "some" as not all.

Equations

• Franke2011.SomeAll.scalarReceiver Franke2011.SomeAll.Message.some = Franke2011.SomeAll.State.someNotAll
• Franke2011.SomeAll.scalarReceiver Franke2011.SomeAll.Message.all = Franke2011.SomeAll.State.all

def Franke2011.SomeAll.reversedSender : State → Message

The reversed play (71) swaps the messages.

Equations

• Franke2011.SomeAll.reversedSender Franke2011.SomeAll.State.someNotAll = Franke2011.SomeAll.Message.all
• Franke2011.SomeAll.reversedSender Franke2011.SomeAll.State.all = Franke2011.SomeAll.Message.some

def Franke2011.SomeAll.reversedReceiver : Message → State

The receiver of the reversed play (71) reads "some" as all.

Equations

• Franke2011.SomeAll.reversedReceiver Franke2011.SomeAll.Message.some = Franke2011.SomeAll.State.all
• Franke2011.SomeAll.reversedReceiver Franke2011.SomeAll.Message.all = Franke2011.SomeAll.State.someNotAll

theorem Franke2011.SomeAll.isNashEquilibrium_scalar_and_reversed : game.IsNashEquilibrium scalarSender scalarReceiver ∧ game.IsNashEquilibrium reversedSender reversedReceiver

The attested play and the reversed play are both Nash equilibria, so equilibrium does not select the implicature (§7).

theorem Franke2011.SomeAll.scalar_implicature : (receiverChain game.trueStates 1 = fun (m : Message) => {scalarReceiver m}) ∧ (senderChain game.trueStates 1 = fun (t : State) => {scalarSender t}) ∧ Function.IsFixedPt (receiverStep game.trueStates ∘ senderStep game.trueStates) fun (m : Message) => {scalarReceiver m}

Both chains reach the attested play at their first sophisticated level and stay there, so "some" conveys not-all.

theorem Franke2011.SomeAll.receiverChain_ne_reversed (n : ℕ) : receiverChain game.trueStates n ≠ fun (m : Message) => {reversedReceiver m}

No chain reaches the reversed play, which reads "all" where it is false, since reasoning that starts from literal meaning keeps to it (Lemma 2).

Two disjuncts (Figures 5 and 7; tables (84)–(86))

Alternatives A, B and A ∨ B give three states whether the disjunction is plain (Examples.ex8), under a possibility modal (Examples.ex12a), or in a conditional antecedent (Examples.ex18): one game, three constructions. Its fixed point maps the disjunction to the state where both disjuncts hold, which is the free choice inference, the simplification of disjunctive antecedents, and at base level a conjunctive reading of plain disjunction (§9.2).

inductive Franke2011.TwoDisjuncts.State : Type

• onlyA : State
• onlyB : State
• both : State

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instDecidableEqState : DecidableEq State

Equations

• Franke2011.TwoDisjuncts.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instFintypeState : Fintype State

Equations

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

def Franke2011.TwoDisjuncts.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instReprState : Repr State

Equations

• Franke2011.TwoDisjuncts.instReprState = { reprPrec := Franke2011.TwoDisjuncts.instReprState.repr }

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.TwoDisjuncts.instMeasurableSpaceState = ⊤

inductive Franke2011.TwoDisjuncts.Message : Type

• first : Message
• second : Message
• either : Message

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instDecidableEqMessage : DecidableEq Message

Equations

• Franke2011.TwoDisjuncts.instDecidableEqMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instFintypeMessage : Fintype Message

Equations

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

def Franke2011.TwoDisjuncts.instReprMessage.repr : Message → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instReprMessage : Repr Message

Equations

• Franke2011.TwoDisjuncts.instReprMessage = { reprPrec := Franke2011.TwoDisjuncts.instReprMessage.repr }

@[instance_reducible]

instance Franke2011.TwoDisjuncts.instMeasurableSpaceMessage : MeasurableSpace Message

Equations

• Franke2011.TwoDisjuncts.instMeasurableSpaceMessage = ⊤

noncomputable def Franke2011.TwoDisjuncts.game : InterpGame State Message

The interpretation game of Figure 5 has flat priors.

Equations

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

instance Franke2011.TwoDisjuncts.instIsFiniteMeasureStatePriorMessageGame : MeasureTheory.IsFiniteMeasure game.prior

def Franke2011.TwoDisjuncts.freeChoiceSender : State → Message

In the free choice play (70) each state sends the message true at it alone.

Equations

• Franke2011.TwoDisjuncts.freeChoiceSender Franke2011.TwoDisjuncts.State.onlyA = Franke2011.TwoDisjuncts.Message.first
• Franke2011.TwoDisjuncts.freeChoiceSender Franke2011.TwoDisjuncts.State.onlyB = Franke2011.TwoDisjuncts.Message.second
• Franke2011.TwoDisjuncts.freeChoiceSender Franke2011.TwoDisjuncts.State.both = Franke2011.TwoDisjuncts.Message.either

def Franke2011.TwoDisjuncts.freeChoiceReceiver : Message → State

In the free choice play (70) the disjunction is read as both disjuncts.

Equations

• Franke2011.TwoDisjuncts.freeChoiceReceiver Franke2011.TwoDisjuncts.Message.first = Franke2011.TwoDisjuncts.State.onlyA
• Franke2011.TwoDisjuncts.freeChoiceReceiver Franke2011.TwoDisjuncts.Message.second = Franke2011.TwoDisjuncts.State.onlyB
• Franke2011.TwoDisjuncts.freeChoiceReceiver Franke2011.TwoDisjuncts.Message.either = Franke2011.TwoDisjuncts.State.both

def Franke2011.TwoDisjuncts.crossedSender : State → Message

In the crossed play (72) the disjunction and the first disjunct swap roles.

Equations

• Franke2011.TwoDisjuncts.crossedSender Franke2011.TwoDisjuncts.State.onlyA = Franke2011.TwoDisjuncts.Message.either
• Franke2011.TwoDisjuncts.crossedSender Franke2011.TwoDisjuncts.State.onlyB = Franke2011.TwoDisjuncts.Message.second
• Franke2011.TwoDisjuncts.crossedSender Franke2011.TwoDisjuncts.State.both = Franke2011.TwoDisjuncts.Message.first

def Franke2011.TwoDisjuncts.crossedReceiver : Message → State

The receiver of the crossed play (72) reads the disjunction as the first disjunct alone.

Equations

• Franke2011.TwoDisjuncts.crossedReceiver Franke2011.TwoDisjuncts.Message.first = Franke2011.TwoDisjuncts.State.both
• Franke2011.TwoDisjuncts.crossedReceiver Franke2011.TwoDisjuncts.Message.second = Franke2011.TwoDisjuncts.State.onlyB
• Franke2011.TwoDisjuncts.crossedReceiver Franke2011.TwoDisjuncts.Message.either = Franke2011.TwoDisjuncts.State.onlyA

theorem Franke2011.TwoDisjuncts.isNashEquilibrium_freeChoice_and_crossed : game.IsNashEquilibrium freeChoiceSender freeChoiceReceiver ∧ game.IsNashEquilibrium crossedSender crossedReceiver

The free choice play and the crossed play both communicate perfectly, so both are Nash equilibria and no refinement by payoffs separates them (§7).

theorem Franke2011.TwoDisjuncts.free_choice : (receiverChain game.trueStates 2 = fun (m : Message) => {freeChoiceReceiver m}) ∧ (senderChain game.trueStates 2 = fun (t : State) => {freeChoiceSender t}) ∧ Function.IsFixedPt (receiverStep game.trueStates ∘ senderStep game.trueStates) fun (m : Message) => {freeChoiceReceiver m}

Both chains reach the free choice play at level 4 (Figure 7), where it is a fixed point.

theorem Franke2011.TwoDisjuncts.receiverChain_one_either : receiverChain game.trueStates 1 Message.either = {State.onlyA, State.onlyB, State.both}

On the way the disjunction is a surprise message to R₂, read literally (137).

theorem Franke2011.TwoDisjuncts.receiverChain_ne_crossed (n : ℕ) : receiverChain game.trueStates n ≠ fun (m : Message) => {crossedReceiver m}

The chain from the literal receiver never reaches the crossed play, although it respects literal meaning as well.

Epistemic "some" and "all" (Figures 6, 8 and 9)

Three speaker belief states within belief in "some": believes not-all, believes all, undecided about all. Flat priors give the general epistemic implicature, competence (67) the strong and incompetence (68) the weak one, in both chains.

inductive Franke2011.SomeAllEpistemic.State : Type

States are named by their belief-value vectors over ("some", "all").

• t10 : State
• t11 : State
• t1u : State

@[instance_reducible]

instance Franke2011.SomeAllEpistemic.instDecidableEqState : DecidableEq State

Equations

• Franke2011.SomeAllEpistemic.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.SomeAllEpistemic.instFintypeState : Fintype State

Equations

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

def Franke2011.SomeAllEpistemic.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.SomeAllEpistemic.instReprState : Repr State

Equations

• Franke2011.SomeAllEpistemic.instReprState = { reprPrec := Franke2011.SomeAllEpistemic.instReprState.repr }

@[instance_reducible]

instance Franke2011.SomeAllEpistemic.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.SomeAllEpistemic.instMeasurableSpaceState = ⊤

def Franke2011.SomeAllEpistemic.table : State → SomeAll.Message → BeliefValue

This table gives the belief values of Figure 6.

Equations

• Franke2011.SomeAllEpistemic.table x✝ Franke2011.SomeAll.Message.some = Franke2011.BeliefValue.yes
• Franke2011.SomeAllEpistemic.table Franke2011.SomeAllEpistemic.State.t10 Franke2011.SomeAll.Message.all = Franke2011.BeliefValue.no
• Franke2011.SomeAllEpistemic.table Franke2011.SomeAllEpistemic.State.t11 Franke2011.SomeAll.Message.all = Franke2011.BeliefValue.yes
• Franke2011.SomeAllEpistemic.table Franke2011.SomeAllEpistemic.State.t1u Franke2011.SomeAll.Message.all = Franke2011.BeliefValue.unc

noncomputable def Franke2011.SomeAllEpistemic.game : InterpGame State SomeAll.Message

This is the game of Figure 6 with a = b.

Equations

• Franke2011.SomeAllEpistemic.game = Franke2011.ofTable Franke2011.SomeAllEpistemic.table (ProbabilityTheory.uniformOn Set.univ)

theorem Franke2011.SomeAllEpistemic.exists_table_eq_iff (v : SomeAll.Message → BeliefValue) : (∃ (t : State), table t = v) ↔ ∃ (X : Finset SomeAll.State), X.Nonempty ∧ v = fun (m : SomeAll.Message) => beliefValue X (SomeAll.game.trueStates m)

The states of Figure 6 are the belief-value vectors of the nonempty sets of states of Figure 4 (66).

theorem Franke2011.SomeAllEpistemic.general : receiverChain game.trueStates 1 SomeAll.Message.some = {State.t10, State.t1u} ∧ Function.IsFixedPt (receiverStep game.trueStates ∘ senderStep game.trueStates) (receiverChain game.trueStates 1) ∧ receiverStep game.trueStates (senderChain game.trueStates 1) = receiverChain game.trueStates 1

With flat priors both chains settle at their first sophisticated level on reading "some" as the speaker not believing "all" (Figure 8).

theorem Franke2011.SomeAllEpistemic.strong {p : State → ℝ} (hp : CompetencePrior table p) : receiverChainBy game.trueStates p 1 SomeAll.Message.some = {State.t10} ∧ Function.IsFixedPt (receiverStepBy game.trueStates p ∘ senderStep game.trueStates) (receiverChainBy game.trueStates p 1) ∧ receiverStepBy game.trueStates p (senderChainBy game.trueStates p 1) = receiverChainBy game.trueStates p 1

Under every competence prior both chains read "some" as the speaker believing "all" false (Figure 9).

theorem Franke2011.SomeAllEpistemic.weak {p : State → ℝ} (hp : IncompetencePrior table p) : receiverChainBy game.trueStates p 1 SomeAll.Message.some = {State.t1u} ∧ Function.IsFixedPt (receiverStepBy game.trueStates p ∘ senderStep game.trueStates) (receiverChainBy game.trueStates p 1) ∧ receiverStepBy game.trueStates p (senderChainBy game.trueStates p 1) = receiverChainBy game.trueStates p 1

Under every incompetence prior both chains read "some" as the speaker undecided about "all".

Epistemic disjunction (tables (87)–(88), Figure 10)

Six belief states within belief in A ∨ B. In all six constellations, two chains under three prior regimes, the fixed point reads the disjunction as the state undecided about both disjuncts, which is the ignorance implicature; a single disjunct is read as belief in it without belief in the other, as knowledge that the other is false under competence, and as uncertainty about the other under incompetence.

inductive Franke2011.DisjunctionEpistemic.State : Type

States are named by belief-value vectors over (A, B, A ∨ B).

• t101 : State
• t011 : State
• t111 : State
• t1u1 : State
• tu11 : State
• tuu1 : State

@[instance_reducible]

instance Franke2011.DisjunctionEpistemic.instDecidableEqState : DecidableEq State

Equations

• Franke2011.DisjunctionEpistemic.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.DisjunctionEpistemic.instFintypeState : Fintype State

Equations

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

@[instance_reducible]

instance Franke2011.DisjunctionEpistemic.instReprState : Repr State

Equations

• Franke2011.DisjunctionEpistemic.instReprState = { reprPrec := Franke2011.DisjunctionEpistemic.instReprState.repr }

def Franke2011.DisjunctionEpistemic.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.DisjunctionEpistemic.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.DisjunctionEpistemic.instMeasurableSpaceState = ⊤

def Franke2011.DisjunctionEpistemic.table : State → TwoDisjuncts.Message → BeliefValue

This table gives the belief values of (87).

Equations

• Franke2011.DisjunctionEpistemic.table x✝ Franke2011.TwoDisjuncts.Message.either = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t101 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t111 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t1u1 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t011 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.no
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.tu11 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.tuu1 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t011 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t111 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.tu11 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t101 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.no
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.t1u1 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionEpistemic.table Franke2011.DisjunctionEpistemic.State.tuu1 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.unc

noncomputable def Franke2011.DisjunctionEpistemic.game : InterpGame State TwoDisjuncts.Message

This is the game of table (87) with a = b = c in (88).

Equations

• Franke2011.DisjunctionEpistemic.game = Franke2011.ofTable Franke2011.DisjunctionEpistemic.table (ProbabilityTheory.uniformOn Set.univ)

theorem Franke2011.DisjunctionEpistemic.exists_table_eq_iff (v : TwoDisjuncts.Message → BeliefValue) : (∃ (t : State), table t = v) ↔ ∃ (X : Finset TwoDisjuncts.State), X.Nonempty ∧ v = fun (m : TwoDisjuncts.Message) => beliefValue X (TwoDisjuncts.game.trueStates m)

The states of (87) are the belief-value vectors of the nonempty sets of states of (85) (66).

theorem Franke2011.DisjunctionEpistemic.ignorance : (receiverChain game.trueStates 1 = fun (m : TwoDisjuncts.Message) => match m with | TwoDisjuncts.Message.first => {State.t101, State.t1u1} | TwoDisjuncts.Message.second => {State.t011, State.tu11} | TwoDisjuncts.Message.either => {State.tuu1}) ∧ Function.IsFixedPt (receiverStep game.trueStates ∘ senderStep game.trueStates) (receiverChain game.trueStates 1) ∧ receiverStep game.trueStates (senderChain game.trueStates 1) = receiverChain game.trueStates 1

With flat priors both chains settle at their first sophisticated level on the ignorance reading of the disjunction (Figure 10).

theorem Franke2011.DisjunctionEpistemic.ignorance_of_competencePrior {p : State → ℝ} (hp : CompetencePrior table p) : (receiverChainBy game.trueStates p 1 = fun (m : TwoDisjuncts.Message) => match m with | TwoDisjuncts.Message.first => {State.t101} | TwoDisjuncts.Message.second => {State.t011} | TwoDisjuncts.Message.either => {State.tuu1}) ∧ Function.IsFixedPt (receiverStepBy game.trueStates p ∘ senderStep game.trueStates) (receiverChainBy game.trueStates p 1) ∧ receiverStepBy game.trueStates p (senderChainBy game.trueStates p 1) = receiverChainBy game.trueStates p 1

Under every competence prior the fixed point of both chains keeps the ignorance reading and reads a single disjunct as knowledge that the other is false.

theorem Franke2011.DisjunctionEpistemic.ignorance_of_incompetencePrior {p : State → ℝ} (hp : IncompetencePrior table p) : (receiverChainBy game.trueStates p 1 = fun (m : TwoDisjuncts.Message) => match m with | TwoDisjuncts.Message.first => {State.t1u1} | TwoDisjuncts.Message.second => {State.tu11} | TwoDisjuncts.Message.either => {State.tuu1}) ∧ Function.IsFixedPt (receiverStepBy game.trueStates p ∘ senderStep game.trueStates) (receiverChainBy game.trueStates p 1) ∧ receiverStepBy game.trueStates p (senderChainBy game.trueStates p 1) = receiverChainBy game.trueStates p 1

Under every incompetence prior the fixed point of both chains keeps the ignorance reading and reads a single disjunct as uncertainty about the other.

Disjunction with a conjunctive alternative (tables (89)–(92), Figures 11–14)

Plain disjunction at base level with A ∧ B among the alternatives (table (89), Figure 11).

inductive Franke2011.DisjunctionConj.Message : Type

• first : Message
• second : Message
• both : Message
• either : Message

@[instance_reducible]

instance Franke2011.DisjunctionConj.instDecidableEqMessage : DecidableEq Message

Equations

• Franke2011.DisjunctionConj.instDecidableEqMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.DisjunctionConj.instFintypeMessage : Fintype Message

Equations

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

@[instance_reducible]

instance Franke2011.DisjunctionConj.instReprMessage : Repr Message

Equations

• Franke2011.DisjunctionConj.instReprMessage = { reprPrec := Franke2011.DisjunctionConj.instReprMessage.repr }

def Franke2011.DisjunctionConj.instReprMessage.repr : Message → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.DisjunctionConj.instMeasurableSpaceMessage : MeasurableSpace Message

Equations

• Franke2011.DisjunctionConj.instMeasurableSpaceMessage = ⊤

noncomputable def Franke2011.DisjunctionConj.game : InterpGame TwoDisjuncts.State Message

The interpretation game of table (89) has flat priors.

Equations

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

theorem Franke2011.DisjunctionConj.disjunction_surprise : (receiverChain game.trueStates 1 = fun (m : Message) => match m with | Message.first => {TwoDisjuncts.State.onlyA} | Message.second => {TwoDisjuncts.State.onlyB} | Message.both => {TwoDisjuncts.State.both} | Message.either => {TwoDisjuncts.State.onlyA, TwoDisjuncts.State.onlyB, TwoDisjuncts.State.both}) ∧ Function.IsFixedPt (receiverStep game.trueStates ∘ senderStep game.trueStates) (receiverChain game.trueStates 1) ∧ receiverStep game.trueStates (senderChain game.trueStates 1) = receiverChain game.trueStates 1 ∧ inverse (senderStep game.trueStates (receiverChain game.trueStates 1)) Message.either = ∅

In the fixed point of both chains no state sends the disjunction, so it is a surprise message, read literally.

Free choice with the conjunctive alternative (table (90), Figure 12): the state where both are permitted but not jointly is now possible, and the fixed point delivers free choice together with the exclusivity implicature. Figure 12 draws the chain from the literal receiver, which the text calls the S₀-sequence.

inductive Franke2011.FreeChoiceConj.State : Type

States are named by truth vectors over (◇A, ◇B, ◇(A ∧ B), ◇(A ∨ B)).

• t1001 : State
• t0101 : State
• t1111 : State
• t1101 : State

@[instance_reducible]

instance Franke2011.FreeChoiceConj.instDecidableEqState : DecidableEq State

Equations

• Franke2011.FreeChoiceConj.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.FreeChoiceConj.instFintypeState : Fintype State

Equations

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

@[instance_reducible]

instance Franke2011.FreeChoiceConj.instReprState : Repr State

Equations

• Franke2011.FreeChoiceConj.instReprState = { reprPrec := Franke2011.FreeChoiceConj.instReprState.repr }

def Franke2011.FreeChoiceConj.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.FreeChoiceConj.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.FreeChoiceConj.instMeasurableSpaceState = ⊤

noncomputable def Franke2011.FreeChoiceConj.game : InterpGame State DisjunctionConj.Message

The interpretation game of table (90) has flat priors.

Equations

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

theorem Franke2011.FreeChoiceConj.freeChoice_exclusivity : (receiverChain game.trueStates 2 = fun (m : DisjunctionConj.Message) => match m with | DisjunctionConj.Message.first => {State.t1001} | DisjunctionConj.Message.second => {State.t0101} | DisjunctionConj.Message.both => {State.t1111} | DisjunctionConj.Message.either => {State.t1101}) ∧ Function.IsFixedPt (receiverStep game.trueStates ∘ senderStep game.trueStates) (receiverChain game.trueStates 2)

From the literal receiver the chain reaches at level 4 a fixed point reading the disjunction as free choice without joint permission.

Simplification of disjunctive antecedents with the conjunctive alternative (table (91), Figure 13): six states, and the fixed point after R₄ gives simplification together with the exclusivity implicature; the chain from the literal sender agrees on the disjunction (footnote 29).

inductive Franke2011.SdaConj.State : Type

States are named by truth vectors over (A > C, B > C, (A ∧ B) > C, (A ∨ B) > C).

• t1001 : State
• t0101 : State
• t1011 : State
• t0111 : State
• t1101 : State
• t1111 : State

@[instance_reducible]

instance Franke2011.SdaConj.instDecidableEqState : DecidableEq State

Equations

• Franke2011.SdaConj.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.SdaConj.instFintypeState : Fintype State

Equations

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

@[instance_reducible]

instance Franke2011.SdaConj.instReprState : Repr State

Equations

• Franke2011.SdaConj.instReprState = { reprPrec := Franke2011.SdaConj.instReprState.repr }

def Franke2011.SdaConj.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.SdaConj.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.SdaConj.instMeasurableSpaceState = ⊤

noncomputable def Franke2011.SdaConj.game : InterpGame State DisjunctionConj.Message

The interpretation game of table (91) has flat priors.

Equations

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

theorem Franke2011.SdaConj.sda_exclusivity : receiverChain game.trueStates 2 DisjunctionConj.Message.either = {State.t1101} ∧ Function.IsFixedPt (receiverStep game.trueStates ∘ senderStep game.trueStates) (receiverChain game.trueStates 2) ∧ receiverStep game.trueStates (senderChain game.trueStates 2) DisjunctionConj.Message.either = {State.t1101} ∧ Function.IsFixedPt (senderStep game.trueStates ∘ receiverStep game.trueStates) (senderChain game.trueStates 2)

Both chains reach a fixed point reading the disjunctive antecedent as both conditionals true and the conjunctive one false.

Epistemic disjunction with the conjunctive alternative (table (92), Figure 14): without a competence assumption the disjunction conveys that the speaker does not believe A ∧ B, under competence that she believes it false, and under incompetence that she is undecided.

inductive Franke2011.DisjunctionConjEpistemic.State : Type

States are named by belief-value vectors over (A, B, A ∧ B, A ∨ B).

• t1001 : State
• t0101 : State
• t1111 : State
• tuu01 : State
• t1uu1 : State
• tu1u1 : State
• tuuu1 : State

@[instance_reducible]

instance Franke2011.DisjunctionConjEpistemic.instDecidableEqState : DecidableEq State

Equations

• Franke2011.DisjunctionConjEpistemic.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.DisjunctionConjEpistemic.instFintypeState : Fintype State

Equations

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

@[instance_reducible]

instance Franke2011.DisjunctionConjEpistemic.instReprState : Repr State

Equations

• Franke2011.DisjunctionConjEpistemic.instReprState = { reprPrec := Franke2011.DisjunctionConjEpistemic.instReprState.repr }

def Franke2011.DisjunctionConjEpistemic.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.DisjunctionConjEpistemic.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.DisjunctionConjEpistemic.instMeasurableSpaceState = ⊤

def Franke2011.DisjunctionConjEpistemic.table : State → DisjunctionConj.Message → BeliefValue

This table gives the belief values of (92).

Equations

• Franke2011.DisjunctionConjEpistemic.table x✝ Franke2011.DisjunctionConj.Message.either = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1001 Franke2011.DisjunctionConj.Message.first = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1111 Franke2011.DisjunctionConj.Message.first = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1uu1 Franke2011.DisjunctionConj.Message.first = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t0101 Franke2011.DisjunctionConj.Message.first = Franke2011.BeliefValue.no
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tuu01 Franke2011.DisjunctionConj.Message.first = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tu1u1 Franke2011.DisjunctionConj.Message.first = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tuuu1 Franke2011.DisjunctionConj.Message.first = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t0101 Franke2011.DisjunctionConj.Message.second = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1111 Franke2011.DisjunctionConj.Message.second = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tu1u1 Franke2011.DisjunctionConj.Message.second = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1001 Franke2011.DisjunctionConj.Message.second = Franke2011.BeliefValue.no
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tuu01 Franke2011.DisjunctionConj.Message.second = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1uu1 Franke2011.DisjunctionConj.Message.second = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tuuu1 Franke2011.DisjunctionConj.Message.second = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1111 Franke2011.DisjunctionConj.Message.both = Franke2011.BeliefValue.yes
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1001 Franke2011.DisjunctionConj.Message.both = Franke2011.BeliefValue.no
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t0101 Franke2011.DisjunctionConj.Message.both = Franke2011.BeliefValue.no
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tuu01 Franke2011.DisjunctionConj.Message.both = Franke2011.BeliefValue.no
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.t1uu1 Franke2011.DisjunctionConj.Message.both = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tu1u1 Franke2011.DisjunctionConj.Message.both = Franke2011.BeliefValue.unc
• Franke2011.DisjunctionConjEpistemic.table Franke2011.DisjunctionConjEpistemic.State.tuuu1 Franke2011.DisjunctionConj.Message.both = Franke2011.BeliefValue.unc

noncomputable def Franke2011.DisjunctionConjEpistemic.game : InterpGame State DisjunctionConj.Message

The game of table (92) has flat priors.

Equations

• Franke2011.DisjunctionConjEpistemic.game = Franke2011.ofTable Franke2011.DisjunctionConjEpistemic.table (ProbabilityTheory.uniformOn Set.univ)

theorem Franke2011.DisjunctionConjEpistemic.exists_table_eq_iff (v : DisjunctionConj.Message → BeliefValue) : (∃ (t : State), table t = v) ↔ ∃ (X : Finset TwoDisjuncts.State), X.Nonempty ∧ v = fun (m : DisjunctionConj.Message) => beliefValue X (DisjunctionConj.game.trueStates m)

The states of (92) are the belief-value vectors of the nonempty sets of states of (89) (66).

theorem Franke2011.DisjunctionConjEpistemic.exclusivity : receiverStep game.trueStates (senderChain game.trueStates 1) DisjunctionConj.Message.either = {State.tuu01, State.tuuu1}

With flat priors the chain from the literal sender reads the disjunction as the speaker not believing A ∧ B (Figure 14).

theorem Franke2011.DisjunctionConjEpistemic.exclusivity_of_competencePrior {p : State → ℝ} (hp : CompetencePrior table p) : receiverStepBy game.trueStates p (senderChainBy game.trueStates p 1) DisjunctionConj.Message.either = {State.tuu01}

Under every competence prior the disjunction conveys that the speaker believes A ∧ B false.

theorem Franke2011.DisjunctionConjEpistemic.exclusivity_of_incompetencePrior {p : State → ℝ} (hp : IncompetencePrior table p) : receiverStepBy game.trueStates p (senderChainBy game.trueStates p 1) DisjunctionConj.Message.either = {State.tuuu1}

Under every incompetence prior the disjunction conveys that the speaker is undecided about A ∧ B.

Entailing disjuncts (table (97), Figure 16)

"John or (John and Mary)" (Examples.ex95a) is truth-conditionally "John", yet conveys that the speaker considers Mary's coming possible. With the disjunction nominally costlier than its equivalent and a competent speaker, the chain from the literal receiver reads the disjunction as t[1,u,1].

inductive Franke2011.EntailingDisjuncts.Message : Type

• john : Message
• johnAndMary : Message
• johnOrBoth : Message

@[instance_reducible]

instance Franke2011.EntailingDisjuncts.instDecidableEqMessage : DecidableEq Message

Equations

• Franke2011.EntailingDisjuncts.instDecidableEqMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.EntailingDisjuncts.instFintypeMessage : Fintype Message

Equations

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

@[instance_reducible]

instance Franke2011.EntailingDisjuncts.instReprMessage : Repr Message

Equations

• Franke2011.EntailingDisjuncts.instReprMessage = { reprPrec := Franke2011.EntailingDisjuncts.instReprMessage.repr }

def Franke2011.EntailingDisjuncts.instReprMessage.repr : Message → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.EntailingDisjuncts.instMeasurableSpaceMessage : MeasurableSpace Message

Equations

• Franke2011.EntailingDisjuncts.instMeasurableSpaceMessage = ⊤

def Franke2011.EntailingDisjuncts.table : SomeAllEpistemic.State → Message → BeliefValue

This table gives the belief values of (97).

Equations

• Franke2011.EntailingDisjuncts.table x✝ Franke2011.EntailingDisjuncts.Message.john = Franke2011.BeliefValue.yes
• Franke2011.EntailingDisjuncts.table x✝ Franke2011.EntailingDisjuncts.Message.johnOrBoth = Franke2011.BeliefValue.yes
• Franke2011.EntailingDisjuncts.table Franke2011.SomeAllEpistemic.State.t10 Franke2011.EntailingDisjuncts.Message.johnAndMary = Franke2011.BeliefValue.no
• Franke2011.EntailingDisjuncts.table Franke2011.SomeAllEpistemic.State.t11 Franke2011.EntailingDisjuncts.Message.johnAndMary = Franke2011.BeliefValue.yes
• Franke2011.EntailingDisjuncts.table Franke2011.SomeAllEpistemic.State.t1u Franke2011.EntailingDisjuncts.Message.johnAndMary = Franke2011.BeliefValue.unc

noncomputable def Franke2011.EntailingDisjuncts.game : InterpGame SomeAllEpistemic.State Message

The game of table (97) has flat priors.

Equations

• Franke2011.EntailingDisjuncts.game = Franke2011.ofTable Franke2011.EntailingDisjuncts.table (ProbabilityTheory.uniformOn Set.univ)

def Franke2011.EntailingDisjuncts.cost : Message → ℕ

The disjunction is nominally costlier than its equivalent.

Equations

• Franke2011.EntailingDisjuncts.cost Franke2011.EntailingDisjuncts.Message.johnOrBoth = 1
• Franke2011.EntailingDisjuncts.cost x✝ = 0

theorem Franke2011.EntailingDisjuncts.possibility_of_competencePrior {p : SomeAllEpistemic.State → ℝ} (hp : CompetencePrior table p) : have round := receiverStepBy game.trueStates p ∘ senderStepBy game.trueStates (⇑OrderDual.toDual ∘ cost); round^[2] game.trueStates Message.johnOrBoth = {SomeAllEpistemic.State.t1u} ∧ Function.IsFixedPt round (round^[2] game.trueStates)

Under every competence prior, with costs breaking the sender's ties, the chain from the literal receiver reaches at level 4 a fixed point reading the disjunction as the speaker knowing that John came and being undecided about Mary.

Universal free choice (tables (101)–(102), Figure 17)

"Everybody may take an apple or a pear" (Examples.ex99) with alternatives "everybody may take an apple" and "everybody may take a pear": the full game reads the sentence as a mixed group, and pruning the mixed state by group homogeneity restores universal free choice.

inductive Franke2011.GroupPermission.State : Type

States are named by truth vectors over (∀◇A, ∀◇B, ∀◇(A ∨ B)).

• t101 : State
• t011 : State
• t111 : State
• t001 : State

@[instance_reducible]

instance Franke2011.GroupPermission.instDecidableEqState : DecidableEq State

Equations

• Franke2011.GroupPermission.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Franke2011.GroupPermission.instFintypeState : Fintype State

Equations

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

def Franke2011.GroupPermission.instReprState.repr : State → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Franke2011.GroupPermission.instReprState : Repr State

Equations

• Franke2011.GroupPermission.instReprState = { reprPrec := Franke2011.GroupPermission.instReprState.repr }

@[instance_reducible]

instance Franke2011.GroupPermission.instMeasurableSpaceState : MeasurableSpace State

Equations

• Franke2011.GroupPermission.instMeasurableSpaceState = ⊤

def Franke2011.GroupPermission.table : State → TwoDisjuncts.Message → BeliefValue

This table gives the truth values of (101).

Equations

• Franke2011.GroupPermission.table x✝ Franke2011.TwoDisjuncts.Message.either = Franke2011.BeliefValue.yes
• Franke2011.GroupPermission.table Franke2011.GroupPermission.State.t101 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.yes
• Franke2011.GroupPermission.table Franke2011.GroupPermission.State.t111 Franke2011.TwoDisjuncts.Message.first = Franke2011.BeliefValue.yes
• Franke2011.GroupPermission.table Franke2011.GroupPermission.State.t011 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.yes
• Franke2011.GroupPermission.table Franke2011.GroupPermission.State.t111 Franke2011.TwoDisjuncts.Message.second = Franke2011.BeliefValue.yes
• Franke2011.GroupPermission.table x✝¹ x✝ = Franke2011.BeliefValue.no

noncomputable def Franke2011.GroupPermission.game : InterpGame State TwoDisjuncts.Message

The game of table (101) has flat priors.

Equations

• Franke2011.GroupPermission.game = Franke2011.ofTable Franke2011.GroupPermission.table (ProbabilityTheory.uniformOn Set.univ)

noncomputable def Franke2011.GroupPermission.pruned : InterpGame { t : State // t ≠ State.t001 } TwoDisjuncts.Message

The pruned game (102) drops the mixed state.

Equations

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

theorem Franke2011.GroupPermission.mixed_group : receiverStep game.trueStates (senderChain game.trueStates 0) TwoDisjuncts.Message.either = {State.t001} ∧ Function.IsFixedPt (senderStep game.trueStates ∘ receiverStep game.trueStates) (senderChain game.trueStates 1)

The full game reads the sentence as a mixed group (Figure 17).

theorem Franke2011.GroupPermission.universal_free_choice : receiverStep pruned.trueStates (senderChain pruned.trueStates 1) TwoDisjuncts.Message.either = {⟨State.t111, universal_free_choice._proof_1⟩}

Pruned, the sentence conveys that everybody may take either (102).

The heavy system (Appendix B.1)

Player types are still sets of pure strategies, and an unbiased belief in a type is uniform over it ((115), (118)): the kernel unbiased X sends each argument to the uniform measure on the choices of X. Under matching utility the expected utility of sending m in t is the probability that the receiver guesses t after m (129), so a level-k + 1 sender maximises that probability among the true messages ((116), (117)). The receiver maximises the posterior, which is the prior times the probability of the message up to normalisation ((119)–(121)), and reads a message no state sends literally (122).

noncomputable def Franke2011.unbiased {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] (X : α → Finset γ) : ProbabilityTheory.Kernel α γ

The unbiased belief in a player type X is uniform, at each argument, over the choices the type allows ((115), (118)).

Equations

• Franke2011.unbiased X = ProbabilityTheory.Kernel.ofFunOfCountable fun (a : α) => ProbabilityTheory.uniformOn ↑(X a)

instance Franke2011.instIsFiniteKernelUnbiased {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] (X : α → Finset γ) : ProbabilityTheory.IsFiniteKernel (unbiased X)

theorem Franke2011.unbiased_apply_singleton {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] (a : α) (c : γ) : ((unbiased X) a) {c} = if c ∈ X a then (↑(X a).card)⁻¹ else 0

theorem Franke2011.unbiased_real_singleton {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] (a : α) (c : γ) : ((unbiased X) a).real {c} = if c ∈ X a then (↑(X a).card)⁻¹ else 0

theorem Franke2011.unbiased_real_of_mem {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] {a : α} {c : γ} (h : c ∈ X a) : ((unbiased X) a).real {c} = (↑(X a).card)⁻¹

theorem Franke2011.unbiased_real_of_notMem {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] {a : α} {c : γ} (h : c ∉ X a) : ((unbiased X) a).real {c} = 0

theorem Franke2011.unbiased_real_pos_iff {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] {a : α} {c : γ} : 0 < ((unbiased X) a).real {c} ↔ c ∈ X a

theorem Franke2011.sum_unbiased_real {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] [Fintype γ] (a : α) : ∑ c : γ, ((unbiased X) a).real {c} = if (X a).Nonempty then 1 else 0

The unbiased belief at an argument is a probability over the choices when the type allows one, and zero otherwise.

theorem Franke2011.sum_unbiased_real_le_one {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] [Fintype γ] (a : α) : ∑ c : γ, ((unbiased X) a).real {c} ≤ 1

theorem Franke2011.sum_unbiased_real_mul_of_eq_argmax {α : Type u_1} {γ : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] [MeasurableSpace γ] {X : α → Finset γ} [MeasurableSingletonClass γ] [DecidableEq γ] {a : α} [Fintype γ] {s : Finset γ} {f : γ → ℝ} (hX : X a = s.argmax f) {c₀ : γ} (h : c₀ ∈ s.argmax f) : ∑ c : γ, ((unbiased X) a).real {c} * f c = f c₀

Under the unbiased belief in a type choosing the maximisers of f on s, the expectation of f is its maximum.

theorem Franke2011.inverse_trueStates {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [MeasurableSpace T] (G : InterpGame T M) : inverse G.trueStates = G.trueMessages

noncomputable def Franke2011.senderResponse {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] [MeasurableSpace M] [MeasurableSingletonClass M] (G : InterpGame T M) (R : M → Finset T) (t : T) : Finset M

The level-k + 1 sender type from the level-k receiver type R keeps, in each state, the true messages after which the receiver is likeliest to guess it ((116), (117)).

Equations

• Franke2011.senderResponse G R t = (G.trueMessages t).argmax fun (m : M) => ((Franke2011.unbiased R) m).real {t}

noncomputable def Franke2011.receiverResponse {T : Type u_1} {M : Type u_2} [Fintype T] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] (G : InterpGame T M) (S : T → Finset M) (m : M) : Finset T

The level-k + 1 receiver type from the level-k sender type S keeps, after each message, the states of greatest posterior probability ((119)–(121)); a message no state sends is read literally (122).

Equations

• Franke2011.receiverResponse G S m = if Franke2011.inverse S m = ∅ then G.trueStates m else Finset.univ.argmax fun (t : T) => G.prior.real {t} * ((Franke2011.unbiased S) t).real {m}

noncomputable def Franke2011.receiverLevel {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] (G : InterpGame T M) (n : ℕ) : M → Finset T

receiverLevel G n is the receiver type R₂ₙ of the heavy chain from the literal receiver.

Equations

• Franke2011.receiverLevel G n = (Franke2011.receiverResponse G ∘ Franke2011.senderResponse G)^[n] G.trueStates

noncomputable def Franke2011.senderLevel {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] (G : InterpGame T M) (n : ℕ) : T → Finset M

senderLevel G n is the sender type S₂ₙ of the heavy chain from the literal sender.

Equations

• Franke2011.senderLevel G n = (Franke2011.senderResponse G ∘ Franke2011.receiverResponse G)^[n] G.trueMessages

noncomputable def Franke2011.expectedGain {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] (G : InterpGame T M) (S : T → Finset M) (R : M → Finset T) : ℝ

The expected gain (144) of a sender and a receiver type is the probability of successful communication under the unbiased beliefs in them: the prior expectation of the probability that the receiver guesses the state.

Equations

• Franke2011.expectedGain G S R = ∫ (t : T), (((Franke2011.unbiased R).comp (Franke2011.unbiased S)) t).real {t} ∂G.prior

theorem Franke2011.expectedGain_eq_sum {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] (G : InterpGame T M) [MeasureTheory.IsFiniteMeasure G.prior] (S : T → Finset M) (R : M → Finset T) : expectedGain G S R = ∑ t : T, G.prior.real {t} * ∑ m : M, ((unbiased S) t).real {m} * ((unbiased R) m).real {t}

def Franke2011.NearFlat {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] (G : InterpGame T M) : Prop

Under the near-flat condition (132), stated with the inequality its proof needs, prior ratios stay above (|M| - 1)/|M|.

Equations

• Franke2011.NearFlat G = ∀ (t t' : T), (↑(Fintype.card M) - 1) * G.prior.real {t'} < ↑(Fintype.card M) * G.prior.real {t}

theorem Franke2011.mem_senderResponse {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} {R : M → Finset T} {t : T} {m : M} : m ∈ senderResponse G R t ↔ G.meaning m t ∧ ∀ (m' : M), G.meaning m' t → ((unbiased R) m').real {t} ≤ ((unbiased R) m).real {t}

theorem Franke2011.senderResponse_subset {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} (R : M → Finset T) (t : T) : senderResponse G R t ⊆ G.trueMessages t

theorem Franke2011.receiverResponse_subset_inverse {T : Type u_1} {M : Type u_2} [Fintype T] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) {S : T → Finset M} {m : M} (hm : inverse S m ≠ ∅) : receiverResponse G S m ⊆ inverse S m

With positive priors the receiver only chooses states that send the message.

theorem Franke2011.receiverResponse_subset {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) {S : T → Finset M} (hS : ∀ (t : T), S t ⊆ G.trueMessages t) (m : M) : receiverResponse G S m ⊆ G.trueStates m

A receiver who believes every message sent true only assigns true interpretations (Lemma 2).

Theorems 1 and 2: the light system is the heavy system with flat or near-flat priors

theorem Franke2011.senderResponse_eq_senderStep {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} {R : M → Finset T} (hR : ∀ (m : M), R m ⊆ G.trueStates m) : senderResponse G R = senderStep G.trueStates R

Against the unbiased belief in a receiver type that respects truth, the heavy sender is the light sender (76), since the probability of being understood is one over the number of interpretations (129).

theorem Franke2011.argmax_prior_mul_uniform_of_nearFlat {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hnf : NearFlat G) {S : T → Finset M} {m : M} (hne : inverse S m ≠ ∅) : (Finset.univ.argmax fun (t : T) => G.prior.real {t} * ((unbiased S) t).real {m}) = ((inverse S m).argmin fun (t : T) => (S t).card).argmax fun (t : T) => G.prior.real {t}

Under near-flat priors the states maximising the prior times the probability of sending m are the most probable of the light receiver's states, since sending fewer messages outweighs any difference in prior.

theorem Franke2011.receiverResponse_eq_receiverStepBy {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hnf : NearFlat G) : receiverResponse G = receiverStepBy G.trueStates fun (t : T) => G.prior.real {t}

Under near-flat priors the heavy receiver is the light receiver refined by the prior (Theorem 2).

theorem Franke2011.nearFlat_of_forall_eq {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hflat : ∀ (t t' : T), G.prior {t} = G.prior {t'}) : NearFlat G

theorem Franke2011.receiverResponse_eq_receiverStep {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hflat : ∀ (t t' : T), G.prior {t} = G.prior {t'}) : receiverResponse G = receiverStep G.trueStates

Under flat priors the heavy receiver is the light receiver (77).

theorem Franke2011.receiverLevel_eq_receiverChainBy {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hnf : NearFlat G) (n : ℕ) : receiverLevel G n = receiverChainBy G.trueStates (fun (t : T) => G.prior.real {t}) n

Under near-flat priors the receiver chain of the heavy system is the light chain refined by the prior (Theorem 2).

theorem Franke2011.senderLevel_eq_senderChainBy {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hnf : NearFlat G) (n : ℕ) : senderLevel G n = senderChainBy G.trueStates (fun (t : T) => G.prior.real {t}) n

Under near-flat priors the sender chain of the heavy system is the light chain with its receivers refined by the prior (Theorem 2).

theorem Franke2011.receiverLevel_eq_receiverChain {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hflat : ∀ (t t' : T), G.prior {t} = G.prior {t'}) (n : ℕ) : receiverLevel G n = receiverChain G.trueStates n

Under flat priors the heavy chains are the light chains (Theorem 1).

theorem Franke2011.senderLevel_eq_senderChain {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (hflat : ∀ (t t' : T), G.prior {t} = G.prior {t'}) (n : ℕ) : senderLevel G n = senderChain G.trueStates n

Lemma 3 and Theorem 3: convergence (Appendix B.4)

Expected gain never decreases along a chain: the sender step averages the receiver's probability of the true state over its maximisers, and the receiver step averages the posterior weight over its maximisers. A chain lives in a finite type, so it cycles; on a cycle the gain is constant, so the sender's choices only grow around it, hence stay put, and the chain has reached a fixed point.

theorem Franke2011.expectedGain_le_senderResponse {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] {S : T → Finset M} (hS : ∀ (t : T), S t ⊆ G.trueMessages t) (R : M → Finset T) : expectedGain G S R ≤ expectedGain G (senderResponse G R) R

A level-k + 1 sender does at least as well against R as any truthful sender type (Lemma 3 (i)).

theorem Franke2011.expectedGain_le_receiverResponse {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (S : T → Finset M) (R : M → Finset T) : expectedGain G S R ≤ expectedGain G S (receiverResponse G S)

A level-k + 1 receiver does at least as well against S as any receiver type (Lemma 3 (ii)).

theorem Franke2011.senderResponse_subset_of_expectedGain_eq {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) {R₁ R₂ : M → Finset T} (h : expectedGain G (senderResponse G R₁) R₂ = expectedGain G (senderResponse G R₂) R₂) (t : T) : senderResponse G R₁ t ⊆ senderResponse G R₂ t

If the sender's response to R₁ does as well against R₂ as the response to R₂, then every message the first sends the second sends too.

theorem Franke2011.exists_isFixedPt_iterate {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) (R : M → Finset T) : ∃ (n : ℕ), Function.IsFixedPt (receiverResponse G ∘ senderResponse G) ((receiverResponse G ∘ senderResponse G)^[n] R)

Every chain of the heavy system reaches a fixed point (Theorem 3).

theorem Franke2011.exists_isFixedPt_receiverLevel {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) : ∃ (n : ℕ), Function.IsFixedPt (receiverResponse G ∘ senderResponse G) (receiverLevel G n)

The receiver chain of the heavy system reaches a fixed point (Theorem 3).

theorem Franke2011.exists_isFixedPt_senderLevel {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) : ∃ (n : ℕ), Function.IsFixedPt (senderResponse G ∘ receiverResponse G) (senderLevel G n)

The sender chain of the heavy system reaches a fixed point (Theorem 3).

theorem Franke2011.receiverLevel_ofTable_of_competencePrior {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {table : T → M → BeliefValue} {p : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure p] (hp : CompetencePrior table fun (t : T) => p.real {t}) (hpos : ∀ (t : T), p {t} ≠ 0) (hnf : NearFlat (ofTable table p)) (n : ℕ) : receiverLevel (ofTable table p) n = receiverChainBy (ofTable table p).trueStates (⇑OrderDual.toDual ∘ uncertaintyCount table) n

Under a competence prior that is nearly flat, the heavy receiver chain is the light chain refined by fewest undecided alternatives, so the competence results below are predictions of the heavy system.

Theorem 4: fixed points are perfect Bayesian equilibria

structure Franke2011.IsPBE {T : Type u_1} {M : Type u_2} [Fintype T] [MeasurableSpace T] [MeasurableSpace M] (G : InterpGame T M) (σ : ProbabilityTheory.Kernel T M) (ρ : ProbabilityTheory.Kernel M T) (μ : M → MeasureTheory.Measure T) : Prop

A sender strategy σ, a receiver strategy ρ and posterior beliefs μ form a perfect Bayesian equilibrium when every message σ sends maximises, among all messages, the probability that the receiver guesses the sender's state, every interpretation ρ chooses is a most probable state under μ, and μ conditions the prior on σ after every message that is sent with positive probability.

• sender_rational (t : T) (m : M) : 0 < (σ t).real {m} → ∀ (m' : M), (ρ m').real {t} ≤ (ρ m).real {t}
• receiver_rational (m : M) (t : T) : 0 < (ρ m).real {t} → t ∈ Finset.univ.argmax fun (t' : T) => (μ m).real {t'}
• isProbabilityMeasure (m : M) : MeasureTheory.IsProbabilityMeasure (μ m)
• consistent (m : M) : (G.prior.bind ⇑σ) {m} ≠ 0 → ∀ (t : T), (μ m).real {t} = G.prior.real {t} * (σ t).real {m} / (G.prior.bind ⇑σ).real {m}

theorem Franke2011.exists_isPBE_of_isFixedPt {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace M] [MeasurableSingletonClass M] {G : InterpGame T M} [Nonempty T] [MeasureTheory.IsFiniteMeasure G.prior] (hprior : ∀ (t : T), G.prior {t} ≠ 0) {R : M → Finset T} (hR : Function.IsFixedPt (receiverResponse G ∘ senderResponse G) R) : ∃ (μ : M → MeasureTheory.Measure T), IsPBE G (unbiased (senderResponse G R)) (unbiased R) μ

The unbiased beliefs in a fixed point of the heavy system form a perfect Bayesian equilibrium, with the Bayesian posterior after every message sent and the literal reading after the others (Theorem 4).

theorem Franke2011.exists_isFixedPt_receiverChain {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) : ∃ (n : ℕ), Function.IsFixedPt (receiverStep den ∘ senderStep den) (receiverChain den n)

Counting reasoning reaches a fixed point along the chain from the literal receiver, for every denotation (Theorems 1 and 3), as the heavy chain of a flat prior.

theorem Franke2011.exists_isFixedPt_senderChain {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] (den : M → Finset T) : ∃ (n : ℕ), Function.IsFixedPt (senderStep den ∘ receiverStep den) (senderChain den n)

Counting reasoning reaches a fixed point along the chain from the literal sender, for every denotation (Theorems 1 and 3), as the heavy chain of a flat prior.

The free choice implicature in the heavy system (Appendix B.3)

theorem Franke2011.TwoDisjuncts.receiverLevel_free_choice : receiverLevel game 1 Message.either = {State.onlyA, State.onlyB, State.both} ∧ receiverLevel game 2 = fun (m : Message) => {freeChoiceReceiver m}

With the flat priors of Figure 5 the heavy system's second receiver reads the disjunction literally (137) and its fourth reads it as free choice (139).

Level-1 interpretation and exhaustification by minimal models (§10)

The first sophisticated receiver of the chain from the literal sender keeps the states where a message is true that make fewest messages true (107); exhaustification by minimal models keeps those minimal in the inclusion order on true messages.

def Franke2011.alternatives {T : Type u_1} {M : Type u_2} [MeasurableSpace T] (G : InterpGame T M) : Set (Set T)

The alternatives of an interpretation game are the sets of states where its messages are true.

Equations

• Franke2011.alternatives G = Set.range fun (m : M) => {t : T | G.meaning m t}

theorem Franke2011.leALT_alternatives_iff {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] {G : InterpGame T M} {t' t : T} : Exhaustification.leALT (alternatives G) t' t ↔ G.trueMessages t' ⊆ G.trueMessages t

theorem Franke2011.ltALT_alternatives_iff {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] {G : InterpGame T M} {t' t : T} : Exhaustification.ltALT (alternatives G) t' t ↔ G.trueMessages t' ⊂ G.trueMessages t

theorem Franke2011.mem_exhMW_alternatives {T : Type u_1} {M : Type u_2} [Fintype M] [MeasurableSpace T] {G : InterpGame T M} {m : M} {t : T} : t ∈ Exhaustification.exhMW (alternatives G) {t : T | G.meaning m t} ↔ G.meaning m t ∧ ∀ (t' : T), G.meaning m t' → ¬G.trueMessages t' ⊂ G.trueMessages t

theorem Franke2011.coe_receiverStep_subset_exhMW {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq T] [DecidableEq M] [MeasurableSpace T] {G : InterpGame T M} (m : M) : ↑(receiverStep G.trueStates (inverse G.trueStates) m) ⊆ Exhaustification.exhMW (alternatives G) {t : T | G.meaning m t}

The first sophisticated receiver's reading of a message entails its exhaustification by minimal models (Fact 1).

theorem Franke2011.TwoDisjuncts.exhMW_eq_receiverStep (m : Message) : Exhaustification.exhMW (alternatives game) {t : State | game.meaning m t} = ↑(receiverStep game.trueStates (inverse game.trueStates) m)

In the free choice game exhaustification by minimal models is the first sophisticated receiver's reading, as footnote 37 says of all the examples, and not the second's (§10, Figure 7).

theorem Franke2011.TwoDisjuncts.exhMW_ne_receiverChain : Exhaustification.exhMW (alternatives game) {t : State | game.meaning Message.either t} ≠ ↑(receiverChain game.trueStates 1 Message.either)

Comparison of exhaustivity operators (Appendix A)

Exhaustification by minimal models entails innocent exclusion (Fact 3, Exhaustification.exhMW_subset_exhIE). Fact 2 claims that the order on worlds, hence exhaustification by minimal models, is invariant under adding an alternative whose truth value the others determine; this holds when the determination is monotone, as for conjunctions in the paper's example, and fails for the negation of an alternative.

def Franke2011.MonotoneDetermined {W : Type u_1} (ALT : Set (Set W)) (A : Set W) : Prop

A is monotonically determined by the alternatives when, whenever every alternative true at w is true at v, A at w forces A at v.

Equations

• Franke2011.MonotoneDetermined ALT A = ∀ (w v : W), Exhaustification.leALT ALT w v → w ∈ A → v ∈ A

theorem Franke2011.ltALT_insert_of_monotoneDetermined {W : Type u_1} (ALT : Set (Set W)) {A : Set W} (hA : MonotoneDetermined ALT A) : Exhaustification.ltALT (insert A ALT) = Exhaustification.ltALT ALT

Adding a monotonically determined alternative leaves the order on worlds unchanged (Fact 2).

theorem Franke2011.exhMW_insert_of_monotoneDetermined {W : Type u_1} (ALT : Set (Set W)) (φ : Set W) {A : Set W} (hA : MonotoneDetermined ALT A) : Exhaustification.exhMW (insert A ALT) φ = Exhaustification.exhMW ALT φ

Exhaustification by minimal models ignores a monotonically determined alternative.

theorem Franke2011.not_ltALT_insert_compl : Exhaustification.ltALT {fun (x : Bool) => x = true} false true ∧ ¬Exhaustification.ltALT {fun (x : Bool) => x = false, fun (x : Bool) => x = true} false true

Fact 2 as printed fails. Over two worlds with one alternative, adding its negation, which the alternative determines but not monotonically, removes the strict order between them.

def Franke2011.Indistinguishable {W : Type u_1} (ALT : Set (Set W)) (X : Set W) (w : W) : Prop

A world is indistinguishable from a set of worlds by the alternatives when every alternative true throughout the set is true at it and every alternative false throughout the set is false at it.

Equations

• Franke2011.Indistinguishable ALT X w = ∀ a ∈ ALT, (X ⊆ a → w ∈ a) ∧ (X ⊆ aᶜ → w ∉ a)

theorem Franke2011.exhIE_eq_setOf_indistinguishable {W : Type u_1} (ALT : Set (Set W)) (φ : Set W) (hfin : ALT.Finite) : Exhaustification.exhIE ALT φ = {w : W | w ∈ φ ∧ Indistinguishable ALT (Exhaustification.exhMW ALT φ) w}

With finitely many alternatives, innocent exclusion keeps the prejacent worlds that the alternatives cannot distinguish from the minimal worlds (Lemma 1).

The paper's example (108)–(113): "A or B" with and without the conjunctive alternative.

def Franke2011.DisjunctionOperators.A : Set (Bool × Bool)

A world is a pair of truth values for A and B, and A is the set of worlds where the first is true.

Equations

• Franke2011.DisjunctionOperators.A = {w : Bool × Bool | w.1 = true}

def Franke2011.DisjunctionOperators.B : Set (Bool × Bool)

B is the set of worlds where the second truth value is true.

Equations

• Franke2011.DisjunctionOperators.B = {w : Bool × Bool | w.2 = true}

def Franke2011.DisjunctionOperators.alt₁ : Set (Set (Bool × Bool))

These are the alternatives (109a).

Equations

• Franke2011.DisjunctionOperators.alt₁ = {Franke2011.DisjunctionOperators.A, Franke2011.DisjunctionOperators.B, Franke2011.DisjunctionOperators.A ∪ Franke2011.DisjunctionOperators.B}

def Franke2011.DisjunctionOperators.alt₂ : Set (Set (Bool × Bool))

The alternatives (109b) add the conjunction.

Equations

• Franke2011.DisjunctionOperators.alt₂ = insert (Franke2011.DisjunctionOperators.A ∩ Franke2011.DisjunctionOperators.B) Franke2011.DisjunctionOperators.alt₁

theorem Franke2011.DisjunctionOperators.exhMW_alt₁ : Exhaustification.exhMW alt₁ (A ∪ B) = {(true, false), (false, true)}

theorem Franke2011.DisjunctionOperators.exhMW_alt₂ : Exhaustification.exhMW alt₂ (A ∪ B) = Exhaustification.exhMW alt₁ (A ∪ B)

theorem Franke2011.DisjunctionOperators.exhaustivity_operators : Exhaustification.exhMW alt₁ (A ∪ B) = Exhaustification.exhMW alt₂ (A ∪ B) ∧ Exhaustification.exhMW alt₂ (A ∪ B) = Exhaustification.exhIE alt₂ (A ∪ B) ∧ Exhaustification.exhIE alt₂ (A ∪ B) ⊂ Exhaustification.exhIE alt₁ (A ∪ B)

The minimal-models exhaustifier does not see the conjunctive alternative and agrees with innocent exclusion over the larger set, while innocent exclusion over the smaller set excludes nothing (113).