Asymmetric entailment over a finite world set

A polymorphic primitive: ψ asymmetrically entails φ over a finite set of worlds when every ψ-world is a φ-world and at least one φ-world is not a ψ-world. Equivalently, worlds.filter ψ ⊂ worlds.filter φ.

This is the shared core of "primary-implicature triggering" (Sauerland 2004 over EpistemicState.possible) and the asymmetric-entailment fragment of various exhaustification operators. The intent is that any study or theory file needing asymmetric entailment over a finite domain of world predicates uses this rather than reinventing it.

Why a polymorphic version

Theories/Semantics/Entailment/Basic.lean defines entails over a concrete World enum (w0–w3) for testbed purposes. That file is not the right home for a polymorphic primitive. This file is.

What this does NOT subsume

• RSA.IBR.strongestAt (Theories/Pragmatics/IBR/ScalarGames.lean) — expresses "m is the strongest true message at s" as a unary predicate on messages, not the binary asymmetric-entailment relation. The two are linked (m strongest ↔ ∀ m', ¬ asymStrongerOn univ (G.meaning m') (G.meaning m) ∨ m' false at s) but the proofs in ScalarGames.lean are 200+ lines built around the unary form. Rewriting them on top of this primitive is a separate refactor.

• Magri2014.innerExcludable (Phenomena/Plurals/Studies/Magri2014.lean) — combines (a) a hand-wired entails : Role → Role → Bool on a three-element role enum with (b) a Horn-mateness filter. The entails is not derivable as asymStrongerOn over a world set because Magri's Scenario type isn't Fintype (arbitrary total : Nat). Lifting Magri to use this primitive would require either a Fintype-restricted Scenario or a separate non-Fintype variant.

Both are noted as future consolidation targets but require deeper architectural work than a literal find-and-replace.

def Semantics.Entailment.asymStrongerOn {W : Type u_1} (worlds : Finset W) (ψ φ : W → Prop) [DecidablePred ψ] [DecidablePred φ] : Prop

ψ asymmetrically entails φ over worlds: every ψ-world in worlds is a φ-world, and at least one φ-world in worlds is not a ψ-world.

Defined in explicit forall-exists form (matching mathlib's MonotoneOn idiom). Equivalent to worlds.filter ψ ⊂ worlds.filter φ — see asymStrongerOn_iff_filter_ssubset.

Equations

• Semantics.Entailment.asymStrongerOn worlds ψ φ = ((∀ w ∈ worlds, ψ w → φ w) ∧ ∃ w ∈ worlds, φ w ∧ ¬ψ w)

@[implicit_reducible]

instance Semantics.Entailment.instDecidableAsymStrongerOn {W : Type u_1} (worlds : Finset W) (ψ φ : W → Prop) [DecidablePred ψ] [DecidablePred φ] : Decidable (asymStrongerOn worlds ψ φ)

Equations

• Semantics.Entailment.instDecidableAsymStrongerOn worlds ψ φ = Semantics.Entailment.instDecidableAsymStrongerOn._aux_1 worlds ψ φ

theorem Semantics.Entailment.asymStrongerOn_iff_filter_ssubset {W : Type u_1} (worlds : Finset W) (ψ φ : W → Prop) [DecidablePred ψ] [DecidablePred φ] : asymStrongerOn worlds ψ φ ↔ Finset.filter ψ worlds ⊂ Finset.filter φ worlds

Bridge to the mathlib filter form: asymStrongerOn is exactly strict subset of the filtered subsets.

theorem Semantics.Entailment.not_asymStrongerOn_self {W : Type u_1} (worlds : Finset W) (φ : W → Prop) [DecidablePred φ] : ¬asymStrongerOn worlds φ φ

Asymmetric entailment is irreflexive.