Heim (1983): Projection and Partial Context Change

[Hei83] [Kar73]

The classic King and factive-verb examples, their PartialProp denotations, NeoGricean PresupDerivation wrappers, and the filtering predictions derived from partial context change potentials.

Main declarations

• kingExists, kingBald, ifKingThenBald: the King example, with ifKingThenBald_no_presup showing conditional filtering.
• johnKnowsRaining: the factive example.
• conditional_admitted_everywhere / bare_consequent_not_admitted: the filtering recorded in the trigger tables, derived from PartialCCP admittance rather than stipulated.

inductive Heim1983.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

@[implicit_reducible]

instance Heim1983.instDecidableEqKingWorld : DecidableEq KingWorld

Equations

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

@[implicit_reducible]

instance Heim1983.instReprKingWorld : Repr KingWorld

Equations

• Heim1983.instReprKingWorld = { reprPrec := Heim1983.instReprKingWorld.repr }

def Heim1983.instReprKingWorld.repr : KingWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Heim1983.instReprKingWorld.repr Heim1983.KingWorld.noKing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1983.KingWorld.noKing")).group prec✝

@[implicit_reducible]

instance Heim1983.instInhabitedKingWorld : Inhabited KingWorld

Equations

• Heim1983.instInhabitedKingWorld = { default := Heim1983.instInhabitedKingWorld.default }

def Heim1983.kingExists : Semantics.Presupposition.PartialProp 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 Heim1983.kingBald : Semantics.Presupposition.PartialProp 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 Heim1983.ifKingThenBald : Semantics.Presupposition.PartialProp 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

• Heim1983.ifKingThenBald = Heim1983.kingExists.impFilter Heim1983.kingBald

theorem Heim1983.ifKingThenBald_no_presup : ifKingThenBald.presup = fun (x : KingWorld) => True

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

This demonstrates presupposition filtering.

inductive Heim1983.RainWorld : Type

World type for factive verb examples.

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

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

@[implicit_reducible]

instance Heim1983.instDecidableEqRainWorld : DecidableEq RainWorld

Equations

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

def Heim1983.instReprRainWorld.repr : RainWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Heim1983.instReprRainWorld : Repr RainWorld

Equations

• Heim1983.instReprRainWorld = { reprPrec := Heim1983.instReprRainWorld.repr }

@[implicit_reducible]

instance Heim1983.instInhabitedRainWorld : Inhabited RainWorld

Equations

• Heim1983.instInhabitedRainWorld = { default := Heim1983.instInhabitedRainWorld.default }

def Heim1983.johnKnowsRaining : Semantics.Presupposition.PartialProp 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 Heim1983.kingBaldDerivation : Semantics.Presupposition.TriggerTypology.PresupDerivation KingWorld

The King example as a PresupDerivation, adding trigger information for NeoGricean SI computation.

Equations

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

def Heim1983.ifKingThenBaldDerivation : Semantics.Presupposition.TriggerTypology.PresupDerivation KingWorld

The conditional "If the king exists, the king is bald" as a derivation.

Note: No presupposition triggers project because filtering eliminates them.

Equations

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

def Heim1983.johnKnowsRainingDerivation : Semantics.Presupposition.TriggerTypology.PresupDerivation RainWorld

Factive verb example as a derivation.

Equations

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

theorem Heim1983.filtering_removes_trigger : ifKingThenBaldDerivation.triggers = []

Filtering affects which triggers are relevant for SI.

When a presupposition is filtered (locally satisfied), the corresponding trigger no longer contributes to global presupposition, and alternatives involving that trigger may behave differently. (The triggers := [] entry is derived below: conditional_admitted_everywhere proves the filtering from the partial-CCP semantics rather than stipulating it.)

Filtering derived from partial CCPs

[Hei83]'s actual machinery: sentences denote partial context change potentials (Semantics.Dynamic.Core.PartialCCP), and admittance does the projection work. The conditional's CCP is admitted by every context — the antecedent's update satisfies the consequent's king-presupposition — while the bare consequent's CCP is not admitted by the full context. The filtering recorded in the trigger tables above is a theorem, not a table entry.

theorem Heim1983.conditional_admitted_everywhere (c : Set KingWorld) : ((Semantics.Dynamic.Core.PartialCCP.ofPartialProp kingExists).pcond (Semantics.Dynamic.Core.PartialCCP.ofPartialProp kingBald)).admits c

Every context admits ⟦if the king exists, the king is bald⟧: the antecedent's update filters the consequent's presupposition ([Hei83]'s conditional CCP).

theorem Heim1983.bare_consequent_not_admitted : ¬(Semantics.Dynamic.Core.PartialCCP.ofPartialProp kingBald).admits Set.univ

The bare consequent ⟦the king is bald⟧ is NOT admitted by the full context: the noKing world fails the presupposition, which therefore projects.