[War22]: Presupposition Triggering and Utterance Utility [War22]

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 ⋯

@[implicit_reducible]

instance Warstadt2022.instReprGCWorld : Repr GCWorld

Equations

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

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

Equations

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

@[implicit_reducible]

instance Warstadt2022.instInhabitedGCWorld : Inhabited GCWorld

Equations

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

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.GCAssertion : Type

Assertable content for the green card scenario (silence is added separately via RSA.WithSilence).

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

• us : GCAssertion
• notUS : GCAssertion
• greenCard : GCAssertion
• notGreenCard : GCAssertion

@[implicit_reducible]

instance Warstadt2022.instDecidableEqGCAssertion : DecidableEq GCAssertion

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprGCAssertion : Repr GCAssertion

Equations

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

def Warstadt2022.instReprGCAssertion.repr : GCAssertion → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instInhabitedGCAssertion : Inhabited GCAssertion

Equations

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

@[implicit_reducible]

instance Warstadt2022.instFintypeGCAssertion : Fintype GCAssertion

Equations

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

@[reducible, inline]

abbrev Warstadt2022.GCUtterance : Type

Utterances for the green card scenario: none is the null utterance, some a a paper-utterance.

Equations

• Warstadt2022.GCUtterance = RSA.WithSilence Warstadt2022.GCAssertion

def Warstadt2022.allGCUtterances : List GCUtterance

Equations

• Warstadt2022.allGCUtterances = [none, some Warstadt2022.GCAssertion.us, some Warstadt2022.GCAssertion.notUS, some Warstadt2022.GCAssertion.greenCard, some Warstadt2022.GCAssertion.notGreenCard]

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.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.gcAssertionMeaning : GCAssertion → GCWorld → Bool

Truth conditions from Table 1. All negations are Boolean.

Equations

• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.us Warstadt2022.GCWorld.usCitizen = true
• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.us x✝ = false
• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.notUS Warstadt2022.GCWorld.usCitizen = false
• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.notUS x✝ = true
• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.greenCard Warstadt2022.GCWorld.gcHolder = true
• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.greenCard x✝ = false
• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.notGreenCard Warstadt2022.GCWorld.gcHolder = false
• Warstadt2022.gcAssertionMeaning Warstadt2022.GCAssertion.notGreenCard x✝ = true

def Warstadt2022.gcMeaning : GCUtterance → GCWorld → Bool

Utterance-level meaning: silence is universally true.

Equations

• Warstadt2022.gcMeaning = RSA.liftMeaning Warstadt2022.gcAssertionMeaning

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.greenCardPartialProp : Semantics.Presupposition.PartialProp GCWorld

PartialProp 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 (some GCAssertion.greenCard) w = true ↔ greenCardPartialProp.presup w ∧ greenCardPartialProp.assertion w

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

theorem Warstadt2022.gcMeaning_notGreenCard_eq_neg (w : GCWorld) : gcMeaning (some GCAssertion.notGreenCard) w = !gcMeaning (some GCAssertion.greenCard) w

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

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

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

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprFGSWorld : Repr FGSWorld

Equations

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

@[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.FGSAssertion : Type

Assertable content for the family-genus-species scenario (silence is added separately via RSA.WithSilence).

Six utterances: three positive descriptions at each taxonomic level plus their Boolean negations.

• olympicSprinter : FGSAssertion
• notOlympicSprinter : FGSAssertion
• runner : FGSAssertion
• notRunner : FGSAssertion
• athlete : FGSAssertion
• notAthlete : FGSAssertion

@[implicit_reducible]

instance Warstadt2022.instDecidableEqFGSAssertion : DecidableEq FGSAssertion

Equations

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

@[implicit_reducible]

instance Warstadt2022.instReprFGSAssertion : Repr FGSAssertion

Equations

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

def Warstadt2022.instReprFGSAssertion.repr : FGSAssertion → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Warstadt2022.instInhabitedFGSAssertion : Inhabited FGSAssertion

Equations

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

@[implicit_reducible]

instance Warstadt2022.instFintypeFGSAssertion : Fintype FGSAssertion

Equations

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

@[reducible, inline]

abbrev Warstadt2022.FGSUtterance : Type

Utterances for the family-genus-species scenario: none is the null utterance, some a a paper-utterance.

Equations

• Warstadt2022.FGSUtterance = RSA.WithSilence Warstadt2022.FGSAssertion

def Warstadt2022.allFGSUtterances : List FGSUtterance

Equations

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

def Warstadt2022.fgsAssertionMeaning : FGSAssertion → FGSWorld → Bool

Truth conditions from Table 2.

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

Equations

• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.olympicSprinter Warstadt2022.FGSWorld.olympicSprinter = true
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.olympicSprinter x✝ = false
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.notOlympicSprinter Warstadt2022.FGSWorld.olympicSprinter = false
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.notOlympicSprinter x✝ = true
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.runner Warstadt2022.FGSWorld.olympicSprinter = true
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.runner Warstadt2022.FGSWorld.runner = true
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.runner x✝ = false
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.notRunner Warstadt2022.FGSWorld.olympicSprinter = false
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.notRunner Warstadt2022.FGSWorld.runner = false
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.notRunner x✝ = true
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.athlete Warstadt2022.FGSWorld.nonAthlete = false
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.athlete x✝ = true
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.notAthlete Warstadt2022.FGSWorld.nonAthlete = true
• Warstadt2022.fgsAssertionMeaning Warstadt2022.FGSAssertion.notAthlete x✝ = false

def Warstadt2022.fgsMeaning : FGSUtterance → FGSWorld → Bool

Utterance-level meaning: silence is universally true.

Equations

• Warstadt2022.fgsMeaning = RSA.liftMeaning Warstadt2022.fgsAssertionMeaning

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 (some FGSAssertion.olympicSprinter) w = true → fgsMeaning (some FGSAssertion.runner) w = true

Olympic sprinter entails runner.

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

Runner entails athlete.

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

Olympic sprinter entails athlete (transitivity).

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

Boolean negation: not Olympic sprinter = ¬ Olympic sprinter.

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

Boolean negation: not runner = ¬ runner.

theorem Warstadt2022.fgsMeaning_notAthlete_eq_neg (w : FGSWorld) : fgsMeaning (some FGSAssertion.notAthlete) w = !fgsMeaning (some FGSAssertion.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

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.instDecidableEqGCContext : DecidableEq GCContext

Equations

• Warstadt2022.instDecidableEqGCContext = Warstadt2022.instDecidableEqGCContext.decEq

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

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 }

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

@[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.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✝

PartialProp Connection

theorem Warstadt2022.greenCard_meaning_from_prprop (w : GCWorld) : gcMeaning (some GCAssertion.greenCard) w = true ↔ greenCardPartialProp.presup w ∧ greenCardPartialProp.assertion w

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

theorem Warstadt2022.notGreenCard_is_boolean_negation (w : GCWorld) : gcMeaning (some GCAssertion.notGreenCard) w = !gcMeaning (some GCAssertion.greenCard) w

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