Fox (2018): Partition by Exhaustification

This file formalizes [Fox18]'s reconstruction of [Day96]'s maximality presupposition as a matching condition between a question's Hamblin set and the partition it induces. Each member is exhaustified pointwise into a cell of the contextual partition; Cell Identification demands that every cell be so reached and Non-Vacuity that every member reach a cell, and qpm_iff_partitionsBy shows that together they say that pointwise exhaustification partitions the context set. With exhaustification as the strongest true member, Cell Identification is Dayal's presupposition (cellIdentification_exhCell_iff) and Non-Vacuity fails whenever the set contains the disjunction of two incomparable members, the negative island of higher-order questions (not_nonVacuity_exhCell_of_union), unless a necessity modal intervenes (nonVacuity_box). With exhaustification as [BLF20]'s cell operator, a question closed under conjunction and its disjunctive counterpart identify the same cells by different members (cell_biInter, cell_biUnion), and the answer set of the paper's revised answer operator is a singleton for the former but not for the latter: mention-all against mention-some.

Implementation notes

Questions are Hamblin sets Set (Set W) rather than Question lower sets, since the paper's sets are not antichains. The three-location model is a family of atoms a : ι → Set W with every set of atoms true at some world (Rich); the closures of the atoms under conjunction and under disjunction, infClosure (range a) and supClosure (range a), are the paper's two denotations; their innocently excludable sets are characterized and the cells read off. Sections 5–7 on the distribution of mention-some enter only through the rows on singular wh-phrases.

References

• [Fox18]
• [Day96]
• [Spe08]
• [BLF20]
• [FH06b]
• [Hei94b]

Question Partition Matching

def Fox2018.contextualPartition {W : Type u_1} (H : Set (Set W)) (A : Set W) : Set (Set W)

The contextual partition restricts the strong answers to the context set.

Equations

• Fox2018.contextualPartition H A = {C : Set W | ∃ w ∈ A, C = Question.strongAnswer H w ∩ A}

def Fox2018.CellIdentification {W : Type u_1} (Exh : Set W → Set W) (H : Set (Set W)) (A : Set W) : Prop

Cell Identification holds when every cell of the contextual partition is the exhaustification of some member.

Equations

• Fox2018.CellIdentification Exh H A = ∀ C ∈ Fox2018.contextualPartition H A, ∃ p ∈ H, Exh p ∩ A = C

def Fox2018.NonVacuity {W : Type u_1} (Exh : Set W → Set W) (H : Set (Set W)) (A : Set W) : Prop

Non-Vacuity holds when every member exhaustifies to a cell of the contextual partition.

Equations

• Fox2018.NonVacuity Exh H A = ∀ p ∈ H, ∃ C ∈ Fox2018.contextualPartition H A, Exh p ∩ A = C

def Fox2018.QPM {W : Type u_1} (Exh : Set W → Set W) (H : Set (Set W)) (A : Set W) : Prop

Question Partition Matching.

Equations

• Fox2018.QPM Exh H A = (Fox2018.CellIdentification Exh H A ∧ Fox2018.NonVacuity Exh H A)

def Fox2018.PartitionsBy {W : Type u_1} (Exh : Set W → Set W) (H : Set (Set W)) (A : Set W) : Prop

The pointwise exhaustifications partition the context set.

Equations

• Fox2018.PartitionsBy Exh H A = ((∀ p ∈ H, (Exh p ∩ A).Nonempty) ∧ (∀ p ∈ H, ∀ q ∈ H, Exh p ∩ A = Exh q ∩ A ∨ Disjoint (Exh p ∩ A) (Exh q ∩ A)) ∧ ∀ w ∈ A, ∃ p ∈ H, w ∈ Exh p)

def Fox2018.IsCellValued {W : Type u_1} (Exh : Set W → Set W) (H : Set (Set W)) : Prop

An exhaustifier identifies cells when each of its non-empty values is a strong answer.

Equations

• Fox2018.IsCellValued Exh H = ∀ p ∈ H, ∀ w ∈ Exh p, Exh p = Question.strongAnswer H w

theorem Fox2018.mem_contextualPartition {W : Type u_1} {H : Set (Set W)} {A C : Set W} : C ∈ contextualPartition H A ↔ ∃ w ∈ A, C = Question.strongAnswer H w ∩ A

theorem Fox2018.qpm_iff_partitionsBy {W : Type u_1} {Exh : Set W → Set W} {H : Set (Set W)} {A : Set W} (h : IsCellValued Exh H) : QPM Exh H A ↔ PartitionsBy Exh H A

For a cell-identifying exhaustifier, matching is partitioning.

Dayal's presupposition

theorem Fox2018.isCellValued_exhCell {W : Type u_1} {H : Set (Set W)} : IsCellValued (Question.exhCell H) H

theorem Fox2018.cellIdentification_exhCell_iff {W : Type u_1} {H : Set (Set W)} {A : Set W} : CellIdentification (Question.exhCell H) H A ↔ ∀ w ∈ A, Question.IsExhaustivelyResolvable H w

With exhaustification as the strongest true member, Cell Identification is Dayal's presupposition on the context set.

theorem Fox2018.nonVacuity_exhCell_iff {W : Type u_1} {H : Set (Set W)} {A : Set W} : NonVacuity (Question.exhCell H) H A ↔ ∀ p ∈ H, ∃ w ∈ A, Question.IsStrongestTrueAnswer H w p

Non-Vacuity holds for exhCell iff every member is the strongest true member at some context world.

theorem Fox2018.isExhaustivelyResolvable_range_iff_existsUnique {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (ha : ∀ (i j : ι), a i ⊆ a j → i = j) (w : W) : Question.IsExhaustivelyResolvable (Set.range a) w ↔ ∃! i : ι, w ∈ a i

For a singular which-question over pairwise incomparable atoms, Dayal's presupposition is that exactly one atom is true.

theorem Fox2018.isExhaustivelyResolvable_infClosure_range {W : Type u_1} {ι : Type u_2} [Fintype ι] {a : ι → Set W} {w : W} (hw : ∃ (i : ι), w ∈ a i) : Question.IsExhaustivelyResolvable (infClosure (Set.range a)) w

A plural which-question, closed under conjunction, is resolvable wherever some member is true.

Negative islands

theorem Fox2018.not_isStrongestTrueAnswer_union {W : Type u_1} {H : Set (Set W)} {q₁ q₂ : Set W} (h₁ : q₁ ∈ H) (h₂ : q₂ ∈ H) (h₁₂ : ¬q₁ ⊆ q₂) (h₂₁ : ¬q₂ ⊆ q₁) (w : W) : ¬Question.IsStrongestTrueAnswer H w (q₁ ∪ q₂)

The disjunction of two incomparable members is never the strongest true member.

theorem Fox2018.not_nonVacuity_exhCell_of_union {W : Type u_1} {H : Set (Set W)} {A q₁ q₂ : Set W} (h₁ : q₁ ∈ H) (h₂ : q₂ ∈ H) (hu : q₁ ∪ q₂ ∈ H) (h₁₂ : ¬q₁ ⊆ q₂) (h₂₁ : ¬q₂ ⊆ q₁) : ¬NonVacuity (Question.exhCell H) H A

A higher-order question under negation contains the negated conjunction of two readings together with each negated reading, so Non-Vacuity fails, which is the negative island.

theorem Fox2018.isStrongestTrueAnswer_box {W : Type u_1} {H : Set (Set W)} {W' : Type u_2} {R : SetRel W' W} {p : Set W} (hp : p ∈ H) {x : W'} (hx : ∀ (v : W), (x, v) ∈ R ↔ v ∈ p) : Question.IsStrongestTrueAnswer (Question.box H R) x (R.core p)

Under a necessity modal, a member that is exactly the modal base of a context world is the strongest true member there, so the island is obviated.

theorem Fox2018.nonVacuity_box {W : Type u_1} {H : Set (Set W)} {W' : Type u_2} {R : SetRel W' W} {A : Set W'} (h : ∀ p ∈ H, ∃ x ∈ A, ∀ (v : W), (x, v) ∈ R ↔ v ∈ p) : NonVacuity (Question.exhCell (Question.box H R)) (Question.box H R) A

Non-Vacuity holds for the necessitated question whenever every member is exactly the modal base of some context world.

Exhaustivity as cell identification

theorem Fox2018.cell_eq_strongAnswer {W : Type u_1} {H : Set (Set W)} {p : Set W} (hp : p ∈ H) {w : W} (hw : w ∈ Exhaustification.cell H p) : Exhaustification.cell H p = Question.strongAnswer H w

Each non-empty value of the cell operator is a strong answer, so the operator identifies cells.

theorem Fox2018.isCellValued_cell {W : Type u_1} {H : Set (Set W)} : IsCellValued (Exhaustification.cell H) H

theorem Fox2018.qpm_cell_iff_partitionsBy {W : Type u_1} {H : Set (Set W)} {A : Set W} : QPM (Exhaustification.cell H) H A ↔ PartitionsBy (Exhaustification.cell H) H A

With the cell operator, matching is partitioning.

theorem Fox2018.cell_diamond {W : Type u_1} {w s n e : Set W} (h : Fox2007.IsDiamond w s n e) : Exhaustification.cell {w, s, n, e} w = (s ∩ n) \ e

On [Fox07]'s diamond the cell operator asserts both independent alternatives and denies the strongest, deriving free choice in one step.

theorem Fox2018.cell_eq_exhIter_two {W : Type u_1} {w s n e : Set W} (h : Fox2007.IsDiamond w s n e) (hne : ((s ∩ n) \ e).Nonempty) : Exhaustification.cell {w, s, n, e} w = Fox2007.exhIter {w, s, n, e} 2 w

The cell operator agrees with [Fox07]'s recursive exhaustification wherever free choice is consistent.

Mention-some and mention-all

def Fox2018.Rich {W : Type u_1} {ι : Type u_2} (a : ι → Set W) : Prop

Every set of atoms is the set true at some world.

Equations

• Fox2018.Rich a = ∀ (T : Finset ι), ∃ (w : W), Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w = ↑T

def Fox2018.atomCell {W : Type u_1} {ι : Type u_2} (a : ι → Set W) (T : Finset ι) : Set W

The worlds at which exactly the atoms of T are true form a cell of the logical partition of either closure.

Equations

• Fox2018.atomCell a T = {v : W | Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ v = ↑T}

theorem Fox2018.mem_atomCell {W : Type u_1} {ι : Type u_2} {a : ι → Set W} {T : Finset ι} {v : W} : v ∈ atomCell a T ↔ Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ v = ↑T

theorem Fox2018.strongAnswer_infClosure_range_eq {W : Type u_1} {ι : Type u_2} {a : ι → Set W} {T : Finset ι} {w : W} (hw : Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w = ↑T) : Question.strongAnswer (infClosure (Set.range a)) w = atomCell a T

Both closures induce the atom cells.

theorem Fox2018.strongAnswer_supClosure_range_eq {W : Type u_1} {ι : Type u_2} {a : ι → Set W} {T : Finset ι} {w : W} (hw : Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w = ↑T) : Question.strongAnswer (supClosure (Set.range a)) w = atomCell a T

theorem Fox2018.leALT_infClosure_range_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} {u v : W} : Exhaustification.leALT (infClosure (Set.range a)) u v ↔ Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ u ⊆ Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ v

Under either closure, a world lies below another iff its true atoms are among the other's.

theorem Fox2018.leALT_supClosure_range_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} {u v : W} : Exhaustification.leALT (supClosure (Set.range a)) u v ↔ Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ u ⊆ Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ v

theorem Fox2018.biInter_subset_biInter_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) {S T : Finset ι} : ⋂ i ∈ T, a i ⊆ ⋂ i ∈ S, a i ↔ S ⊆ T

theorem Fox2018.biUnion_subset_biUnion_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) {S T : Finset ι} : ⋃ i ∈ S, a i ⊆ ⋃ i ∈ T, a i ↔ S ⊆ T

theorem Fox2018.isInnocentlyExcludable_conj_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) [Fintype ι] {S T : Finset ι} (hS : S.Nonempty) : Exhaustification.IsInnocentlyExcludable (infClosure (Set.range a)) (⋂ i ∈ T, a i) (⋂ i ∈ S, a i) ↔ ¬S ⊆ T

Given the conjunction over a group, a member is innocently excludable iff its group is not included, as the paper computes for the low-type question.

theorem Fox2018.mem_exhMW_supClosure_range_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) {T : Finset ι} {u : W} : u ∈ Exhaustification.exhMW (supClosure (Set.range a)) (⋃ i ∈ T, a i) ↔ ∃ i ∈ T, Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ u = ↑{i}

The minimal worlds given the disjunction over a group are the sole witnesses of its members.

theorem Fox2018.isInnocentlyExcludable_disj_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) {S T : Finset ι} (hS : S.Nonempty) : Exhaustification.IsInnocentlyExcludable (supClosure (Set.range a)) (⋃ i ∈ T, a i) (⋃ i ∈ S, a i) ↔ Disjoint S T

Given the disjunction over a group, a member is innocently excludable iff its group is disjoint from it, as the paper computes for the high-type question.

theorem Fox2018.cell_biInter {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) [Fintype ι] (T : Finset ι) : Exhaustification.cell (infClosure (Set.range a)) (⋂ i ∈ T, a i) = atomCell a T

For the conjunctive question, the member for a group identifies the cell of those atoms.

theorem Fox2018.cell_biUnion {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) {T : Finset ι} (hT : T.Nonempty) : Exhaustification.cell (supClosure (Set.range a)) (⋃ i ∈ T, a i) = atomCell a T

For the disjunctive question, the member for a group identifies the same cell.

def Fox2018.ans {W : Type u_1} (Exh : Set W → Set W) (H : Set (Set W)) (w : W) : Set (Set W)

The revised answer operator returns the true members entailing the cell identifier.

Equations

• Fox2018.ans Exh H w = {q : Set W | q ∈ H ∧ w ∈ q ∧ ∀ p ∈ H, w ∈ Exh p → q ⊆ p}

theorem Fox2018.ans_infClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) [Fintype ι] {T : Finset ι} (hT : T.Nonempty) {w : W} (hw : Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w = ↑T) : ans (Exhaustification.cell (infClosure (Set.range a))) (infClosure (Set.range a)) w = {⋂ i ∈ T, a i}

The conjunctive question's answer set is the conjunction over the true atoms, the mention-all reading.

theorem Fox2018.ans_supClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) {T : Finset ι} (hT : T.Nonempty) {w : W} (hw : Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w = ↑T) : ans (Exhaustification.cell (supClosure (Set.range a))) (supClosure (Set.range a)) w = (fun (S : Finset ι) => ⋃ i ∈ S, a i) '' {S : Finset ι | S.Nonempty ∧ S ⊆ T}

The disjunctive question's answer set consists of the disjunctions over the non-empty sub-groups of the true atoms, the mention-some reading.

theorem Fox2018.not_subsingleton_ans_supClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (hrich : Rich a) {T : Finset ι} (hT : 1 < T.card) {w : W} (hw : Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w = ↑T) : ¬(ans (Exhaustification.cell (supClosure (Set.range a))) (supClosure (Set.range a)) w).Subsingleton

With two or more true atoms, the disjunctive question's answer set has more than one member, which is the mention-some reading.

The data

structure Fox2018.Row : Type

A question of the data records whether it is a degree question, whether negation and a modal intervene, whether the wh-phrase is singular, and whether the island reading is blocked.

• negation : Bool
• modal : Bool
• singular : Bool
• blocked : Bool

@[instance_reducible]

instance Fox2018.instDecidableEqRow : DecidableEq Row

Equations

• Fox2018.instDecidableEqRow = Fox2018.instDecidableEqRow.decEq

def Fox2018.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def Fox2018.yesNoTable : List (String × Bool)

Equations

• Fox2018.yesNoTable = [("yes", true), ("no", false)]

def Fox2018.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Fox2018.rows : List Row

Equations

• Fox2018.rows = List.filterMap Fox2018.Row.ofDatum Fox2018.Examples.all

theorem Fox2018.rows_predicted (r : Row) : r ∈ rows → (r.blocked = true ↔ r.negation = true ∧ r.modal = false ∨ r.singular = true)

The theory predicts the islands of the data, where a reading is blocked under negation without an intervening modal, or for a singular wh-phrase.