[PL15]: lexical uncertainty and speaker expertise with disjunction

Hurford-violating disjunctions ("X or A" with A ⊆ ⟦X⟧) are felicitous and carry ignorance implicatures. The paper derives both from RSA with lexical uncertainty (BLS 41, pp. 417–445): the listener jointly infers the world and the speaker's lexicon (eq. 14), and an expertise speaker (eq. 15) signals both world knowledge (α term) and lexicon knowledge (β term). Domain: 5 utterances × 3 states (w₁, w₂, and the uncertainty join w₁₂, where truth requires truth at both atoms) × 3 lexica for X (base = A ∪ B, excl = B, syn = A).

Main results

• l1_uncertainty, l1_lexicon: hearing "A or X", the joint listener infers speaker uncertainty (w₁₂ > w₁ > w₂) and the exclusivized lexicon (excl > base > syn).
• s1_disjunction_iff_uncertain: the eq. 11 speaker uses the disjunction exactly when uncertain.
• s2End_disjunction_iff_uncertain, AorX_signals_excl_vs_A: eq. 15's informativity and expertise components verified independently.
• l2_uncertainty, l2_lexicon, s2Exp_disjunction_iff_uncertain: the same at the stacked expertise level, Figure 10's regime α = 2, β = 1, C(or) = 1 (its L₂ margins are .91 > .09 > 0 over worlds and .49 > .34 > .17 over lexica; p. 436: "S₂'s preferred message given observed state w₁∨w₂ and lexicon L₁ from Figure 10 is A or X").
• excl_is_base_minus_A: the excl lexicon is exhaustification — excl(X) = base(X) ∧ ¬A.

Implementation notes

α = 2 and β = 1 are natural powers, so each agent is a PMF.ofScores cast of an exact-ℚ≥0 score function the kernel computes with; the tower recurses through the score functions. No utterance row is dead (null is true everywhere), so the uniform fallback never fires. The disjunction cost exp(−1) is rationalized as 37/100 (qualitative predictions robust, paper §5.4). s2PMF is the endorsement reading of S₂ over the level-1 listener (an informativity-component decomposition); s2ExpPMF is the paper's eq. 17 lexicon-marginalized expertise speaker.

The definitional regime (syn dominating, "wine lover or oenophile") requires β > α (paper §5.4) and is not modeled.

TODO

Model the definitional regime (β > α) and the implicature-blocking simulations of paper §5.3. Relate the lexica to Semantics.Exhaustification operators (excl_is_base_minus_A is the exh clause over alternatives {A, X}).

Domain

inductive PottsLevy2015.World : Type

World states: w₁ (only A), w₂ (only B), and the uncertainty join w₁₂ (both possible).

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

@[implicit_reducible]

instance PottsLevy2015.instDecidableEqWorld : DecidableEq World

Equations

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

def PottsLevy2015.instReprWorld.repr : World → ℕ → Std.Format

Equations

• PottsLevy2015.instReprWorld.repr PottsLevy2015.World.w₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsLevy2015.World.w₁")).group prec✝
• PottsLevy2015.instReprWorld.repr PottsLevy2015.World.w₂ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsLevy2015.World.w₂")).group prec✝
• PottsLevy2015.instReprWorld.repr PottsLevy2015.World.w₁₂ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsLevy2015.World.w₁₂")).group prec✝

@[implicit_reducible]

instance PottsLevy2015.instReprWorld : Repr World

Equations

• PottsLevy2015.instReprWorld = { reprPrec := PottsLevy2015.instReprWorld.repr }

@[implicit_reducible]

instance PottsLevy2015.instInhabitedWorld : Inhabited World

Equations

• PottsLevy2015.instInhabitedWorld = { default := PottsLevy2015.instInhabitedWorld.default }

@[implicit_reducible]

instance PottsLevy2015.instFintypeWorld : Fintype World

Equations

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

inductive PottsLevy2015.Utterance : Type

Utterances: the atoms A, B, the ambiguous term X, the disjunction, and the designated null message.

• A : Utterance
• B : Utterance
• X : Utterance
• AorX : Utterance
• null : Utterance

@[implicit_reducible]

instance PottsLevy2015.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

@[implicit_reducible]

instance PottsLevy2015.instReprUtterance : Repr Utterance

Equations

• PottsLevy2015.instReprUtterance = { reprPrec := PottsLevy2015.instReprUtterance.repr }

def PottsLevy2015.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance PottsLevy2015.instInhabitedUtterance : Inhabited Utterance

Equations

• PottsLevy2015.instInhabitedUtterance = { default := PottsLevy2015.instInhabitedUtterance.default }

@[implicit_reducible]

instance PottsLevy2015.instFintypeUtterance : Fintype Utterance

Equations

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

inductive PottsLevy2015.Lex : Type

Lexica for X: base (X = A ∪ B), excl (X = B, exhaustified), syn (X = A, synonymous).

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

@[implicit_reducible]

instance PottsLevy2015.instDecidableEqLex : DecidableEq Lex

Equations

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

def PottsLevy2015.instReprLex.repr : Lex → ℕ → Std.Format

Equations

• PottsLevy2015.instReprLex.repr PottsLevy2015.Lex.base prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsLevy2015.Lex.base")).group prec✝
• PottsLevy2015.instReprLex.repr PottsLevy2015.Lex.excl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsLevy2015.Lex.excl")).group prec✝
• PottsLevy2015.instReprLex.repr PottsLevy2015.Lex.syn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PottsLevy2015.Lex.syn")).group prec✝

@[implicit_reducible]

instance PottsLevy2015.instReprLex : Repr Lex

Equations

• PottsLevy2015.instReprLex = { reprPrec := PottsLevy2015.instReprLex.repr }

@[implicit_reducible]

instance PottsLevy2015.instInhabitedLex : Inhabited Lex

Equations

• PottsLevy2015.instInhabitedLex = { default := PottsLevy2015.instInhabitedLex.default }

@[implicit_reducible]

instance PottsLevy2015.instFintypeLex : Fintype Lex

Equations

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

Truth conditions

def PottsLevy2015.atomicTruth : Lex → Utterance → World → Bool

Truth of non-disjunctive utterances at atomic worlds.

Equations

• PottsLevy2015.atomicTruth x✝ PottsLevy2015.Utterance.A PottsLevy2015.World.w₁ = true
• PottsLevy2015.atomicTruth x✝ PottsLevy2015.Utterance.B PottsLevy2015.World.w₂ = true
• PottsLevy2015.atomicTruth PottsLevy2015.Lex.base PottsLevy2015.Utterance.X PottsLevy2015.World.w₁ = true
• PottsLevy2015.atomicTruth PottsLevy2015.Lex.base PottsLevy2015.Utterance.X PottsLevy2015.World.w₂ = true
• PottsLevy2015.atomicTruth PottsLevy2015.Lex.excl PottsLevy2015.Utterance.X PottsLevy2015.World.w₂ = true
• PottsLevy2015.atomicTruth PottsLevy2015.Lex.syn PottsLevy2015.Utterance.X PottsLevy2015.World.w₁ = true
• PottsLevy2015.atomicTruth x✝¹ PottsLevy2015.Utterance.null x✝ = true
• PottsLevy2015.atomicTruth x✝² x✝¹ x✝ = false

def PottsLevy2015.truth (l : Lex) (u : Utterance) (w : World) : Bool

Truth at all worlds: "A or X" is A ∨ X, and truth at the join w₁₂ requires truth at both atoms (the speaker asserts only what holds across all epistemically accessible worlds).

Equations

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

Truth-conditional facts

theorem PottsLevy2015.excl_is_base_minus_A (w : World) : atomicTruth Lex.excl Utterance.X w = (atomicTruth Lex.base Utterance.X w && !atomicTruth Lex.base Utterance.A w)

excl(X) = base(X) ∧ ¬A: the excl lexicon is the exhaustification of X relative to the alternative A.

theorem PottsLevy2015.syn_is_base_A (w : World) : atomicTruth Lex.syn Utterance.X w = atomicTruth Lex.base Utterance.A w

syn(X) = A: the syn lexicon narrows X to its overlap with A.

theorem PottsLevy2015.base_entails_excl : (∀ (w : World), atomicTruth Lex.excl Utterance.X w = true → atomicTruth Lex.base Utterance.X w = true) ∧ ∃ (w : World), atomicTruth Lex.base Utterance.X w = true ∧ atomicTruth Lex.excl Utterance.X w = false

excl is a proper refinement of base.

theorem PottsLevy2015.syn_AorX_eq_A (w : World) : truth Lex.syn Utterance.AorX w = truth Lex.syn Utterance.A w

Under syn, "A or X" is extensionally "A": the Hurford violation.

theorem PottsLevy2015.excl_disjoint : ¬∃ (w : World), truth Lex.excl Utterance.A w = true ∧ truth Lex.excl Utterance.X w = true

Under excl, A and X are disjoint: the exhaustified reading that rescues the disjunction.

theorem PottsLevy2015.excl_w12_AorX_unique : truth Lex.excl Utterance.AorX World.w₁₂ = true ∧ truth Lex.excl Utterance.A World.w₁₂ = false ∧ truth Lex.excl Utterance.B World.w₁₂ = false ∧ truth Lex.excl Utterance.X World.w₁₂ = false

Under excl, "A or X" is the only non-null utterance true at w₁₂.

theorem PottsLevy2015.syn_w12_AorX_false : truth Lex.syn Utterance.AorX World.w₁₂ = false

Under syn, "A or X" is false at w₁₂ (it reduces to A, which fails at w₂).

theorem PottsLevy2015.base_w12_AorX_true : truth Lex.base Utterance.AorX World.w₁₂ = true

Under base, "A or X" is true at w₁₂.

The agent tower (eqs. 10–17)

Agents are PMFs, each with one ℚ≥0 score function as its computational face: the tower recurses through the normalized scores (÷0 = 0, though no row here is dead), the PMF is their PMF.ofScores cast, and PMF.ofScores_apply is the pointwise hom between the two.

def PottsLevy2015.s1Score (l : Lex) (w : World) : Utterance → ℚ≥0

Speaker scores (eq. 11 at α = 2, uniform world prior, zero cost): the normalized squared literal listener of eq. 10.

Equations

• PottsLevy2015.s1Score l w = PMF.normalizeScores fun (u : PottsLevy2015.Utterance) => RSA.Score.l0 (PottsLevy2015.truth l) (fun (x : PottsLevy2015.World) => 1) u w ^ 2

noncomputable def PottsLevy2015.s1 (l : Lex) (w : World) : PMF Utterance

Speaker (eq. 11).

Equations

• PottsLevy2015.s1 l w = PMF.ofScores PMF.Fallback.uniform (PottsLevy2015.s1Score l w)

def PottsLevy2015.l1FixedScore (l : Lex) (u : Utterance) : World → ℚ≥0

Fixed-lexicon pragmatic listener (the paper's lowercase l₁, eq. 12): the speaker renormalized over worlds — Bayes with a uniform prior, at a single lexicon (Figure 2's "fixed 𝓛" column).

Equations

• PottsLevy2015.l1FixedScore l u = PMF.normalizeScores fun (w : PottsLevy2015.World) => PottsLevy2015.s1Score l w u

def PottsLevy2015.l1Score (u : Utterance) : World → ℚ≥0

Lexical-uncertainty listener over worlds (the paper's uppercase L₁, eq. 14/16): the per-lexicon normaliser cancels under uniform priors, leaving ∑ s₁.

Equations

• PottsLevy2015.l1Score u = PMF.normalizeScores fun (w : PottsLevy2015.World) => ∑ l : PottsLevy2015.Lex, PottsLevy2015.s1Score l w u

noncomputable def PottsLevy2015.l1 (u : Utterance) : PMF World

Joint listener over worlds (eq. 16).

Equations

• PottsLevy2015.l1 u = PMF.ofScores PMF.Fallback.uniform (PottsLevy2015.l1Score u)

def PottsLevy2015.l1LatScore (u : Utterance) : Lex → ℚ≥0

Joint-listener lexicon-posterior scores (eq. 14).

Equations

• PottsLevy2015.l1LatScore u = PMF.normalizeScores fun (l : PottsLevy2015.Lex) => ∑ w : PottsLevy2015.World, PottsLevy2015.s1Score l w u

noncomputable def PottsLevy2015.l1Lat (u : Utterance) : PMF Lex

Joint listener over lexica (eq. 14).

Equations

• PottsLevy2015.l1Lat u = PMF.ofScores PMF.Fallback.uniform (PottsLevy2015.l1LatScore u)

def PottsLevy2015.disjCost : Utterance → ℚ≥0

Disjunction cost factor exp(−C(m)) with C(or) = 1, rationalized as 37/100 ≈ exp(−1).

Equations

• PottsLevy2015.disjCost PottsLevy2015.Utterance.AorX = 37 / 100
• PottsLevy2015.disjCost x✝ = 1

def PottsLevy2015.s2Score (l : Lex) (w : World) : Utterance → ℚ≥0

Expertise-speaker scores (eq. 15 at α = 2, β = 1): normalized l₁(w|m,L)² · L₁(L|m) · exp(−C(m)).

Equations

• PottsLevy2015.s2Score l w = PMF.normalizeScores fun (u : PottsLevy2015.Utterance) => PottsLevy2015.l1FixedScore l u w ^ 2 * PottsLevy2015.l1LatScore u l * PottsLevy2015.disjCost u

noncomputable def PottsLevy2015.s2End (w : World) : PMF Utterance

Endorsement speaker: the L₁ world posterior renormalized per world (the informativity component of eq. 15 in isolation).

Equations

• PottsLevy2015.s2End w = PMF.ofScores PMF.Fallback.uniform fun (u : PottsLevy2015.Utterance) => PottsLevy2015.l1Score u w

def PottsLevy2015.l2Score (u : Utterance) (w : World) : ℚ≥0

L₂ scores (eq. 14 at k = 2): summed expertise speakers. At fixed u they are the world-posterior scores; at fixed w, the eq. 17 lexicon-marginalized speaker scores.

Equations

• PottsLevy2015.l2Score u w = ∑ l : PottsLevy2015.Lex, PottsLevy2015.s2Score l w u

noncomputable def PottsLevy2015.l2 (u : Utterance) : PMF World

L₂ listener over worlds (eq. 16 at k = 2).

Equations

• PottsLevy2015.l2 u = PMF.ofScores PMF.Fallback.uniform (PottsLevy2015.l2Score u)

noncomputable def PottsLevy2015.l2Lat (u : Utterance) : PMF Lex

L₂ listener over lexica (eq. 14 at k = 2).

Equations

• PottsLevy2015.l2Lat u = PMF.ofScores PMF.Fallback.uniform fun (l : PottsLevy2015.Lex) => ∑ w : PottsLevy2015.World, PottsLevy2015.s2Score l w u

noncomputable def PottsLevy2015.s2Exp (w : World) : PMF Utterance

Marginal expertise speaker (eq. 17 at k = 2, uniform lexicon prior).

Equations

• PottsLevy2015.s2Exp w = PMF.ofScores PMF.Fallback.uniform fun (u : PottsLevy2015.Utterance) => PottsLevy2015.l2Score u w

The L₁ inferences

theorem PottsLevy2015.l1_uncertainty : (l1 Utterance.AorX) World.w₂ < (l1 Utterance.AorX) World.w₁ ∧ (l1 Utterance.AorX) World.w₁ < (l1 Utterance.AorX) World.w₁₂

The ignorance implicature: hearing "A or X", L₁ ranks the uncertainty state on top — w₁₂ > w₁ > w₂. The speaker could have said "A" knowing w₁ or "X" knowing w₂ (under excl), so the disjunction signals commitment to neither disjunct.

theorem PottsLevy2015.l1_lexicon : (l1Lat Utterance.AorX) Lex.syn < (l1Lat Utterance.AorX) Lex.base ∧ (l1Lat Utterance.AorX) Lex.base < (l1Lat Utterance.AorX) Lex.excl

The Hurford rescue: hearing "A or X", L₁ ranks the exclusivized lexicon on top — excl > base > syn. excl makes the disjunction maximally informative; syn makes it redundant.

Speaker rationality

theorem PottsLevy2015.s1_disjunction_iff_uncertain : (s1 Lex.excl World.w₁₂) Utterance.A < (s1 Lex.excl World.w₁₂) Utterance.AorX ∧ (s1 Lex.excl World.w₁₂) Utterance.X < (s1 Lex.excl World.w₁₂) Utterance.AorX ∧ (s1 Lex.excl World.w₁) Utterance.AorX < (s1 Lex.excl World.w₁) Utterance.A

The eq. 11 speaker (under excl) uses the disjunction exactly when uncertain: at w₁₂ it beats both bare disjuncts, while knowing w₁ the bare "A" wins.

Endorsement decomposition

Eq. 15's two utility terms as independent components: informativity via the endorsement speaker s2End (S₂(u|w) ∝ L₁(w|u)) and expertise via lexicon signaling. With β > 0 the speaker has both reasons to use the disjunction.

theorem PottsLevy2015.s2End_disjunction_iff_uncertain : (s2End World.w₁₂) Utterance.A < (s2End World.w₁₂) Utterance.AorX ∧ (s2End World.w₁) Utterance.AorX < (s2End World.w₁) Utterance.A

The informativity component alone already selects the disjunction exactly when uncertain ("A" is false at w₁₂ under every lexicon).

theorem PottsLevy2015.AorX_signals_excl_vs_A : (l1Lat Utterance.A) Lex.excl < (l1Lat Utterance.AorX) Lex.excl

The expertise component: "A or X" signals the excl lexicon more strongly than "A" does (all lexica agree on "A", so its lexicon posterior is near-uniform). This asymmetry is what β > 0 amplifies.

Predictions at the stacked level (Figure 10)

theorem PottsLevy2015.l2_uncertainty : (l2 Utterance.AorX) World.w₂ < (l2 Utterance.AorX) World.w₁ ∧ (l2 Utterance.AorX) World.w₁ < (l2 Utterance.AorX) World.w₁₂

L₂ hearing "A or X" reproduces the uncertainty ordering w₁₂ > w₁ > w₂ (Figure 10 world margins .91 > .09 > 0).

theorem PottsLevy2015.l2_lexicon : (l2Lat Utterance.AorX) Lex.syn < (l2Lat Utterance.AorX) Lex.base ∧ (l2Lat Utterance.AorX) Lex.base < (l2Lat Utterance.AorX) Lex.excl

L₂ hearing "A or X" reproduces the lexicon ordering excl > base > syn (Figure 10 lexicon margins .49 > .34 > .17).

theorem PottsLevy2015.s2Exp_disjunction_iff_uncertain : (s2Exp World.w₁₂) Utterance.A < (s2Exp World.w₁₂) Utterance.AorX ∧ (s2Exp World.w₁) Utterance.AorX < (s2Exp World.w₁) Utterance.A

The eq. 17 marginal speaker uses the disjunction exactly when uncertain (p. 436).