Economy of Structure and Information

@cite{heim-1991} @cite{hurford-1974} @cite{katzir-2007} @cite{katzir-singh-2015} @cite{magri-2009} @cite{spector-2014}

@cite{katzir-singh-2015}. Proceedings of Sinn und Bedeutung 19, pp. 322–339.

Two felicity conditions on assertions:

1. Question Condition (def 8): An assertion must address a good question — one not trivially settled by the common ground.

2. Answer Condition (def 15): An assertion must not be needlessly inferior to any alternative — where inferiority combines structural complexity with semantic strength.

These two conditions unify:

• @cite{magri-2009} oddness (# Some Italians come from a warm country)
• @cite{spector-2014} oddness (# All Italians...; # John has one wife)
• Hurford's constraint (# John visited France or Paris)
• Maximize Presupposition! (# A sun is shining)
• DE reversal of oddness patterns

Open problem: oddness under embedding (K&S §4) — the conditions are stated globally but oddness persists in embedded constituents.

structure KatzirSingh2015.Scenario (W : Type u_1) (U : Type u_2) : Type (max u_1 u_2)

Discourse scenario packaging meaning, complexity, context, and QUD.

• meaning: interpretation of each utterance at each world
• complexity: structural complexity; lower = simpler
• context: common knowledge; context w = true iff w is CK-compatible
• qud: question under discussion (equivalence relation on worlds)
• utterances: speaker's available alternatives
• worlds: exhaustive world enumeration

• meaning : U → W → Bool
• complexity : U → ℕ
• context : W → Bool
• qud : QUD W
• utterances : List U
• worlds : List W

def KatzirSingh2015.Scenario.cWorlds {W : Type u_1} {U : Type u_2} (s : Scenario W U) : List W

Context-compatible worlds.

Equations

• s.cWorlds = List.filter s.context s.worlds

def KatzirSingh2015.Scenario.badQuestion {W : Type u_1} {U : Type u_2} (s : Scenario W U) : Bool

Question Condition violation (K&S def 7–8): the QUD is trivially settled by CK — all context-compatible worlds give the same answer.

Each scenario defines its QUD via a content-specific projection function (e.g., warmthAnswer, gradeAnswer) that maps worlds to semantically meaningful answer types. For minimal world types, these projections happen to be injective (each world encodes a distinct answer), but making the question explicit ensures the model extends correctly to richer world types where multiple worlds could give the same answer.

Equations

• s.badQuestion = s.cWorlds.all fun (w : W) => s.cWorlds.all fun (v : W) => s.qud.sameAnswer w v

def KatzirSingh2015.Scenario.semEntails {W : Type u_1} {U : Type u_2} (s : Scenario W U) (u v : U) : Bool

Semantic entailment over ALL worlds: ⟦u⟧ ⊆ ⟦v⟧. Uses all worlds (not just context), since the better-than relation compares general semantic strength (K&S def 16a).

Equations

• s.semEntails u v = s.worlds.all fun (w : W) => !s.meaning u w || s.meaning v w

def KatzirSingh2015.Scenario.atLeastAsGood {W : Type u_1} {U : Type u_2} (s : Scenario W U) (u v : U) : Bool

At-least-as-good-as (K&S def 16a): φ ≲ ψ iff φ is at most as complex as ψ AND semantically at least as strong (⟦φ⟧ ⊆ ⟦ψ⟧).

Equations

• s.atLeastAsGood u v = (decide (s.complexity u ≤ s.complexity v) && s.semEntails u v)

def KatzirSingh2015.Scenario.betterThan {W : Type u_1} {U : Type u_2} (s : Scenario W U) (u v : U) : Bool

Strictly better-than (K&S def 16b): φ ≺ ψ := φ ≲ ψ ∧ ¬(ψ ≲ φ).

Equations

• s.betterThan u v = (s.atLeastAsGood u v && !s.atLeastAsGood v u)

def KatzirSingh2015.Scenario.needlesslyInferior {W : Type u_1} {U : Type u_2} (s : Scenario W U) (u : U) : Bool

Answer Condition violation (K&S def 15): u is needlessly inferior — there exists a strictly better alternative.

Equations

• s.needlesslyInferior u = s.utterances.any fun (v : U) => s.betterThan v u

def KatzirSingh2015.Scenario.isOdd {W : Type u_1} {U : Type u_2} (s : Scenario W U) (u : U) : Bool

K&S Oddness: violates Question Condition or Answer Condition.

Equations

• s.isOdd u = (s.badQuestion || s.needlesslyInferior u)

def KatzirSingh2015.Scenario.contextEquiv {W : Type u_1} {U : Type u_2} (s : Scenario W U) (u v : U) : Bool

Contextual equivalence: same truth value at all CK-compatible worlds.

Equations

• s.contextEquiv u v = s.cWorlds.all fun (w : W) => s.meaning u w == s.meaning v w

def KatzirSingh2015.Scenario.needlesslyInferiorStrict {W : Type u_1} {U : Type u_2} (s : Scenario W U) (u : U) : Bool

Strengthened Answer Condition: also requires the dominating alternative to be compatible with the context (true at some CK-world). This closes a truth gap where needlesslyInferior could flag an utterance as odd because a false-but-simpler alternative exists.

For all 5 K&S scenarios, this coincides with needlesslyInferior (verified below).

Equations

• s.needlesslyInferiorStrict u = s.utterances.any fun (v : U) => s.betterThan v u && s.cWorlds.any (s.meaning v)

structure KatzirSingh2015.SemanticModel (W : Type u_1) (U : Type u_2) : Type (max u_1 u_2)

Reusable semantic model: meaning, complexity, world enumeration, and utterance alternatives. Factored out of Scenario so the same model can be paired with different discourse contexts.

• meaning : U → W → Bool
• complexity : U → ℕ
• worlds : List W
• utterances : List U

structure KatzirSingh2015.DiscourseContext (W : Type u_1) : Type u_1

Discourse context: context set + QUD. Factored out so different questions/contexts can be explored with the same semantic model.

• context : W → Bool
• qud : QUD W

def KatzirSingh2015.Scenario.mk' {W : Type u_1} {U : Type u_2} (m : SemanticModel W U) (d : DiscourseContext W) : Scenario W U

Build a Scenario from composable pieces.

Equations

• KatzirSingh2015.Scenario.mk' m d = { meaning := m.meaning, complexity := m.complexity, context := d.context, qud := d.qud, utterances := m.utterances, worlds := m.worlds }

def KatzirSingh2015.isCContradiction {W : Type u_1} (worlds : List W) (C φ' : W → Bool) : Bool

C-contradiction: incompatible with context. (@cite{spector-2014}, def 4a)

Equations

• KatzirSingh2015.isCContradiction worlds C φ' = worlds.all fun (w : W) => !C w || !φ' w

def KatzirSingh2015.isCTautology {W : Type u_1} (worlds : List W) (C φ' : W → Bool) : Bool

C-tautology: entailed by context. (@cite{spector-2014}, def 4b)

Equations

• KatzirSingh2015.isCTautology worlds C φ' = worlds.all fun (w : W) => !C w || φ' w

def KatzirSingh2015.isCEquivalent {W : Type u_1} (worlds : List W) (C φ φ' : W → Bool) : Bool

C-equivalent to φ: same truth value in context. (@cite{spector-2014}, def 4c)

Equations

• KatzirSingh2015.isCEquivalent worlds C φ φ' = worlds.all fun (w : W) => !C w || φ w == φ' w

def KatzirSingh2015.isTrivialInC {W : Type u_1} (worlds : List W) (C φ φ' : W → Bool) : Bool

Trivial in C given φ. (@cite{spector-2014}, def 4)

Equations

• KatzirSingh2015.isTrivialInC worlds C φ φ' = (KatzirSingh2015.isCContradiction worlds C φ' || KatzirSingh2015.isCTautology worlds C φ' || KatzirSingh2015.isCEquivalent worlds C φ φ')

def KatzirSingh2015.allAlternativesTrivial {W : Type u_1} (worlds : List W) (C φ : W → Bool) (alts : List (W → Bool)) : Bool

No Trivial Alternatives violation (@cite{spector-2014}, def 5): ALL alternatives are trivial in C given φ.

Equations

• KatzirSingh2015.allAlternativesTrivial worlds C φ alts = alts.all fun (φ' : W → Bool) => KatzirSingh2015.isTrivialInC worlds C φ φ'

K&S ex. (1)–(2): "# Some/All Italians come from a warm country"

The example is due to @cite{magri-2009}, who explains the oddness via blind mandatory scalar implicatures (see Magri2009.lean). K&S offer an alternative explanation: the QUD is trivially settled by CK.

CK: Italy is a warm country. Since all Italians come from Italy, the QUD "Do [some/all] Italians come from a warm country?" is trivially settled → Question Condition violation.

Both K&S and @cite{spector-2014} predict oddness here (§1.2).

inductive KatzirSingh2015.ItalyWorld : Type

• allWarm : ItalyWorld
• noneWarm : ItalyWorld

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqItalyWorld : DecidableEq ItalyWorld

Equations

• KatzirSingh2015.instDecidableEqItalyWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprItalyWorld.repr : ItalyWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KatzirSingh2015.instReprItalyWorld : Repr ItalyWorld

Equations

• KatzirSingh2015.instReprItalyWorld = { reprPrec := KatzirSingh2015.instReprItalyWorld.repr }

inductive KatzirSingh2015.ItalyUtt : Type

• some_ : ItalyUtt
• all_ : ItalyUtt

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqItalyUtt : DecidableEq ItalyUtt

Equations

• KatzirSingh2015.instDecidableEqItalyUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprItalyUtt.repr : ItalyUtt → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KatzirSingh2015.instReprItalyUtt : Repr ItalyUtt

Equations

• KatzirSingh2015.instReprItalyUtt = { reprPrec := KatzirSingh2015.instReprItalyUtt.repr }

def KatzirSingh2015.warmthAnswer : ItalyWorld → Bool

"Do Italians come from a warm country?" — a yes/no question.

Equations

• KatzirSingh2015.warmthAnswer KatzirSingh2015.ItalyWorld.allWarm = true
• KatzirSingh2015.warmthAnswer KatzirSingh2015.ItalyWorld.noneWarm = false

def KatzirSingh2015.italianWarmthScenario : Scenario ItalyWorld ItalyUtt

Equations

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

theorem KatzirSingh2015.italianWarmth_contextEquiv : italianWarmthScenario.contextEquiv ItalyUtt.some_ ItalyUtt.all_ = true

Contextual equivalence: some ↔ all (CK makes them interchangeable).

theorem KatzirSingh2015.italianWarmth_badQuestion : italianWarmthScenario.badQuestion = true

QUD trivially settled by CK → Question Condition violated.

theorem KatzirSingh2015.italianWarmth_some_odd : italianWarmthScenario.isOdd ItalyUtt.some_ = true

K&S prediction: "some" is odd.

theorem KatzirSingh2015.italianWarmth_all_odd : italianWarmthScenario.isOdd ItalyUtt.all_ = true

K&S prediction: "all" is odd.

theorem KatzirSingh2015.spector_agrees_italianWarmth : allAlternativesTrivial [ItalyWorld.allWarm, ItalyWorld.noneWarm] (fun (w : ItalyWorld) => w == ItalyWorld.allWarm) (italianWarmthScenario.meaning ItalyUtt.some_) [italianWarmthScenario.meaning ItalyUtt.all_] = true

Bridge: @cite{spector-2014} makes the same prediction (all alternatives trivial).

K&S ex. (14)/(17): "In this department, every professor gives the same grade to all of his students. Kim is a professor." (a) # This year, Kim assigned an A to some of his students — ODD (b) This year, Kim assigned an A to all of his students — OK

The QUD is good (we don't know Kim's grade). But "some" is needlessly weak: "all" is equally complex and semantically stronger.

Connects to Core.Scale: the ⟦all⟧ ⊆ ⟦some⟧ entailment that drives the Answer Condition is the same relationship captured by Alternatives.Quantifiers.entails.all.some_ = true.

inductive KatzirSingh2015.GradeWorld : Type

• allA : GradeWorld
• someNotAll : GradeWorld
• noneA : GradeWorld

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqGradeWorld : DecidableEq GradeWorld

Equations

• KatzirSingh2015.instDecidableEqGradeWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprGradeWorld.repr : GradeWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KatzirSingh2015.instReprGradeWorld : Repr GradeWorld

Equations

• KatzirSingh2015.instReprGradeWorld = { reprPrec := KatzirSingh2015.instReprGradeWorld.repr }

inductive KatzirSingh2015.GradeUtt : Type

• some_ : GradeUtt
• all_ : GradeUtt

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqGradeUtt : DecidableEq GradeUtt

Equations

• KatzirSingh2015.instDecidableEqGradeUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KatzirSingh2015.instReprGradeUtt : Repr GradeUtt

Equations

• KatzirSingh2015.instReprGradeUtt = { reprPrec := KatzirSingh2015.instReprGradeUtt.repr }

def KatzirSingh2015.instReprGradeUtt.repr : GradeUtt → ℕ → Std.Format

Equations

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

def KatzirSingh2015.gradeAnswer : GradeWorld → Bool × Bool

"How many of Kim's students got an A?" — answer encoded as (some-got-A, all-got-A) truth values on the ⟨some, all⟩ scale.

Equations

• KatzirSingh2015.gradeAnswer KatzirSingh2015.GradeWorld.allA = (true, true)
• KatzirSingh2015.gradeAnswer KatzirSingh2015.GradeWorld.someNotAll = (true, false)
• KatzirSingh2015.gradeAnswer KatzirSingh2015.GradeWorld.noneA = (false, false)

def KatzirSingh2015.gradeScenario : Scenario GradeWorld GradeUtt

Equations

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

theorem KatzirSingh2015.grade_goodQuestion : gradeScenario.badQuestion = false

QUD is NOT trivially settled (Kim might or might not have given A).

theorem KatzirSingh2015.grade_all_entails_some : gradeScenario.semEntails GradeUtt.all_ GradeUtt.some_ = true

"all" entails "some" (semantically stronger in all worlds).

theorem KatzirSingh2015.grade_some_not_entails_all : gradeScenario.semEntails GradeUtt.some_ GradeUtt.all_ = false

"some" does NOT entail "all" (true at someNotAll where "all" is false).

theorem KatzirSingh2015.grade_all_better_than_some : gradeScenario.betterThan GradeUtt.all_ GradeUtt.some_ = true

"all" ≺ "some" (equally complex, strictly stronger).

theorem KatzirSingh2015.grade_some_odd : gradeScenario.isOdd GradeUtt.some_ = true

K&S prediction: "some" is odd (needlessly weak).

theorem KatzirSingh2015.grade_all_ok : gradeScenario.isOdd GradeUtt.all_ = false

K&S prediction: "all" is fine (best available answer).

theorem KatzirSingh2015.grade_contextEquiv : gradeScenario.contextEquiv GradeUtt.some_ GradeUtt.all_ = true

Contextual equivalence despite general non-equivalence.

K&S ex. (22): "# John visited France or Paris"

Since Paris ⊆ France, "France or Paris" ≡ "France" semantically. But the disjunction is structurally more complex (complexity 2 vs 1). So "France" ≺ "France or Paris" → disjunction is needlessly complex.

Connects to RSA/ScalarImplicatures/Hurford.lean which models Hurford's constraint via speaker rationality. K&S derive the same prediction from economy, without RSA machinery.

inductive KatzirSingh2015.VisitWorld : Type

• parisOnly : VisitWorld
• franceNotParis : VisitWorld
• neither : VisitWorld

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqVisitWorld : DecidableEq VisitWorld

Equations

• KatzirSingh2015.instDecidableEqVisitWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KatzirSingh2015.instReprVisitWorld : Repr VisitWorld

Equations

• KatzirSingh2015.instReprVisitWorld = { reprPrec := KatzirSingh2015.instReprVisitWorld.repr }

def KatzirSingh2015.instReprVisitWorld.repr : VisitWorld → ℕ → Std.Format

Equations

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

inductive KatzirSingh2015.VisitUtt : Type

• france : VisitUtt
• franceOrParis : VisitUtt

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqVisitUtt : DecidableEq VisitUtt

Equations

• KatzirSingh2015.instDecidableEqVisitUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprVisitUtt.repr : VisitUtt → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KatzirSingh2015.instReprVisitUtt : Repr VisitUtt

Equations

• KatzirSingh2015.instReprVisitUtt = { reprPrec := KatzirSingh2015.instReprVisitUtt.repr }

def KatzirSingh2015.visitAnswer : VisitWorld → Bool

"Did John visit France?" — a yes/no question. Genuinely coarser than identity: parisOnly and franceNotParis collapse (both → visited).

Equations

• KatzirSingh2015.visitAnswer KatzirSingh2015.VisitWorld.parisOnly = true
• KatzirSingh2015.visitAnswer KatzirSingh2015.VisitWorld.franceNotParis = true
• KatzirSingh2015.visitAnswer KatzirSingh2015.VisitWorld.neither = false

def KatzirSingh2015.hurfordScenario : Scenario VisitWorld VisitUtt

Hurford alternatives: the disjunction vs. its simple equivalent. "Paris" is excluded from utterance alternatives because the Hurford comparison is between a complex form and its semantically equivalent simpler form, not between independently informative expressions.

Equations

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

theorem KatzirSingh2015.hurford_equiv : hurfordScenario.semEntails VisitUtt.france VisitUtt.franceOrParis = true ∧ hurfordScenario.semEntails VisitUtt.franceOrParis VisitUtt.france = true

"France" and "France or Paris" are semantically equivalent (Paris ⊆ France, so the disjunction adds nothing).

theorem KatzirSingh2015.hurford_france_better : hurfordScenario.betterThan VisitUtt.france VisitUtt.franceOrParis = true

"France" ≺ "France or Paris" (simpler + equally strong).

theorem KatzirSingh2015.hurford_disjunction_odd : hurfordScenario.isOdd VisitUtt.franceOrParis = true

K&S prediction: "France or Paris" is odd (needlessly complex).

theorem KatzirSingh2015.hurford_france_ok : hurfordScenario.isOdd VisitUtt.france = false

K&S prediction: "France" is fine (no better alternative available).

K&S ex. (18): "Every prof who assigned an A to [some/all] got a raise"

In DE restrictor, "some" picks out MORE professors → stronger universal. The entailment direction reverses: ⟦some⟧_DE ⊆ ⟦all⟧_DE. So "all" becomes needlessly weak (opposite of UE).

Connects to Semantics.Montague/Sentence/Entailment/Monotonicity.lean: the reversal here is the same phenomenon as every_restr_DE.

inductive KatzirSingh2015.DEWorld : Type

• w1 : DEWorld
• w2 : DEWorld
• w3 : DEWorld

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqDEWorld : DecidableEq DEWorld

Equations

• KatzirSingh2015.instDecidableEqDEWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprDEWorld.repr : DEWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KatzirSingh2015.instReprDEWorld : Repr DEWorld

Equations

• KatzirSingh2015.instReprDEWorld = { reprPrec := KatzirSingh2015.instReprDEWorld.repr }

inductive KatzirSingh2015.DEUtt : Type

• some_ : DEUtt
• all_ : DEUtt

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqDEUtt : DecidableEq DEUtt

Equations

• KatzirSingh2015.instDecidableEqDEUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KatzirSingh2015.instReprDEUtt : Repr DEUtt

Equations

• KatzirSingh2015.instReprDEUtt = { reprPrec := KatzirSingh2015.instReprDEUtt.repr }

def KatzirSingh2015.instReprDEUtt.repr : DEUtt → ℕ → Std.Format

Equations

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

def KatzirSingh2015.deAnswer : DEWorld → Bool × Bool

"A to some or all?" in DE — answer encoded as (some_DE, all_DE) truth values.

Equations

• KatzirSingh2015.deAnswer KatzirSingh2015.DEWorld.w1 = (true, true)
• KatzirSingh2015.deAnswer KatzirSingh2015.DEWorld.w2 = (false, true)
• KatzirSingh2015.deAnswer KatzirSingh2015.DEWorld.w3 = (false, false)

def KatzirSingh2015.deScenario : Scenario DEWorld DEUtt

DE scenario: "some" version is stronger (narrower truth set). In UE, ⟦all⟧ ⊆ ⟦some⟧; in DE, this reverses to ⟦some⟧_DE ⊆ ⟦all⟧_DE.

Equations

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

theorem KatzirSingh2015.de_some_entails_all : deScenario.semEntails DEUtt.some_ DEUtt.all_ = true

DE reversal: "some" entails "all" (opposite of UE).

theorem KatzirSingh2015.de_all_not_entails_some : deScenario.semEntails DEUtt.all_ DEUtt.some_ = false

"all" does NOT entail "some" in DE.

theorem KatzirSingh2015.de_some_better_than_all : deScenario.betterThan DEUtt.some_ DEUtt.all_ = true

DE: "some" ≺ "all" (reversed from UE where "all" ≺ "some").

theorem KatzirSingh2015.de_all_odd : deScenario.isOdd DEUtt.all_ = true

K&S prediction in DE: "all" is odd (needlessly weak).

theorem KatzirSingh2015.de_some_ok : deScenario.isOdd DEUtt.some_ = false

K&S prediction in DE: "some" is fine (the stronger answer).

theorem KatzirSingh2015.ue_de_reversal : gradeScenario.semEntails GradeUtt.all_ GradeUtt.some_ = true ∧ deScenario.semEntails DEUtt.some_ DEUtt.all_ = true

Cross-scenario bridge: UE and DE have opposite entailment directions.

theorem KatzirSingh2015.ue_de_oddness_flips : gradeScenario.isOdd GradeUtt.some_ = true ∧ gradeScenario.isOdd GradeUtt.all_ = false ∧ deScenario.isOdd DEUtt.all_ = true ∧ deScenario.isOdd DEUtt.some_ = false

Cross-scenario bridge: UE and DE have opposite oddness verdicts.

K&S ex. (21): "# A sun is shining" vs. "The sun is shining"

CK: there is exactly one sun. Both utterances are contextually equivalent. But "the sun" presupposes uniqueness, making it semantically stronger (⟦the sun is shining⟧ ⊂ ⟦a sun is shining⟧). So "a sun" is needlessly weak → Maximize Presupposition falls out as Answer Condition.

Connects to Core/Presupposition.lean: the definite's stronger presupposition is what gives "the" its semantic advantage under K&S's ordering.

inductive KatzirSingh2015.SunWorld : Type

• oneShining : SunWorld
• oneNotShining : SunWorld
• manySuns : SunWorld

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqSunWorld : DecidableEq SunWorld

Equations

• KatzirSingh2015.instDecidableEqSunWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KatzirSingh2015.instReprSunWorld : Repr SunWorld

Equations

• KatzirSingh2015.instReprSunWorld = { reprPrec := KatzirSingh2015.instReprSunWorld.repr }

def KatzirSingh2015.instReprSunWorld.repr : SunWorld → ℕ → Std.Format

Equations

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

inductive KatzirSingh2015.SunUtt : Type

• aSun : SunUtt
• theSun : SunUtt

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqSunUtt : DecidableEq SunUtt

Equations

• KatzirSingh2015.instDecidableEqSunUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KatzirSingh2015.instReprSunUtt : Repr SunUtt

Equations

• KatzirSingh2015.instReprSunUtt = { reprPrec := KatzirSingh2015.instReprSunUtt.repr }

def KatzirSingh2015.instReprSunUtt.repr : SunUtt → ℕ → Std.Format

Equations

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

def KatzirSingh2015.sunAnswer : SunWorld → Option Bool

"Is the sun shining?" — presupposition-sensitive answer. manySuns is a presupposition failure (uniqueness violated), distinct from both yes and no.

Equations

• KatzirSingh2015.sunAnswer KatzirSingh2015.SunWorld.oneShining = some true
• KatzirSingh2015.sunAnswer KatzirSingh2015.SunWorld.oneNotShining = some false
• KatzirSingh2015.sunAnswer KatzirSingh2015.SunWorld.manySuns = none

def KatzirSingh2015.maxPresupScenario : Scenario SunWorld SunUtt

Equations

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

theorem KatzirSingh2015.maxPresup_the_entails_a : maxPresupScenario.semEntails SunUtt.theSun SunUtt.aSun = true

"the sun" entails "a sun" (presuppositional strength).

theorem KatzirSingh2015.maxPresup_a_not_entails_the : maxPresupScenario.semEntails SunUtt.aSun SunUtt.theSun = false

"a sun" does NOT entail "the sun" (true at manySuns where "the" fails).

theorem KatzirSingh2015.maxPresup_the_better : maxPresupScenario.betterThan SunUtt.theSun SunUtt.aSun = true

"the sun" ≺ "a sun" (equally complex, strictly stronger).

theorem KatzirSingh2015.maxPresup_indefinite_odd : maxPresupScenario.isOdd SunUtt.aSun = true

K&S prediction: "a sun" is odd (= Maximize Presupposition!).

theorem KatzirSingh2015.maxPresup_definite_ok : maxPresupScenario.isOdd SunUtt.theSun = false

K&S prediction: "the sun" is fine.

theorem KatzirSingh2015.maxPresup_contextEquiv : maxPresupScenario.contextEquiv SunUtt.aSun SunUtt.theSun = true

Contextual equivalence: CK (unique sun) makes a/the equivalent.

theorem KatzirSingh2015.conditions_independent : italianWarmthScenario.badQuestion = true ∧ gradeScenario.badQuestion = false ∧ gradeScenario.needlesslyInferior GradeUtt.some_ = true ∧ italianWarmthScenario.needlesslyInferior ItalyUtt.some_ = false

The Question Condition and Answer Condition are independent:

• Italian warmth: Question Condition violated, Answer Condition irrelevant
• Grade: Question Condition satisfied, Answer Condition violated This shows neither condition subsumes the other.

Verify that needlesslyInferiorStrict (context-aware) coincides with needlesslyInferior on all 5 scenarios. This confirms the truth gap doesn't affect the existing examples.

theorem KatzirSingh2015.strict_agrees_italianWarmth : italianWarmthScenario.needlesslyInferiorStrict ItalyUtt.some_ = italianWarmthScenario.needlesslyInferior ItalyUtt.some_

theorem KatzirSingh2015.strict_agrees_grade : gradeScenario.needlesslyInferiorStrict GradeUtt.some_ = gradeScenario.needlesslyInferior GradeUtt.some_

theorem KatzirSingh2015.strict_agrees_hurford : hurfordScenario.needlesslyInferiorStrict VisitUtt.franceOrParis = hurfordScenario.needlesslyInferior VisitUtt.franceOrParis

theorem KatzirSingh2015.strict_agrees_de : deScenario.needlesslyInferiorStrict DEUtt.all_ = deScenario.needlesslyInferior DEUtt.all_

theorem KatzirSingh2015.strict_agrees_maxPresup : maxPresupScenario.needlesslyInferiorStrict SunUtt.aSun = maxPresupScenario.needlesslyInferior SunUtt.aSun

Demonstrate that SemanticModel + DiscourseContext can be composed via Scenario.mk'. The DE scenario's semantic model is reused with a different discourse context (all worlds CK-compatible).

def KatzirSingh2015.deModel : SemanticModel DEWorld DEUtt

DE scenario's semantic model, factored out for reuse.

Equations

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

def KatzirSingh2015.deDiscourseOriginal : DiscourseContext DEWorld

Original DE discourse context (w2 ruled out by CK).

Equations

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

def KatzirSingh2015.deDiscourseOpen : DiscourseContext DEWorld

Alternative discourse context: all worlds CK-compatible.

Equations

• KatzirSingh2015.deDiscourseOpen = { context := fun (x : KatzirSingh2015.DEWorld) => true, qud := QUD.ofDecEq KatzirSingh2015.deAnswer "A to some or all? (open CK)" }

theorem KatzirSingh2015.compose_matches_de : have s := Scenario.mk' deModel deDiscourseOriginal; s.isOdd DEUtt.all_ = true ∧ s.isOdd DEUtt.some_ = false

The composed scenario matches the original deScenario.

theorem KatzirSingh2015.compose_open_context : have s := Scenario.mk' deModel deDiscourseOpen; s.isOdd DEUtt.all_ = true ∧ s.isOdd DEUtt.some_ = false

With open context (w2 now CK-compatible), "all" is still odd: "some" still entails "all" in the DE model, so the Answer Condition is unchanged. But the context change demonstrates reuse of the semantic model with a different discourse context.

K&S predict that an explicit question neutralizes the Question Condition.

(3a) # John has one wife — odd (no explicit question) (11a) (How many wives does John have?) John has one wife — OK

The explicit question makes the QUD a "good question" (K&S (7)) regardless of whether CK settles it. Oddness then depends solely on the Answer Condition. Since "one wife" is not needlessly inferior (all alternatives are CK-incompatible), the sentence is felicitous.

This is a genuine prediction difference with @cite{spector-2014}: Spector predicts oddness persists because the triviality of alternatives is unchanged by the explicit question (K&S §2.2, p. 327).

inductive KatzirSingh2015.WifeWorld : Type

• oneWife : WifeWorld
• twoWives : WifeWorld
• noWife : WifeWorld

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqWifeWorld : DecidableEq WifeWorld

Equations

• KatzirSingh2015.instDecidableEqWifeWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KatzirSingh2015.instReprWifeWorld : Repr WifeWorld

Equations

• KatzirSingh2015.instReprWifeWorld = { reprPrec := KatzirSingh2015.instReprWifeWorld.repr }

def KatzirSingh2015.instReprWifeWorld.repr : WifeWorld → ℕ → Std.Format

Equations

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

inductive KatzirSingh2015.WifeUtt : Type

• one : WifeUtt
• two : WifeUtt
• zero : WifeUtt

@[implicit_reducible]

instance KatzirSingh2015.instDecidableEqWifeUtt : DecidableEq WifeUtt

Equations

• KatzirSingh2015.instDecidableEqWifeUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KatzirSingh2015.instReprWifeUtt : Repr WifeUtt

Equations

• KatzirSingh2015.instReprWifeUtt = { reprPrec := KatzirSingh2015.instReprWifeUtt.repr }

def KatzirSingh2015.instReprWifeUtt.repr : WifeUtt → ℕ → Std.Format

Equations

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

def KatzirSingh2015.wifeModel : SemanticModel WifeWorld WifeUtt

Semantic model for "John has N wives" (shared across discourse contexts).

Equations

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

def KatzirSingh2015.wifeCount : WifeWorld → ℕ

"How many wives does John have?" — answer is a count.

Equations

• KatzirSingh2015.wifeCount KatzirSingh2015.WifeWorld.oneWife = 1
• KatzirSingh2015.wifeCount KatzirSingh2015.WifeWorld.twoWives = 2
• KatzirSingh2015.wifeCount KatzirSingh2015.WifeWorld.noWife = 0

def KatzirSingh2015.wifeContextCK : DiscourseContext WifeWorld

Discourse context: CK = monogamous society (John has exactly one wife).

Equations

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

def KatzirSingh2015.wifeScenario : Scenario WifeWorld WifeUtt

Equations

• KatzirSingh2015.wifeScenario = KatzirSingh2015.Scenario.mk' KatzirSingh2015.wifeModel KatzirSingh2015.wifeContextCK

theorem KatzirSingh2015.wife_badQuestion : wifeScenario.badQuestion = true

QUD trivially settled by CK (everyone knows John has one wife).

theorem KatzirSingh2015.wife_one_not_inferior : wifeScenario.needlesslyInferior WifeUtt.one = false

"One wife" is NOT needlessly inferior: the alternatives ("two wives", "zero wives") are CK-incompatible and semantically independent, so neither is strictly better.

theorem KatzirSingh2015.wife_one_odd : wifeScenario.isOdd WifeUtt.one = true

Without explicit question: "John has one wife" is odd. K&S (3a): the QUD is trivially settled → Question Condition violated.

theorem KatzirSingh2015.wife_rescue_answer_condition : wifeScenario.needlesslyInferior WifeUtt.one = false

K&S prediction with explicit question (K&S (11a)):

When "How many wives does John have?" is explicitly asked, the Question Condition is satisfied (the question is good by K&S (7) — all participants are committed to settling it). Oddness depends solely on the Answer Condition. Since "one wife" is not needlessly inferior, the sentence becomes felicitous.

Formally: isOdd = badQuestion ∨ needlesslyInferior. The explicit question eliminates badQuestion, leaving only needlesslyInferior, which is false.

theorem KatzirSingh2015.spector_wife_still_odd : allAlternativesTrivial [WifeWorld.oneWife, WifeWorld.twoWives, WifeWorld.noWife] (fun (w : WifeWorld) => w == WifeWorld.oneWife) (wifeScenario.meaning WifeUtt.one) [wifeScenario.meaning WifeUtt.two, wifeScenario.meaning WifeUtt.zero] = true

@cite{spector-2014} disagrees: "John has one wife" remains odd even with the explicit question. All alternatives are trivial in CK:

• "two wives" is a C-contradiction (incompatible with CK)
• "zero wives" is a C-contradiction (incompatible with CK) Since ALL alternatives are trivial, Spector's No Trivial Alternatives condition (K&S (5)) is violated regardless of whether a question was asked. Triviality is a property of the alternatives in context, not of the discourse.

theorem KatzirSingh2015.ks_spector_diverge_wife : wifeScenario.needlesslyInferior WifeUtt.one = false ∧ allAlternativesTrivial [WifeWorld.oneWife, WifeWorld.twoWives, WifeWorld.noWife] (fun (w : WifeWorld) => w == WifeWorld.oneWife) (wifeScenario.meaning WifeUtt.one) [wifeScenario.meaning WifeUtt.two, wifeScenario.meaning WifeUtt.zero] = true

K&S vs Spector divergence on explicit question rescue:

• K&S: Answer Condition alone → "one wife" is fine (not needlessly inferior)
• Spector: all alternatives trivial → still odd (explicit question irrelevant) This is the core empirical test case between the two theories.

K&S's Hurford scenario (§5, K&S (22)) models entailing disjunctions as needlessly complex answers. This bridges to the empirical Hurford data in ScalarImplicatures.Basic, showing the theory accounts for the observed infelicity judgments.

The rescue cases (K&S (24): "some or all", "possible or necessary") require embedded exhaustification + a grammatical knowledge operator (K&S §3.3.2, citing Meyer 2013). This additional machinery is beyond the scope of the current formalization.

theorem KatzirSingh2015.ks_hurford_matches_empirical : hurfordScenario.isOdd VisitUtt.franceOrParis = true ∧ (Phenomena.ScalarImplicatures.hurfordViolations.all fun (x : Phenomena.ScalarImplicatures.HurfordDatum) => x.felicitous == false) = true

K&S's theoretical prediction matches the empirical Hurford data:

• Theory: entailing disjunctions are needlessly complex → odd
• Data: hurfordViolations are all infelicitous

The theoretical mechanism (Answer Condition: betterThan .france .franceOrParis) produces the same verdict as the empirical observation.

theorem KatzirSingh2015.ks_hurford_mechanism : hurfordScenario.semEntails VisitUtt.france VisitUtt.franceOrParis = true ∧ hurfordScenario.semEntails VisitUtt.franceOrParis VisitUtt.france = true ∧ hurfordScenario.betterThan VisitUtt.france VisitUtt.franceOrParis = true ∧ hurfordScenario.isOdd VisitUtt.france = false

The theoretical mechanism: "France" ≺ "France or Paris" because "France" is simpler (complexity 1 < 2) and semantically equivalent (Paris ⊆ France). This is the same entailment pattern observed in the empirical Hurford data: each violation has B ⊆ A or A ⊆ B.

theorem KatzirSingh2015.hurford_rescued_match_data : (Phenomena.ScalarImplicatures.hurfordRescuedCases.all fun (x : Phenomena.ScalarImplicatures.HurfordDatum) => x.felicitous == true) = true

Empirical prediction: rescued Hurford cases are felicitous. K&S argues rescue requires embedded exhaustification (K&S §3.3.2, (24)): exh(some) breaks the entailment, so "some or all" ≠ "all" semantically. The data confirms this: all rescued cases are felicitous.

Three competing theories of oddness on the Italian warmth example:

Sentence	Magri 2009	K&S 2015	Spector 2014
# Some Italians…	ODD	ODD	ODD
All Italians…	ok	ODD	ODD

All three agree on "some". The disagreement on "all" reveals:

• @cite{magri-2009} is the most targeted: only oddness when a blind implicature contradicts CK. "All" generates no implicature, so it's fine.
• K&S casts the widest net via the Question Condition: ANY utterance addressing a trivially settled QUD is odd.
• @cite{spector-2014} predicts oddness via triviality: "all" is a C-tautology (entailed by CK), so the only alternative is trivial → odd.

theorem KatzirSingh2015.three_way_agree_some : Magri2009.italianScenario.blindOdd Magri2009.ItalyUtt.some_ = true ∧ italianWarmthScenario.isOdd ItalyUtt.some_ = true ∧ allAlternativesTrivial [Magri2009.ItalyWorld₃.allWarm, Magri2009.ItalyWorld₃.someNotAll, Magri2009.ItalyWorld₃.noneWarm] (fun (w : Magri2009.ItalyWorld₃) => w == Magri2009.ItalyWorld₃.allWarm) (Magri2009.italianScenario.meaning Magri2009.ItalyUtt.all_) [Magri2009.italianScenario.meaning Magri2009.ItalyUtt.some_] = true

Three-way agreement on "some Italians come from a warm country": all three theories predict oddness, via different mechanisms.

theorem KatzirSingh2015.three_way_disagree_all : Magri2009.italianScenario.blindOdd Magri2009.ItalyUtt.all_ = false ∧ italianWarmthScenario.isOdd ItalyUtt.all_ = true ∧ allAlternativesTrivial [Magri2009.ItalyWorld₃.allWarm, Magri2009.ItalyWorld₃.someNotAll, Magri2009.ItalyWorld₃.noneWarm] (fun (w : Magri2009.ItalyWorld₃) => w == Magri2009.ItalyWorld₃.allWarm) (Magri2009.italianScenario.meaning Magri2009.ItalyUtt.all_) [Magri2009.italianScenario.meaning Magri2009.ItalyUtt.some_] = true

Three-way comparison on "all Italians come from a warm country": Magri says fine; K&S and Spector both say odd.