RSA Conditional Antecedent Embedding

@cite{chierchia-2004} @cite{geurts-2010} @cite{von-fintel-1999}

Models scalar implicatures embedded in conditional antecedents.

The Phenomenon

"If some students passed, the professor will be happy"

The antecedent of a conditional is a DOWNWARD-ENTAILING context:

• "If all students passed, P" entails "If some students passed, P"

This predicts DE-like blocking of local implicatures, similar to "no one".

Theoretical Background

Conditional antecedents are DE because:

• Let p ⊆ q (p entails q)
• Then: "If q, r" entails "If p, r" (contrapositive reasoning)

For scalar implicatures:

• "some" ⊆ "all" (in terms of truth conditions)
• So: "If all passed, happy" entails "If some passed, happy"

Local SI would strengthen "some" to "some-but-not-all", making:

• "If some-but-not-all passed, happy"

This is WEAKER than "If some passed, happy" (true in fewer cases). RSA should prefer the more informative global interpretation.

inductive RSA.ConditionalEmbedding.StudentResult : Type

Student outcome for conditional scenario.

• noneP : StudentResult
• someP : StudentResult
• allP : StudentResult

instance RSA.ConditionalEmbedding.instDecidableEqStudentResult : DecidableEq StudentResult

Equations

• RSA.ConditionalEmbedding.instDecidableEqStudentResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.ConditionalEmbedding.instReprStudentResult : Repr StudentResult

Equations

• RSA.ConditionalEmbedding.instReprStudentResult = { reprPrec := RSA.ConditionalEmbedding.instReprStudentResult.repr }

def RSA.ConditionalEmbedding.instReprStudentResult.repr : StudentResult → ℕ → Std.Format

Equations

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

instance RSA.ConditionalEmbedding.instBEqStudentResult : BEq StudentResult

Equations

• RSA.ConditionalEmbedding.instBEqStudentResult = { beq := RSA.ConditionalEmbedding.instBEqStudentResult.beq }

def RSA.ConditionalEmbedding.instBEqStudentResult.beq : StudentResult → StudentResult → Bool

Equations

• RSA.ConditionalEmbedding.instBEqStudentResult.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.ConditionalEmbedding.instInhabitedStudentResult : Inhabited StudentResult

Equations

• RSA.ConditionalEmbedding.instInhabitedStudentResult = { default := RSA.ConditionalEmbedding.instInhabitedStudentResult.default }

def RSA.ConditionalEmbedding.instInhabitedStudentResult.default : StudentResult

Equations

• RSA.ConditionalEmbedding.instInhabitedStudentResult.default = RSA.ConditionalEmbedding.StudentResult.noneP

inductive RSA.ConditionalEmbedding.ProfState : Type

Professor's happiness state.

• unhappy : ProfState
• happy : ProfState

instance RSA.ConditionalEmbedding.instDecidableEqProfState : DecidableEq ProfState

Equations

• RSA.ConditionalEmbedding.instDecidableEqProfState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.ConditionalEmbedding.instReprProfState : Repr ProfState

Equations

• RSA.ConditionalEmbedding.instReprProfState = { reprPrec := RSA.ConditionalEmbedding.instReprProfState.repr }

def RSA.ConditionalEmbedding.instReprProfState.repr : ProfState → ℕ → Std.Format

Equations

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

instance RSA.ConditionalEmbedding.instBEqProfState : BEq ProfState

Equations

• RSA.ConditionalEmbedding.instBEqProfState = { beq := RSA.ConditionalEmbedding.instBEqProfState.beq }

def RSA.ConditionalEmbedding.instBEqProfState.beq : ProfState → ProfState → Bool

Equations

• RSA.ConditionalEmbedding.instBEqProfState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.ConditionalEmbedding.instInhabitedProfState : Inhabited ProfState

Equations

• RSA.ConditionalEmbedding.instInhabitedProfState = { default := RSA.ConditionalEmbedding.instInhabitedProfState.default }

def RSA.ConditionalEmbedding.instInhabitedProfState.default : ProfState

Equations

• RSA.ConditionalEmbedding.instInhabitedProfState.default = RSA.ConditionalEmbedding.ProfState.unhappy

structure RSA.ConditionalEmbedding.CondWorld : Type

World for conditional embedding.

Tracks both the student outcome and whether the professor is happy.

• students : StudentResult
• professor : ProfState

def RSA.ConditionalEmbedding.instDecidableEqCondWorld.decEq (x✝ x✝¹ : CondWorld) : Decidable (x✝ = x✝¹)

Equations

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

instance RSA.ConditionalEmbedding.instDecidableEqCondWorld : DecidableEq CondWorld

Equations

• RSA.ConditionalEmbedding.instDecidableEqCondWorld = RSA.ConditionalEmbedding.instDecidableEqCondWorld.decEq

instance RSA.ConditionalEmbedding.instReprCondWorld : Repr CondWorld

Equations

• RSA.ConditionalEmbedding.instReprCondWorld = { reprPrec := RSA.ConditionalEmbedding.instReprCondWorld.repr }

def RSA.ConditionalEmbedding.instReprCondWorld.repr : CondWorld → ℕ → Std.Format

Equations

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

instance RSA.ConditionalEmbedding.instBEqCondWorld : BEq CondWorld

Equations

• RSA.ConditionalEmbedding.instBEqCondWorld = { beq := RSA.ConditionalEmbedding.instBEqCondWorld.beq }

def RSA.ConditionalEmbedding.instBEqCondWorld.beq : CondWorld → CondWorld → Bool

Equations

• RSA.ConditionalEmbedding.instBEqCondWorld.beq { students := a, professor := a_1 } { students := b, professor := b_1 } = (a == b && a_1 == b_1)
• RSA.ConditionalEmbedding.instBEqCondWorld.beq x✝¹ x✝ = false

def RSA.ConditionalEmbedding.instInhabitedCondWorld.default : CondWorld

Equations

• RSA.ConditionalEmbedding.instInhabitedCondWorld.default = { students := default, professor := default }

instance RSA.ConditionalEmbedding.instInhabitedCondWorld : Inhabited CondWorld

Equations

• RSA.ConditionalEmbedding.instInhabitedCondWorld = { default := RSA.ConditionalEmbedding.instInhabitedCondWorld.default }

def RSA.ConditionalEmbedding.somePassed (w : CondWorld) : Bool

"Some students passed" - weak (existential) reading.

Equations

• RSA.ConditionalEmbedding.somePassed w = (w.students == RSA.ConditionalEmbedding.StudentResult.someP || w.students == RSA.ConditionalEmbedding.StudentResult.allP)

def RSA.ConditionalEmbedding.someNotAllPassed (w : CondWorld) : Bool

"Some-but-not-all students passed" - strong (exact) reading.

Equations

• RSA.ConditionalEmbedding.someNotAllPassed w = (w.students == RSA.ConditionalEmbedding.StudentResult.someP)

def RSA.ConditionalEmbedding.allPassed (w : CondWorld) : Bool

"All students passed".

Equations

• RSA.ConditionalEmbedding.allPassed w = (w.students == RSA.ConditionalEmbedding.StudentResult.allP)

def RSA.ConditionalEmbedding.nonePassed (w : CondWorld) : Bool

"No students passed".

Equations

• RSA.ConditionalEmbedding.nonePassed w = (w.students == RSA.ConditionalEmbedding.StudentResult.noneP)

def RSA.ConditionalEmbedding.profHappy (w : CondWorld) : Bool

"The professor is happy".

Equations

• RSA.ConditionalEmbedding.profHappy w = (w.professor == RSA.ConditionalEmbedding.ProfState.happy)

inductive RSA.ConditionalEmbedding.CondInterpretation : Type

Interpretations of "If some students passed, the professor will be happy":

1. Global: "some" is weak; if any student passed, prof is happy
2. Local: "some" is strong; if some-but-not-all passed, prof is happy

• global : CondInterpretation
• local_ : CondInterpretation

instance RSA.ConditionalEmbedding.instDecidableEqCondInterpretation : DecidableEq CondInterpretation

Equations

• RSA.ConditionalEmbedding.instDecidableEqCondInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.ConditionalEmbedding.instReprCondInterpretation : Repr CondInterpretation

Equations

• RSA.ConditionalEmbedding.instReprCondInterpretation = { reprPrec := RSA.ConditionalEmbedding.instReprCondInterpretation.repr }

def RSA.ConditionalEmbedding.instReprCondInterpretation.repr : CondInterpretation → ℕ → Std.Format

Equations

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

instance RSA.ConditionalEmbedding.instBEqCondInterpretation : BEq CondInterpretation

Equations

• RSA.ConditionalEmbedding.instBEqCondInterpretation = { beq := RSA.ConditionalEmbedding.instBEqCondInterpretation.beq }

def RSA.ConditionalEmbedding.instBEqCondInterpretation.beq : CondInterpretation → CondInterpretation → Bool

Equations

• RSA.ConditionalEmbedding.instBEqCondInterpretation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.ConditionalEmbedding.instInhabitedCondInterpretation : Inhabited CondInterpretation

Equations

• RSA.ConditionalEmbedding.instInhabitedCondInterpretation = { default := RSA.ConditionalEmbedding.instInhabitedCondInterpretation.default }

def RSA.ConditionalEmbedding.instInhabitedCondInterpretation.default : CondInterpretation

Equations

• RSA.ConditionalEmbedding.instInhabitedCondInterpretation.default = RSA.ConditionalEmbedding.CondInterpretation.global

instance RSA.ConditionalEmbedding.instFintypeCondInterpretation : Fintype CondInterpretation

Equations

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

def RSA.ConditionalEmbedding.conditionalMeaning (interp : CondInterpretation) (w : CondWorld) : Bool

Material conditional semantics: "If P, Q" = ¬P ∨ Q.

• Global: ¬(some passed) ∨ happy = (none passed) ∨ happy
• Local: ¬(some-not-all passed) ∨ happy = (none ∨ all passed) ∨ happy

Equations

• RSA.ConditionalEmbedding.conditionalMeaning RSA.ConditionalEmbedding.CondInterpretation.global w = (!RSA.ConditionalEmbedding.somePassed w || RSA.ConditionalEmbedding.profHappy w)
• RSA.ConditionalEmbedding.conditionalMeaning RSA.ConditionalEmbedding.CondInterpretation.local_ w = (!RSA.ConditionalEmbedding.someNotAllPassed w || RSA.ConditionalEmbedding.profHappy w)

def RSA.ConditionalEmbedding.condWorlds : List CondWorld

Relevant worlds for the conditional scenario.

We include worlds where the conditional's consequent may or may not hold.

Equations

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

instance RSA.ConditionalEmbedding.instFintypeStudentResult : Fintype StudentResult

Equations

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

instance RSA.ConditionalEmbedding.instFintypeProfState : Fintype ProfState

Equations

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

instance RSA.ConditionalEmbedding.instFintypeCondWorld : Fintype CondWorld

Equations

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

theorem RSA.ConditionalEmbedding.global_false_when_passed_unhappy : conditionalMeaning CondInterpretation.global { students := StudentResult.someP, professor := ProfState.unhappy } = false

Global interpretation: "If some passed, happy"

• False only when: some passed AND prof unhappy
• True when: none passed OR prof happy

theorem RSA.ConditionalEmbedding.global_true_when_none_passed : conditionalMeaning CondInterpretation.global { students := StudentResult.noneP, professor := ProfState.unhappy } = true

theorem RSA.ConditionalEmbedding.local_false_when_someNotAll_unhappy : conditionalMeaning CondInterpretation.local_ { students := StudentResult.someP, professor := ProfState.unhappy } = false

Local interpretation: "If some-but-not-all passed, happy"

• False only when: some-but-not-all passed AND prof unhappy
• True when: (none OR all passed) OR prof happy

theorem RSA.ConditionalEmbedding.local_true_when_all_passed : conditionalMeaning CondInterpretation.local_ { students := StudentResult.allP, professor := ProfState.unhappy } = true

theorem RSA.ConditionalEmbedding.global_entails_local (w : CondWorld) : conditionalMeaning CondInterpretation.global w = true → conditionalMeaning CondInterpretation.local_ w = true

The key DE property: Global ENTAILS Local.

"If some passed, happy" → "If some-but-not-all passed, happy"

This is because:

• Global is false when (some ∧ unhappy) - includes someP and allP
• Local is false only when (some-not-all ∧ unhappy) - only someP

So Global being true implies Local is true.

theorem RSA.ConditionalEmbedding.local_not_entails_global : ∃ (w : CondWorld), conditionalMeaning CondInterpretation.local_ w = true ∧ conditionalMeaning CondInterpretation.global w = false

Local does NOT entail Global. When all students passed and prof is unhappy:

• Local is true (antecedent "some-not-all" is false)
• Global is false (antecedent "some" is true, consequent false)

theorem RSA.ConditionalEmbedding.conditional_antecedent_is_DE (w : CondWorld) : (!somePassed w || profHappy w) = true → (!allPassed w || profHappy w) = true

The conditional antecedent is DE: weakening the antecedent strengthens the conditional.

"If some passed, happy" entails "If all passed, happy" because:

• some ⊇ all (some is satisfied by more worlds than all)
• So the weaker antecedent gives a stronger conditional

This is the DE property: p ⊆ q implies "If q, r" ⊆ "If p, r"

theorem RSA.ConditionalEmbedding.conditional_like_de_context : (∀ (w : CondWorld), conditionalMeaning CondInterpretation.global w = true → conditionalMeaning CondInterpretation.local_ w = true) ∧ ∃ (w : CondWorld), conditionalMeaning CondInterpretation.local_ w = true ∧ conditionalMeaning CondInterpretation.global w = false

RSA predicts: in conditional antecedents, global is preferred over local. This is the same prediction as for DE contexts under "no".