Economy of Structure and Information

@cite{heim-1991} @cite{hurford-1974} @cite{katzir-2007} @cite{katzir-singh-2015} @cite{magri-2009} @cite{magri-2011} @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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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.

Equations

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

def Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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

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

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

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

Equations

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

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

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

Equations

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

def Semantics.Questions.EconomyOddness.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

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

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

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

Equations

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

def Semantics.Questions.EconomyOddness.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

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

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

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 Semantics.Questions.EconomyOddness.ItalyWorld : Type

• allWarm : ItalyWorld
• noneWarm : ItalyWorld

instance Semantics.Questions.EconomyOddness.instDecidableEqItalyWorld : DecidableEq ItalyWorld

Equations

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

def Semantics.Questions.EconomyOddness.instBEqItalyWorld.beq : ItalyWorld → ItalyWorld → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqItalyWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instBEqItalyWorld : BEq ItalyWorld

Equations

• Semantics.Questions.EconomyOddness.instBEqItalyWorld = { beq := Semantics.Questions.EconomyOddness.instBEqItalyWorld.beq }

def Semantics.Questions.EconomyOddness.instReprItalyWorld.repr : ItalyWorld → ℕ → Std.Format

Equations

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

instance Semantics.Questions.EconomyOddness.instReprItalyWorld : Repr ItalyWorld

Equations

• Semantics.Questions.EconomyOddness.instReprItalyWorld = { reprPrec := Semantics.Questions.EconomyOddness.instReprItalyWorld.repr }

inductive Semantics.Questions.EconomyOddness.ItalyUtt : Type

• some_ : ItalyUtt
• all_ : ItalyUtt

instance Semantics.Questions.EconomyOddness.instDecidableEqItalyUtt : DecidableEq ItalyUtt

Equations

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

instance Semantics.Questions.EconomyOddness.instBEqItalyUtt : BEq ItalyUtt

Equations

• Semantics.Questions.EconomyOddness.instBEqItalyUtt = { beq := Semantics.Questions.EconomyOddness.instBEqItalyUtt.beq }

def Semantics.Questions.EconomyOddness.instBEqItalyUtt.beq : ItalyUtt → ItalyUtt → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqItalyUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instReprItalyUtt : Repr ItalyUtt

Equations

• Semantics.Questions.EconomyOddness.instReprItalyUtt = { reprPrec := Semantics.Questions.EconomyOddness.instReprItalyUtt.repr }

def Semantics.Questions.EconomyOddness.instReprItalyUtt.repr : ItalyUtt → ℕ → Std.Format

Equations

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

def Semantics.Questions.EconomyOddness.magriScenario : Scenario ItalyWorld ItalyUtt

Equations

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

theorem Semantics.Questions.EconomyOddness.magri_contextEquiv : magriScenario.contextEquiv ItalyUtt.some_ ItalyUtt.all_ = true

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

theorem Semantics.Questions.EconomyOddness.magri_badQuestion : magriScenario.badQuestion = true

QUD trivially settled by CK → Question Condition violated.

theorem Semantics.Questions.EconomyOddness.magri_some_odd : magriScenario.isOdd ItalyUtt.some_ = true

K&S prediction: "some" is odd.

theorem Semantics.Questions.EconomyOddness.magri_all_odd : magriScenario.isOdd ItalyUtt.all_ = true

K&S prediction: "all" is odd.

theorem Semantics.Questions.EconomyOddness.spector_agrees_magri : allAlternativesTrivial [ItalyWorld.allWarm, ItalyWorld.noneWarm] (fun (w : ItalyWorld) => w == ItalyWorld.allWarm) (magriScenario.meaning ItalyUtt.some_) [magriScenario.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 Core.Scale.Quantifiers.entails.all.some_ = true.

inductive Semantics.Questions.EconomyOddness.GradeWorld : Type

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

instance Semantics.Questions.EconomyOddness.instDecidableEqGradeWorld : DecidableEq GradeWorld

Equations

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

def Semantics.Questions.EconomyOddness.instBEqGradeWorld.beq : GradeWorld → GradeWorld → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqGradeWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instBEqGradeWorld : BEq GradeWorld

Equations

• Semantics.Questions.EconomyOddness.instBEqGradeWorld = { beq := Semantics.Questions.EconomyOddness.instBEqGradeWorld.beq }

instance Semantics.Questions.EconomyOddness.instReprGradeWorld : Repr GradeWorld

Equations

• Semantics.Questions.EconomyOddness.instReprGradeWorld = { reprPrec := Semantics.Questions.EconomyOddness.instReprGradeWorld.repr }

def Semantics.Questions.EconomyOddness.instReprGradeWorld.repr : GradeWorld → ℕ → Std.Format

Equations

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

inductive Semantics.Questions.EconomyOddness.GradeUtt : Type

• some_ : GradeUtt
• all_ : GradeUtt

instance Semantics.Questions.EconomyOddness.instDecidableEqGradeUtt : DecidableEq GradeUtt

Equations

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

instance Semantics.Questions.EconomyOddness.instBEqGradeUtt : BEq GradeUtt

Equations

• Semantics.Questions.EconomyOddness.instBEqGradeUtt = { beq := Semantics.Questions.EconomyOddness.instBEqGradeUtt.beq }

def Semantics.Questions.EconomyOddness.instBEqGradeUtt.beq : GradeUtt → GradeUtt → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqGradeUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instReprGradeUtt : Repr GradeUtt

Equations

• Semantics.Questions.EconomyOddness.instReprGradeUtt = { reprPrec := Semantics.Questions.EconomyOddness.instReprGradeUtt.repr }

def Semantics.Questions.EconomyOddness.instReprGradeUtt.repr : GradeUtt → ℕ → Std.Format

Equations

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

def Semantics.Questions.EconomyOddness.gradeScenario : Scenario GradeWorld GradeUtt

Equations

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

theorem Semantics.Questions.EconomyOddness.grade_goodQuestion : gradeScenario.badQuestion = false

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

theorem Semantics.Questions.EconomyOddness.grade_all_entails_some : gradeScenario.semEntails GradeUtt.all_ GradeUtt.some_ = true

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

theorem Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.grade_all_better_than_some : gradeScenario.betterThan GradeUtt.all_ GradeUtt.some_ = true

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

theorem Semantics.Questions.EconomyOddness.grade_some_odd : gradeScenario.isOdd GradeUtt.some_ = true

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

theorem Semantics.Questions.EconomyOddness.grade_all_ok : gradeScenario.isOdd GradeUtt.all_ = false

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

theorem Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.VisitWorld : Type

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

instance Semantics.Questions.EconomyOddness.instDecidableEqVisitWorld : DecidableEq VisitWorld

Equations

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

def Semantics.Questions.EconomyOddness.instBEqVisitWorld.beq : VisitWorld → VisitWorld → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqVisitWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instBEqVisitWorld : BEq VisitWorld

Equations

• Semantics.Questions.EconomyOddness.instBEqVisitWorld = { beq := Semantics.Questions.EconomyOddness.instBEqVisitWorld.beq }

instance Semantics.Questions.EconomyOddness.instReprVisitWorld : Repr VisitWorld

Equations

• Semantics.Questions.EconomyOddness.instReprVisitWorld = { reprPrec := Semantics.Questions.EconomyOddness.instReprVisitWorld.repr }

def Semantics.Questions.EconomyOddness.instReprVisitWorld.repr : VisitWorld → ℕ → Std.Format

Equations

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

inductive Semantics.Questions.EconomyOddness.VisitUtt : Type

• france : VisitUtt
• franceOrParis : VisitUtt

instance Semantics.Questions.EconomyOddness.instDecidableEqVisitUtt : DecidableEq VisitUtt

Equations

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

instance Semantics.Questions.EconomyOddness.instBEqVisitUtt : BEq VisitUtt

Equations

• Semantics.Questions.EconomyOddness.instBEqVisitUtt = { beq := Semantics.Questions.EconomyOddness.instBEqVisitUtt.beq }

def Semantics.Questions.EconomyOddness.instBEqVisitUtt.beq : VisitUtt → VisitUtt → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqVisitUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instReprVisitUtt : Repr VisitUtt

Equations

• Semantics.Questions.EconomyOddness.instReprVisitUtt = { reprPrec := Semantics.Questions.EconomyOddness.instReprVisitUtt.repr }

def Semantics.Questions.EconomyOddness.instReprVisitUtt.repr : VisitUtt → ℕ → Std.Format

Equations

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

def Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.hurford_france_better : hurfordScenario.betterThan VisitUtt.france VisitUtt.franceOrParis = true

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

theorem Semantics.Questions.EconomyOddness.hurford_disjunction_odd : hurfordScenario.isOdd VisitUtt.franceOrParis = true

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

theorem Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.DEWorld : Type

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

instance Semantics.Questions.EconomyOddness.instDecidableEqDEWorld : DecidableEq DEWorld

Equations

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

instance Semantics.Questions.EconomyOddness.instBEqDEWorld : BEq DEWorld

Equations

• Semantics.Questions.EconomyOddness.instBEqDEWorld = { beq := Semantics.Questions.EconomyOddness.instBEqDEWorld.beq }

def Semantics.Questions.EconomyOddness.instBEqDEWorld.beq : DEWorld → DEWorld → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqDEWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Questions.EconomyOddness.instReprDEWorld.repr : DEWorld → ℕ → Std.Format

Equations

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

instance Semantics.Questions.EconomyOddness.instReprDEWorld : Repr DEWorld

Equations

• Semantics.Questions.EconomyOddness.instReprDEWorld = { reprPrec := Semantics.Questions.EconomyOddness.instReprDEWorld.repr }

inductive Semantics.Questions.EconomyOddness.DEUtt : Type

• some_ : DEUtt
• all_ : DEUtt

instance Semantics.Questions.EconomyOddness.instDecidableEqDEUtt : DecidableEq DEUtt

Equations

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

def Semantics.Questions.EconomyOddness.instBEqDEUtt.beq : DEUtt → DEUtt → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqDEUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instBEqDEUtt : BEq DEUtt

Equations

• Semantics.Questions.EconomyOddness.instBEqDEUtt = { beq := Semantics.Questions.EconomyOddness.instBEqDEUtt.beq }

instance Semantics.Questions.EconomyOddness.instReprDEUtt : Repr DEUtt

Equations

• Semantics.Questions.EconomyOddness.instReprDEUtt = { reprPrec := Semantics.Questions.EconomyOddness.instReprDEUtt.repr }

def Semantics.Questions.EconomyOddness.instReprDEUtt.repr : DEUtt → ℕ → Std.Format

Equations

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

def Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.de_some_entails_all : deScenario.semEntails DEUtt.some_ DEUtt.all_ = true

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

theorem Semantics.Questions.EconomyOddness.de_all_not_entails_some : deScenario.semEntails DEUtt.all_ DEUtt.some_ = false

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

theorem Semantics.Questions.EconomyOddness.de_some_better_than_all : deScenario.betterThan DEUtt.some_ DEUtt.all_ = true

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

theorem Semantics.Questions.EconomyOddness.de_all_odd : deScenario.isOdd DEUtt.all_ = true

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

theorem Semantics.Questions.EconomyOddness.de_some_ok : deScenario.isOdd DEUtt.some_ = false

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

theorem Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.SunWorld : Type

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

instance Semantics.Questions.EconomyOddness.instDecidableEqSunWorld : DecidableEq SunWorld

Equations

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

instance Semantics.Questions.EconomyOddness.instBEqSunWorld : BEq SunWorld

Equations

• Semantics.Questions.EconomyOddness.instBEqSunWorld = { beq := Semantics.Questions.EconomyOddness.instBEqSunWorld.beq }

def Semantics.Questions.EconomyOddness.instBEqSunWorld.beq : SunWorld → SunWorld → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqSunWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Questions.EconomyOddness.instReprSunWorld : Repr SunWorld

Equations

• Semantics.Questions.EconomyOddness.instReprSunWorld = { reprPrec := Semantics.Questions.EconomyOddness.instReprSunWorld.repr }

def Semantics.Questions.EconomyOddness.instReprSunWorld.repr : SunWorld → ℕ → Std.Format

Equations

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

inductive Semantics.Questions.EconomyOddness.SunUtt : Type

• aSun : SunUtt
• theSun : SunUtt

instance Semantics.Questions.EconomyOddness.instDecidableEqSunUtt : DecidableEq SunUtt

Equations

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

instance Semantics.Questions.EconomyOddness.instBEqSunUtt : BEq SunUtt

Equations

• Semantics.Questions.EconomyOddness.instBEqSunUtt = { beq := Semantics.Questions.EconomyOddness.instBEqSunUtt.beq }

def Semantics.Questions.EconomyOddness.instBEqSunUtt.beq : SunUtt → SunUtt → Bool

Equations

• Semantics.Questions.EconomyOddness.instBEqSunUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Questions.EconomyOddness.instReprSunUtt.repr : SunUtt → ℕ → Std.Format

Equations

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

instance Semantics.Questions.EconomyOddness.instReprSunUtt : Repr SunUtt

Equations

• Semantics.Questions.EconomyOddness.instReprSunUtt = { reprPrec := Semantics.Questions.EconomyOddness.instReprSunUtt.repr }

def Semantics.Questions.EconomyOddness.maxPresupScenario : Scenario SunWorld SunUtt

Equations

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

theorem Semantics.Questions.EconomyOddness.maxPresup_the_entails_a : maxPresupScenario.semEntails SunUtt.theSun SunUtt.aSun = true

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

theorem Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.maxPresup_the_better : maxPresupScenario.betterThan SunUtt.theSun SunUtt.aSun = true

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

theorem Semantics.Questions.EconomyOddness.maxPresup_indefinite_odd : maxPresupScenario.isOdd SunUtt.aSun = true

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

theorem Semantics.Questions.EconomyOddness.maxPresup_definite_ok : maxPresupScenario.isOdd SunUtt.theSun = false

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

theorem Semantics.Questions.EconomyOddness.maxPresup_contextEquiv : maxPresupScenario.contextEquiv SunUtt.aSun SunUtt.theSun = true

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

theorem Semantics.Questions.EconomyOddness.conditions_independent : magriScenario.badQuestion = true ∧ gradeScenario.badQuestion = false ∧ gradeScenario.needlesslyInferior GradeUtt.some_ = true ∧ magriScenario.needlesslyInferior ItalyUtt.some_ = false

The Question Condition and Answer Condition are independent:

• Magri: 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 Semantics.Questions.EconomyOddness.strict_agrees_magri : magriScenario.needlesslyInferiorStrict ItalyUtt.some_ = magriScenario.needlesslyInferior ItalyUtt.some_

theorem Semantics.Questions.EconomyOddness.strict_agrees_grade : gradeScenario.needlesslyInferiorStrict GradeUtt.some_ = gradeScenario.needlesslyInferior GradeUtt.some_

theorem Semantics.Questions.EconomyOddness.strict_agrees_hurford : hurfordScenario.needlesslyInferiorStrict VisitUtt.franceOrParis = hurfordScenario.needlesslyInferior VisitUtt.franceOrParis

theorem Semantics.Questions.EconomyOddness.strict_agrees_de : deScenario.needlesslyInferiorStrict DEUtt.all_ = deScenario.needlesslyInferior DEUtt.all_

theorem Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.deDiscourseOpen : DiscourseContext DEWorld

Alternative discourse context: all worlds CK-compatible.

Equations

• Semantics.Questions.EconomyOddness.deDiscourseOpen = { context := fun (x : Semantics.Questions.EconomyOddness.DEWorld) => true, qud := QUD.ofDecEq id }

theorem Semantics.Questions.EconomyOddness.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 Semantics.Questions.EconomyOddness.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.