Presuppositional Exhaustification (pex)

[DPBS24] [BDPS21]

Formalization of [DPBS24] "Free choice and presuppositional exhaustification" Semantics & Pragmatics 17, Article 3: 1–52.

Core idea

Standard exhaustification (exh) produces flat, fully assertive output: it asserts the prejacent plus negated IE alternatives plus II alternatives. pex splits this output into two dimensions:

• asserts: only the prejacent φ
• presupposes: (i) the negation of each IE alternative, and (ii) a homogeneity presupposition — that all II alternatives have the same truth value

This structuring is the mirror image of only: only presupposes its prejacent and asserts the negation of alternatives.

Why it matters

The assertive/presuppositional split lets pex derive:

1. Free choice for ◇∨ from local application
2. Double prohibition for ¬◇∨ from negation over pex's assertive component
3. Negative FC for ¬□∧ analogously
4. Correct predictions for embedded FC puzzles (under negative factives, in disjunctions, under quantifiers) via standard presupposition projection and filtering

Standard exh cannot solve these embedded puzzles because its output is flat — negation, factives, and filtering operators cannot distinguish assertive from presuppositional content.

Architecture

pexIEII takes the same IE/II computation from Operators.lean and produces a PartialProp World — a Prop-based partial proposition with separate assertive and presuppositional components. This directly integrates with the presupposition projection infrastructure in Semantics.Presupposition.

This file contains only the abstract pex theory (parameterized by an arbitrary World type and abstract ALT, φ). The concrete worked example over FCWorld (the five-world toy from [BLF20]) and all consequences specific to that example — pexFC, pex_fc, pex_double_prohibition, the negative-FC isomorphism, and the embedding puzzles from §3–§5 — live in the study file Studies/DelPinalBassiSauerland2024.lean.

Homogeneity

A set of propositions is homogeneous at a world w when all members agree on their truth value at w: either all true or all false.

This captures the presupposition triggered by pex for II alternatives. For FC: the II alternatives are ◇p and ◇q, so homogeneity gives ◇p ↔ ◇q.

def Exhaustification.Presuppositional.homogeneous {World : Type u_1} (S : Set (Set World)) (w : World) : Prop

Homogeneity: all propositions in a set have the same truth value. For the empty set, homogeneity holds vacuously.

Equations

• Exhaustification.Presuppositional.homogeneous S w = ∀ α ∈ S, ∀ β ∈ S, α w ↔ β w

theorem Exhaustification.Presuppositional.homogeneous_pair {World : Type u_1} (p q : Set World) (w : World) : homogeneous {p, q} w ↔ (p w ↔ q w)

Homogeneity over a two-element set is biconditional.

theorem Exhaustification.Presuppositional.homogeneous_and_exists_imp_all {World : Type u_1} (S : Set (Set World)) (w : World) (hHomog : homogeneous S w) (α : Set World) (hα : α ∈ S) (ha : α w) (β : Set World) : β ∈ S → β w

Homogeneity + at-least-one-holds → all hold.

pex^{IE+II}: Presuppositional Exhaustification

Definition (9) from the paper. For a structure φ of propositional type and a local context c:

⟦pex^{IE+II}(φ)⟧: a. asserts: ⟦φ⟧ b. presupposes: (i) ⋂₀ {¬⟦ψ⟧ : ψ ∈ IE(φ) ∧ ⟦ψ⟧ ∈ Rₓ} (ii) homogeneity over relevant II alternatives

We treat Rₓ (the relevance predicate) as a parameter; for basic cases all alternatives are relevant.

def Exhaustification.Presuppositional.pexIEII {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (Rc : Set (Set World)) : Semantics.Presupposition.PartialProp World

pex^{IE+II}: Presuppositional exhaustification with IE and II.

Unlike exhIEII which returns Set World (flat, fully assertive), pexIEII returns PartialProp World (assertive + presuppositional).

• assertion = φ (the prejacent)
• presupposition = (negation of relevant IE alternatives) ∧ (homogeneity of relevant II alternatives)

Equations

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

def Exhaustification.Presuppositional.pexIEII_full {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : Semantics.Presupposition.PartialProp World

pex with all alternatives relevant (the default case).

Equations

• Exhaustification.Presuppositional.pexIEII_full ALT φ = Exhaustification.Presuppositional.pexIEII ALT φ ALT

theorem Exhaustification.Presuppositional.pex_assertion_eq {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (Rc : Set (Set World)) : (pexIEII ALT φ Rc).assertion = φ

pex asserts the prejacent.

theorem Exhaustification.Presuppositional.pex_holds_entails_prejacent {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (Rc : Set (Set World)) (w : World) (h : Semantics.Presupposition.PartialProp.holds w (pexIEII ALT φ Rc)) : φ w

The overall meaning of pex (presupposition ∧ assertion) entails φ.

theorem Exhaustification.Presuppositional.pex_neg_assertion {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (Rc : Set (Set World)) : (pexIEII ALT φ Rc).neg.assertion = fun (w : World) => ¬φ w

Negation applies only to the assertive component; presupposition projects.

theorem Exhaustification.Presuppositional.pex_neg_presup {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (Rc : Set (Set World)) : (pexIEII ALT φ Rc).neg.presup = (pexIEII ALT φ Rc).presup

Negation preserves the presupposition (projection from under negation).

Negative Free Choice (abstract entailment)

For ¬□(p ∧ q)-sentences:

• φ = ¬□(p ∧ q)
• The pex output presupposes ¬□p ↔ ¬□q

Combined with ¬□(p ∧ q), this entails ¬□p ∧ ¬□q.

This result is stated as a pure entailment theorem: the interaction of the assertion ¬□(p ∧ q) and homogeneity ¬□p ↔ ¬□q suffices for negative FC, regardless of how IE/II are computed.

theorem Exhaustification.Presuppositional.negative_fc_entailment {W : Type u_2} (boxP boxQ : Set W) (w : W) (hassert : ¬(boxP w ∧ boxQ w)) (hhomog : ¬boxP w ↔ ¬boxQ w) : ¬boxP w ∧ ¬boxQ w

Negative FC entailment: ¬□(p ∧ q) + homogeneity(¬□p, ¬□q) → ¬□p ∧ ¬□q.

This is the paper's (19a): ⟦pex^{IE+II}[¬□[T ∧ B]]⟧ = (¬□T ∨ ¬□B)_{¬□T↔¬□B} ⊨ ¬□T ∧ ¬□B

Equivalence for Non-FC Cases

For basic (non-FC) scalar sentences, pex^{IE+II} and exh^{IE+II} predict the same overall entailments. When II is empty (no innocent inclusion), pex reduces to asserting φ and presupposing ¬IE — matching pex^{IE}.

This is the paper's (11a): ⟦pex^{IE+II}(∃)⟧ = ⟦pex^{IE}(∃)⟧ = ∃_{¬∀}

theorem Exhaustification.Presuppositional.pex_basic_scalar {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (Rc : Set (Set World)) (hII_empty : ∀ α ∈ II ALT φ, α ∈ Rc → False) (w : World) : (pexIEII ALT φ Rc).presup w ↔ ∀ (ψ : Set World), IsInnocentlyExcludable ALT φ ψ → ψ ∈ Rc → ¬ψ w

For basic scalar sentences (where II ∩ Rc is empty), pex's presupposition reduces to just the negated IE alternatives (homogeneity is vacuous).

Structural Difference: pex vs exh

The key structural difference:

exh^{IE+II}(φ) = φ ∧ ¬IE ∧ II (flat, fully assertive) pex^{IE+II}(φ) = φ_{¬IE ∧ homog(II)} (structured)

For FC (φ = ◇(p∨q)): exh: ◇(p∨q) ∧ ◇p ∧ ◇q ∧ ¬◇(p∧q) pex: asserts ◇(p∨q), presupposes (◇p ↔ ◇q) ∧ ¬◇(p∧q)

The overall entailments are the same (both entail ◇p ∧ ◇q), but the at-issue structure differs. This difference is what allows pex to solve the embedded FC puzzles that exh cannot.

For the concrete worked example over FCWorld and the embedded FC puzzles, see Studies/DelPinalBassiSauerland2024.lean.