Potts and Levy (2015): Negotiating Lexical Uncertainty and Speaker Expertise with Disjunction

This file formalizes the lexical-uncertainty model of Potts and Levy and its Hurfordian context. Disjunctions A or X whose disjunct X covers A violate the generalization of Hurford yet are used, and the listener who hears one infers both that the speaker is uncertain between the disjuncts and that her lexicon keeps them apart. The model is a rational-speech-acts tower over states, messages, and lexica (§3). A literal listener conditions a flat prior on a message's extension under a lexicon (10), a speaker chooses messages by the listener's mass at the state under a rationality and a cost (11), and a pragmatic listener inverts the speaker (12) (L0, S1, l1); the lexical-uncertainty listener infers state and lexicon jointly (14) (L1), the expertise speaker weighs the world information and the lexicon information a message carries (15) (S2), the next listener inverts her (L2), and marginalization recovers simple signaling (16), (17) (S2exp). The state space is closed under joins so that a disjunction can convey uncertainty, a join state satisfying a message when all its atoms do (§4, Figure 6), and the lexica refine the unknown term X (13) (World, Msg, Lex, sem).

In the Hurfordian context of §5.2, three atoms, the terms A, B, X with their disjunctions, and the lexica reading X as the general term, its exclusivization, or the synonym of A, at the paper's rationality α = 2 and lexicon weight β = 1, with the disjunction cost free: the level-one listener hearing A or X ranks the uncertain state first and the exclusivized lexicon first (l1_uncertainty, l1_lexicon), the exclusivizing speaker uses the disjunction exactly when uncertain (s1_disjunction_iff_uncertain), the disjunction signals exclusivization where the bare disjunct does not (AorX_signals_excl), and the expertise speaker who is uncertain and exclusivizes prefers the disjunction to every other message, the paper's production claim for this context (s2_prefers_disjunction, s2exp_uncertain). Each ordering is stated on a range of disjunction costs containing the paper's 1.

Implementation notes

The agents are kernels of Pragmatics/RSA, the speakers power-weight kernels and the listeners Bayesian inverses against uniform priors; the expertise speaker is a weight kernel built from the fixed-lexicon listener and the lexicon posterior. The paper's speakers subtract the cost outside the rationality, so it enters the substrate speaker divided by α. Listener preferences reduce to speaker preferences (l1_real_lt_iff, L1_fst_real_lt_iff, S2_real_lt_iff), and a speaker's share is a rational function of the cost factor exp (−c), so each ordering is a polynomial inequality in it certified by its Bernstein coefficients on the stated range. The definitional regime of §5.1, which needs β > α, and the parameter exploration of §5.4 are not formalized.

TODO

The level-two readings of Figure 10, the listener L2 hearing A or X ranking the uncertain state and the exclusivized lexicon first, and the marginal speaker S2exp preferring the bare A when certain of the first atom, are rational inequalities in the cost factor of very high degree whose symbolic certificates are out of reach; the paper reports them numerically at cost 1.

References

• [PL15]
• [Hur74]

The domain (§4, §5)

inductive PottsLevy2015.Atom : Type

The three atomic states of the context.

• w₁ : Atom
• w₂ : Atom
• w₃ : Atom

@[instance_reducible]

instance PottsLevy2015.instDecidableEqAtom : DecidableEq Atom

Equations

• PottsLevy2015.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsLevy2015.instFintypeAtom : Fintype Atom

Equations

• PottsLevy2015.instFintypeAtom = { elems := { val := ↑PottsLevy2015.Atom.enumList, nodup := PottsLevy2015.Atom.enumList_nodup }, complete := PottsLevy2015.instFintypeAtom._proof_1 }

inductive PottsLevy2015.World : Type

The states are the nonempty joins of the atoms (Figure 6).

• w₁ : World
• w₂ : World
• w₃ : World
• w₁₂ : World
• w₁₃ : World
• w₂₃ : World
• w₁₂₃ : World

@[instance_reducible]

instance PottsLevy2015.instDecidableEqWorld : DecidableEq World

Equations

• PottsLevy2015.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsLevy2015.instFintypeWorld : Fintype World

Equations

• PottsLevy2015.instFintypeWorld = { elems := { val := ↑PottsLevy2015.World.enumList, nodup := PottsLevy2015.World.enumList_nodup }, complete := PottsLevy2015.instFintypeWorld._proof_1 }

instance PottsLevy2015.instNonemptyWorld : Nonempty World

@[instance_reducible]

instance PottsLevy2015.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• PottsLevy2015.instMeasurableSpaceWorld = ⊤

def PottsLevy2015.World.atoms : World → Finset Atom

The atoms a state joins.

Equations

• PottsLevy2015.World.w₁.atoms = {PottsLevy2015.Atom.w₁}
• PottsLevy2015.World.w₂.atoms = {PottsLevy2015.Atom.w₂}
• PottsLevy2015.World.w₃.atoms = {PottsLevy2015.Atom.w₃}
• PottsLevy2015.World.w₁₂.atoms = {PottsLevy2015.Atom.w₁, PottsLevy2015.Atom.w₂}
• PottsLevy2015.World.w₁₃.atoms = {PottsLevy2015.Atom.w₁, PottsLevy2015.Atom.w₃}
• PottsLevy2015.World.w₂₃.atoms = {PottsLevy2015.Atom.w₂, PottsLevy2015.Atom.w₃}
• PottsLevy2015.World.w₁₂₃.atoms = {PottsLevy2015.Atom.w₁, PottsLevy2015.Atom.w₂, PottsLevy2015.Atom.w₃}

inductive PottsLevy2015.Msg : Type

The messages are the basic terms, their disjunctions, and the null message.

• A : Msg
• B : Msg
• X : Msg
• AorB : Msg
• AorX : Msg
• BorX : Msg
• AorBorX : Msg
• null : Msg

@[instance_reducible]

instance PottsLevy2015.instDecidableEqMsg : DecidableEq Msg

Equations

• PottsLevy2015.instDecidableEqMsg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsLevy2015.instFintypeMsg : Fintype Msg

Equations

• PottsLevy2015.instFintypeMsg = { elems := { val := ↑PottsLevy2015.Msg.enumList, nodup := PottsLevy2015.Msg.enumList_nodup }, complete := PottsLevy2015.instFintypeMsg._proof_1 }

instance PottsLevy2015.instNonemptyMsg : Nonempty Msg

@[instance_reducible]

instance PottsLevy2015.instMeasurableSpaceMsg : MeasurableSpace Msg

Equations

• PottsLevy2015.instMeasurableSpaceMsg = ⊤

def PottsLevy2015.Msg.IsDisjunction : Msg → Prop

Whether a message is a disjunction, the messages that carry a cost.

Equations

• PottsLevy2015.Msg.AorB.IsDisjunction = True
• PottsLevy2015.Msg.AorX.IsDisjunction = True
• PottsLevy2015.Msg.BorX.IsDisjunction = True
• PottsLevy2015.Msg.AorBorX.IsDisjunction = True
• x✝.IsDisjunction = False

@[instance_reducible]

instance PottsLevy2015.instDecidablePredMsgIsDisjunction : DecidablePred Msg.IsDisjunction

Equations

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

inductive PottsLevy2015.Lex : Type

The lexica (13) are the base lexicon reading X as the general term over the first two atoms, its exclusivization to the second atom, and the synonym of A.

• base : Lex
• excl : Lex
• syn : Lex

@[instance_reducible]

instance PottsLevy2015.instDecidableEqLex : DecidableEq Lex

Equations

• PottsLevy2015.instDecidableEqLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsLevy2015.instFintypeLex : Fintype Lex

Equations

• PottsLevy2015.instFintypeLex = { elems := { val := ↑PottsLevy2015.Lex.enumList, nodup := PottsLevy2015.Lex.enumList_nodup }, complete := PottsLevy2015.instFintypeLex._proof_1 }

instance PottsLevy2015.instNonemptyLex : Nonempty Lex

@[instance_reducible]

instance PottsLevy2015.instMeasurableSpaceLex : MeasurableSpace Lex

Equations

• PottsLevy2015.instMeasurableSpaceLex = ⊤

def PottsLevy2015.Lex.x : Lex → Finset Atom

The atoms X denotes under a lexicon.

Equations

• PottsLevy2015.Lex.base.x = {PottsLevy2015.Atom.w₁, PottsLevy2015.Atom.w₂}
• PottsLevy2015.Lex.excl.x = {PottsLevy2015.Atom.w₂}
• PottsLevy2015.Lex.syn.x = {PottsLevy2015.Atom.w₁}

def PottsLevy2015.atomDen (l : Lex) : Msg → Finset Atom

Under a lexicon A denotes the first atom, B the second, a disjunction the union, and the null message every atom.

Equations

• PottsLevy2015.atomDen l PottsLevy2015.Msg.A = {PottsLevy2015.Atom.w₁}
• PottsLevy2015.atomDen l PottsLevy2015.Msg.B = {PottsLevy2015.Atom.w₂}
• PottsLevy2015.atomDen l PottsLevy2015.Msg.X = l.x
• PottsLevy2015.atomDen l PottsLevy2015.Msg.AorB = {PottsLevy2015.Atom.w₁, PottsLevy2015.Atom.w₂}
• PottsLevy2015.atomDen l PottsLevy2015.Msg.AorX = {PottsLevy2015.Atom.w₁} ∪ l.x
• PottsLevy2015.atomDen l PottsLevy2015.Msg.BorX = {PottsLevy2015.Atom.w₂} ∪ l.x
• PottsLevy2015.atomDen l PottsLevy2015.Msg.AorBorX = {PottsLevy2015.Atom.w₁, PottsLevy2015.Atom.w₂} ∪ l.x
• PottsLevy2015.atomDen l PottsLevy2015.Msg.null = Finset.univ

def PottsLevy2015.sem (l : Lex) (m : Msg) : Finset World

In the join-closed state space, a message is true of the states all of whose atoms it denotes.

Equations

• PottsLevy2015.sem l m = {w : PottsLevy2015.World | w.atoms ⊆ PottsLevy2015.atomDen l m}

theorem PottsLevy2015.lexica_facts : Disjoint (atomDen Lex.excl Msg.A) (atomDen Lex.excl Msg.X) ∧ atomDen Lex.syn Msg.AorX = atomDen Lex.syn Msg.A ∧ ∀ (m : Msg), World.w₁₂ ∈ sem Lex.excl m ↔ m = Msg.AorX ∨ m = Msg.AorB ∨ m = Msg.AorBorX ∨ m = Msg.null

Under the exclusivized lexicon A and X are disjoint, the Hurford rescue; under the synonym lexicon A or X is A, the Hurford violation; and under the exclusivized lexicon the uncertain state satisfies exactly the disjunctions containing A and the null message.

theorem PottsLevy2015.sem_nonempty (l : Lex) (m : Msg) : ∃ (w : World), w ∈ sem l m

Every message is true at some state under every lexicon.

def PottsLevy2015.semCard : Lex → Msg → ℕ

The null message is true of seven states, a message denoting two atoms of three, and any other message of one.

Equations

• PottsLevy2015.semCard x✝ PottsLevy2015.Msg.null = 7
• PottsLevy2015.semCard x✝ PottsLevy2015.Msg.AorB = 3
• PottsLevy2015.semCard x✝ PottsLevy2015.Msg.AorBorX = 3
• PottsLevy2015.semCard PottsLevy2015.Lex.base PottsLevy2015.Msg.X = 3
• PottsLevy2015.semCard PottsLevy2015.Lex.base PottsLevy2015.Msg.AorX = 3
• PottsLevy2015.semCard PottsLevy2015.Lex.base PottsLevy2015.Msg.BorX = 3
• PottsLevy2015.semCard PottsLevy2015.Lex.excl PottsLevy2015.Msg.AorX = 3
• PottsLevy2015.semCard PottsLevy2015.Lex.syn PottsLevy2015.Msg.BorX = 3
• PottsLevy2015.semCard x✝¹ x✝ = 1

theorem PottsLevy2015.card_sem (l : Lex) (m : Msg) : (sem l m).card = semCard l m

The tower (§3)

def PottsLevy2015.cost (c : ℝ) (m : Msg) : ℝ

A disjunction costs c and any other message nothing (9).

Equations

• PottsLevy2015.cost c m = if m.IsDisjunction then c else 0

noncomputable def PottsLevy2015.L0 (l : Lex) : ProbabilityTheory.Kernel Msg World

The literal listener (10) conditions a flat prior on the message's extension.

Equations

• PottsLevy2015.L0 l = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (m : PottsLevy2015.Msg) => ↑(PottsLevy2015.sem l m))

instance PottsLevy2015.instIsFiniteKernelMsgWorldL0 (l : Lex) : ProbabilityTheory.IsFiniteKernel (L0 l)

noncomputable def PottsLevy2015.S1 (α c : ℝ) (l : Lex) : ProbabilityTheory.Kernel World Msg

The speaker (11) is the substrate's speaker, with the cost divided by the rationality since the paper subtracts it outside.

Equations

• PottsLevy2015.S1 α c l = RSA.speaker α (fun (x : PottsLevy2015.Msg) => PottsLevy2015.cost c x / α) (⇑(PottsLevy2015.L0 l)) MeasureTheory.Measure.dirac

instance PottsLevy2015.instIsFiniteKernelWorldMsgS1 (α c : ℝ) (l : Lex) : ProbabilityTheory.IsFiniteKernel (S1 α c l)

noncomputable def PottsLevy2015.l1 (α c : ℝ) (l : Lex) : ProbabilityTheory.Kernel Msg World

The fixed-lexicon pragmatic listener (12) inverts the speaker against a flat prior.

Equations

• PottsLevy2015.l1 α c l = RSA.listener (ProbabilityTheory.uniformOn Set.univ) ⇑(PottsLevy2015.S1 α c l)

instance PottsLevy2015.instIsFiniteKernelMsgWorldL1 (α c : ℝ) (l : Lex) : ProbabilityTheory.IsFiniteKernel (l1 α c l)

noncomputable def PottsLevy2015.L1 (α c : ℝ) : ProbabilityTheory.Kernel Msg (World × Lex)

The lexical-uncertainty listener (14) at k = 1 inverts the lexicon-indexed speaker against a flat prior over states and lexica.

Equations

• PottsLevy2015.L1 α c = RSA.listener (ProbabilityTheory.uniformOn Set.univ) fun (p : PottsLevy2015.World × PottsLevy2015.Lex) => (PottsLevy2015.S1 α c p.2) p.1

instance PottsLevy2015.instIsFiniteKernelMsgProdWorldLexL1 (α c : ℝ) : ProbabilityTheory.IsFiniteKernel (L1 α c)

noncomputable def PottsLevy2015.S2 (α β c : ℝ) : ProbabilityTheory.Kernel (World × Lex) Msg

The expertise speaker (15) at k = 2 weighs the fixed-lexicon listener's mass at the state to the rationality, the lexicon posterior to the lexicon weight, and the cost.

Equations

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

instance PottsLevy2015.instIsFiniteKernelProdWorldLexMsgS2 (α β c : ℝ) : ProbabilityTheory.IsFiniteKernel (S2 α β c)

noncomputable def PottsLevy2015.L2 (α β c : ℝ) : ProbabilityTheory.Kernel Msg (World × Lex)

The lexical-uncertainty listener (14) at k = 2.

Equations

• PottsLevy2015.L2 α β c = RSA.listener (ProbabilityTheory.uniformOn Set.univ) ⇑(PottsLevy2015.S2 α β c)

noncomputable def PottsLevy2015.S2exp (α β c : ℝ) : ProbabilityTheory.Kernel World Msg

The marginal expertise speaker (17) at a flat lexicon prior.

Equations

• PottsLevy2015.S2exp α β c = ∑ l : PottsLevy2015.Lex, (ProbabilityTheory.uniformOn Set.univ) {l} • (PottsLevy2015.S2 α β c).comap (fun (x : PottsLevy2015.World) => (x, l)) ⋯

Support and preference reductions

theorem PottsLevy2015.l1_real_lt_iff {α c : ℝ} (l : Lex) (m : Msg) (v v' : World) : ((l1 α c l) m).real {v} < ((l1 α c l) m).real {v'} ↔ ((S1 α c l) v).real {m} < ((S1 α c l) v').real {m}

State preference of the fixed-lexicon listener is the speaker's preference.

theorem PottsLevy2015.l1_real {α c : ℝ} (l : Lex) (m : Msg) (w : World) : ((l1 α c l) m).real {w} = ((S1 α c l) w).real {m} / ∑ w' : World, ((S1 α c l) w').real {m}

On reals, the fixed-lexicon listener's mass is the speaker's share of the message at the state over its shares at every state.

theorem PottsLevy2015.L1_fst_real_lt_iff {α c : ℝ} (m : Msg) (v v' : World) : ((L1 α c) m).fst.real {v} < ((L1 α c) m).fst.real {v'} ↔ ∑ l : Lex, ((S1 α c l) v).real {m} < ∑ l : Lex, ((S1 α c l) v').real {m}

State preference of the joint listener is the pooled speaker preference.

theorem PottsLevy2015.L1_snd_real_lt_iff {α c : ℝ} (m : Msg) (l₁ l₂ : Lex) : ((L1 α c) m).snd.real {l₁} < ((L1 α c) m).snd.real {l₂} ↔ ∑ w : World, ((S1 α c l₁) w).real {m} < ∑ w : World, ((S1 α c l₂) w).real {m}

Lexicon preference of the joint listener is the speaker preference pooled over states.

theorem PottsLevy2015.L1_snd_real {α c : ℝ} (m : Msg) (l : Lex) : ((L1 α c) m).snd.real {l} = (∑ w : World, ((S1 α c l) w).real {m}) / ∑ p : World × Lex, ((S1 α c p.2) p.1).real {m}

On reals, the lexicon posterior is the lexicon's speakers' shares of the message pooled over states, over the shares of every state–lexicon pair.

theorem PottsLevy2015.S1_ne_zero_iff {α : ℝ} (hα : 0 < α) {c : ℝ} (l : Lex) (w : World) (m : Msg) : ((S1 α c l) w) {m} ≠ 0 ↔ w ∈ sem l m

The speaker produces a message at a state exactly when it is true there.

theorem PottsLevy2015.l1_ne_zero_iff {α : ℝ} (hα : 0 < α) {c : ℝ} (l : Lex) (m : Msg) (w : World) : ((l1 α c l) m) {w} ≠ 0 ↔ w ∈ sem l m

The fixed-lexicon listener assigns mass to a state exactly when the message is true there.

theorem PottsLevy2015.L1_ne_zero_iff {α : ℝ} (hα : 0 < α) {c : ℝ} (m : Msg) (p : World × Lex) : ((L1 α c) m) {p} ≠ 0 ↔ p.1 ∈ sem p.2 m

The joint listener assigns mass to a state–lexicon pair exactly when the message is true at the state under the lexicon.

theorem PottsLevy2015.L1_snd_ne_zero {α : ℝ} (hα : 0 < α) {c : ℝ} (m : Msg) (l : Lex) : ((L1 α c) m).snd {l} ≠ 0

Every lexicon keeps positive posterior mass under every message.

noncomputable def PottsLevy2015.costFactor (c : ℝ) (m : Msg) : ℝ

The factor a message's cost puts on its weight.

Equations

• PottsLevy2015.costFactor c m = Real.exp (-PottsLevy2015.cost c m)

noncomputable def PottsLevy2015.l0r (l : Lex) (m : Msg) (w : World) : ℝ

The literal listener's mass at a state on reals.

Equations

• PottsLevy2015.l0r l m w = if w ∈ PottsLevy2015.sem l m then (↑(PottsLevy2015.sem l m).card)⁻¹ else 0

theorem PottsLevy2015.L0_rpow_toReal {α : ℝ} (hα : 0 < α) (l : Lex) (m : Msg) (w : World) : (((L0 l) m) {w} ^ α).toReal = l0r l m w ^ α

theorem PottsLevy2015.S1_real {α : ℝ} (hα : 0 < α) (c : ℝ) (l : Lex) (w : World) (m : Msg) : ((S1 α c l) w).real {m} = l0r l m w ^ α * costFactor c m / ∑ m' : Msg, l0r l m' w ^ α * costFactor c m'

The speaker's share of a message is its weight, the literal listener's mass to the rationality times the cost factor, over the weights of every message.

theorem PottsLevy2015.S2_apply_eq_zero {α β : ℝ} (hα : 0 < α) {c : ℝ} {p : World × Lex} {m : Msg} (hm : p.1 ∉ sem p.2 m) : ((S2 α β c) p) {m} = 0

The expertise speaker gives no mass to a message false at the state under her lexicon.

theorem PottsLevy2015.S2_real_lt_iff {α β : ℝ} (hα : 0 < α) {c : ℝ} (hβ : 0 ≤ β) (p : World × Lex) (m₁ m₂ : Msg) : ((S2 α β c) p).real {m₁} < ((S2 α β c) p).real {m₂} ↔ ((l1 α c p.2) m₁).real {p.1} ^ α * ((L1 α c) m₁).snd.real {p.2} ^ β * costFactor c m₁ < ((l1 α c p.2) m₂).real {p.1} ^ α * ((L1 α c) m₂).snd.real {p.2} ^ β * costFactor c m₂

Message preference of the expertise speaker is weight preference on reals.

The sums

def PottsLevy2015.World.equivFin : World ≃ Fin 7

The states as Fin 7.

Equations

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

def PottsLevy2015.Msg.equivFin : Msg ≃ Fin 8

The messages as Fin 8.

Equations

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

def PottsLevy2015.Lex.equivFin : Lex ≃ Fin 3

The lexica as Fin 3.

Equations

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

theorem PottsLevy2015.World.sum_univ {M : Type u_1} [AddCommMonoid M] (f : World → M) : ∑ w : World, f w = f w₁ + f w₂ + f w₃ + f w₁₂ + f w₁₃ + f w₂₃ + f w₁₂₃

theorem PottsLevy2015.Msg.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Msg → M) : ∑ m : Msg, f m = f A + f B + f X + f AorB + f AorX + f BorX + f AorBorX + f null

theorem PottsLevy2015.Lex.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Lex → M) : ∑ l : Lex, f l = f base + f excl + f syn

The Hurfordian context (§5.2, Figure 10)

theorem PottsLevy2015.l1_uncertainty {c : ℝ} (hc : 0 ≤ c) : ((L1 2 c) Msg.AorX).fst.real {World.w₂} < ((L1 2 c) Msg.AorX).fst.real {World.w₁} ∧ ((L1 2 c) Msg.AorX).fst.real {World.w₁} < ((L1 2 c) Msg.AorX).fst.real {World.w₁₂}

Hearing A or X, the lexical-uncertainty listener ranks the uncertain state above the first atom and that above the second, the ignorance implicature.

theorem PottsLevy2015.l1_lexicon {c : ℝ} (hc : 0 ≤ c) : ((L1 2 c) Msg.AorX).snd.real {Lex.syn} < ((L1 2 c) Msg.AorX).snd.real {Lex.base} ∧ ((L1 2 c) Msg.AorX).snd.real {Lex.base} < ((L1 2 c) Msg.AorX).snd.real {Lex.excl}

Hearing A or X, the listener ranks the exclusivized lexicon above the base lexicon and that above the synonym lexicon, the Hurford rescue.

theorem PottsLevy2015.s1_disjunction_iff_uncertain {c : ℝ} (hc : 0 ≤ c) : ((S1 2 c Lex.excl) World.w₁₂).real {Msg.A} < ((S1 2 c Lex.excl) World.w₁₂).real {Msg.AorX} ∧ ((S1 2 c Lex.excl) World.w₁₂).real {Msg.X} < ((S1 2 c Lex.excl) World.w₁₂).real {Msg.AorX} ∧ ((S1 2 c Lex.excl) World.w₁).real {Msg.AorX} < ((S1 2 c Lex.excl) World.w₁).real {Msg.A}

The exclusivizing speaker uses the disjunction exactly when uncertain. At the uncertain state it beats both bare disjuncts, while knowing the first atom the bare A wins.

theorem PottsLevy2015.AorX_signals_excl {c : ℝ} (hc : Real.log 2 ≤ c) : ((L1 2 c) Msg.A).snd.real {Lex.excl} < ((L1 2 c) Msg.AorX).snd.real {Lex.excl}

At a disjunction cost of at least log 2, A or X signals the exclusivized lexicon more strongly than the bare A does, which every lexicon reads alike.

theorem PottsLevy2015.s2_prefers_disjunction {c : ℝ} (hc0 : 0 ≤ c) (hc10 : c ≤ Real.log 10) (m : Msg) (hm : m ≠ Msg.AorX) : ((S2 2 1 c) (World.w₁₂, Lex.excl)).real {m} < ((S2 2 1 c) (World.w₁₂, Lex.excl)).real {Msg.AorX}

At a disjunction cost between 0 and log 10, the expertise speaker who observes the uncertain state with the exclusivized lexicon prefers A or X to every other message, the paper's production claim for the context.

theorem PottsLevy2015.s2exp_uncertain {c : ℝ} : ((S2exp 2 1 c) World.w₁₂) {Msg.A} = 0 ∧ ((S2exp 2 1 c) World.w₁₂) {Msg.AorX} ≠ 0

The marginal expertise speaker at the uncertain state never uses the bare A and does use the disjunction.