Relevance-Sensitive Exhaustification (Magri 2009)

@cite{magri-2009}

@cite{magri-2009} parameterizes EXH by a contextual relevance relation R on alternatives. Only alternatives that are both innocently excludable and relevant get negated; irrelevant alternatives are silently dropped.

Design

Magri's operator is a one-line specialization of the post-exclusion combinator Excluder.restrict defined in Combinators.lean: magri R := innocent.restrict R. The combinator algebra (idempotence, identity, monotonicity, the Fox–Katzir asymmetry theorem restrict_preserves_no_implicature) lives in Combinators.lean so it can be reused by other base excluders. This file holds only the Magri-specific naming and corollaries.

This factoring is faithful to @cite{magri-2009} eq. (42), which writes relevance as a side filter on the I-E set, and matches the way @cite{fox-katzir-2011} treats the contextual constraint C as orthogonal to the choice-of-alternatives problem solved by the structural source.

def Exhaustification.magri {W : Type u_1} [Fintype W] [DecidableEq W] (R : Finset W → Bool) : Excluder W

Magri 2009's relevance-sensitive operator: innocent exclusion filtered by a contextual relevance predicate on alternatives.

@cite{magri-2009} eq. (42): EXH_R(A)(p)(w) = p(w) ∧ ∀q ∈ I-E(p,A). (¬R(q) ∨ ¬q(w)). Irrelevant alternatives drop out of the conjunction.

Equations

• Exhaustification.magri R = Exhaustification.innocent.restrict R

theorem Exhaustification.magri_const_true_eq_innocent {W : Type u_1} [Fintype W] [DecidableEq W] : (magri fun (x : Finset W) => true) = innocent

When every alternative is relevant, Magri's operator agrees with Fox's innocent exclusion.

theorem Exhaustification.innocent_exh_subset_magri_exh {W : Type u_1} [Fintype W] [DecidableEq W] (R : Finset W → Bool) (ALT : Finset (Finset W)) (φ : Finset W) : innocent.exh ALT φ ⊆ (magri R).exh ALT φ

Relevance can only weaken innocent.exh (more worlds survive). Direct corollary of Excluder.exh_subset_restrict_exh.