Documentation

Linglib.Theories.Semantics.Exhaustification.Tolerant

Tolerant Exhaustification (Chierchia 2013) #

@cite{chierchia-2013}

A second Excluder: negate every alternative not entailed by the prejacent, even if the result is contradictory.

An alternative a is non-weaker than φ iff φ ⊄ a (some φ-world is outside a). Innocent exclusion further requires that the negation of a be jointly compatible with the negations of other choices; the tolerant operator drops that requirement and excludes every non-weaker alternative unconditionally. The result tolerant.exh may therefore be empty (a contradiction).

Tolerance is empirically motivated by EFCIs (@cite{alonso-ovalle-moghiseh-2025}): applying tolerant to an unembedded existential free-choice item produces the contradiction that drives modal insertion or partial exhaustification.

Relationship to innocent #

Tolerance always excludes at least as much as innocent exclusion (every innocently-excludable alternative is non-weaker), so tolerant.exh ⊆ innocent.exh. The converse can fail when symmetric alternatives leave both choices outside IE while still being non-weaker.

source
def Exhaustification.tolerant {W : Type u_1} [Fintype W] [DecidableEq W] :
Excluder W

Chierchia 2013's contradiction-tolerating excluder: pick every alternative not entailed by the prejacent.

Equations
  • Exhaustification.tolerant = { excluded := fun (ALT : Finset (Finset W)) (φ : Finset W) => {a ∈ ALT | ¬φ ⊆ a}, excluded_subset := ⋯ }
Instances For
    source
    @[simp]
    theorem Exhaustification.tolerant_excluded {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) :
    tolerant.excluded ALT φ = {a ∈ ALT | ¬φ ⊆ a}
    source
    theorem Exhaustification.mem_tolerant_excluded {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ a : Finset W} :
    a ∈ tolerant.excluded ALT φ ↔ a ∈ ALT ∧ ¬φ ⊆ a
    source
    theorem Exhaustification.mem_tolerant_exh_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) {w : W} :
    w ∈ tolerant.exh ALT φ ↔ w ∈ φ ∧ ∀ a ∈ ALT, ¬φ ⊆ a → w ∉ a

    A world w survives tolerant.exh iff it satisfies the prejacent and falsifies every non-entailed alternative.

    source
    theorem Exhaustification.entailed_not_excluded {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ a : Finset W} (h : φ ⊆ a) :
    a ∉ tolerant.excluded ALT φ

    Alternatives entailed by the prejacent are kept, never negated.