def Exhaustification.entails {World : Type u_1} (φ ψ : Prop' World) : Prop

Entailment: φ ⊆ ψ (Spector uses set-theoretic notation) "I also adopt the set-theoretic notation φ ⊆ ψ to mean that φ entails ψ."

Equations

• (φ ⊆ₚ ψ) = ∀ (w : World), φ w → ψ w

def Exhaustification.«term_⊆ₚ_» : Lean.TrailingParserDescr

Equations

• Exhaustification.«term_⊆ₚ_» = Lean.ParserDescr.trailingNode `Exhaustification.«term_⊆ₚ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ₚ ") (Lean.ParserDescr.cat `term 0))

def Exhaustification.pequiv {World : Type u_1} (φ ψ : Prop' World) : Prop

Equivalence of propositions

Equations

• (φ ≡ₚ ψ) = ((φ ⊆ₚ ψ) ∧ ψ ⊆ₚ φ)

def Exhaustification.«term_≡ₚ_» : Lean.TrailingParserDescr

Equations

• Exhaustification.«term_≡ₚ_» = Lean.ParserDescr.trailingNode `Exhaustification.«term_≡ₚ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ₚ ") (Lean.ParserDescr.cat `term 0))

def Exhaustification.pneg {World : Type u_1} (φ : Prop' World) : Prop' World

Negation of a proposition

Equations

• (∼φ) w = ¬φ w

def Exhaustification.«term∼_» : Lean.ParserDescr

Equations

• Exhaustification.«term∼_» = Lean.ParserDescr.node `Exhaustification.«term∼_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 75))

def Exhaustification.pand {World : Type u_1} (φ ψ : Prop' World) : Prop' World

Conjunction of two propositions

Equations

• (φ ∧ₚ ψ) w = (φ w ∧ ψ w)

def Exhaustification.«term_∧ₚ_» : Lean.TrailingParserDescr

Equations

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

def Exhaustification.bigConj {World : Type u_1} (X : Set (Prop' World)) : Prop' World

Conjunction of a set of propositions (grand conjunction ⋀X) "⋀X refers to the grand conjunction of its members, i.e., the proposition that is true in a world u if and only if every member of X is true in u"

Equations

• ⋀ X w = ∀ φ ∈ X, φ w

def Exhaustification.«term⋀» : Lean.ParserDescr

Equations

• Exhaustification.«term⋀» = Lean.ParserDescr.node `Exhaustification.«term⋀» 1024 (Lean.ParserDescr.symbol "⋀")

def Exhaustification.bigDisj {World : Type u_1} (X : Set (Prop' World)) : Prop' World

Disjunction of a set of propositions (grand disjunction ⋁X) "⋁X refers to the grand disjunction of the members of X, i.e., the proposition that is true in a world u if and only if at least one member of X is true in u"

Equations

• ⋁ X w = ∃ φ ∈ X, φ w

def Exhaustification.«term⋁» : Lean.ParserDescr

Equations

• Exhaustification.«term⋁» = Lean.ParserDescr.node `Exhaustification.«term⋁» 1024 (Lean.ParserDescr.symbol "⋁")

def Exhaustification.leALT {World : Type u_1} (ALT : Set (Prop' World)) (u v : World) : Prop

Definition 1.1: Given a set of alternatives ALT, ≤_ALT is the preorder over possible worlds defined as follows:

u ≤_ALT v iff {a ∈ ALT : a(u) = 1} ⊆ {a ∈ ALT : a(v) = 1}

"u makes true a subset of the alternatives that v makes true"

Equations

• (u ≤[ALT] v) = ∀ a ∈ ALT, a u → a v

def Exhaustification.ltALT {World : Type u_1} (ALT : Set (Prop' World)) (u v : World) : Prop

Definition 1.2: <_ALT is the strict preorder corresponding to ≤_ALT:

u <_ALT v iff u ≤_ALT v ∧ ¬(v ≤_ALT u)

"The alternatives that u makes true are a proper subset of those that v makes true."

Equations

• (u <[ALT] v) = ((u ≤[ALT] v) ∧ ¬v ≤[ALT] u)

def Exhaustification.«term_≤[_]_» : Lean.TrailingParserDescr

Equations

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

def Exhaustification.«term_<[_]_» : Lean.TrailingParserDescr

Equations

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

theorem Exhaustification.leALT_refl {World : Type u_1} (ALT : Set (Prop' World)) (u : World) : u ≤[ALT] u

theorem Exhaustification.leALT_trans {World : Type u_1} (ALT : Set (Prop' World)) (u v w : World) (huv : u ≤[ALT] v) (hvw : v ≤[ALT] w) : u ≤[ALT] w

def Exhaustification.exhMW {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : Prop' World

Definition 2: Exhaustivity operator based on minimal worlds (exh_mw)

Given a set of propositions ALT and a proposition φ,

exh_mw(ALT, φ) = {u : φ(u) = 1 ∧ ¬∃v(φ(v) = 1 ∧ v <_ALT u)}

Equivalently: exh_mw(ALT, φ) = φ ∩ {u : ¬∃v(φ(v) = 1 ∧ v <_ALT u)}

"The set of φ-worlds that are minimal relative to <_ALT"

Equations

• Exhaustification.exhMW ALT φ u = (φ u ∧ ¬∃ (v : World), φ v ∧ v <[ALT] u)

def Exhaustification.isMinimal {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) : Prop

A world u is minimal among φ-worlds relative to <_ALT.

Equations

• Exhaustification.isMinimal ALT φ u = (φ u ∧ ¬∃ (v : World), φ v ∧ v <[ALT] u)

theorem Exhaustification.exhMW_entails {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : exhMW ALT φ ⊆ₚ φ

def Exhaustification.SetConsistent {World : Type u_1} (X : Set (Prop' World)) : Prop

Definition 3.1: A set of propositions X is consistent if there exists a world u in which every member of X is true.

Equations

• Exhaustification.SetConsistent X = ∃ (u : World), ∀ ψ ∈ X, ψ u

def Exhaustification.isCompatible {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (E : Set (Prop' World)) : Prop

Definition 3.2: Given a proposition φ and a set of alternatives ALT, a set of propositions E is (ALT, φ)-compatible if and only if: a) φ ∈ E b) every member of E distinct from φ is the negation of a member of ALT c) E is consistent

Equations

• Exhaustification.isCompatible ALT φ E = (φ ∈ E ∧ (∀ ψ ∈ E, ψ = φ ∨ ∃ a ∈ ALT, ψ = ∼a) ∧ Exhaustification.SetConsistent E)

def Exhaustification.isMCSet {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (E : Set (Prop' World)) : Prop

Definition 3.3: MC_(ALT,φ)-sets

A set is maximal (ALT, φ)-compatible (MC_(ALT,φ)-set for short) if it is (ALT, φ)-compatible and is not properly included in any other (ALT, φ)-compatible set.

Equations

• Exhaustification.isMCSet ALT φ E = (Exhaustification.isCompatible ALT φ E ∧ ∀ (E' : Set (Prop' World)), Exhaustification.isCompatible ALT φ E' → E ⊆ E' → E' ⊆ E)

def Exhaustification.IE {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : Set (Prop' World)

Definition 3.4: IE_(ALT,φ) = {ψ : ψ belongs to every MC_(ALT,φ)-set}

"Note that, somewhat counter-intuitively, the set IE_(ALT,φ) is not the set of innocently excludable alternatives, but rather the set that contains φ and all the negations of innocently excludable alternatives."

Equations

• Exhaustification.IE ALT φ = {ψ : Prop' World | ∀ (E : Set (Prop' World)), Exhaustification.isMCSet ALT φ E → ψ ∈ E}

def Exhaustification.isInnocentlyExcludable {World : Type u_1} (ALT : Set (Prop' World)) (φ a : Prop' World) : Prop

Definition 3.5: An alternative a is innocently excludable given ALT and φ if and only if ¬a ∈ IE_(ALT,φ).

Equations

• Exhaustification.isInnocentlyExcludable ALT φ a = (a ∈ ALT ∧ ∼a ∈ Exhaustification.IE ALT φ)

def Exhaustification.exhIE {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : Prop' World

Definition 4: Exhaustivity operator based on innocent exclusion (exh_ie)

exh_ie(ALT, φ) = {u : ∀ψ(ψ ∈ IE_(ALT,φ) → ψ(u) = 1)}

Equivalently: exh_ie(ALT, φ) = ⋀ IE_(ALT,φ)

Equivalently: exh_ie(ALT, φ) = φ ∧ ⋀{¬a : a is a member of ALT that is innocently excludable given ALT and φ}

Equations

• Exhaustification.exhIE ALT φ u = ∀ ψ ∈ Exhaustification.IE ALT φ, ψ u

def Exhaustification.closedUnderConj {World : Type u_1} (ALT : Set (Prop' World)) : Prop

A set ALT is closed under conjunction if for any subset X of ALT, ⋀X ∈ ALT.

(Definition 5 in Spector)

Equations

• Exhaustification.closedUnderConj ALT = ∀ X ⊆ ALT, ⋀ X ∈ ALT

def Exhaustification.closedUnderDisj {World : Type u_1} (ALT : Set (Prop' World)) : Prop

A set ALT is closed under disjunction if for any subset X of ALT, ⋁X ∈ ALT.

Equations

• Exhaustification.closedUnderDisj ALT = ∀ X ⊆ ALT, ⋁ X ∈ ALT

theorem Exhaustification.ltALT_wf_of_finite {World : Type u_1} (ALT : Set (Prop' World)) (hfin : ALT.Finite) : WellFounded (ltALT ALT)

Well-foundedness for finite ALT: The strict ordering <_ALT is well-founded when ALT is finite.

Proof idea: For any infinite descending chain w₁ >_ALT w₂ >_ALT..., the set of true alternatives strictly increases at each step. Since ALT is finite, this cannot continue indefinitely.

theorem Exhaustification.exists_minimal_of_finite {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hfin : ALT.Finite) (hsat : ∃ (w : World), φ w) : ∃ (u : World), isMinimal ALT φ u

Existence of minimal worlds for finite ALT: When ALT is finite and φ is satisfiable, there exists a minimal φ-world.

def Exhaustification.X_of_world {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) : Set (Prop' World)

Definition from Section 5.3: X(u) = {φ} ∪ {¬a : a ∈ ALT ∧ a(u) = 0}

For any world u, X(u) is the set containing φ and the negations of all alternatives that are false at u.

"XALT,φ(u) = {φ} ∪ {¬a: a ∈ ALT ∧ a(u) = 0}"

Equations

• Exhaustification.X_of_world ALT φ u = {φ} ∪ {ψ : Prop' World | ∃ a ∈ ALT, ψ = ∼a ∧ ¬a u}

theorem Exhaustification.pneg_injective {World : Type u_1} {a a' : Prop' World} (h : ∼a = ∼a') : a = a'

Helper lemma: If ∼a = ∼a' then a = a' (negation is injective on propositions).

theorem Exhaustification.ltALT_iff_X_ssubset {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u v : World) (hu : φ u) (hv : φ v) : (u <[ALT] v) ↔ X_of_world ALT φ v ⊂ X_of_world ALT φ u

Key equivalence (from proof of Lemma 1): For any two φ-worlds u and v: u <_ALT v ⟺ X(v) ⊊ X(u)

"The alternatives that u makes true are a proper subset of those v makes true" is equivalent to "X(v) is a proper subset of X(u)".

theorem Exhaustification.X_contains_phi {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) : φ ∈ X_of_world ALT φ u

X(u) contains φ.

theorem Exhaustification.X_elements {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) (ψ : Prop' World) (hψ : ψ ∈ X_of_world ALT φ u) : ψ = φ ∨ ∃ a ∈ ALT, ψ = ∼a

Every element of X(u) is either φ or the negation of some alternative.

theorem Exhaustification.u_satisfies_X {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) (hu : φ u) (ψ : Prop' World) : ψ ∈ X_of_world ALT φ u → ψ u

u satisfies everything in X(u).

theorem Exhaustification.X_is_compatible {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) (hu : φ u) : isCompatible ALT φ (X_of_world ALT φ u)

X(u) is (ALT, φ)-compatible when φ u holds.

theorem Exhaustification.lemma1_minimal_iff_MCset {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) (hu : φ u) : isMinimal ALT φ u ↔ isMCSet ALT φ (X_of_world ALT φ u)

Lemma 1 (Spector p.22): For any φ-world u: u is a minimal φ-world relative to <ALT ⟺ X(u) is an MC(ALT,φ)-set.

This is the key connection between the two definitions of exhaustivity.

Note: We add the explicit hypothesis (hu : φ u) since both directions require it.

theorem Exhaustification.exists_MCset_of_minimal {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hmin : ∃ (u : World), isMinimal ALT φ u) : ∃ (E : Set (Prop' World)), isMCSet ALT φ E

MC-set existence from minimal world existence (Spector's approach): When a minimal φ-world exists, an MC-set exists.

This follows directly from Lemma 1: if u is minimal, then X(u) is an MC-set.

theorem Exhaustification.exists_MCset {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hfin : ALT.Finite) (hsat : ∃ (w : World), φ w) : ∃ (E : Set (Prop' World)), isMCSet ALT φ E

MC-set existence for finite ALT: When ALT is finite and φ is satisfiable, an MC-set exists.

This combines:

1. exists_minimal_of_finite: finite ALT + satisfiable φ → minimal world exists
2. exists_MCset_of_minimal: minimal world exists → MC-set exists

theorem Exhaustification.IE_structure {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hfin : ALT.Finite) (ψ : Prop' World) (hψ : ψ ∈ IE ALT φ) (hsat : ∃ (w : World), φ w) : ψ = φ ∨ ∃ a ∈ ALT, ψ = ∼a

Every element of IE is either φ or ∼a for some a ∈ ALT. This follows from the structure of compatible sets.

Note: Requires finite ALT to ensure MC-sets exist.

theorem Exhaustification.lemma2_exhMW_iff_satisfies_MCset {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (u : World) : exhMW ALT φ u ↔ ∃ (E : Set (Prop' World)), isMCSet ALT φ E ∧ ∀ ψ ∈ E, ψ u

Lemma 2 (Spector p.23, Core Lemma): For every proposition φ, every set of alternatives ALT, and every world u, exh_mw(ALT, φ)(u) = 1 ⟺ there is an MC_(ALT,φ)-set X that u satisfies.

Equivalently: u is a minimal φ-world relative to <ALT ⟺ there is an MC(ALT,φ)-set X that u satisfies.

theorem Exhaustification.lemma3_exhMW_eq_disj_MCsets {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : exhMW ALT φ ≡ₚ fun (u : World) => ∃ (E : Set (Prop' World)), isMCSet ALT φ E ∧ ∀ ψ ∈ E, ψ u

Lemma 3 (reformulation of Lemma 2): exh_mw(ALT, φ) = ⋁{⋀X : X is an MC_(ALT,φ)-set}

The minimal-worlds exhaustification is the disjunction of the conjunctions of all MC-sets.

theorem Exhaustification.prop6_exhMW_entails_exhIE {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : exhMW ALT φ ⊆ₚ exhIE ALT φ

Proposition 6 (Spector p.12): For any proposition φ with alternatives ALT, exh_mw(ALT, φ) entails exh_ie(ALT, φ).

Proof idea: Any world satisfying exh_mw satisfies some MC-set, hence satisfies the intersection of all MC-sets, hence satisfies IE.

theorem Exhaustification.prop7_IE_iff_exhMW_entails_neg {World : Type u_1} (ALT : Set (Prop' World)) (φ a : Prop' World) (ha : a ∈ ALT) : isInnocentlyExcludable ALT φ a ↔ exhMW ALT φ ⊆ₚ ∼a

Proposition 7 (Spector p.12): For any ALT, any a ∈ ALT, and any proposition φ, a is innocently excludable given ALT and φ if and only if exh_mw(ALT, φ) entails ¬a.

This characterizes innocent exclusion in terms of the minimal-worlds operator.

theorem Exhaustification.corollary8 {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hfin : ALT.Finite) : exhIE ALT φ ≡ₚ fun (u : World) => φ u ∧ ∀ a ∈ ALT, (exhMW ALT φ ⊆ₚ ∼a) → ¬a u

Corollary 8 (Spector p.12): exh_ie(ALT, φ) = φ ∧ ⋀{¬a : a ∈ ALT ∧ exh_mw(ALT, φ) ⊆ ¬a}

This gives an alternative characterization of exh_ie in terms of exh_mw.

Note: The backward direction requires finite ALT for IE_structure.

theorem Exhaustification.theorem9_main {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hclosed : closedUnderConj ALT) : exhMW ALT φ ≡ₚ exhIE ALT φ

Theorem 9 (Main Result, Spector p.12-13): For any φ and any ALT, if ALT is closed under conjunction, then

exh_mw(ALT, φ) = exh_ie(ALT, φ)

Proof outline (from Section 5.4): Since exh_mw always entails exh_ie (Prop 6), we need to show exh_ie ⊆ exh_mw when ALT is closed under conjunction.

Suppose exh_mw(φ)(u) = 0 but φ(u) = 1. We must show exh_ie(φ)(u) = 0.

Let A = {a ∈ ALT : a(u) = 1}. Since u is not minimal, every MC-set contains a negation of some member of A. Consider ⋀A. Since every MC-set has a member whose negation is in A, ⋀A is false in every world satisfying an MC-set. Therefore ¬(⋀A) is consistent with every MC-set.

Since ALT is closed under conjunction, ⋀A ∈ ALT. Since ¬(⋀A) is consistent with every MC-set and MC-sets are maximal, ¬(⋀A) ∈ IE. But (⋀A)(u) = 1, so u fails to satisfy IE, hence exh_ie(φ)(u) = 0.

theorem Exhaustification.neg_bigDisj_iff {World : Type u_1} (X : Set (Prop' World)) (w : World) : (∼⋁ X) w ↔ ∀ a ∈ X, (∼a) w

De Morgan for big disjunction: ¬(⋁X) at w iff ∀ a ∈ X, ¬a at w

theorem Exhaustification.subset_disjClosure {World : Type u_1} (ALT ALT' : Set (Prop' World)) (h : ALT' = {p : Prop' World | ∃ X ⊆ ALT, p = ⋁ X}) : ALT ⊆ ALT'

The disjunction closure contains the original set (via singleton disjunctions).

theorem Exhaustification.mem_disjClosure_iff {World : Type u_1} (ALT ALT' : Set (Prop' World)) (h : ALT' = {p : Prop' World | ∃ X ⊆ ALT, p = ⋁ X}) (p : Prop' World) : p ∈ ALT' ↔ ∃ X ⊆ ALT, p = ⋁ X

Every element of the disjunction closure is a disjunction of ALT elements.

theorem Exhaustification.leALT_disjClosure_eq {World : Type u_1} (ALT ALT' : Set (Prop' World)) (h : ALT' = {p : Prop' World | ∃ X ⊆ ALT, p = ⋁ X}) (u v : World) : (u ≤[ALT] v) ↔ u ≤[ALT'] v

Key lemma: The preorder ≤_ALT is unchanged by disjunction closure.

If ALT' is the disjunction closure of ALT, then u ≤{ALT} v ↔ u ≤{ALT'} v.

Proof: If a disjunction (⋁X) is true at u where X ⊆ ALT, then some b ∈ X is true at u. If u ≤_{ALT} v, then b is true at v, so (⋁X) is true at v.

theorem Exhaustification.ltALT_disjClosure_eq {World : Type u_1} (ALT ALT' : Set (Prop' World)) (h : ALT' = {p : Prop' World | ∃ X ⊆ ALT, p = ⋁ X}) (u v : World) : (u <[ALT] v) ↔ u <[ALT'] v

Corollary: The strict ordering <_ALT is unchanged by disjunction closure.

theorem Exhaustification.exhMW_disjClosure_eq {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (ALT' : Set (Prop' World)) (h : ALT' = {p : Prop' World | ∃ X ⊆ ALT, p = ⋁ X}) : exhMW ALT φ ≡ₚ exhMW ALT' φ

Corollary: exh_mw is unchanged by disjunction closure.

theorem Exhaustification.theorem10_disj_closure_vacuous {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hfin : ALT.Finite) (ALT' : Set (Prop' World)) (h : ALT' = {p : Prop' World | ∃ X ⊆ ALT, p = ⋁ X}) : exhIE ALT φ ≡ₚ exhIE ALT' φ

Theorem 10 (Spector p.13): For any proposition φ and any alternative set ALT, exh_ie(ALT, φ) = exh_ie(ALT∨, φ)

where ALT∨ is the closure of ALT under disjunction.

"Closing the alternatives under disjunction (but crucially not conjunction) is vacuous for exh_ie."

Proof strategy: Use Corollary 8's characterization: exhIE ALT φ ≡ₚ λ u => φ u ∧ ∀ a ∈ ALT, (exhMW ALT φ ⊆ₚ ∼a) → ¬(a u)

Since exhMW is unchanged by disjunction closure, we just need to check that the extra conditions for ALT' (disjunctions) are implied by the ALT conditions.

theorem Exhaustification.corollary11 {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hfin : ALT.Finite) (hcond : closedUnderConj {p : Prop' World | ∃ Y ⊆ ALT, p = ⋁ Y}) : exhMW ALT φ ≡ₚ exhIE ALT φ

Corollary 11 (Spector p.13): For any proposition φ and any alternative set ALT, if ALT∨ = ALT∨∧, then exh_mw(ALT, φ) = exh_ie(ALT, φ).

"If the closure of ALT under disjunction is closed under conjunction, applying exh_mw and exh_ie give rise to equivalent results."

@[reducible, inline]

abbrev Exhaustification.SomeAllWorld : Type

Worlds for some/all example: number of students who passed (0 to 3).

Equations

• Exhaustification.SomeAllWorld = Fin 4

def Exhaustification.someStudents : Prop' SomeAllWorld

"Some students passed" (at least one).

Equations

• Exhaustification.someStudents w = (↑w ≥ 1)

def Exhaustification.allStudents : Prop' SomeAllWorld

"All students passed" (all three).

Equations

• Exhaustification.allStudents w = (↑w = 3)

def Exhaustification.someAllALT : Set (Prop' SomeAllWorld)

Alternative set: {some, all}.

Equations

• Exhaustification.someAllALT = {Exhaustification.someStudents, Exhaustification.allStudents}

def Exhaustification.w1 : SomeAllWorld

World where exactly 1 student passed.

Equations

• Exhaustification.w1 = ⟨1, Exhaustification.w1._proof_2⟩

def Exhaustification.w3 : SomeAllWorld

World where all 3 students passed.

Equations

• Exhaustification.w3 = ⟨3, Exhaustification.w3._proof_2⟩

theorem Exhaustification.w1_satisfies_some : someStudents w1

w=1 satisfies "some students passed".

theorem Exhaustification.w1_not_all : ¬allStudents w1

w=1 does not satisfy "all students passed".

theorem Exhaustification.w3_satisfies_both : someStudents w3 ∧ allStudents w3

w=3 satisfies both "some" and "all".

theorem Exhaustification.w1_leALT_w3 : w1 ≤[someAllALT] w3

w=1 ≤_ALT w=3: alternatives true at w=1 are a subset of those at w=3.

theorem Exhaustification.w3_not_leALT_w1 : ¬w3 ≤[someAllALT] w1

w=3 does not satisfy ≤_ALT w=1: w=3 satisfies "all" but w=1 does not.

theorem Exhaustification.w1_ltALT_w3 : w1 <[someAllALT] w3

w=1 <_ALT w=3: strict ordering holds.

theorem Exhaustification.w1_minimal_some : isMinimal someAllALT someStudents w1

w=1 is minimal among "some"-worlds relative to <_ALT.

theorem Exhaustification.w3_not_minimal_some : ¬isMinimal someAllALT someStudents w3

w=3 is not minimal because w=1 <_ALT w=3.

theorem Exhaustification.exhMW_some_at_w1 : exhMW someAllALT someStudents w1

Main result for some/all: exh_mw(some) holds at w=1.

This captures the scalar implicature: "some but not all".

theorem Exhaustification.exhMW_some_not_w3 : ¬exhMW someAllALT someStudents w3

Corollary: exh_mw(some) does not hold at w=3.

Worlds where "all" holds are excluded by exhaustification.

inductive Exhaustification.OrAndWorld : Type

Four worlds for or/and example.

• neither : OrAndWorld
• onlySang : OrAndWorld
• onlyDanced : OrAndWorld
• both : OrAndWorld

instance Exhaustification.instDecidableEqOrAndWorld : DecidableEq OrAndWorld

Equations

• Exhaustification.instDecidableEqOrAndWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Exhaustification.instReprOrAndWorld : Repr OrAndWorld

Equations

• Exhaustification.instReprOrAndWorld = { reprPrec := Exhaustification.instReprOrAndWorld.repr }

def Exhaustification.instReprOrAndWorld.repr : OrAndWorld → ℕ → Std.Format

Equations

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

def Exhaustification.sang : Prop' OrAndWorld

"John sang"

Equations

• Exhaustification.sang Exhaustification.OrAndWorld.neither = False
• Exhaustification.sang Exhaustification.OrAndWorld.onlySang = True
• Exhaustification.sang Exhaustification.OrAndWorld.onlyDanced = False
• Exhaustification.sang Exhaustification.OrAndWorld.both = True

def Exhaustification.danced : Prop' OrAndWorld

"John danced"

Equations

• Exhaustification.danced Exhaustification.OrAndWorld.neither = False
• Exhaustification.danced Exhaustification.OrAndWorld.onlySang = False
• Exhaustification.danced Exhaustification.OrAndWorld.onlyDanced = True
• Exhaustification.danced Exhaustification.OrAndWorld.both = True

def Exhaustification.sangOrDanced : Prop' OrAndWorld

"John sang or danced" (inclusive)

Equations

• Exhaustification.sangOrDanced w = (Exhaustification.sang w ∨ Exhaustification.danced w)

def Exhaustification.sangAndDanced : Prop' OrAndWorld

"John sang and danced"

Equations

• Exhaustification.sangAndDanced w = (Exhaustification.sang w ∧ Exhaustification.danced w)

def Exhaustification.orAndALT : Set (Prop' OrAndWorld)

Alternative set: {or, and}.

Equations

• Exhaustification.orAndALT = {Exhaustification.sangOrDanced, Exhaustification.sangAndDanced}

def Exhaustification.wSang : OrAndWorld

The "only sang" world.

Equations

• Exhaustification.wSang = Exhaustification.OrAndWorld.onlySang

def Exhaustification.wBoth : OrAndWorld

The "both" world.

Equations

• Exhaustification.wBoth = Exhaustification.OrAndWorld.both

theorem Exhaustification.wSang_satisfies_or : sangOrDanced wSang

wSang satisfies "or".

theorem Exhaustification.wSang_not_and : ¬sangAndDanced wSang

wSang does not satisfy "and".

theorem Exhaustification.wBoth_satisfies_both : sangOrDanced wBoth ∧ sangAndDanced wBoth

wBoth satisfies both "or" and "and".

theorem Exhaustification.wSang_leALT_wBoth : wSang ≤[orAndALT] wBoth

wSang ≤_ALT wBoth.

theorem Exhaustification.wBoth_not_leALT_wSang : ¬wBoth ≤[orAndALT] wSang

wBoth does not satisfy ≤_ALT wSang.

theorem Exhaustification.wSang_ltALT_wBoth : wSang <[orAndALT] wBoth

wSang <_ALT wBoth.

theorem Exhaustification.wSang_minimal : isMinimal orAndALT sangOrDanced wSang

wSang is minimal among or-worlds.

theorem Exhaustification.exhMW_or_at_wSang : exhMW orAndALT sangOrDanced wSang

Main result for or/and: exh_mw(or) at wSang (exclusive reading).

theorem Exhaustification.exhMW_or_not_wBoth : ¬exhMW orAndALT sangOrDanced wBoth

Corollary: exh_mw(or) excludes the "both" world.

This is the exclusive disjunction reading.

theorem Exhaustification.allStudents_entails_someStudents : allStudents ⊆ₚ someStudents

For the some/all scale, the stronger alternative (all) entails the weaker (some).

theorem Exhaustification.someAll_exhMW_iff_exhIE : exhMW someAllALT someStudents ≡ₚ exhIE someAllALT someStudents

For the some/all scale: exhMW ≡ exhIE.

We prove this using Proposition 6 (⊆) and a direct argument for (⊇). The key insight: at any exhIE world, the stronger alternative is false, which means the world is minimal (no world below it satisfies more alternatives).

theorem Exhaustification.sangAndDanced_entails_sangOrDanced : sangAndDanced ⊆ₚ sangOrDanced

For the or/and scale, the stronger alternative (and) entails the weaker (or).

theorem Exhaustification.orAnd_exhMW_iff_exhIE : exhMW orAndALT sangOrDanced ≡ₚ exhIE orAndALT sangOrDanced

For the or/and scale: exhMW ≡ exhIE.

theorem Exhaustification.exhIE_some_at_w1 : exhIE someAllALT someStudents w1

Theorem 9 application: At w1, both exhMW and exhIE agree.

theorem Exhaustification.exhIE_some_not_w3 : ¬exhIE someAllALT someStudents w3

Theorem 9 application: At w3, both exhMW and exhIE agree (both false).

theorem Exhaustification.exhIE_or_at_wSang : exhIE orAndALT sangOrDanced wSang

Theorem 9 application: At wSang, both exhMW and exhIE agree.

theorem Exhaustification.exhIE_or_not_wBoth : ¬exhIE orAndALT sangOrDanced wBoth

Theorem 9 application: At wBoth, both exhMW and exhIE agree (both false).

Maximize Strength

@cite{chierchia-2013} "Logic in Grammar" proposes that scalar implicature computation follows the Maximize Strength principle:

"Don't add an implicature if it leads to weakening, unless you have to"

This explains the distribution of scalar implicatures across contexts:

Context	Polarity	Effect of SI	SI computed?
Upward Entailing	UE	Strengthens	✓ Yes
Downward Entailing	DE	Weakens	✗ No

Examples

UE context (positive sentence):

• "John saw some students" → "John saw some but not all students"
• SI strengthens: original entails exhaustified

DE context (antecedent of conditional):

• "If John saw some students, he's happy" → No SI
• SI would weaken: exhaustified entails original
• Adding "not all" to antecedent makes the conditional weaker

Connection to Exhaustification

Maximize Strength captures when exh is applied:

• In UE contexts: exh(φ) ⊆ₚ φ (strengthening) → apply exh
• In DE contexts: φ ⊆ₚ exh(φ) (weakening in overall sentence) → don't apply exh

Theoretical Significance

This principle unifies several phenomena:

1. Why SIs are optional in positive contexts (strengthening available)
2. Why SIs disappear in DE contexts (would weaken)
3. Why NPIs need DE contexts (exhaustification contradicts in UE)
4. Why FCIs have complex distribution (modal rescue)

def Exhaustification.Context (World : Type u_2) : Type u_2

A context is a function that embeds a proposition into a larger structure.

Equations

• Exhaustification.Context World = (Prop' World → Prop' World)

def Exhaustification.IsUpwardEntailing {World : Type u_1} (C : Context World) : Prop

A context is upward entailing (monotone) if φ ⊆ ψ implies C(φ) ⊆ C(ψ).

Equations

• Exhaustification.IsUpwardEntailing C = ∀ (φ ψ : Prop' World), (φ ⊆ₚ ψ) → C φ ⊆ₚ C ψ

def Exhaustification.IsDownwardEntailing {World : Type u_1} (C : Context World) : Prop

A context is downward entailing (antitone) if φ ⊆ ψ implies C(ψ) ⊆ C(φ).

Equations

• Exhaustification.IsDownwardEntailing C = ∀ (φ ψ : Prop' World), (φ ⊆ₚ ψ) → C ψ ⊆ₚ C φ

theorem Exhaustification.exh_in_ue_strengthens {World : Type u_1} (C : Context World) (hUE : IsUpwardEntailing C) (φ exhφ : Prop' World) (hExhStronger : exhφ ⊆ₚ φ) : C exhφ ⊆ₚ C φ

In a UE context, exhaustification strengthens the embedded proposition. That is: C(exh(φ)) ⊆ C(φ) when C is UE and exh(φ) ⊆ φ.

theorem Exhaustification.exh_in_de_weakens {World : Type u_1} (C : Context World) (hDE : IsDownwardEntailing C) (φ exhφ : Prop' World) (hExhStronger : exhφ ⊆ₚ φ) : C φ ⊆ₚ C exhφ

In a DE context, exhaustification weakens the overall sentence. That is: C(φ) ⊆ C(exh(φ)) when C is DE and exh(φ) ⊆ φ.

theorem Exhaustification.id_context_is_UE {World : Type u_1} : IsUpwardEntailing id

The identity context is upward entailing.

theorem Exhaustification.neg_context_is_DE {World : Type u_1} : IsDownwardEntailing pneg

Negation context is downward entailing.

def Exhaustification.maximizeStrength {World : Type u_1} (φ exhφ : Prop' World) (polarity : Core.NaturalLogic.ContextPolarity) : Prop' World

Maximize Strength: compute SI iff context is UE (strengthening).

This is the core principle: only apply exhaustification when it results in strengthening of the overall assertion.

Equations

• Exhaustification.maximizeStrength φ exhφ Core.NaturalLogic.ContextPolarity.upward = exhφ
• Exhaustification.maximizeStrength φ exhφ Core.NaturalLogic.ContextPolarity.downward = φ
• Exhaustification.maximizeStrength φ exhφ Core.NaturalLogic.ContextPolarity.nonMonotonic = φ

def Exhaustification.maximizeStrengthCtx {World : Type u_1} (C : Context World) (φ exhφ : Prop' World) (hUE : Bool) : Prop' World

Maximize Strength with explicit context.

Equations

• Exhaustification.maximizeStrengthCtx C φ exhφ hUE = if hUE = true then C exhφ else C φ

theorem Exhaustification.exhMW_strengthens {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : exhMW ALT φ ⊆ₚ φ

exh_mw strengthens the proposition by conjoining negations of excludable alternatives.

theorem Exhaustification.exhMW_strengthens_in_UE {World : Type u_1} (C : Context World) (hUE : IsUpwardEntailing C) (ALT : Set (Prop' World)) (φ : Prop' World) : C (exhMW ALT φ) ⊆ₚ C φ

In a UE context, exh_mw results in a stronger overall sentence.

theorem Exhaustification.exhMW_weakens_in_DE {World : Type u_1} (C : Context World) (hDE : IsDownwardEntailing C) (ALT : Set (Prop' World)) (φ : Prop' World) : C φ ⊆ₚ C (exhMW ALT φ)

In a DE context, applying exh_mw weakens the overall sentence. Hence, Maximize Strength predicts no scalar implicature in DE contexts.

Example: "Some students passed" in UE context

Positive sentence: C = id (identity context)

• φ = "some students passed"
• exh(φ) = "some but not all students passed"
• C(exh(φ)) ⊆ C(φ) ✓ Strengthens
• Prediction: SI computed → "not all"

Example: "If some students passed,..." (antecedent)

Conditional antecedent: C = (λp. p → q) is DE

• φ = "some students passed"
• exh(φ) = "some but not all students passed"
• C(φ) ⊆ C(exh(φ)) - SI would weaken the conditional
• Prediction: no SI in antecedent

This matches empirical observations:

• "If some students passed, the teacher is happy" does not implicate "If some but not all students passed..."

structure Exhaustification.MaximizeStrengthExample : Type

Maximize Strength predictions summary:

Context Type	SI Effect	Prediction	Example
Matrix clause (UE)	Strengthens	Compute SI	"some → not all"
Negation scope (DE)	Weakens	No SI	"not some → some or none"
Conditional antecedent (DE)	Weakens	No SI	"if some, then..."
Universal restrictor (DE)	Weakens	No SI	"every... who saw some..."
Question nucleus (NM)	Neither	No SI	"Did some...?"

• description : String
• contextType : Core.NaturalLogic.ContextPolarity
• siComputed : Bool
• explanation : String

instance Exhaustification.instReprMaximizeStrengthExample : Repr MaximizeStrengthExample

Equations

• Exhaustification.instReprMaximizeStrengthExample = { reprPrec := Exhaustification.instReprMaximizeStrengthExample.repr }

def Exhaustification.instReprMaximizeStrengthExample.repr : MaximizeStrengthExample → ℕ → Std.Format

Equations

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

def Exhaustification.ms_matrix_clause : MaximizeStrengthExample

Equations

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

def Exhaustification.ms_negation : MaximizeStrengthExample

Equations

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

def Exhaustification.ms_antecedent : MaximizeStrengthExample

Equations

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

def Exhaustification.ms_universal_restrictor : MaximizeStrengthExample

Equations

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

def Exhaustification.maximizeStrengthExamples : List MaximizeStrengthExample

Equations

• Exhaustification.maximizeStrengthExamples = [Exhaustification.ms_matrix_clause, Exhaustification.ms_negation, Exhaustification.ms_antecedent, Exhaustification.ms_universal_restrictor]

exh_mx: The Third Exhaustification Operator

@cite{wang-2025} "Presupposition, Competition, and Coherence" introduces exh_mx, which yields one exhaustified proposition per maximal consistent subset (MC-set), rather than intersecting all MC-sets (as exh_ie does).

When all MC-sets agree (i.e., ALT is closed under ∧), exh_mx = exh_ie = exh_mw (by Theorem 9). When MC-sets diverge, exh_mx produces multiple readings—one per MC-set—capturing ambiguity in presuppositional alternatives.

Key relationships:

• exh_mw = ⋁{⋀E : E is MC-set} (Lemma 3 above)
• exh_ie = ⋀(⋂ all MC-sets) (Definition 4 above)
• exh_mx = one reading per MC-set: for each E, ⋀E

def Exhaustification.exhMXReading {World : Type u_2} (E : Set (Prop' World)) : Prop' World

An exh_mx reading for a specific MC-set E: the conjunction of E.

Unlike exh_ie (which is the conjunction of the intersection of all MC-sets), exh_mx gives one reading per MC-set. When MC-sets disagree about which alternatives to exclude, exh_mx captures the resulting ambiguity.

@cite{wang-2025} Ch4: "exh_mx(ALT, φ, w) = φ(w) ∧ ∀q ∈ Max(φ, ALT)[¬q(w)]" where Max is a specific maximal consistent subset.

Equations

• Exhaustification.exhMXReading E u = ∀ ψ ∈ E, ψ u

def Exhaustification.exhMXReadings {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) : Set (Prop' World)

The set of all exh_mx readings: one per MC-set.

This is the set of propositions, not a single proposition. Each reading corresponds to a different way of consistently excluding alternatives.

Equations

• Exhaustification.exhMXReadings ALT φ = {p : Prop' World | ∃ (E : Set (Prop' World)), Exhaustification.isMCSet ALT φ E ∧ p = Exhaustification.exhMXReading E}

theorem Exhaustification.bigConj_exhMX_entails_exhIE {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) (hne : ∃ (E : Set (Prop' World)), isMCSet ALT φ E) : (fun (u : World) => ∀ p ∈ exhMXReadings ALT φ, p u) ⊆ₚ exhIE ALT φ

The conjunction of all exh_mx readings entails exh_ie.

Together with exhMXReading_entails_exhIE (each reading entails exh_ie), this gives the full picture of how exh_ie relates to exh_mx readings:

⋀(readings) ⊆ₚ each reading ⊆ₚ exh_ie

Note: the REVERSE direction (exhIE ⊆ₚ ⋀ readings) does NOT hold in general. When MC-sets diverge, an MC-set E may contain alternatives ψ ∉ IE. Satisfying all of IE (exhIE) does not guarantee satisfying all of E (a specific reading), because E may require excluding alternatives that other MC-sets include.

theorem Exhaustification.exhMXReading_entails_exhIE {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) (E : Set (Prop' World)) (hmc : isMCSet ALT φ E) : exhMXReading E ⊆ₚ exhIE ALT φ

Every exh_mx reading entails exh_ie.

Since exh_ie is the intersection of all MC-sets and each exh_mx reading is a single MC-set, each reading is at least as strong as exh_ie.

theorem Exhaustification.exhMW_eq_bigDisj_exhMX {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) : exhMW ALT φ ≡ₚ fun (u : World) => ∃ p ∈ exhMXReadings ALT φ, p u

exh_mw is the disjunction of all exh_mx readings (Lemma 3 restated).

This connects all three operators:

• exh_mw = ⋁(exh_mx readings) (disjunction — some MC-set is satisfied)
• exh_ie = ⋀(exh_mx readings) (conjunction — all MC-sets are satisfied)
• When there is exactly one MC-set: exh_mw = exh_ie = exh_mx

theorem Exhaustification.exhOperators_coincide_under_closure {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) (hclosed : closedUnderConj ALT) : exhIE ALT φ ≡ₚ fun (u : World) => ∃ p ∈ exhMXReadings ALT φ, p u

Under conjunction closure, all three exhaustification operators coincide: exh_ie = exh_mw = ⋁(exh_mx readings).

This does NOT mean there is only one reading. When MC-sets diverge, individual readings remain distinct — but their disjunction equals exh_ie.

Combines Theorem 9 (exhMW ≡ₚ exhIE) with Lemma 3 (exhMW ≡ₚ ⋁ readings).

theorem Exhaustification.exhMX_unique_when_unique_MCset {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) {p q : Prop' World} (hp : p ∈ exhMXReadings ALT φ) (hq : q ∈ exhMXReadings ALT φ) (huniq : ∀ (E₁ E₂ : Set (Prop' World)), isMCSet ALT φ E₁ → isMCSet ALT φ E₂ → E₁ = E₂) : p ≡ₚ q

When there is a unique MC-set, all exh_mx readings are equivalent.

MC-set uniqueness is a stronger condition than conjunction closure alone. It holds when ALT has additional structural properties (e.g., symmetric closure under both conjunction and disjunction, per @cite{spector-2016}).

FLAT: Collapsing Nested Alternative Sets

@cite{wang-2025} Ch4 defines the FLAT operator for collapsing nested alternative sets (sets of sets of propositions) into a flat set via cross-product conjunction.

Given S = {A₁, A₂,...} where each Aᵢ is a set of propositions, FLAT(S) = {⋀{f(Aᵢ) | i} | f is a choice function picking one from each Aᵢ}

This is proved equivalent to @cite{groenendijk-stokhof-1984} pointwise answerhood (Ans_PW).

def Exhaustification.flat {World : Type u_2} (S : Set (Set (Prop' World))) : Set (Prop' World)

FLAT: Collapse a family of alternative sets into a flat set via cross-product conjunction. Each element of FLAT(S) is the conjunction of one choice from each alternative set in S.

@cite{wang-2025} Ch4: FLAT({A₁,...,Aₙ}) = {a₁ ∧... ∧ aₙ | aᵢ ∈ Aᵢ}

Uses a total choice function restricted to S to avoid dependent types.

Equations

• Exhaustification.flat S = {p : Prop' World | ∃ (f : Set (Prop' World) → Prop' World), (∀ A ∈ S, f A ∈ A) ∧ p = fun (u : World) => ∀ A ∈ S, f A u}

theorem Exhaustification.flat_singleton {World : Type u_2} (A : Set (Prop' World)) : flat {A} = A

FLAT of a singleton is the set itself.

theorem Exhaustification.flat_empty {World : Type u_2} : flat ∅ = {fun (x : World) => True}

FLAT of the empty family is the tautology set.

Innocent Inclusion

From @cite{bar-lev-fox-2020}, Definition (51):

II(p, C) = ∩{C'' ⊆ C : C'' is maximal s.t. {r : r ∈ C''} ∪ {p} ∪ {¬q : q ∈ IE(p,C)} is consistent}

After computing IE, find all maximal subsets of alternatives that can consistently be assigned TRUE (given that IE alternatives are false). An alternative is innocently includable iff it appears in ALL such maximal sets.

def Exhaustification.isIICompatible {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) (R : Set (Prop' World)) : Prop

Definition (II-compatible set): A set of propositions R is (ALT, φ, IE)-compatible for inclusion if: a) R ⊆ ALT b) {r : r ∈ R} ∪ {φ} ∪ {¬q : q ∈ IE(ALT, φ)} is consistent

Equations

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

def Exhaustification.isMISet {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) (R : Set (Prop' World)) : Prop

Definition (MI-set): Maximal II-compatible set. A set R is maximally (ALT, φ, IE)-compatible if it is II-compatible and not properly included in any other II-compatible set.

Equations

• Exhaustification.isMISet ALT φ R = (Exhaustification.isIICompatible ALT φ R ∧ ∀ (R' : Set (Prop' World)), Exhaustification.isIICompatible ALT φ R' → R ⊆ R' → R' ⊆ R)

def Exhaustification.II {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) : Set (Prop' World)

Definition (II): II(ALT, φ) = {r ∈ ALT : r belongs to every MI-set}

An alternative r is innocently includable iff it belongs to every MI-set.

Equations

• Exhaustification.II ALT φ = {r : Prop' World | r ∈ ALT ∧ ∀ (R : Set (Prop' World)), Exhaustification.isMISet ALT φ R → r ∈ R}

def Exhaustification.isInnocentlyIncludable {World : Type u_2} (ALT : Set (Prop' World)) (φ a : Prop' World) : Prop

An alternative a is innocently includable given ALT and φ if and only if a ∈ II(ALT, φ).

Equations

• Exhaustification.isInnocentlyIncludable ALT φ a = (a ∈ Exhaustification.II ALT φ)

def Exhaustification.exhIEII {World : Type u_2} (ALT : Set (Prop' World)) (φ : Prop' World) : Prop' World

Definition (Exh^{IE+II}): The exhaustivity operator with both IE and II.

⟦Exh^{IE+II}⟧(ALT)(φ)(w) ⇔ φ(w) ∧ ∀q ∈ IE(ALT,φ)[¬q(w)] ∧ -- exclude IE alternatives ∀r ∈ II(ALT,φ)[r(w)] -- include II alternatives

This is Bar-Lev & Fox's key operator that derives free choice.

Equations

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

Decidable Innocent Exclusion

The exhIE above is a specification: it quantifies over all Set (Prop' World), so it cannot be evaluated computationally. The functions below implement the same algorithm over [Fintype World] types using Bool-valued meanings and explicit subset enumeration. This makes them usable by native_decide and rsa_predict.

def Exhaustification.isSatBool {W : Type} (worlds : List W) (f : W → Bool) : Bool

Satisfiability check over an explicit list of worlds.

Equations

• Exhaustification.isSatBool worlds f = worlds.any f

def Exhaustification.entailsBool {W : Type} (worlds : List W) (f g : W → Bool) : Bool

Pointwise entailment over an explicit list of worlds.

Equations

• Exhaustification.entailsBool worlds f g = worlds.all fun (w : W) => !f w || g w

def Exhaustification.sublists : List ℕ → List (List ℕ)

All sublists (subsets) of a list of indices.

Equations

• Exhaustification.sublists [] = [[]]
• Exhaustification.sublists (a :: as) = List.map (fun (x : List ℕ) => a :: x) (Exhaustification.sublists as) ++ Exhaustification.sublists as

def Exhaustification.ieIndicesBool {W : Type} (worlds : List W) (prejacent : W → Bool) (alts : List (W → Bool)) : List ℕ

Innocent Exclusion over Bool-valued meanings: find indices of alternatives that appear in every maximal consistent exclusion set. worlds must enumerate all inhabitants of W.

Equations

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

def Exhaustification.applyIEBool {W : Type} (worlds : List W) (prejacent : W → Bool) (alts : List (W → Bool)) : W → Bool

Apply Innocent Exclusion: conjoin prejacent with negations of IE alternatives. worlds must enumerate all inhabitants of W.

Equations

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