@cite{fox-2018}: Partition by Exhaustification @cite{fox-2018}

@cite{fox-2018} "Partition by Exhaustification" derives Dayal's EP from the exhaustification operator Exh. The key insight: a question partitions the logical space iff every world has exactly one exhaustified true answer.

The definitions below are Bool-valued analogues of the Prop-valued MC-set/IE machinery in Exhaustification.Operators, specialized to question cells for decidable computation via native_decide.

• cellMCSets mirrors isMCSet from Exhaustification
• cellIE mirrors IE from Exhaustification
• foxExh mirrors exhIE from Exhaustification
• foxAns implements @cite{fox-2018}'s answer operator (definition 35)
• foxPartition implements the partition condition from @cite{fox-2018}'s restated Ans operator (presupposition of (38))

def Theories.Semantics.Questions.Exhaustivity.sublists : List ℕ → List (List ℕ)

All sublists (power set) of a list, preserving order. Used to enumerate candidate MC-sets of cell indices.

Equations

• One or more equations did not get rendered due to their size.
• Theories.Semantics.Questions.Exhaustivity.sublists [] = [[]]

def Theories.Semantics.Questions.Exhaustivity.getCell {W : Type u_1} (cells : List (W → Bool)) (i : ℕ) : W → Bool

Safe cell accessor: returns the cell at index i, or (λ _ => false) for OOB.

Equations

• Theories.Semantics.Questions.Exhaustivity.getCell cells i = cells.getD i fun (x : W) => false

def Theories.Semantics.Questions.Exhaustivity.negConsistent {W : Type u_1} (cells : List (W → Bool)) (pIdx : ℕ) (excluded : List ℕ) (worlds : List W) : Bool

Negation consistency: can cells at excluded indices be simultaneously negated while cell pIdx stays true?

negConsistent cells pIdx excluded worlds = true iff ∃w ∈ worlds. cellspIdx ∧ ∀j ∈ excluded. ¬cellsj

This is the Bool analogue of SetConsistent in Exhaustification, specialized to the pattern φ ∧ ⋀{¬a : a ∈ excluded}.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.cellMCSets {W : Type u_1} (cells : List (W → Bool)) (pIdx : ℕ) (worlds : List W) : List (List ℕ)

MC-sets (maximal consistent sets) of cell indices for cell pIdx.

A subset S of alternative indices (excluding pIdx) is an MC-set iff:

1. Negating all cells in S is consistent with pIdx being true
2. No proper superset of S is also consistent

Bool analogue of isMCSet in Exhaustification.Operators.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.cellIE {W : Type u_1} (cells : List (W → Bool)) (pIdx : ℕ) (worlds : List W) : List ℕ

Innocently excludable alternatives for cell pIdx: the indices that appear in every MC-set (intersection of all MC-sets).

Bool analogue of IE in Exhaustification.Operators: IE_(ALT,φ) = {ψ : ψ belongs to every MC_(ALT,φ)-set}

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxExh {W : Type u_1} (cells : List (W → Bool)) (pIdx : ℕ) (worlds : List W) : W → Bool

Fox's exhaustified cell: Exh(Q)(p)(w) = cellspIdx ∧ ∀j ∈ IE. ¬cellsj.

The exhaustified meaning of answer p negates all innocently excludable alternatives. Bool analogue of exhIE in Exhaustification.Operators.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxNV {W : Type u_1} (cells : List (W → Bool)) (pIdx : ℕ) (worlds : List W) : Bool

Non-vacuity: Exh(Q)(p) is satisfiable (true at some world). @cite{fox-2018} requires non-vacuity for QPM.

Equations

• Theories.Semantics.Questions.Exhaustivity.foxNV cells pIdx worlds = worlds.any (Theories.Semantics.Questions.Exhaustivity.foxExh cells pIdx worlds)

def Theories.Semantics.Questions.Exhaustivity.exhTrueCount {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) (w : W) : ℕ

Count of Exh-true cells at world w: the number of cells whose exhaustified meaning holds at w. This is NOT Fox's |Ans| but a simpler diagnostic: how many exclusive readings are true at w. When = 0, no cell exclusively holds (overlap); when = 1, one cell dominates; when > 1, multiple exclusive readings coexist.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.pointwiseNV {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) (w : W) : Bool

Pointwise non-vacuity: every cell true at w has a satisfiable exhaustified version. This is a necessary condition for Fox's QPM but weaker — it checks NV for true cells at a single world, while Fox's QPM requires both CI and NV globally over the partition induced by Q.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxAns {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) (w : W) : ℕ

Fox's answer operator. At world w, finds the unique cell-identifier (the unique j where foxExh(cells, j, worlds)(w) = true) and returns the count of Q-members that are true at w AND whose denotation entails the cell-identifier proposition cells[j].

@cite{fox-2018}, definition 35: Ans(Q)(w) = {q∈Q : w∈q ∧ q ⊆ (ιp∈Q)[Exh(Q,p,w)=1]} The ι picks the unique proposition p whose exhaustification is true at w; the entailment check is q ⊆ p (q entails the proposition p, not Exh(p)).

Returns 0 if no unique cell-identifier exists (zero or multiple Exh-true cells at w). When foxAns > 1, Fox predicts mention-some (the cell-identifier is weaker than individual true answers). When = 1, mention-all (the cell-identifier is the strongest true answer).

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxPartition {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) : Bool

Schwarzschild's partition test: do the exhaustified cells {Exh(Q)(p) : p ∈ Q} partition the world set? Holds iff every world has exactly one Exh-true cell.

This is the partition condition that appears as the presupposition of @cite{fox-2018}'s restated Ans operator (38): Ans is defined only when pointwise exhaustification of Q is a partition of the context set.

Equations

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