Postsuppositions

@cite{brasoveanu-2009} @cite{lauer-2009} @cite{glass-2025}

Output-context constraints: conditions on the Common Ground after an utterance updates it, as opposed to presuppositions which constrain the input context.

@cite{glass-2025} argues that Mandarin yǐwéi has a postsupposition ◇¬p — after accepting "x yǐwéi p", the CG must be compatible with ¬p. This is distinct from a presupposition (input-context condition) and cannot be derived from veridicality alone.

structure Core.Postsupposition.Postsupposition (W : Type u_1) : Type u_1

A postsupposition: a constraint on the output context after a discourse update.

Unlike presuppositions (input-context constraints on PrProp.presup), postsuppositions constrain what must hold of the context after the at-issue content updates it.

The condition takes a context set (as List W) and the embedded proposition p, returning whether the output-context requirement holds.

• condition : List W → (W → Bool) → Bool

def Core.Postsupposition.Postsupposition.none {W : Type u_1} : Postsupposition W

No postsupposition (trivially satisfied).

Equations

• Core.Postsupposition.Postsupposition.none = { condition := fun (x : List W) (x_1 : W → Bool) => true }

def Core.Postsupposition.Postsupposition.weakContrafactive {W : Type u_1} : Postsupposition W

Weak contrafactive postsupposition: the output context must be compatible with ¬p. That is, at least one world in the output context has p false.

This is yǐwéi's ◇¬p (@cite{glass-2025}, @cite{glass-2023}).

Equations

• Core.Postsupposition.Postsupposition.weakContrafactive = { condition := fun (cs : List W) (p : W → Bool) => cs.any fun (x : W) => !p x }

def Core.Postsupposition.Postsupposition.strongContrafactive {W : Type u_1} : Postsupposition W

Strong contrafactive postsupposition: the output context must entail ¬p. That is, all worlds in the output context have p false.

This is the hypothetical contra verb's requirement — UNATTESTED.

Equations

• Core.Postsupposition.Postsupposition.strongContrafactive = { condition := fun (cs : List W) (p : W → Bool) => cs.all fun (x : W) => !p x }

def Core.Postsupposition.Postsupposition.satisfied {W : Type u_1} (ps : Postsupposition W) (outputCtx : List W) (p : W → Bool) : Bool

Check satisfaction against a concrete context set and proposition.

Equations

• ps.satisfied outputCtx p = ps.condition outputCtx p

theorem Core.Postsupposition.Postsupposition.none_always_satisfied {W : Type u_1} (cs : List W) (p : W → Bool) : none.satisfied cs p = true

The trivial postsupposition is always satisfied.

theorem Core.Postsupposition.Postsupposition.strong_entails_weak {W : Type u_1} (cs : List W) (p : W → Bool) (hne : cs ≠ []) : strongContrafactive.satisfied cs p = true → weakContrafactive.satisfied cs p = true

Strong contrafactivity entails weak contrafactivity (for nonempty contexts): if CG ⊨ ¬p (all worlds have ¬p), then CG ◇ ¬p (some world has ¬p). This captures @cite{glass-2025}'s key observation that yǐwéi's requirement is strictly weaker than the hypothetical contra verb's.

theorem Core.Postsupposition.Postsupposition.weak_not_entails_strong : ∃ (cs : List Bool), ∃ (p : Bool → Bool), weakContrafactive.satisfied cs p = true ∧ strongContrafactive.satisfied cs p = false

Weak contrafactivity does NOT entail strong: a context can be compatible with ¬p without entailing ¬p.