Križ and Spector (2021): Interpreting Plural Predication

Križ and Spector account for homogeneity and non-maximality as follows. A sentence with a plural definite is underspecified between a family of candidate interpretations: the definite is read as an existential quantifier over a convex set of pluralities generated by some parts of its denotation x together with x itself (Cand, the paper's (21)). The sentence is true when every candidate is true, false when every candidate is false, and undefined otherwise (TrueOnAll, FalseOnAll). The candidate interpretations are the library's readings of a plural predication (image_Cand_eq_readings), and on a distributive predicate the resulting value is Križ's trivalent plural (value_reading_distributive). Non-maximality comes from pragmatics: only the candidates strongly relevant to the current issue count (TrueOnRelevant), so that under an issue that lumps reading eight books with reading all of them, Mary read the books conveys that she read at least eight (trueOnRelevant_reading) and its negation that she read fewer than three (trueOnRelevant_not_reading).

The compositional half of the paper interprets predicates relative to a homogeneity parameter HParam assigning a candidate domain to every argument index and plurality, and treats all as universal quantification over the parameters that differ from the current one only at its indices (all, the paper's (71)). This removes homogeneity and non-maximality on the associated argument while leaving other arguments alone (all_pred, all_pred₂), makes the girls all didn't dance mean that no girl danced (all_not_pred), renders floating all vacuous under a quantifier that already neutralizes the parameter (all_all), collapses coordinated predicates to the strong reading (all_and), and does not reach a pronoun bound by its associate (all_binding). The set of candidate interpretations is the same whether negation scopes above or below the distributivity operator (interpretations_not_dist, the paper's footnote proof by disjunctive normal form).

The comparison with Križ's earlier account is the paper's own (§4): Križ's Addressing condition has strong relevance as its special case on bivalent propositions (addressesIssue_iff_stronglyRelevant), and on the exam issue of the paper's (36) Križ's account communicates that Mary passed while no candidate is strongly relevant on the present account (communicatedContent_solvedMath, not_felicitous_solvedMath). The appendix's candidates with superpluralities (CandUp) yield the upward-homogeneity falsity condition and coincide with Križ's generalised homogeneity (valueUp_eq_generalisedTruthValue).

Implementation notes

Pluralities are Finset Atom ordered by inclusion, so parts are nonempty subsets, the convex closure of (21) is a union of Finset.Icc intervals, and candidate domains are finite. A candidate interpretation is presented by its domain; reading D P is the existential quantifier over D applied to the predicate P on pluralities. Sentence frames take the domain as an argument (TrueOnAll x φ), which covers negation and non-monotonic embeddings such as the paper's (22). Strong relevance is the substrate's Homogeneity.isStronglyRelevantProp, constancy on the cells of the issue, the paper's gloss of (25). The reading-list example (26)–(28) is stated for any thresholds 0 < lo ≤ hi ≤ |books| in place of the paper's 3, 8, and 10.

TODO

• The paper's §2.2 critique of Malamud's decision-theoretic account and its §6 open problems (functional non-maximality, overt questions) are not formalized.
• The appendix's revision of all in terms of maximal individual witnesses, (117)–(119), is not formalized; CandUp covers only the candidate side of the appendix.

References

• [KS21b]
• [Kri16]
• [KC15]
• [Kri96]
• [Mal12]

Candidate denotations (§3.1)

@[reducible, inline]

abbrev KrizSpector2021.parts {Atom : Type u_1} [DecidableEq Atom] (x : Finset Atom) : Finset (Finset Atom)

The nonempty mereological parts of a plurality.

Equations

• KrizSpector2021.parts x = Finset.Ioc ⊥ x

theorem KrizSpector2021.mem_parts {Atom : Type u_1} [DecidableEq Atom] {x z : Finset Atom} : z ∈ parts x ↔ z.Nonempty ∧ z ⊆ x

def KrizSpector2021.conv {Atom : Type u_1} [DecidableEq Atom] (A : Finset (Finset Atom)) : Finset (Finset Atom)

The convex closure of a set of pluralities collects everything in between two of its members, the paper's (21).

Equations

• KrizSpector2021.conv A = A.biUnion fun (a : Finset Atom) => A.biUnion fun (b : Finset Atom) => Finset.Icc a b

theorem KrizSpector2021.mem_conv {Atom : Type u_1} [DecidableEq Atom] {A : Finset (Finset Atom)} {z : Finset Atom} : z ∈ conv A ↔ ∃ a ∈ A, ∃ b ∈ A, a ⊆ z ∧ z ⊆ b

theorem KrizSpector2021.mem_conv_insert {Atom : Type u_1} [DecidableEq Atom] {x : Finset Atom} {S : Finset (Finset Atom)} (hS : S ⊆ parts x) {z : Finset Atom} : z ∈ conv (insert x S) ↔ z ⊆ x ∧ ∃ s ∈ insert x S, s ⊆ z

def KrizSpector2021.Cand {Atom : Type u_1} [DecidableEq Atom] (x : Finset Atom) : Finset (Finset (Finset Atom))

The candidate denotations of x, the paper's (21), are the existential quantifiers over the convex closure of a set of parts of x together with x, presented by their domains.

Equations

• KrizSpector2021.Cand x = Finset.image (fun (S : Finset (Finset Atom)) => KrizSpector2021.conv (insert x S)) (KrizSpector2021.parts x).powerset

theorem KrizSpector2021.mem_Cand {Atom : Type u_1} [DecidableEq Atom] {x : Finset Atom} {D : Finset (Finset Atom)} : D ∈ Cand x ↔ ∃ S ⊆ parts x, conv (insert x S) = D

theorem KrizSpector2021.self_mem_of_mem_Cand {Atom : Type u_1} [DecidableEq Atom] {x : Finset Atom} {D : Finset (Finset Atom)} (hD : D ∈ Cand x) : x ∈ D

Every candidate is entailed by the universal one, since x lies in every domain.

theorem KrizSpector2021.mem_parts_of_mem_Cand {Atom : Type u_1} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) {D : Finset (Finset Atom)} (hD : D ∈ Cand x) {z : Finset Atom} (hz : z ∈ D) : z ∈ parts x

theorem KrizSpector2021.singleton_mem_Cand {Atom : Type u_1} [DecidableEq Atom] (x : Finset Atom) : {x} ∈ Cand x

The universal candidate, from the empty set of parts.

theorem KrizSpector2021.parts_mem_Cand {Atom : Type u_1} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) : parts x ∈ Cand x

The existential candidate, from all the parts.

def KrizSpector2021.twoCand {Atom : Type u_1} [DecidableEq Atom] (x : Finset Atom) : Finset (Finset (Finset Atom))

The two candidates of [Kri96], the universal and the existential reading (§2.1).

Equations

• KrizSpector2021.twoCand x = {{x}, KrizSpector2021.parts x}

theorem KrizSpector2021.twoCand_subset_Cand {Atom : Type u_1} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) : twoCand x ⊆ Cand x

Truth on all readings (§2.1, §3.1)

def KrizSpector2021.reading {Atom : Type u_1} {W : Type u_2} (D : Finset (Finset Atom)) (P : Finset Atom → W → Prop) (w : W) : Prop

The reading of the predicate P on pluralities under the candidate domain D holds when some member of D satisfies P.

Equations

• KrizSpector2021.reading D P w = ∃ z ∈ D, P z w

theorem KrizSpector2021.image_Cand_eq_readings {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) (P : Finset Atom → W → Prop) : (fun (D : Finset (Finset Atom)) => {w : W | reading D P w}) '' ↑(Cand x) = Homogeneity.readings (fun (z : Finset Atom) => {w : W | P z w}) x

The candidate interpretations, (21), are the library's readings of the plural predication, each candidate domain being the trace on the parts of x of an upper set containing x.

@[instance_reducible]

instance KrizSpector2021.instDecidableReading {Atom : Type u_1} {W : Type u_2} (D : Finset (Finset Atom)) (P : Finset Atom → W → Prop) [(z : Finset Atom) → (w : W) → Decidable (P z w)] (w : W) : Decidable (reading D P w)

Equations

• KrizSpector2021.instDecidableReading D P w = { decide := decide (∃ (a : Finset Atom) (_ : a ∈ D), (fun (z : Finset Atom) => P z w) a), reflects_decide := ⋯ }

def KrizSpector2021.TrueOnAll {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) (w : W) : Prop

A sentence frame φ sends the candidate domain chosen for the plural definite to the resulting candidate interpretation. The sentence is true when every candidate is.

Equations

• KrizSpector2021.TrueOnAll x φ w = ∀ D ∈ KrizSpector2021.Cand x, φ D w

def KrizSpector2021.FalseOnAll {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) (w : W) : Prop

The sentence is false when every candidate is.

Equations

• KrizSpector2021.FalseOnAll x φ w = ∀ D ∈ KrizSpector2021.Cand x, ¬φ D w

@[instance_reducible]

instance KrizSpector2021.instDecidableTrueOnAll {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) [(D : Finset (Finset Atom)) → (w : W) → Decidable (φ D w)] (w : W) : Decidable (TrueOnAll x φ w)

Equations

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

@[instance_reducible]

instance KrizSpector2021.instDecidableFalseOnAll {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) [(D : Finset (Finset Atom)) → (w : W) → Decidable (φ D w)] (w : W) : Decidable (FalseOnAll x φ w)

Equations

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

def KrizSpector2021.value {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) [(D : Finset (Finset Atom)) → (w : W) → Decidable (φ D w)] (w : W) : SignType

The trivalent value of the sentence is true, false, or undefined on its candidates.

Equations

• KrizSpector2021.value x φ w = if KrizSpector2021.TrueOnAll x φ w then 1 else if KrizSpector2021.FalseOnAll x φ w then -1 else 0

theorem KrizSpector2021.falseOnAll_iff_trueOnAll_not {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) (w : W) : FalseOnAll x φ w ↔ TrueOnAll x (fun (D : Finset (Finset Atom)) (w : W) => ¬φ D w) w

Negating the sentence negates its candidates — falsity on all readings of φ is truth on all readings of ¬ φ, the paper's (61)–(62).

theorem KrizSpector2021.trueOnAll_reading {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) (P : Finset Atom → W → Prop) (w : W) : TrueOnAll x (fun (x : Finset (Finset Atom)) => reading x P) w ↔ P x w

Plural predication is true on all readings iff the predicate holds of the whole plurality.

theorem KrizSpector2021.falseOnAll_reading {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) (P : Finset Atom → W → Prop) (w : W) : FalseOnAll x (fun (x : Finset (Finset Atom)) => reading x P) w ↔ ∀ z ∈ parts x, ¬P z w

Plural predication is false on all readings iff the predicate fails of every part.

theorem KrizSpector2021.value_reading_distributive {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) (Q : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (Q a w)] (w : W) : value x (fun (x : Finset (Finset Atom)) => reading x fun (z : Finset Atom) (w : W) => ∀ a ∈ z, Q a w) w = Homogeneity.barePlural Q x w

On a distributive predicate, the meta-language distributivity operator of the paper's (63a), the value on the candidates is [Kri16]'s trivalent plural, true when every atom satisfies the predicate and false when none does.

Non-monotonic contexts (§3.1)

The paper's (22): Mary read all of the books, Sue read half of them and Peter the other half. On the two candidates of [Kri96], Exactly two of the students read the books is false; the candidate generated by the half Peter read, the paper's (23), is true while the universal candidate is false, so on the enriched candidate set the sentence is neither true nor false.

inductive KrizSpector2021.Student : Type

• mary : Student
• sue : Student
• peter : Student

@[instance_reducible]

instance KrizSpector2021.instDecidableEqStudent : DecidableEq Student

Equations

• KrizSpector2021.instDecidableEqStudent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive KrizSpector2021.Book : Type

• a : Book
• b : Book
• c : Book
• d : Book

@[instance_reducible]

instance KrizSpector2021.instDecidableEqBook : DecidableEq Book

Equations

• KrizSpector2021.instDecidableEqBook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KrizSpector2021.books : Finset Book

The books.

Equations

• KrizSpector2021.books = {KrizSpector2021.Book.a, KrizSpector2021.Book.b, KrizSpector2021.Book.c, KrizSpector2021.Book.d}

def KrizSpector2021.read₀ : Student → Finset Book

The scenario records which books each student read.

Equations

• KrizSpector2021.read₀ KrizSpector2021.Student.mary = {KrizSpector2021.Book.a, KrizSpector2021.Book.b, KrizSpector2021.Book.c, KrizSpector2021.Book.d}
• KrizSpector2021.read₀ KrizSpector2021.Student.sue = {KrizSpector2021.Book.c, KrizSpector2021.Book.d}
• KrizSpector2021.read₀ KrizSpector2021.Student.peter = {KrizSpector2021.Book.a, KrizSpector2021.Book.b}

def KrizSpector2021.exactlyTwo (D : Finset (Finset Book)) (w : Student → Finset Book) : Prop

Exactly two of the students read the books under the candidate domain D, at a world w recording which books each student read.

Equations

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

@[instance_reducible]

instance KrizSpector2021.instDecidableExactlyTwo (D : Finset (Finset Book)) (w : Student → Finset Book) : Decidable (exactlyTwo D w)

Equations

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

theorem KrizSpector2021.exactlyTwo_twoCand (D : Finset (Finset Book)) : D ∈ twoCand books → ¬exactlyTwo D read₀

Both of Krifka's candidates are false in the scenario.

theorem KrizSpector2021.exactlyTwo_not_trueOnAll : ¬TrueOnAll books exactlyTwo read₀

The universal candidate is false, since only Mary read all the books.

theorem KrizSpector2021.exactlyTwo_not_falseOnAll : ¬FalseOnAll books exactlyTwo read₀

The candidate generated by Peter's half is true, since exactly two students read a plurality containing both of those books, the paper's (23).

theorem KrizSpector2021.value_exactlyTwo : value books exactlyTwo read₀ = 0

Strong relevance and non-maximality (§3.2)

def KrizSpector2021.TrueOnRelevant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : Setoid W) (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) (w : W) : Prop

The sentence is judged true when every strongly relevant candidate is true.

Equations

• KrizSpector2021.TrueOnRelevant q x φ w = ∀ D ∈ KrizSpector2021.Cand x, Homogeneity.isStronglyRelevantProp q (φ D) → φ D w

def KrizSpector2021.FalseOnRelevant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : Setoid W) (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) (w : W) : Prop

The sentence is judged false when every strongly relevant candidate is false.

Equations

• KrizSpector2021.FalseOnRelevant q x φ w = ∀ D ∈ KrizSpector2021.Cand x, Homogeneity.isStronglyRelevantProp q (φ D) → ¬φ D w

def KrizSpector2021.Felicitous {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : Setoid W) (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) : Prop

Felicity requires some strongly relevant candidate (the paper's fn. 17).

Equations

• KrizSpector2021.Felicitous q x φ = ∃ D ∈ KrizSpector2021.Cand x, Homogeneity.isStronglyRelevantProp q (φ D)

theorem KrizSpector2021.trueOnRelevant_and_falseOnRelevant_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : Setoid W) (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) (w : W) : TrueOnRelevant q x φ w ∧ FalseOnRelevant q x φ w ↔ ¬Felicitous q x φ

Without a strongly relevant candidate the sentence is judged both true and false.

theorem KrizSpector2021.trueOnRelevant_of_r {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : Setoid W) (x : Finset Atom) (φ : Finset (Finset Atom) → W → Prop) {w w' : W} (h : q w w') (hw' : TrueOnAll x φ w') : TrueOnRelevant q x φ w

Truth on all readings at an issue-equivalent world gives truth on the relevant ones.

theorem KrizSpector2021.reading_conv_insert {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (x : Finset Atom) {S : Finset (Finset Atom)} (hS : S ⊆ parts x) {P : Finset Atom → W → Prop} {w : W} (hP : ∀ (z z' : Finset Atom), z' ⊆ z → P z w → P z' w) : reading (conv (insert x S)) P w ↔ ∃ s ∈ insert x S, P s w

Under a monotone-decreasing predicate the reading generated by a set of parts is the disjunction over those parts.

The reading list (§3.2)

The paper's (26)–(28): reading hi or more of the books is as good as reading all of them and reading fewer than lo is as bad as reading none. A world records which books Mary read.

@[reducible, inline]

abbrev KrizSpector2021.readP {Book : Type u_3} : Finset Book → Finset Book → Prop

Mary read the plurality z at w when every book in z is among those she read.

Equations

• KrizSpector2021.readP z w = (z ⊆ w)

@[reducible, inline]

abbrev KrizSpector2021.issue {Book : Type u_3} (lo hi : ℕ) : Setoid (Finset Book)

The issue (26) asks whether Mary read at least lo of the books, and whether at least hi.

Equations

• KrizSpector2021.issue lo hi = Setoid.ker fun (w : Finset Book) => (decide (lo ≤ w.card), decide (hi ≤ w.card))

theorem KrizSpector2021.issue_r {Book : Type u_3} (lo hi : ℕ) (w v : Finset Book) : (issue lo hi) w v ↔ (lo ≤ w.card ↔ lo ≤ v.card) ∧ (hi ≤ w.card ↔ hi ≤ v.card)

theorem KrizSpector2021.powersetCard_subset_parts {Book : Type u_3} [Fintype Book] [DecidableEq Book] {n : ℕ} (hn : 0 < n) : Finset.powersetCard n Finset.univ ⊆ parts Finset.univ

theorem KrizSpector2021.reading_powersetCard {Book : Type u_3} [Fintype Book] [DecidableEq Book] {n : ℕ} (hn₀ : 0 < n) (hn : n ≤ Fintype.card Book) (w : Finset Book) : reading (conv (insert Finset.univ (Finset.powersetCard n Finset.univ))) readP w ↔ n ≤ w.card

The candidate generated by the n-element parts reads as Mary read n or more.

theorem KrizSpector2021.stronglyRelevant_powersetCard {Book : Type u_3} [Fintype Book] [DecidableEq Book] {lo hi n : ℕ} (hn₀ : 0 < n) (hn : n ≤ Fintype.card Book) (h : n = lo ∨ n = hi) : Homogeneity.isStronglyRelevantProp (issue lo hi) (reading (conv (insert Finset.univ (Finset.powersetCard n Finset.univ))) readP)

theorem KrizSpector2021.trueOnRelevant_reading {Book : Type u_3} [Fintype Book] [DecidableEq Book] {lo hi : ℕ} (h₀ : 0 < lo) (hlh : lo ≤ hi) (hhi : hi ≤ Fintype.card Book) (w : Finset Book) : TrueOnRelevant (issue lo hi) Finset.univ (fun (x : Finset (Finset Book)) => reading x readP) w ↔ hi ≤ w.card

Mary read the books, judged on its strongly relevant candidates, conveys that she read hi or more of them, the paper's (27).

theorem KrizSpector2021.trueOnRelevant_not_reading {Book : Type u_3} [Fintype Book] [DecidableEq Book] {lo hi : ℕ} (h₀ : 0 < lo) (hlh : lo ≤ hi) (hhi : hi ≤ Fintype.card Book) (w : Finset Book) : TrueOnRelevant (issue lo hi) Finset.univ (fun (D : Finset (Finset Book)) (w : Finset Book) => ¬reading D readP w) w ↔ w.card < lo

Mary didn't read the books conveys that she read fewer than lo of them, the paper's (28), since the negated candidates that are strongly relevant are the negations of the relevant ones and their conjunction is the bottom cell.

Comparison with Križ (2016) (§4)

theorem KrizSpector2021.addressesIssue_iff_stronglyRelevant {W : Type u_2} {S : W → SignType} (hbiv : Trivalent.IsBivalent S) (q : Setoid W) : Homogeneity.addressesIssue q S ↔ Homogeneity.isStronglyRelevantProp q fun (x : W) => x ∈ Trivalent.posExt S

Križ's Addressing condition, the paper's (34a), has strong relevance as its special case on bivalent propositions.

The paper's (36): to pass, Mary must solve all of the math problems, or some of them and a physics problem, and the issue is whether she passed. On Križ's account Mary solved the math problems addresses the issue and communicates that she passed; on the present account no candidate is strongly relevant, so the sentence cannot address this issue at all.

@[reducible, inline]

abbrev KrizSpector2021.ExamWorld (Math : Type u_4) : Type u_4

A world records the math problems Mary solved, and whether she solved a physics problem.

Equations

• KrizSpector2021.ExamWorld Math = (Finset Math × Bool)

def KrizSpector2021.Pass {Math : Type u_3} [Fintype Math] (w : ExamWorld Math) : Prop

Passing requires all of the math problems, or some of them and a physics problem.

Equations

• KrizSpector2021.Pass w = (w.1 = Finset.univ ∨ w.1.Nonempty ∧ w.2 = true)

@[instance_reducible]

instance KrizSpector2021.instDecidablePass {Math : Type u_3} [Fintype Math] [DecidableEq Math] (w : ExamWorld Math) : Decidable (Pass w)

Equations

• KrizSpector2021.instDecidablePass w = { decide := decide (w.1 = Finset.univ) || decide (w.1.Nonempty ∧ w.2 = true), reflects_decide := ⋯ }

@[reducible, inline]

abbrev KrizSpector2021.passFail {Math : Type u_3} [Fintype Math] [DecidableEq Math] : Setoid (ExamWorld Math)

The issue asks whether Mary passed.

Equations

• KrizSpector2021.passFail = Setoid.ker fun (w : KrizSpector2021.ExamWorld Math) => decide (KrizSpector2021.Pass w)

theorem KrizSpector2021.passFail_r {Math : Type u_3} [Fintype Math] [DecidableEq Math] (w v : ExamWorld Math) : passFail w v ↔ (Pass w ↔ Pass v)

def KrizSpector2021.solvedMath {Math : Type u_3} [Fintype Math] [DecidableEq Math] : ExamWorld Math → SignType

Mary solved the math problems as Križ's trivalent sentence.

Equations

• KrizSpector2021.solvedMath = Homogeneity.barePlural (fun (m : Math) (w : KrizSpector2021.ExamWorld Math) => m ∈ w.1) Finset.univ

theorem KrizSpector2021.solvedMath_eq_one_iff {Math : Type u_3} [Fintype Math] [DecidableEq Math] (w : ExamWorld Math) : solvedMath w = 1 ↔ w.1 = Finset.univ

theorem KrizSpector2021.solvedMath_eq_neg_one_iff {Math : Type u_3} [Fintype Math] [DecidableEq Math] [Nonempty Math] (w : ExamWorld Math) : solvedMath w = -1 ↔ w.1 = ∅

theorem KrizSpector2021.addressesIssue_solvedMath {Math : Type u_3} [Fintype Math] [DecidableEq Math] [Nonempty Math] : Homogeneity.addressesIssue passFail solvedMath

Križ's sentence addresses the pass/fail issue, since its true worlds pass and its false worlds fail.

theorem KrizSpector2021.communicatedContent_solvedMath {Math : Type u_3} [Fintype Math] [DecidableEq Math] [Nonempty Math] : Homogeneity.communicatedContent passFail solvedMath = {w : ExamWorld Math | Pass w}

On Križ's account the sentence communicates that Mary passed.

theorem KrizSpector2021.not_felicitous_solvedMath {Math : Type u_3} [Fintype Math] [DecidableEq Math] (h : 1 < Fintype.card Math) : ¬Felicitous passFail Finset.univ fun (x : Finset (Finset Math)) => reading x fun (z : Finset Math) (w : ExamWorld Math) => z ⊆ w.1

On the present account no candidate interpretation is strongly relevant to the pass/fail issue, since the universal candidate splits the passing worlds and any other candidate splits the failing ones.

Homogeneity parameters and all (§5.3)

@[reducible, inline]

abbrev KrizSpector2021.HParam (Atom : Type u_3) : Type u_3

A homogeneity parameter assigns a candidate domain to every argument index and plurality (§5.3.1).

Equations

• KrizSpector2021.HParam Atom = (ℕ → Finset Atom → Finset (Finset Atom))

def KrizSpector2021.HParam.EquivExcept {Atom : Type u_1} (I : Finset ℕ) (H H' : HParam Atom) : Prop

Two parameters agree except at the indices in I, the paper's (70).

Equations

• KrizSpector2021.HParam.EquivExcept I H H' = ∀ k ∉ I, ∀ (x : Finset Atom), H k x = H' k x

theorem KrizSpector2021.HParam.EquivExcept.refl {Atom : Type u_1} (I : Finset ℕ) (H : HParam Atom) : EquivExcept I H H

theorem KrizSpector2021.HParam.EquivExcept.trans {Atom : Type u_1} {I : Finset ℕ} {H H' H'' : HParam Atom} (h : EquivExcept I H H') (h' : EquivExcept I H' H'') : EquivExcept I H H''

def KrizSpector2021.HParam.univAt {Atom : Type u_1} (H : HParam Atom) (i : ℕ) : HParam Atom

The parameter that reads index i universally and agrees with H elsewhere.

Equations

• H.univAt i k x = if k = i then {x} else H k x

theorem KrizSpector2021.HParam.equivExcept_univAt {Atom : Type u_1} (H : HParam Atom) {I : Finset ℕ} {i : ℕ} (hi : i ∈ I) : EquivExcept I H (H.univAt i)

def KrizSpector2021.HParam.Admissible {Atom : Type u_1} [DecidableEq Atom] (H : HParam Atom) : Prop

A parameter is admissible when each of its values is a candidate for its plurality.

Equations

• H.Admissible = ∀ (i : ℕ) (x : Finset Atom), H i x ∈ KrizSpector2021.Cand x

theorem KrizSpector2021.HParam.Admissible.univAt {Atom : Type u_1} [DecidableEq Atom] {H : HParam Atom} (hH : H.Admissible) (i : ℕ) : (H.univAt i).Admissible

def KrizSpector2021.pred {Atom : Type u_1} {W : Type u_2} (H : HParam Atom) (i : ℕ) (P : Finset Atom → W → Prop) (x : Finset Atom) (w : W) : Prop

A one-place predicate with argument index i, the paper's (53a).

Equations

• KrizSpector2021.pred H i P x w = KrizSpector2021.reading (H i x) P w

def KrizSpector2021.pred₂ {Atom : Type u_1} {W : Type u_2} (H : HParam Atom) (i j : ℕ) (R : Finset Atom → Finset Atom → W → Prop) (a b : Finset Atom) (w : W) : Prop

A two-place predicate with argument indices i and j, the paper's (53b).

Equations

• KrizSpector2021.pred₂ H i j R a b w = ∃ z ∈ H i a, ∃ y ∈ H j b, R z y w

def KrizSpector2021.dist {Atom : Type u_1} {W : Type u_2} (H : HParam Atom) (i : ℕ) (Q : Atom → W → Prop) (x : Finset Atom) (w : W) : Prop

The distributivity operator with argument index i, the paper's (63b).

Equations

• KrizSpector2021.dist H i Q x w = KrizSpector2021.pred H i (fun (z : Finset Atom) (w : W) => ∀ a ∈ z, Q a w) x w

def KrizSpector2021.all {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (I : Finset ℕ) (φ : HParam Atom → Finset Atom → W → Prop) (H : HParam Atom) (x : Finset Atom) (w : W) : Prop

all with indices I, the paper's (71), is true relative to every admissible parameter that agrees with the current one outside I.

Equations

• KrizSpector2021.all I φ H x w = ∀ (H' : KrizSpector2021.HParam Atom), H'.Admissible → KrizSpector2021.HParam.EquivExcept I H H' → φ H' x w

def KrizSpector2021.interpretations {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (φ : HParam Atom → W → Prop) : Set (W → Prop)

The candidate interpretations of a sentence collect one proposition per admissible parameter.

Equations

• KrizSpector2021.interpretations φ = {p : W → Prop | ∃ (H : KrizSpector2021.HParam Atom), H.Admissible ∧ p = φ H}

theorem KrizSpector2021.all_and {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {H : HParam Atom} {I : Finset ℕ} (φ ψ : HParam Atom → Finset Atom → W → Prop) (x : Finset Atom) (w : W) : all I (fun (H' : HParam Atom) (x : Finset Atom) (w : W) => φ H' x w ∧ ψ H' x w) H x w ↔ all I φ H x w ∧ all I ψ H x w

all distributes over predicate coordination.

theorem KrizSpector2021.all_all {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {H : HParam Atom} {I : Finset ℕ} (hH : H.Admissible) (φ : HParam Atom → Finset Atom → W → Prop) (x : Finset Atom) (w : W) : all I (fun (H' : HParam Atom) => all I φ H') H x w ↔ all I φ H x w

all is idempotent, so floating all is vacuous under a quantifier that already neutralizes the parameter, the paper's (92) and (97).

theorem KrizSpector2021.all_pred {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {H : HParam Atom} {I : Finset ℕ} {i : ℕ} (hH : H.Admissible) (hi : i ∈ I) (P : Finset Atom → W → Prop) (x : Finset Atom) (w : W) : all I (fun (H' : HParam Atom) => pred H' i P) H x w ↔ P x w

all removes homogeneity and non-maximality on its argument, the sentence holding iff the predicate holds of the whole plurality, whatever the parameter, the paper's (73)–(74).

theorem KrizSpector2021.all_not_pred {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {H : HParam Atom} {I : Finset ℕ} {i : ℕ} (hH : H.Admissible) (hi : i ∈ I) {x : Finset Atom} (hx : x.Nonempty) (P : Finset Atom → W → Prop) (w : W) : all I (fun (H' : HParam Atom) (x : Finset Atom) (w : W) => ¬pred H' i P x w) H x w ↔ ∀ z ∈ parts x, ¬P z w

With all above negation, the paper's (78), the girls all didn't dance holds iff no part of the girls danced.

theorem KrizSpector2021.all_pred₂ {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {H : HParam Atom} {I : Finset ℕ} {i : ℕ} (hH : H.Admissible) (hi : i ∈ I) {j : ℕ} (hj : j ∉ I) (R : Finset Atom → Finset Atom → W → Prop) (a b : Finset Atom) (w : W) : all I (fun (H' : HParam Atom) (a : Finset Atom) (w : W) => pred₂ H' i j R a b w) H a w ↔ ∃ y ∈ H j b, R a y w

all is selective, the paper's (82), so with all on the subject of a two-place predicate the object still ranges over its candidate.

theorem KrizSpector2021.all_pred_and {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {H : HParam Atom} {I : Finset ℕ} {i : ℕ} (hH : H.Admissible) (hi : i ∈ I) {j : ℕ} (hj : j ∈ I) (P Q : Finset Atom → W → Prop) (x : Finset Atom) (w : W) : all I (fun (H' : HParam Atom) (x : Finset Atom) (w : W) => pred H' i P x w ∧ pred H' j Q x w) H x w ↔ P x w ∧ Q x w

With all over coordinated predicates, the paper's (104), the professors all smiled and left holds iff both predicates hold of the whole plurality.

theorem KrizSpector2021.all_binding {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {H : HParam Atom} {I : Finset ℕ} {i : ℕ} (hH : H.Admissible) (hi : i ∈ I) {k : ℕ} (hk : k ∉ I) (L : Finset Atom → W → Prop) (like met : Finset Atom → Finset Atom → W → Prop) (x : Finset Atom) (w : W) : all I (fun (H' : HParam Atom) (x : Finset Atom) (w : W) => ∃ (y : Finset Atom), L y w ∧ pred H' k (like y) x w ∧ pred H' i (met y) x w) H x w ↔ ∃ (y : Finset Atom), L y w ∧ pred H k (like y) x w ∧ met y x w

all does not reach a pronoun bound by its associate, the paper's (108), so the chemists all met a linguist they like reads the subject universally while the pronoun keeps its candidate.

theorem KrizSpector2021.exists_cand_not_dist {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) {D : Finset (Finset Atom)} (hD : D ∈ Cand x) (Q : Atom → W → Prop) : ∃ D' ∈ Cand x, ∀ (w : W), ¬reading D (fun (z : Finset Atom) (w : W) => ∀ a ∈ z, Q a w) w ↔ reading D' (fun (z : Finset Atom) (w : W) => ∀ a ∈ z, ¬Q a w) w

The negation of a distributive candidate is a distributive candidate for the negated predicate, with the domain generated by the transversals of the original parts, after the paper's footnote proof through disjunctive normal form.

theorem KrizSpector2021.interpretations_not_dist {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] {x : Finset Atom} (hx : x.Nonempty) (i : ℕ) (Q : Atom → W → Prop) : (interpretations fun (H : HParam Atom) (w : W) => ¬dist H i Q x w) = interpretations fun (H : HParam Atom) (w : W) => dist H i (fun (a : Atom) (w : W) => ¬Q a w) x w

Negation and distributivity commute in the set of candidate interpretations, the paper's (69), so scoping negation below or above dist yields the same propositions.

Upward homogeneity (§3.3, Appendix)

The appendix's candidates (113) are generated by parts of x together with pluralities containing x; the sentence is then false only when no plurality overlapping x satisfies the predicate, which is [Kri16]'s generalised homogeneity.

@[reducible, inline]

abbrev KrizSpector2021.sups {Atom : Type u_1} [DecidableEq Atom] [Fintype Atom] (x : Finset Atom) : Finset (Finset Atom)

The pluralities containing x.

Equations

• KrizSpector2021.sups x = Finset.Icc x ⊤

def KrizSpector2021.CandUp {Atom : Type u_1} [DecidableEq Atom] [Fintype Atom] (x : Finset Atom) : Finset (Finset (Finset Atom))

The candidate domains of the appendix, (113), are convex closures of some parts of x and some pluralities containing x, restricted to those containing x itself.

Equations

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

theorem KrizSpector2021.mem_CandUp {Atom : Type u_1} [DecidableEq Atom] [Fintype Atom] {x : Finset Atom} {D : Finset (Finset Atom)} : D ∈ CandUp x ↔ (∃ A ⊆ parts x, ∃ B ⊆ sups x, conv (A ∪ B) = D) ∧ x ∈ D

theorem KrizSpector2021.Cand_subset_CandUp {Atom : Type u_1} [DecidableEq Atom] [Fintype Atom] (x : Finset Atom) : Cand x ⊆ CandUp x

The paper's candidates are the appendix's with x as the only superplurality.

theorem KrizSpector2021.not_disjoint_of_mem_CandUp {Atom : Type u_1} [DecidableEq Atom] [Fintype Atom] {x : Finset Atom} (hx : x.Nonempty) {D : Finset (Finset Atom)} (hD : D ∈ CandUp x) {z : Finset Atom} (hz : z ∈ D) : ¬Disjoint x z

Every member of an appendix candidate overlaps x.

theorem KrizSpector2021.filter_not_disjoint_mem_CandUp {Atom : Type u_1} [DecidableEq Atom] [Fintype Atom] {x : Finset Atom} (hx : x.Nonempty) : {z : Finset Atom | ¬Disjoint x z} ∈ CandUp x

The weakest appendix candidate admits every plurality overlapping x.

theorem KrizSpector2021.trueOnAllUp_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] (x : Finset Atom) (P : Finset Atom → W → Prop) (w : W) : (∀ D ∈ CandUp x, reading D P w) ↔ P x w

Truth on all appendix readings is still truth of the whole plurality.

theorem KrizSpector2021.falseOnAllUp_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] {x : Finset Atom} (hx : x.Nonempty) (P : Finset Atom → W → Prop) (w : W) : (∀ D ∈ CandUp x, ¬reading D P w) ↔ ∀ (z : Finset Atom), ¬Disjoint x z → ¬P z w

Falsity on all appendix readings is the upward-homogeneity condition of the paper's (114b), that no plurality overlapping x satisfies the predicate.

def KrizSpector2021.valueUp {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] (x : Finset Atom) (P : Finset Atom → W → Prop) [(z : Finset Atom) → (w : W) → Decidable (P z w)] (w : W) : SignType

The trivalent value on the appendix's candidates.

Equations

• KrizSpector2021.valueUp x P w = if ∀ D ∈ KrizSpector2021.CandUp x, KrizSpector2021.reading D P w then 1 else if ∀ D ∈ KrizSpector2021.CandUp x, ¬KrizSpector2021.reading D P w then -1 else 0

theorem KrizSpector2021.valueUp_eq_generalisedTruthValue {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] {x : Finset Atom} (hx : x.Nonempty) (P : Finset Atom → W → Prop) [(z : Finset Atom) → (w : W) → Decidable (P z w)] (w : W) : valueUp x P w = Kriz2016.generalisedTruthValue (fun (x : Finset Atom) => P x w) Finset.univ x

The appendix's candidates give [Kri16]'s generalised homogeneity over all pluralities.