@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 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

@[implicit_reducible]

instance Warstadt2022.instDecidableEqGCWorld : DecidableEq GCWorld

Equations

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

def Warstadt2022.instReprGCWorld.repr : GCWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprGCWorld : Repr GCWorld

Equations

• Warstadt2022.instReprGCWorld = { reprPrec := Warstadt2022.instReprGCWorld.repr }

@[implicit_reducible]

instance Warstadt2022.instInhabitedGCWorld : Inhabited GCWorld

Equations

• Warstadt2022.instInhabitedGCWorld = { default := Warstadt2022.instInhabitedGCWorld.default }

def Warstadt2022.instInhabitedGCWorld.default : GCWorld

Equations

• Warstadt2022.instInhabitedGCWorld.default = Warstadt2022.GCWorld.usCitizen

def Warstadt2022.allGCWorlds : List GCWorld

Equations

• Warstadt2022.allGCWorlds = [Warstadt2022.GCWorld.usCitizen, Warstadt2022.GCWorld.gcHolder, Warstadt2022.GCWorld.nonUS]

@[implicit_reducible]

instance Warstadt2022.instFintypeGCWorld : Fintype GCWorld

Equations

• Warstadt2022.instFintypeGCWorld = { elems := {Warstadt2022.GCWorld.usCitizen, Warstadt2022.GCWorld.gcHolder, Warstadt2022.GCWorld.nonUS}, complete := Warstadt2022.instFintypeGCWorld._proof_1 }

inductive 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

@[implicit_reducible]

instance Warstadt2022.instDecidableEqGCUtterance : DecidableEq GCUtterance

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprGCUtterance : Repr GCUtterance

Equations

• Warstadt2022.instReprGCUtterance = { reprPrec := Warstadt2022.instReprGCUtterance.repr }

def Warstadt2022.instReprGCUtterance.repr : GCUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instInhabitedGCUtterance : Inhabited GCUtterance

Equations

• Warstadt2022.instInhabitedGCUtterance = { default := Warstadt2022.instInhabitedGCUtterance.default }

def Warstadt2022.instInhabitedGCUtterance.default : GCUtterance

Equations

• Warstadt2022.instInhabitedGCUtterance.default = Warstadt2022.GCUtterance.us

def Warstadt2022.allGCUtterances : List GCUtterance

Equations

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

@[implicit_reducible]

instance Warstadt2022.instFintypeGCUtterance : Fintype GCUtterance

Equations

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

inductive 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

@[implicit_reducible]

instance Warstadt2022.instDecidableEqGCQUD : DecidableEq GCQUD

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprGCQUD : Repr GCQUD

Equations

• Warstadt2022.instReprGCQUD = { reprPrec := Warstadt2022.instReprGCQUD.repr }

def Warstadt2022.instReprGCQUD.repr : GCQUD → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instInhabitedGCQUD : Inhabited GCQUD

Equations

• Warstadt2022.instInhabitedGCQUD = { default := Warstadt2022.instInhabitedGCQUD.default }

def Warstadt2022.instInhabitedGCQUD.default : GCQUD

Equations

• Warstadt2022.instInhabitedGCQUD.default = Warstadt2022.GCQUD.needVisa

def Warstadt2022.allGCQUDs : List GCQUD

Equations

• Warstadt2022.allGCQUDs = [Warstadt2022.GCQUD.needVisa, Warstadt2022.GCQUD.freeDrink]

@[implicit_reducible]

instance Warstadt2022.instFintypeGCQUD : Fintype GCQUD

Equations

• Warstadt2022.instFintypeGCQUD = { elems := {Warstadt2022.GCQUD.needVisa, Warstadt2022.GCQUD.freeDrink}, complete := Warstadt2022.instFintypeGCQUD._proof_1 }

def Warstadt2022.gcMeaning : GCUtterance → GCWorld → Bool

Truth conditions from Table 1. All negations are Boolean.

Equations

• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.us Warstadt2022.GCWorld.usCitizen = true
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.us x✝ = false
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.notUS Warstadt2022.GCWorld.usCitizen = false
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.notUS x✝ = true
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.greenCard Warstadt2022.GCWorld.gcHolder = true
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.greenCard x✝ = false
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.notGreenCard Warstadt2022.GCWorld.gcHolder = false
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.notGreenCard x✝ = true
• Warstadt2022.gcMeaning Warstadt2022.GCUtterance.silence x✝ = true

def Warstadt2022.gcQUDAnswer : GCQUD → GCWorld → Bool

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

Equations

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

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

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

Equations

• Warstadt2022.gcQUDProject q w1 w2 = (Warstadt2022.gcQUDAnswer q w1 == Warstadt2022.gcQUDAnswer q w2)

def Warstadt2022.gcWorldPrior (_w : GCWorld) : ℚ

Uniform world prior.

Equations

• Warstadt2022.gcWorldPrior _w = 1 / 3

def 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 Warstadt2022.gcMeaning_greenCard_eq_prprop (w : GCWorld) : gcMeaning GCUtterance.greenCard w = true ↔ greenCardPrProp.presup w ∧ greenCardPrProp.assertion w

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

theorem 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 Warstadt2022.gcMeaning_notUS_eq_neg (w : GCWorld) : gcMeaning GCUtterance.notUS w = !gcMeaning GCUtterance.us w

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

theorem 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 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 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

@[implicit_reducible]

instance Warstadt2022.instDecidableEqFGSWorld : DecidableEq FGSWorld

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprFGSWorld : Repr FGSWorld

Equations

• Warstadt2022.instReprFGSWorld = { reprPrec := Warstadt2022.instReprFGSWorld.repr }

def Warstadt2022.instReprFGSWorld.repr : FGSWorld → ℕ → Std.Format

Equations

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

def Warstadt2022.instInhabitedFGSWorld.default : FGSWorld

Equations

• Warstadt2022.instInhabitedFGSWorld.default = Warstadt2022.FGSWorld.olympicSprinter

@[implicit_reducible]

instance Warstadt2022.instInhabitedFGSWorld : Inhabited FGSWorld

Equations

• Warstadt2022.instInhabitedFGSWorld = { default := Warstadt2022.instInhabitedFGSWorld.default }

def Warstadt2022.allFGSWorlds : List FGSWorld

Equations

• Warstadt2022.allFGSWorlds = [Warstadt2022.FGSWorld.olympicSprinter, Warstadt2022.FGSWorld.runner, Warstadt2022.FGSWorld.otherAthlete, Warstadt2022.FGSWorld.nonAthlete]

@[implicit_reducible]

instance Warstadt2022.instFintypeFGSWorld : Fintype FGSWorld

Equations

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

inductive 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

@[implicit_reducible]

instance Warstadt2022.instDecidableEqFGSUtterance : DecidableEq FGSUtterance

Equations

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

def Warstadt2022.instReprFGSUtterance.repr : FGSUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprFGSUtterance : Repr FGSUtterance

Equations

• Warstadt2022.instReprFGSUtterance = { reprPrec := Warstadt2022.instReprFGSUtterance.repr }

@[implicit_reducible]

instance Warstadt2022.instInhabitedFGSUtterance : Inhabited FGSUtterance

Equations

• Warstadt2022.instInhabitedFGSUtterance = { default := Warstadt2022.instInhabitedFGSUtterance.default }

def Warstadt2022.instInhabitedFGSUtterance.default : FGSUtterance

Equations

• Warstadt2022.instInhabitedFGSUtterance.default = Warstadt2022.FGSUtterance.olympicSprinter

def Warstadt2022.allFGSUtterances : List FGSUtterance

Equations

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

@[implicit_reducible]

instance Warstadt2022.instFintypeFGSUtterance : Fintype FGSUtterance

Equations

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

def Warstadt2022.fgsMeaning : FGSUtterance → FGSWorld → Bool

Truth conditions from Table 2.

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

Equations

• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.olympicSprinter Warstadt2022.FGSWorld.olympicSprinter = true
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.olympicSprinter x✝ = false
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.notOlympicSprinter Warstadt2022.FGSWorld.olympicSprinter = false
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.notOlympicSprinter x✝ = true
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.runner Warstadt2022.FGSWorld.olympicSprinter = true
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.runner Warstadt2022.FGSWorld.runner = true
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.runner x✝ = false
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.notRunner Warstadt2022.FGSWorld.olympicSprinter = false
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.notRunner Warstadt2022.FGSWorld.runner = false
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.notRunner x✝ = true
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.athlete Warstadt2022.FGSWorld.nonAthlete = false
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.athlete x✝ = true
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.notAthlete Warstadt2022.FGSWorld.nonAthlete = true
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.notAthlete x✝ = false
• Warstadt2022.fgsMeaning Warstadt2022.FGSUtterance.silence x✝ = true

def Warstadt2022.fgsWorldPrior : FGSWorld → ℚ

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

Equations

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

def Warstadt2022.fgsQUDProject (w1 w2 : FGSWorld) : Bool

Max QUD (full world identification).

Equations

• Warstadt2022.fgsQUDProject w1 w2 = (w1 == w2)

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

Olympic sprinter entails runner.

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

Runner entails athlete.

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

Olympic sprinter entails athlete (transitivity).

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

Boolean negation: not Olympic sprinter = ¬ Olympic sprinter.

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

Boolean negation: not runner = ¬ runner.

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

Boolean negation: not athlete = ¬ athlete.

theorem 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 Warstadt2022.GCContext : Type

A context is a subset of GCWorlds.

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

@[implicit_reducible]

instance Warstadt2022.instDecidableEqGCContext : DecidableEq GCContext

Equations

• Warstadt2022.instDecidableEqGCContext = Warstadt2022.instDecidableEqGCContext.decEq

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

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprGCContext : Repr GCContext

Equations

• Warstadt2022.instReprGCContext = { reprPrec := Warstadt2022.instReprGCContext.repr }

def Warstadt2022.instReprGCContext.repr : GCContext → ℕ → Std.Format

Equations

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

def Warstadt2022.instInhabitedGCContext.default : GCContext

Equations

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

@[implicit_reducible]

instance Warstadt2022.instInhabitedGCContext : Inhabited GCContext

Equations

• Warstadt2022.instInhabitedGCContext = { default := Warstadt2022.instInhabitedGCContext.default }

def 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 Warstadt2022.allGCContexts_length : allGCContexts.length = 8

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

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

Equations

• Warstadt2022.gcCompatible c Warstadt2022.GCWorld.usCitizen = c.usCitizen
• Warstadt2022.gcCompatible c Warstadt2022.GCWorld.gcHolder = c.gcHolder
• Warstadt2022.gcCompatible c Warstadt2022.GCWorld.nonUS = c.nonUS

def Warstadt2022.gcContextPrior (_c : GCContext) : ℚ

Equations

• Warstadt2022.gcContextPrior _c = 1 / 8

Family-Genus-Species: Context Types

structure Warstadt2022.FGSContext : Type

A context is a subset of FGSWorlds.

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

@[implicit_reducible]

instance Warstadt2022.instDecidableEqFGSContext : DecidableEq FGSContext

Equations

• Warstadt2022.instDecidableEqFGSContext = Warstadt2022.instDecidableEqFGSContext.decEq

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

Equations

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

def Warstadt2022.instReprFGSContext.repr : FGSContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprFGSContext : Repr FGSContext

Equations

• Warstadt2022.instReprFGSContext = { reprPrec := Warstadt2022.instReprFGSContext.repr }

def Warstadt2022.instInhabitedFGSContext.default : FGSContext

Equations

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

@[implicit_reducible]

instance Warstadt2022.instInhabitedFGSContext : Inhabited FGSContext

Equations

• Warstadt2022.instInhabitedFGSContext = { default := Warstadt2022.instInhabitedFGSContext.default }

def Warstadt2022.allFGSContexts : List FGSContext

All 2⁴ = 16 contexts.

Equations

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

theorem Warstadt2022.allFGSContexts_length : allFGSContexts.length = 16

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

Equations

• Warstadt2022.fgsCompatible c Warstadt2022.FGSWorld.olympicSprinter = c.olympicSprinter
• Warstadt2022.fgsCompatible c Warstadt2022.FGSWorld.runner = c.runner
• Warstadt2022.fgsCompatible c Warstadt2022.FGSWorld.otherAthlete = c.otherAthlete
• Warstadt2022.fgsCompatible c Warstadt2022.FGSWorld.nonAthlete = c.nonAthlete

def Warstadt2022.fgsContextPrior (_c : FGSContext) : ℚ

Equations

• Warstadt2022.fgsContextPrior _c = 1 / 16

inductive Warstadt2022.FGSQUD : Type

• identity : FGSQUD

@[implicit_reducible]

instance Warstadt2022.instDecidableEqFGSQUD : DecidableEq FGSQUD

Equations

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

def Warstadt2022.instReprFGSQUD.repr : FGSQUD → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprFGSQUD : Repr FGSQUD

Equations

• Warstadt2022.instReprFGSQUD = { reprPrec := Warstadt2022.instReprFGSQUD.repr }

@[implicit_reducible]

instance Warstadt2022.instInhabitedFGSQUD : Inhabited FGSQUD

Equations

• Warstadt2022.instInhabitedFGSQUD = { default := Warstadt2022.instInhabitedFGSQUD.default }

def Warstadt2022.instInhabitedFGSQUD.default : FGSQUD

Equations

• Warstadt2022.instInhabitedFGSQUD.default = Warstadt2022.FGSQUD.identity

def Warstadt2022.allFGSQUDs : List FGSQUD

Equations

• Warstadt2022.allFGSQUDs = [Warstadt2022.FGSQUD.identity]

def Warstadt2022.fgsQUDProjectBridge : FGSQUD → FGSWorld → FGSWorld → Bool

Equations

• Warstadt2022.fgsQUDProjectBridge Warstadt2022.FGSQUD.identity x✝¹ x✝ = Warstadt2022.fgsQUDProject x✝¹ x✝

PrProp Connection

theorem Warstadt2022.greenCard_meaning_from_prprop (w : GCWorld) : gcMeaning GCUtterance.greenCard w = true ↔ greenCardPrProp.presup w ∧ greenCardPrProp.assertion w

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

theorem 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.