Docs / Semantics / Alternatives / Relevance

Relevance of alternatives

import Linglib.Semantics.Alternatives.Relevance · namespace Alternatives

Fox and Katzir restrict the formal alternatives of a sentence to the contextually relevant ones, with relevance closed under the Boolean operations. A sentence is exhaustively relevant given a restriction when its only-meaning lies in the Boolean closure of the restriction, and a restriction is allowable when it keeps the assertion and prunes nothing exhaustively relevant. A set in the Boolean closure of a family does not separate worlds that every member of the family treats alike (mem_iff_of_mem_closure), so an alternative whose only-meaning separates two such worlds is not exhaustively relevant (not_exhaustivelyRelevant_of_separates). Relevance relative to a context set is the same notion over the subtype of the context, each proposition restricted to it by preimage.

Main definitions

Alternatives.ExhaustivelyRelevant, Alternatives.IsAllowableRestriction

References

Fox & Katzir 2011, On the Characterization of Alternatives formalized

Declarations

A sentence is exhaustively relevant given a restriction when its only-meaning lies in the Boolean closure of the restriction.

def ExhaustivelyRelevant L36–39

{W : Type u_1} (A : Set (Set W)) (p : Set W) :

Prop

ExhaustivelyRelevant A p = (Exhaustification.exh A p ∈ BooleanSubalgebra.closure A)

Used by IsAllowableRestriction, not_exhaustivelyRelevant_of_separates

Used in Crnic2026b

A restriction of the formal alternatives is allowable when it keeps the assertion and prunes nothing exhaustively relevant.

def IsAllowableRestriction L41–44

{W : Type u_1} (F A : Set (Set W)) (S : Set W) :

Prop

IsAllowableRestriction F A S = (S ∈ A ∧ ∀ p ∈ F \ A, ¬ExhaustivelyRelevant A p)

Built from

Used in Crnic2026b, FoxKatzir2011

A set in the Boolean closure of A does not separate worlds that every member of A treats alike.

theorem mem_iff_of_mem_closure L48–56

{W : Type u_1} {A : Set (Set W)} {X : Set W} {u v : W} (hX : X ∈ BooleanSubalgebra.closure A) (h : ∀ a ∈ A, u ∈ a ↔ v ∈ a) :

u ∈ X ↔ v ∈ X

theorem not_exhaustivelyRelevant_of_separates L58–60

{W : Type u_1} {A : Set (Set W)} {p : Set W} {u v : W} (h : ∀ a ∈ A, u ∈ a ↔ v ∈ a) (hu : u ∈ Exhaustification.exh A p) (hv : v ∉ Exhaustification.exh A p) :

¬ExhaustivelyRelevant A p

Built from