inductive Phenomena.Presupposition.KingWorld : Type

World type for the king example.

Two possible states:

• kingExists: There is a (unique) king in this world
• noKing: There is no king in this world

• kingExists : KingWorld
• noKing : KingWorld

instance Phenomena.Presupposition.instDecidableEqKingWorld : DecidableEq KingWorld

Equations

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

instance Phenomena.Presupposition.instReprKingWorld : Repr KingWorld

Equations

• Phenomena.Presupposition.instReprKingWorld = { reprPrec := Phenomena.Presupposition.instReprKingWorld.repr }

def Phenomena.Presupposition.instReprKingWorld.repr : KingWorld → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.instInhabitedKingWorld.default : KingWorld

Equations

• Phenomena.Presupposition.instInhabitedKingWorld.default = Phenomena.Presupposition.KingWorld.kingExists

instance Phenomena.Presupposition.instInhabitedKingWorld : Inhabited KingWorld

Equations

• Phenomena.Presupposition.instInhabitedKingWorld = { default := Phenomena.Presupposition.instInhabitedKingWorld.default }

instance Phenomena.Presupposition.instFiniteWorldsKingWorld : Core.Proposition.FiniteWorlds KingWorld

Equations

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

def Phenomena.Presupposition.kingExists : Core.Presupposition.PrProp KingWorld

"The king exists" — a presuppositionless assertion.

This sentence has:

• No presupposition (trivially true)
• Assertion: the king exists

Equations

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

def Phenomena.Presupposition.kingBald : Core.Presupposition.PrProp KingWorld

"The king is bald" — presupposes king exists.

This sentence has:

• Presupposition: the king exists
• Assertion: the king is bald (true when king exists)

Equations

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

def Phenomena.Presupposition.ifKingThenBald : Core.Presupposition.PrProp KingWorld

"If the king exists, the king is bald" — using filtering implication.

Demonstrates presupposition filtering: the antecedent's assertion satisfies the consequent's presupposition.

Equations

• Phenomena.Presupposition.ifKingThenBald = Phenomena.Presupposition.kingExists.impFilter Phenomena.Presupposition.kingBald

theorem Phenomena.Presupposition.ifKingThenBald_no_presup : ifKingThenBald.presup = fun (x : KingWorld) => true

"If the king exists, the king is bald" has no presupposition.

This demonstrates presupposition filtering.

def Phenomena.Presupposition.kingNotBald : Core.Presupposition.PrProp KingWorld

"The king isn't bald" — negation preserves presupposition.

Equations

• Phenomena.Presupposition.kingNotBald = Phenomena.Presupposition.kingBald.neg

theorem Phenomena.Presupposition.kingNotBald_presupposes_existence : kingNotBald.presup = kingBald.presup

inductive Phenomena.Presupposition.RainWorld : Type

World type for factive verb examples.

Models whether it's raining and whether John believes it.

• rainingBelieved : RainWorld
• rainingNotBelieved : RainWorld
• notRaining : RainWorld

instance Phenomena.Presupposition.instDecidableEqRainWorld : DecidableEq RainWorld

Equations

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

instance Phenomena.Presupposition.instReprRainWorld : Repr RainWorld

Equations

• Phenomena.Presupposition.instReprRainWorld = { reprPrec := Phenomena.Presupposition.instReprRainWorld.repr }

def Phenomena.Presupposition.instReprRainWorld.repr : RainWorld → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.instInhabitedRainWorld.default : RainWorld

Equations

• Phenomena.Presupposition.instInhabitedRainWorld.default = Phenomena.Presupposition.RainWorld.rainingBelieved

instance Phenomena.Presupposition.instInhabitedRainWorld : Inhabited RainWorld

Equations

• Phenomena.Presupposition.instInhabitedRainWorld = { default := Phenomena.Presupposition.instInhabitedRainWorld.default }

instance Phenomena.Presupposition.instFiniteWorldsRainWorld : Core.Proposition.FiniteWorlds RainWorld

Equations

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

def Phenomena.Presupposition.raining : Core.Presupposition.PrProp RainWorld

"It's raining" — no presupposition.

Equations

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

def Phenomena.Presupposition.johnKnowsRaining : Core.Presupposition.PrProp RainWorld

"John knows that it's raining" — factive presupposition.

Presupposes: it's raining Asserts: John believes it's raining

Equations

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

def Phenomena.Presupposition.johnDoesntKnowRaining : Core.Presupposition.PrProp RainWorld

"John doesn't know that it's raining" — negation preserves factive presupposition.

Equations

• Phenomena.Presupposition.johnDoesntKnowRaining = Phenomena.Presupposition.johnKnowsRaining.neg

theorem Phenomena.Presupposition.negation_preserves_factive : johnDoesntKnowRaining.presup = johnKnowsRaining.presup

inductive Phenomena.Presupposition.SmokingWorld : Type

World type for change-of-state examples.

Models John's smoking history.

• usedToNowQuit : SmokingWorld
• usedToStillDoes : SmokingWorld
• neverSmoked : SmokingWorld

instance Phenomena.Presupposition.instDecidableEqSmokingWorld : DecidableEq SmokingWorld

Equations

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

def Phenomena.Presupposition.instReprSmokingWorld.repr : SmokingWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.instReprSmokingWorld : Repr SmokingWorld

Equations

• Phenomena.Presupposition.instReprSmokingWorld = { reprPrec := Phenomena.Presupposition.instReprSmokingWorld.repr }

def Phenomena.Presupposition.instInhabitedSmokingWorld.default : SmokingWorld

Equations

• Phenomena.Presupposition.instInhabitedSmokingWorld.default = Phenomena.Presupposition.SmokingWorld.usedToNowQuit

instance Phenomena.Presupposition.instInhabitedSmokingWorld : Inhabited SmokingWorld

Equations

• Phenomena.Presupposition.instInhabitedSmokingWorld = { default := Phenomena.Presupposition.instInhabitedSmokingWorld.default }

instance Phenomena.Presupposition.instFiniteWorldsSmokingWorld : Core.Proposition.FiniteWorlds SmokingWorld

Equations

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

def Phenomena.Presupposition.johnStoppedSmoking : Core.Presupposition.PrProp SmokingWorld

"John stopped smoking" — presupposes prior smoking.

Presupposes: John used to smoke Asserts: John no longer smokes

Equations

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

def Phenomena.Presupposition.johnDidntStopSmoking : Core.Presupposition.PrProp SmokingWorld

"John didn't stop smoking" — preserves change-of-state presupposition.

Equations

• Phenomena.Presupposition.johnDidntStopSmoking = Phenomena.Presupposition.johnStoppedSmoking.neg

theorem Phenomena.Presupposition.negation_preserves_change_of_state : johnDidntStopSmoking.presup = johnStoppedSmoking.presup

def Phenomena.Presupposition.johnSmokesAndStopped : Core.Presupposition.PrProp SmokingWorld

"John smokes and he stopped" — contradiction via filtering conjunction.

Left conjunct: John smokes (no presup) Right conjunct: John stopped smoking (presupposes he used to smoke)

With filtering: left conjunct asserts smoking, right presupposes it was prior. This creates a pragmatically odd sentence (you can't currently smoke AND have stopped).

Equations

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

structure Phenomena.Presupposition.ProjectionPattern : Type

Summary of projection patterns across connectives.

These capture the empirical generalizations from @cite{karttunen-1973}.

• name : String

  Name of the pattern

• description : String

  Description

• projects : Bool

  Whether presupposition projects through

def Phenomena.Presupposition.negationPattern : ProjectionPattern

Equations

• Phenomena.Presupposition.negationPattern = { name := "Negation", description := "Presupposition projects unchanged through negation", projects := true }

def Phenomena.Presupposition.conditionalPattern : ProjectionPattern

Equations

• Phenomena.Presupposition.conditionalPattern = { name := "Conditional", description := "Antecedent can satisfy consequent's presupposition", projects := false }

def Phenomena.Presupposition.conjunctionPattern : ProjectionPattern

Equations

• Phenomena.Presupposition.conjunctionPattern = { name := "Conjunction", description := "Left conjunct can satisfy right's presupposition", projects := false }

def Phenomena.Presupposition.disjunctionPattern : ProjectionPattern

Equations

• Phenomena.Presupposition.disjunctionPattern = { name := "Disjunction", description := "Each disjunct can satisfy the other's presupposition", projects := false }