@cite{warstadt-2022}: Presupposition Triggering and Utterance Utility @cite{warstadt-2022}

Empirical domain types and truth conditions for Warstadt's genus-species presupposition model. Two examples demonstrate that presupposition triggering emerges from pragmatic reasoning about utterance utility.

Green Card Example (Table 1)

Three worlds, five utterances, two QUDs. The central prediction: under the "need visa?" QUD, "not green card" triggers the genus inference (Tom is non-US), but under "free drink?" QUD, no such inference arises.

Family-Genus-Species Example (Table 2)

Four worlds in a taxonomic hierarchy (Olympic sprinter ⊂ runner ⊂ athlete), seven utterances, non-uniform priors. Species-level negation ("not Olympic sprinter") triggers stronger accommodation than genus-level ("not runner").

Green Card Example (Table 1)

inductive Phenomena.Presupposition.Studies.Warstadt2022.GCWorld : Type

World states for the green card scenario.

• usCitizen: Tom is a US citizen (no green card possible)
• gcHolder: Tom is a non-US citizen with a green card
• nonUS: Tom is a non-US citizen without a green card

• usCitizen : GCWorld
• gcHolder : GCWorld
• nonUS : GCWorld

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCWorld : DecidableEq GCWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCWorld.beq : GCWorld → GCWorld → Bool

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCWorld : BEq GCWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCWorld = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCWorld.beq }

def Phenomena.Presupposition.Studies.Warstadt2022.instReprGCWorld.repr : GCWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprGCWorld : Repr GCWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprGCWorld = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprGCWorld.repr }

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCWorld : Inhabited GCWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCWorld = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCWorld.default }

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCWorld.default : GCWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCWorld.default = Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.usCitizen

def Phenomena.Presupposition.Studies.Warstadt2022.allGCWorlds : List GCWorld

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instFintypeGCWorld : Fintype GCWorld

Equations

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

inductive Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance : Type

Utterances for the green card scenario.

• us / notUS: genus-level descriptions
• greenCard / notGreenCard: species-level descriptions
• silence: null utterance

• us : GCUtterance
• notUS : GCUtterance
• greenCard : GCUtterance
• notGreenCard : GCUtterance
• silence : GCUtterance

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCUtterance : DecidableEq GCUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCUtterance.beq : GCUtterance → GCUtterance → Bool

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCUtterance : BEq GCUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCUtterance = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCUtterance.beq }

def Phenomena.Presupposition.Studies.Warstadt2022.instReprGCUtterance.repr : GCUtterance → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprGCUtterance : Repr GCUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprGCUtterance = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprGCUtterance.repr }

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCUtterance.default : GCUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCUtterance.default = Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.us

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCUtterance : Inhabited GCUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCUtterance = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCUtterance.default }

def Phenomena.Presupposition.Studies.Warstadt2022.allGCUtterances : List GCUtterance

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instFintypeGCUtterance : Fintype GCUtterance

Equations

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

inductive Phenomena.Presupposition.Studies.Warstadt2022.GCQUD : Type

QUDs for the green card scenario.

• needVisa: Does Tom need a visa? Partition: {usCitizen, gcHolder} vs {nonUS}
• freeDrink: Can Tom get a free drink? Partition: {gcHolder} vs {usCitizen, nonUS}

• needVisa : GCQUD
• freeDrink : GCQUD

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCQUD : DecidableEq GCQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCQUD : BEq GCQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCQUD = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCQUD.beq }

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCQUD.beq : GCQUD → GCQUD → Bool

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCQUD.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Presupposition.Studies.Warstadt2022.instReprGCQUD.repr : GCQUD → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprGCQUD : Repr GCQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprGCQUD = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprGCQUD.repr }

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCQUD : Inhabited GCQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCQUD = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCQUD.default }

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCQUD.default : GCQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCQUD.default = Phenomena.Presupposition.Studies.Warstadt2022.GCQUD.needVisa

def Phenomena.Presupposition.Studies.Warstadt2022.allGCQUDs : List GCQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.allGCQUDs = [Phenomena.Presupposition.Studies.Warstadt2022.GCQUD.needVisa, Phenomena.Presupposition.Studies.Warstadt2022.GCQUD.freeDrink]

instance Phenomena.Presupposition.Studies.Warstadt2022.instFintypeGCQUD : Fintype GCQUD

Equations

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

def Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning : GCUtterance → GCWorld → Bool

Truth conditions from Table 1. All negations are Boolean.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.us Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.usCitizen = true
• Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.us x✝ = false
• Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.notUS Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.usCitizen = false
• Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.notUS x✝ = true
• Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.greenCard x✝ = false
• Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.notGreenCard x✝ = true
• Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning Phenomena.Presupposition.Studies.Warstadt2022.GCUtterance.silence x✝ = true

def Phenomena.Presupposition.Studies.Warstadt2022.gcQUDAnswer : GCQUD → GCWorld → Bool

QUD answer function: maps each QUD to a world's answer.

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.gcQUDAnswer Phenomena.Presupposition.Studies.Warstadt2022.GCQUD.needVisa Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.nonUS = true
• Phenomena.Presupposition.Studies.Warstadt2022.gcQUDAnswer Phenomena.Presupposition.Studies.Warstadt2022.GCQUD.needVisa x✝ = false
• Phenomena.Presupposition.Studies.Warstadt2022.gcQUDAnswer Phenomena.Presupposition.Studies.Warstadt2022.GCQUD.freeDrink Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.gcHolder = true
• Phenomena.Presupposition.Studies.Warstadt2022.gcQUDAnswer Phenomena.Presupposition.Studies.Warstadt2022.GCQUD.freeDrink x✝ = false

def Phenomena.Presupposition.Studies.Warstadt2022.gcQUDProject (q : GCQUD) (w1 w2 : GCWorld) : Bool

QUD projection: two worlds are equivalent iff they give the same QUD answer.

Equations

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

def Phenomena.Presupposition.Studies.Warstadt2022.gcWorldPrior (_w : GCWorld) : ℚ

Uniform world prior.

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.gcWorldPrior _w = 1 / 3

def Phenomena.Presupposition.Studies.Warstadt2022.greenCardPrProp : Core.Presupposition.PrProp GCWorld

PrProp decomposition of "green card": presupposes non-US, asserts has GC.

This captures the traditional presupposition analysis. The paper's key contribution is showing that this presupposition structure EMERGES from RSA reasoning over Boolean truth conditions, without being stipulated.

Equations

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

theorem Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning_greenCard_eq_prprop (w : GCWorld) : gcMeaning GCUtterance.greenCard w = (greenCardPrProp.presup w && greenCardPrProp.assertion w)

The Boolean meaning of "green card" decomposes as presupposition ∧ assertion.

theorem Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning_notGreenCard_eq_neg (w : GCWorld) : gcMeaning GCUtterance.notGreenCard w = !gcMeaning GCUtterance.greenCard w

"not green card" is Boolean negation of "green card".

theorem Phenomena.Presupposition.Studies.Warstadt2022.gcMeaning_notUS_eq_neg (w : GCWorld) : gcMeaning GCUtterance.notUS w = !gcMeaning GCUtterance.us w

"not US" is Boolean negation of "US".

theorem Phenomena.Presupposition.Studies.Warstadt2022.gcQUD_needVisa_partition : gcQUDProject GCQUD.needVisa GCWorld.usCitizen GCWorld.gcHolder = true ∧ gcQUDProject GCQUD.needVisa GCWorld.usCitizen GCWorld.nonUS = false

needVisa QUD partition: {usCitizen, gcHolder} (no) vs {nonUS} (yes).

theorem Phenomena.Presupposition.Studies.Warstadt2022.gcQUD_freeDrink_partition : gcQUDProject GCQUD.freeDrink GCWorld.usCitizen GCWorld.nonUS = true ∧ gcQUDProject GCQUD.freeDrink GCWorld.usCitizen GCWorld.gcHolder = false

freeDrink QUD partition: {usCitizen, nonUS} (no) vs {gcHolder} (yes).

Family-Genus-Species Example (Table 2)

inductive Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld : Type

World states for the family-genus-species hierarchy.

• olympicSprinter: species (⊂ runner ⊂ athlete)
• runner: genus (⊂ athlete)
• otherAthlete: family level
• nonAthlete: outside the hierarchy

• olympicSprinter : FGSWorld
• runner : FGSWorld
• otherAthlete : FGSWorld
• nonAthlete : FGSWorld

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSWorld : DecidableEq FGSWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSWorld.beq : FGSWorld → FGSWorld → Bool

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSWorld : BEq FGSWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSWorld = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSWorld.beq }

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSWorld : Repr FGSWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSWorld = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSWorld.repr }

def Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSWorld.repr : FGSWorld → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSWorld.default : FGSWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSWorld.default = Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.olympicSprinter

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSWorld : Inhabited FGSWorld

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSWorld = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSWorld.default }

def Phenomena.Presupposition.Studies.Warstadt2022.allFGSWorlds : List FGSWorld

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instFintypeFGSWorld : Fintype FGSWorld

Equations

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

inductive Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance : Type

Utterances for the family-genus-species scenario.

Seven utterances: three positive descriptions at each taxonomic level, their Boolean negations, plus silence.

• olympicSprinter : FGSUtterance
• notOlympicSprinter : FGSUtterance
• runner : FGSUtterance
• notRunner : FGSUtterance
• athlete : FGSUtterance
• notAthlete : FGSUtterance
• silence : FGSUtterance

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSUtterance : DecidableEq FGSUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSUtterance : BEq FGSUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSUtterance = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSUtterance.beq }

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSUtterance.beq : FGSUtterance → FGSUtterance → Bool

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSUtterance : Repr FGSUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSUtterance = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSUtterance.repr }

def Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSUtterance.repr : FGSUtterance → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSUtterance : Inhabited FGSUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSUtterance = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSUtterance.default }

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSUtterance.default : FGSUtterance

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSUtterance.default = Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.olympicSprinter

def Phenomena.Presupposition.Studies.Warstadt2022.allFGSUtterances : List FGSUtterance

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instFintypeFGSUtterance : Fintype FGSUtterance

Equations

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

def Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning : FGSUtterance → FGSWorld → Bool

Truth conditions from Table 2.

Respects the taxonomic hierarchy: Olympic sprinter ⊂ runner ⊂ athlete.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.olympicSprinter x✝ = false
• Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.notOlympicSprinter x✝ = true
• Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.runner x✝ = false
• Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.notRunner x✝ = true
• Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.athlete x✝ = true
• Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.notAthlete x✝ = false
• Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning Phenomena.Presupposition.Studies.Warstadt2022.FGSUtterance.silence x✝ = true

def Phenomena.Presupposition.Studies.Warstadt2022.fgsWorldPrior : FGSWorld → ℚ

Non-uniform world prior from Table 2 (percentages).

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.fgsWorldPrior Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.olympicSprinter = 1 / 100
• Phenomena.Presupposition.Studies.Warstadt2022.fgsWorldPrior Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.runner = 5 / 100
• Phenomena.Presupposition.Studies.Warstadt2022.fgsWorldPrior Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.otherAthlete = 10 / 100
• Phenomena.Presupposition.Studies.Warstadt2022.fgsWorldPrior Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.nonAthlete = 84 / 100

def Phenomena.Presupposition.Studies.Warstadt2022.fgsQUDProject (w1 w2 : FGSWorld) : Bool

Max QUD (full world identification).

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.fgsQUDProject w1 w2 = (w1 == w2)

theorem Phenomena.Presupposition.Studies.Warstadt2022.olympicSprinter_entails_runner (w : FGSWorld) : fgsMeaning FGSUtterance.olympicSprinter w = true → fgsMeaning FGSUtterance.runner w = true

Olympic sprinter entails runner.

theorem Phenomena.Presupposition.Studies.Warstadt2022.runner_entails_athlete (w : FGSWorld) : fgsMeaning FGSUtterance.runner w = true → fgsMeaning FGSUtterance.athlete w = true

Runner entails athlete.

theorem Phenomena.Presupposition.Studies.Warstadt2022.olympicSprinter_entails_athlete (w : FGSWorld) : fgsMeaning FGSUtterance.olympicSprinter w = true → fgsMeaning FGSUtterance.athlete w = true

Olympic sprinter entails athlete (transitivity).

theorem Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning_notOS_eq_neg (w : FGSWorld) : fgsMeaning FGSUtterance.notOlympicSprinter w = !fgsMeaning FGSUtterance.olympicSprinter w

Boolean negation: not Olympic sprinter = ¬ Olympic sprinter.

theorem Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning_notRunner_eq_neg (w : FGSWorld) : fgsMeaning FGSUtterance.notRunner w = !fgsMeaning FGSUtterance.runner w

Boolean negation: not runner = ¬ runner.

theorem Phenomena.Presupposition.Studies.Warstadt2022.fgsMeaning_notAthlete_eq_neg (w : FGSWorld) : fgsMeaning FGSUtterance.notAthlete w = !fgsMeaning FGSUtterance.athlete w

Boolean negation: not athlete = ¬ athlete.

theorem Phenomena.Presupposition.Studies.Warstadt2022.fgsWorldPrior_sum : fgsWorldPrior FGSWorld.olympicSprinter + fgsWorldPrior FGSWorld.runner + fgsWorldPrior FGSWorld.otherAthlete + fgsWorldPrior FGSWorld.nonAthlete = 1

FGS priors sum to 1.

Green Card: Context Types

structure Phenomena.Presupposition.Studies.Warstadt2022.GCContext : Type

A context is a subset of GCWorlds.

• usCitizen : Bool
• gcHolder : Bool
• nonUS : Bool

def Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCContext.decEq (x✝ x✝¹ : GCContext) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCContext : DecidableEq GCContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCContext = Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqGCContext.decEq

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCContext.beq : GCContext → GCContext → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCContext.beq x✝¹ x✝ = false

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCContext : BEq GCContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCContext = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqGCContext.beq }

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprGCContext : Repr GCContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprGCContext = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprGCContext.repr }

def Phenomena.Presupposition.Studies.Warstadt2022.instReprGCContext.repr : GCContext → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCContext : Inhabited GCContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCContext = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCContext.default }

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCContext.default : GCContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedGCContext.default = { usCitizen := default, gcHolder := default, nonUS := default }

def Phenomena.Presupposition.Studies.Warstadt2022.allGCContexts : List GCContext

All 2³ = 8 contexts (subsets of GCWorld).

Equations

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

theorem Phenomena.Presupposition.Studies.Warstadt2022.allGCContexts_length : allGCContexts.length = 8

def Phenomena.Presupposition.Studies.Warstadt2022.gcCompatible (c : GCContext) (w : GCWorld) : Bool

A world is compatible with a context iff the context includes it.

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.gcCompatible c Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.usCitizen = c.usCitizen
• Phenomena.Presupposition.Studies.Warstadt2022.gcCompatible c Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.gcHolder = c.gcHolder
• Phenomena.Presupposition.Studies.Warstadt2022.gcCompatible c Phenomena.Presupposition.Studies.Warstadt2022.GCWorld.nonUS = c.nonUS

def Phenomena.Presupposition.Studies.Warstadt2022.gcContextPrior (_c : GCContext) : ℚ

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.gcContextPrior _c = 1 / 8

Family-Genus-Species: Context Types

structure Phenomena.Presupposition.Studies.Warstadt2022.FGSContext : Type

A context is a subset of FGSWorlds.

• olympicSprinter : Bool
• runner : Bool
• otherAthlete : Bool
• nonAthlete : Bool

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSContext : DecidableEq FGSContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSContext = Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSContext.decEq

def Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSContext.decEq (x✝ x✝¹ : FGSContext) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSContext.beq : FGSContext → FGSContext → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSContext.beq x✝¹ x✝ = false

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSContext : BEq FGSContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSContext = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSContext.beq }

def Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSContext.repr : FGSContext → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSContext : Repr FGSContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSContext = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSContext.repr }

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSContext.default : FGSContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSContext.default = { olympicSprinter := default, runner := default, otherAthlete := default, nonAthlete := default }

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSContext : Inhabited FGSContext

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSContext = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSContext.default }

def Phenomena.Presupposition.Studies.Warstadt2022.allFGSContexts : List FGSContext

All 2⁴ = 16 contexts.

Equations

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

theorem Phenomena.Presupposition.Studies.Warstadt2022.allFGSContexts_length : allFGSContexts.length = 16

def Phenomena.Presupposition.Studies.Warstadt2022.fgsCompatible (c : FGSContext) (w : FGSWorld) : Bool

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.fgsCompatible c Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.olympicSprinter = c.olympicSprinter
• Phenomena.Presupposition.Studies.Warstadt2022.fgsCompatible c Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.runner = c.runner
• Phenomena.Presupposition.Studies.Warstadt2022.fgsCompatible c Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.otherAthlete = c.otherAthlete
• Phenomena.Presupposition.Studies.Warstadt2022.fgsCompatible c Phenomena.Presupposition.Studies.Warstadt2022.FGSWorld.nonAthlete = c.nonAthlete

def Phenomena.Presupposition.Studies.Warstadt2022.fgsContextPrior (_c : FGSContext) : ℚ

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.fgsContextPrior _c = 1 / 16

inductive Phenomena.Presupposition.Studies.Warstadt2022.FGSQUD : Type

• identity : FGSQUD

instance Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSQUD : DecidableEq FGSQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instDecidableEqFGSQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSQUD.beq : FGSQUD → FGSQUD → Bool

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSQUD.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSQUD : BEq FGSQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSQUD = { beq := Phenomena.Presupposition.Studies.Warstadt2022.instBEqFGSQUD.beq }

def Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSQUD.repr : FGSQUD → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSQUD : Repr FGSQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSQUD = { reprPrec := Phenomena.Presupposition.Studies.Warstadt2022.instReprFGSQUD.repr }

instance Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSQUD : Inhabited FGSQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSQUD = { default := Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSQUD.default }

def Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSQUD.default : FGSQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.instInhabitedFGSQUD.default = Phenomena.Presupposition.Studies.Warstadt2022.FGSQUD.identity

def Phenomena.Presupposition.Studies.Warstadt2022.allFGSQUDs : List FGSQUD

Equations

• Phenomena.Presupposition.Studies.Warstadt2022.allFGSQUDs = [Phenomena.Presupposition.Studies.Warstadt2022.FGSQUD.identity]

def Phenomena.Presupposition.Studies.Warstadt2022.fgsQUDProjectBridge : FGSQUD → FGSWorld → FGSWorld → Bool

Equations

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

PrProp Connection

theorem Phenomena.Presupposition.Studies.Warstadt2022.greenCard_meaning_from_prprop (w : GCWorld) : gcMeaning GCUtterance.greenCard w = (greenCardPrProp.presup w && greenCardPrProp.assertion w)

The Boolean meaning of "green card" decomposes as presupposition ∧ assertion.

theorem Phenomena.Presupposition.Studies.Warstadt2022.notGreenCard_is_boolean_negation (w : GCWorld) : gcMeaning GCUtterance.notGreenCard w = !gcMeaning GCUtterance.greenCard w

"not green card" is Boolean negation — no presupposition in the semantics.