Docs / Semantics / Presupposition / Strengthening

Presuppositional strengthening

import Linglib.Semantics.Presupposition.Strengthening · namespace Presupposition

Source

This file defines the strengthening of a presupposition by its alternatives: the worlds where it holds and no strictly stronger alternative's does, the domain of the operator EXHp. Removing the stronger presuppositions gives Percus's anti-presuppositions and Sauerland's implicated presuppositions. Heim's Maximize Presupposition, as Schlenker states it, compares presuppositions satisfied in a context: an expression must be a strongest alternative defined there. Strengthening is that condition at one-point contexts, its form after Chemla's epistemic step, and the condition is strengthening through a knowledge operator.

References

Declarations

L35–38
L40–46
L48–50

Maximize Presupposition in a context: φ is a strongest alternative defined throughout c.

theorem minimalFor_preimage_Ici_iffL52–64
{S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ : S} {c : Set W} :
MinimalFor (fun (x : S) => x ∈ insert φ (alts φ) ∩ content ⁻¹' Set.Ici c) content φ ↔ c ⊆ content φ ∧ ∀ ψ ∈ alts φ, content ψ ⊂ content φ → ¬c ⊆ content ψ

Strengthening is Maximize Presupposition at one-point contexts.

theorem mem_strengthen_iff_minimalFor_singletonL66–73
{S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ : S} {w : W} :
w ∈ strengthen alts content φ ↔ MinimalFor (fun (x : S) => x ∈ insert φ (alts φ) ∩ content ⁻¹' Set.Ici {w}) content φ

Built from

Through a knowledge operator, whose presupposition holds of the information states that support it, strengthening is the condition at a context: the operand is defined there and no strictly stronger alternative is.

theorem mem_strengthen_Iic_iffL75–86
{S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ : S} {c : Set W} :
c ∈ strengthen alts (fun (ψ : S) => Set.Iic (content ψ)) φ ↔ c ⊆ content φ ∧ ∀ ψ ∈ alts φ, content ψ ⊂ content φ → ¬c ⊆ content ψ

Built from

L88–90
L92–100
L102–106