Heim (1983): Projection and Partial Context Change

[Hei83] [Kar73]

The classic King and factive-verb examples, their PartialProp denotations, 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: conditional filtering derived from CCP.Partial admittance rather than stipulated.
• admits_seq_iff_conj: [Kar73]'s conjunction filter, relativized to the context as its set of background assumptions, is admittance of the sequenced update.

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

@[instance_reducible]

instance Heim1983.instDecidableEqKingWorld : DecidableEq KingWorld

Equations

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

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✝

@[instance_reducible]

instance Heim1983.instReprKingWorld : Repr KingWorld

Equations

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

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

@[instance_reducible]

instance Heim1983.instDecidableEqRainWorld : DecidableEq RainWorld

Equations

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

@[instance_reducible]

instance Heim1983.instReprRainWorld : Repr RainWorld

Equations

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

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

Equations

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

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

Filtering derived from partial CCPs

[Hei83]'s actual machinery: sentences denote partial context change potentials (DynamicSemantics.CCP.Partial), 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.

theorem Heim1983.conditional_admitted_everywhere (c : Set KingWorld) : ((DynamicSemantics.CCP.Partial.ofPartialProp kingExists).cond (DynamicSemantics.CCP.Partial.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 : ¬(DynamicSemantics.CCP.Partial.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.

theorem Heim1983.admits_seq_iff_conj {W : Type u_1} (c : Set W) (p q : Semantics.Presupposition.PartialProp W) : ((DynamicSemantics.CCP.Partial.ofPartialProp p).seq (DynamicSemantics.CCP.Partial.ofPartialProp q)).admits c ↔ ∀ w ∈ c, (Karttunen1973.conj c p q).presup w

[Kar73]'s filter for conjunction, relativized to the context itself as the set of background assumptions (his §9), is admittance of the sequenced update.