Documentation

Studies.ChampollionAlsopGrosu2019

Champollion, Alsop and Grosu (2019): Free Choice Disjunction as a Rational Speech Act #

Free choice, by which You may take an apple or a pear conveys that each fruit may be taken by itself, does not follow from modal logic, and a speaker who prefers informative utterances never has reason to choose the disjunction over a disjunct. The paper adds semantic uncertainty: two interpretation functions, the classical (6) and the exhaustified (7), over which the pragmatic listener reasons jointly with states and utterances (8). Under the exhaustified function a bare disjunct risks the reading only that fruit, so at the free-choice states Only One and Any Number the disjunction is the speaker's safe choice (speaker_or_onlyOne_exh, speaker_prefers_a_at_onlyA_exh), and the listener inverts the avoidance: hearing or, each free-choice state outweighs each other state at the paper's α = 100 (fci_derived, Table 5), and the free-choice states already carry the majority at α = 2 (fci_majority_low_alpha).

Exclusivity, that not both may be taken, tracks the prior instead. Under a prior favouring Any Number the listener hearing or ranks Any Number above every other state, at every rationality (anyNumber_of_prior, Table 6), which is the paper's account of why exclusivity, unlike free choice, is cancelable. Under negation the negated disjunction is unambiguous and maximally strong, so the listener assigns no mass to the states at which free choice would survive (no_fci_under_negation, Table 9). The variants without the conjunctive alternative (Tables 7–8) are not formalized.

Main results #

speaker_or_onlyOne_exh, speaker_prefers_a_at_onlyA_exh: under exhaustification the disjunction is the safe choice at the free-choice states and a disjunct is not.
fci_derived, fci_majority_low_alpha: hearing or, the listener favours the free-choice states, at the paper's α and at a low one.
anyNumber_of_prior: exclusivity tracks the prior at every rationality.
no_fci_under_negation: the negated disjunction leaves no mass where free choice would arise.

References #

States, utterances, interpretation functions (Table 2, (5)–(7)) #

inductive ChampollionAlsopGrosu2019.FCState :

The permission states of Table 2 split Franke's All True into Any Number and Only Both.

onlyA : FCState
onlyB : FCState
onlyOne : FCState
anyNumber : FCState
onlyBoth : FCState

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidableEqFCState :

DecidableEq FCState

Equations

ChampollionAlsopGrosu2019.instDecidableEqFCState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChampollionAlsopGrosu2019.instReprFCState.repr :

FCState → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instReprFCState :

Equations

ChampollionAlsopGrosu2019.instReprFCState = { reprPrec := ChampollionAlsopGrosu2019.instReprFCState.repr }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instInhabitedFCState :

Inhabited FCState

Equations

ChampollionAlsopGrosu2019.instInhabitedFCState = { default := ChampollionAlsopGrosu2019.instInhabitedFCState.default }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instFintypeFCState :

Fintype FCState

Equations

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

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instMeasurableSpaceFCState :

MeasurableSpace FCState

Equations

ChampollionAlsopGrosu2019.instMeasurableSpaceFCState = ⊤

instance ChampollionAlsopGrosu2019.instDiscreteMeasurableSpaceFCState :

DiscreteMeasurableSpace FCState

instance ChampollionAlsopGrosu2019.instMeasurableSingletonClassFCState :

MeasurableSingletonClass FCState

inductive ChampollionAlsopGrosu2019.Utterance :

The four utterances (5).

a : Utterance
b : Utterance
or_ : Utterance
and_ : Utterance

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidableEqUtterance :

DecidableEq Utterance

Equations

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

def ChampollionAlsopGrosu2019.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instReprUtterance :

Equations

ChampollionAlsopGrosu2019.instReprUtterance = { reprPrec := ChampollionAlsopGrosu2019.instReprUtterance.repr }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instInhabitedUtterance :

Inhabited Utterance

Equations

ChampollionAlsopGrosu2019.instInhabitedUtterance = { default := ChampollionAlsopGrosu2019.instInhabitedUtterance.default }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instFintypeUtterance :

Fintype Utterance

Equations

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

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instMeasurableSpaceUtterance :

MeasurableSpace Utterance

Equations

ChampollionAlsopGrosu2019.instMeasurableSpaceUtterance = ⊤

instance ChampollionAlsopGrosu2019.instDiscreteMeasurableSpaceUtterance :

DiscreteMeasurableSpace Utterance

instance ChampollionAlsopGrosu2019.instMeasurableSingletonClassUtterance :

MeasurableSingletonClass Utterance

inductive ChampollionAlsopGrosu2019.Interp :

An interpretation function is classical modal logic or its exhaustification.

literal : Interp
exhaustified : Interp

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidableEqInterp :

DecidableEq Interp

Equations

ChampollionAlsopGrosu2019.instDecidableEqInterp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChampollionAlsopGrosu2019.instReprInterp.repr :

Interp → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instReprInterp :

Equations

ChampollionAlsopGrosu2019.instReprInterp = { reprPrec := ChampollionAlsopGrosu2019.instReprInterp.repr }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instInhabitedInterp :

Inhabited Interp

Equations

ChampollionAlsopGrosu2019.instInhabitedInterp = { default := ChampollionAlsopGrosu2019.instInhabitedInterp.default }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instFintypeInterp :

Fintype Interp

Equations

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

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instMeasurableSpaceInterp :

MeasurableSpace Interp

Equations

ChampollionAlsopGrosu2019.instMeasurableSpaceInterp = ⊤

instance ChampollionAlsopGrosu2019.instDiscreteMeasurableSpaceInterp :

DiscreteMeasurableSpace Interp

instance ChampollionAlsopGrosu2019.instMeasurableSingletonClassInterp :

MeasurableSingletonClass Interp

def ChampollionAlsopGrosu2019.HasFCI :

FCState → Prop

Free choice holds when each fruit may be taken by itself.

Equations

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidablePredFCStateHasFCI :

DecidablePred HasFCI

Equations

def ChampollionAlsopGrosu2019.I1 :

Utterance → FCState → Prop

Interpretation function 1 (6) is classical modal logic.

Equations

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidablePredFCStateI1 (u : Utterance) :

DecidablePred (I1 u)

Equations

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

def ChampollionAlsopGrosu2019.I2 :

Utterance → FCState → Prop

Interpretation function 2 (7) gives the exhaustified meanings.

Equations

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidablePredFCStateI2 (u : Utterance) :

DecidablePred (I2 u)

Equations

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

def ChampollionAlsopGrosu2019.interpMeaning :

Interp → Utterance → FCState → Prop

Meaning indexed by interpretation function.

Equations

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidablePredFCStateInterpMeaning (i : Interp) (u : Utterance) :

DecidablePred (interpMeaning i u)

Equations

def ChampollionAlsopGrosu2019.sem (i : Interp) (u : Utterance) :

Finset FCState

The extension of each utterance under each interpretation function.

Equations

ChampollionAlsopGrosu2019.sem i u = Finset.filter (ChampollionAlsopGrosu2019.interpMeaning i u) Finset.univ

Instances For

@[simp]

theorem ChampollionAlsopGrosu2019.mem_sem {i : Interp} {u : Utterance} {w : FCState} :

w ∈ sem i u ↔ interpMeaning i u w

theorem ChampollionAlsopGrosu2019.I2_refines_I1 (u : Utterance) (w : FCState) :

I2 u w → I1 u w

Exhaustification only strengthens.

theorem ChampollionAlsopGrosu2019.I1_or_everywhere (w : FCState) :

I1 Utterance.or_ w

The classical disjunction is true everywhere — maximally uninformative.

theorem ChampollionAlsopGrosu2019.I2_or_excludes_onlyBoth (w : FCState) :

I2 Utterance.or_ w ↔ w ≠ FCState.onlyBoth

The exhaustified disjunction excludes exactly Only Both.

theorem ChampollionAlsopGrosu2019.I2_a_singleton (w : FCState) :

I2 Utterance.a w ↔ w = FCState.onlyA

The exhaustified disjunct singles out exactly Only A — the risk the speaker avoids.

The model (8) #

@[reducible, inline]

noncomputable abbrev ChampollionAlsopGrosu2019.literal (μ : MeasureTheory.Measure FCState) (i : Interp) :

ProbabilityTheory.Kernel Utterance FCState

The literal listener under an interpretation function (8a) conditions the state prior on the meaning of the utterance.

Equations

ChampollionAlsopGrosu2019.literal μ i = RSA.listener μ (RSA.truthful fun (u : ChampollionAlsopGrosu2019.Utterance) => ↑(ChampollionAlsopGrosu2019.sem i u))

Instances For

@[reducible, inline]

noncomputable abbrev ChampollionAlsopGrosu2019.speaker (μ : MeasureTheory.Measure FCState) (i : Interp) (α : ℝ) :

ProbabilityTheory.Kernel FCState Utterance

The speaker under an interpretation function (8b) knows the state and addresses that function's literal listener.

Equations

ChampollionAlsopGrosu2019.speaker μ i α = RSA.speaker α 0 (⇑(ChampollionAlsopGrosu2019.literal μ i)) MeasureTheory.Measure.dirac

Instances For

@[reducible, inline]

noncomputable abbrev ChampollionAlsopGrosu2019.listener (α : ℝ) :

ProbabilityTheory.Kernel Utterance (FCState × Interp)

The pragmatic listener (8c) at a uniform prior over states and interpretation functions inverts the speaker of each function, and her first marginal is her belief about the state.

Equations

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

Instances For

theorem ChampollionAlsopGrosu2019.speaker_or_onlyOne_exh {α : ℝ} (hα : 0 < α) :

((speaker (ProbabilityTheory.uniformOn Set.univ) Interp.exhaustified α) FCState.onlyOne) {Utterance.or_} = 1

Under the exhaustified function at Only One, or is the only true utterance, so the speaker produces it with certainty at every rationality (§3.3).

theorem ChampollionAlsopGrosu2019.speaker_or_anyNumber_exh {α : ℝ} (hα : 0 < α) :

((speaker (ProbabilityTheory.uniformOn Set.univ) Interp.exhaustified α) FCState.anyNumber) {Utterance.or_} = 1

Under the exhaustified function at Any Number, or is the only true utterance.

theorem ChampollionAlsopGrosu2019.speaker_or_onlyBoth_exh {α : ℝ} (hα : 0 < α) :

((speaker (ProbabilityTheory.uniformOn Set.univ) Interp.exhaustified α) FCState.onlyBoth) {Utterance.or_} = 0

Under the exhaustified function at Only Both, or is false.

theorem ChampollionAlsopGrosu2019.speaker_prefers_a_at_onlyA_exh {α : ℝ} (hα : 0 < α) :

((speaker (ProbabilityTheory.uniformOn Set.univ) Interp.exhaustified α) FCState.onlyA).real {Utterance.or_} < ((speaker (ProbabilityTheory.uniformOn Set.univ) Interp.exhaustified α) FCState.onlyA).real {Utterance.a}

Under the exhaustified function at Only A the speaker prefers the bare disjunct to the disjunction at every rationality, the avoidance mechanism.

theorem ChampollionAlsopGrosu2019.fci_derived (w : FCState) :

w ∈ {FCState.onlyA, FCState.onlyB, FCState.onlyBoth} → ∀ w' ∈ {FCState.onlyOne, FCState.anyNumber}, ((listener 100) Utterance.or_).fst.real {w} < ((listener 100) Utterance.or_).fst.real {w'}

Hearing or at the paper's α = 100, the listener ranks each free-choice state, Only One and Any Number (the paper's 0.5 each), above each of Only A, Only B, and Only Both (each ≈ 0). This derives free choice (Table 5).

def ChampollionAlsopGrosu2019.fciPairs :

Finset (FCState × Interp)

The free-choice pairs of the joint listener.

Equations

ChampollionAlsopGrosu2019.fciPairs = {p : ChampollionAlsopGrosu2019.FCState × ChampollionAlsopGrosu2019.Interp | ChampollionAlsopGrosu2019.HasFCI p.1}

Instances For

def ChampollionAlsopGrosu2019.nonFciPairs :

Finset (FCState × Interp)

The remaining pairs.

Equations

ChampollionAlsopGrosu2019.nonFciPairs = {p : ChampollionAlsopGrosu2019.FCState × ChampollionAlsopGrosu2019.Interp | ¬ChampollionAlsopGrosu2019.HasFCI p.1}

Instances For

theorem ChampollionAlsopGrosu2019.fci_majority_low_alpha :

((listener 2) Utterance.or_).real ↑nonFciPairs < ((listener 2) Utterance.or_).real ↑fciPairs

At α = 2 the free-choice states still carry the majority of the posterior given or (the paper's "only 70%").

Prior sensitivity (Table 6) #

The prior enters the literal listener (8a) and the pragmatic listener (8c) alike.

def ChampollionAlsopGrosu2019.biasedWeight :

FCState → ℕ

These prior weights favour Any Number, 12 against 1 for each other state (75%).

Equations

Instances For

noncomputable def ChampollionAlsopGrosu2019.priorB :

MeasureTheory.Measure FCState

The state prior.

Equations

ChampollionAlsopGrosu2019.priorB = ∑ w : ChampollionAlsopGrosu2019.FCState, ↑(ChampollionAlsopGrosu2019.biasedWeight w) • MeasureTheory.Measure.dirac w

Instances For

noncomputable def ChampollionAlsopGrosu2019.jointPriorB :

MeasureTheory.Measure (FCState × Interp)

The joint prior, the interpretation function drawn uniformly.

Equations

ChampollionAlsopGrosu2019.jointPriorB = ∑ p : ChampollionAlsopGrosu2019.FCState × ChampollionAlsopGrosu2019.Interp, ↑(ChampollionAlsopGrosu2019.biasedWeight p.1) • MeasureTheory.Measure.dirac p

Instances For

theorem ChampollionAlsopGrosu2019.priorB_singleton (w : FCState) :

priorB {w} = ↑(biasedWeight w)

theorem ChampollionAlsopGrosu2019.jointPriorB_singleton (p : FCState × Interp) :

jointPriorB {p} = ↑(biasedWeight p.1)

instance ChampollionAlsopGrosu2019.instIsFiniteMeasureFCStatePriorB :

MeasureTheory.IsFiniteMeasure priorB

instance ChampollionAlsopGrosu2019.instIsFiniteMeasureProdFCStateInterpJointPriorB :

MeasureTheory.IsFiniteMeasure jointPriorB

noncomputable def ChampollionAlsopGrosu2019.listenerB (α : ℝ) :

ProbabilityTheory.Kernel Utterance (FCState × Interp)

The pragmatic listener at the biased prior.

Equations

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

Instances For

theorem ChampollionAlsopGrosu2019.jointPriorB_real_singleton (p : FCState × Interp) :

jointPriorB.real {p} = ↑(biasedWeight p.1)

theorem ChampollionAlsopGrosu2019.anyNumber_of_prior {α : ℝ} (hα : 0 < α) {w : FCState} (hw : w ≠ FCState.anyNumber) :

((listenerB α) Utterance.or_).fst.real {w} < ((listenerB α) Utterance.or_).fst.real {FCState.anyNumber}

Exclusivity tracks the prior (Table 6). With 75% of the prior on Any Number, the listener hearing or ranks Any Number above every other state at every rationality, since under the exhaustified function or is produced there with certainty and no other state has a comparable prior.

No free choice under negation (§4, Table 9) #

inductive ChampollionAlsopGrosu2019.NegState :

The states of the negation model.

onlyA : NegState
onlyB : NegState
onlyOne : NegState
neither : NegState

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidableEqNegState :

DecidableEq NegState

Equations

ChampollionAlsopGrosu2019.instDecidableEqNegState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChampollionAlsopGrosu2019.instReprNegState.repr :

NegState → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instReprNegState :

Equations

ChampollionAlsopGrosu2019.instReprNegState = { reprPrec := ChampollionAlsopGrosu2019.instReprNegState.repr }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instInhabitedNegState :

Inhabited NegState

Equations

ChampollionAlsopGrosu2019.instInhabitedNegState = { default := ChampollionAlsopGrosu2019.instInhabitedNegState.default }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instFintypeNegState :

Fintype NegState

Equations

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

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instMeasurableSpaceNegState :

MeasurableSpace NegState

Equations

ChampollionAlsopGrosu2019.instMeasurableSpaceNegState = ⊤

instance ChampollionAlsopGrosu2019.instDiscreteMeasurableSpaceNegState :

DiscreteMeasurableSpace NegState

instance ChampollionAlsopGrosu2019.instMeasurableSingletonClassNegState :

MeasurableSingletonClass NegState

inductive ChampollionAlsopGrosu2019.NegUtterance :

The negated utterances (10).

notA : NegUtterance
notB : NegUtterance
notOr : NegUtterance
notAnd : NegUtterance

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidableEqNegUtterance :

DecidableEq NegUtterance

Equations

ChampollionAlsopGrosu2019.instDecidableEqNegUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChampollionAlsopGrosu2019.instReprNegUtterance.repr :

NegUtterance → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instReprNegUtterance :

Repr NegUtterance

Equations

ChampollionAlsopGrosu2019.instReprNegUtterance = { reprPrec := ChampollionAlsopGrosu2019.instReprNegUtterance.repr }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instInhabitedNegUtterance :

Inhabited NegUtterance

Equations

ChampollionAlsopGrosu2019.instInhabitedNegUtterance = { default := ChampollionAlsopGrosu2019.instInhabitedNegUtterance.default }

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instFintypeNegUtterance :

Fintype NegUtterance

Equations

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

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instMeasurableSpaceNegUtterance :

MeasurableSpace NegUtterance

Equations

ChampollionAlsopGrosu2019.instMeasurableSpaceNegUtterance = ⊤

instance ChampollionAlsopGrosu2019.instDiscreteMeasurableSpaceNegUtterance :

DiscreteMeasurableSpace NegUtterance

instance ChampollionAlsopGrosu2019.instMeasurableSingletonClassNegUtterance :

MeasurableSingletonClass NegUtterance

def ChampollionAlsopGrosu2019.N1 :

NegUtterance → NegState → Prop

Interpretation function 1 under negation (11).

Equations

Instances For

def ChampollionAlsopGrosu2019.N2 :

NegUtterance → NegState → Prop

Under negation, interpretation function 2 (12) weakens rather than strengthens.

Equations

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidablePredNegStateN1 (u : NegUtterance) :

DecidablePred (N1 u)

Equations

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

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidablePredNegStateN2 (u : NegUtterance) :

DecidablePred (N2 u)

Equations

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

def ChampollionAlsopGrosu2019.negMeaning :

Interp → NegUtterance → NegState → Prop

The negated meanings indexed by interpretation function.

Equations

Instances For

@[instance_reducible]

instance ChampollionAlsopGrosu2019.instDecidablePredNegStateNegMeaning (i : Interp) (u : NegUtterance) :

DecidablePred (negMeaning i u)

Equations

def ChampollionAlsopGrosu2019.negSem (i : Interp) (u : NegUtterance) :

Finset NegState

The extensions of the negation model.

Equations

ChampollionAlsopGrosu2019.negSem i u = Finset.filter (ChampollionAlsopGrosu2019.negMeaning i u) Finset.univ

Instances For

@[simp]

theorem ChampollionAlsopGrosu2019.mem_negSem {i : Interp} {u : NegUtterance} {w : NegState} :

w ∈ negSem i u ↔ negMeaning i u w

theorem ChampollionAlsopGrosu2019.negSem_notOr (i : Interp) :

negSem i NegUtterance.notOr = {NegState.neither}

The negated disjunction is unambiguous, true exactly at Neither under both functions.

@[reducible, inline]

noncomputable abbrev ChampollionAlsopGrosu2019.negListener (α : ℝ) :

ProbabilityTheory.Kernel NegUtterance (NegState × Interp)

The listener of the negation model.

Equations

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

Instances For

theorem ChampollionAlsopGrosu2019.no_fci_under_negation {α : ℝ} (hα : 0 < α) {p : NegState × Interp} (hp : p.1 ≠ NegState.neither) :

((negListener α) NegUtterance.notOr) {p} = 0

Hearing you may not take an apple or a pear, the listener assigns no mass to any state other than Neither, in particular none to Only A and Only B, where a free-choice reading of the negated disjunction would be true. There is no free choice under negation (Table 9).