Lücking and Ginzburg (2022): Referential Transparency as the Proper Treatment for Quantification

This file formalizes the denotations of quantified noun phrases in the referential transparency theory of [LG22]. In place of the sets of sets of generalized quantifier theory ([BC81]), a quantified noun phrase denotes a set of ordered bipartitions of the head noun's extension into a reference set and its complement set, the quantifier word acting as a sieve on them through a descriptive condition on the two cardinalities (sieve). Such a condition is a quantifier on [vB84]'s tree of numbers (Quantifier.NumberTree), and the sieve reads only the row of the tree at the size of the noun (sieve_eq_iff), which yields the paper's count of 2 ^ (k + 1) - 1 denotations over a noun with k instances (card_Ioc_antidiagonal). A verb phrase predicates on the reference set and anti-predicates on the complement set (AntiPredication), so the sentence is true exactly when the condition holds of the sizes of N \ VP and N ∩ VP (exists_antiPredication_iff). So referential transparency has the truth conditions of the tree quantifier of its condition (exists_antiPredication_iff_toGQ), which recovers the paper's claim that the set-up entails the conservativity universal (livesOn_toGQ), and the surviving reference sets are exactly the witness sets of [BC81] (mem_sieve_iff_witness). The quantifier perspective, whether the bipartition with an empty reference set survives the sieve, gates anaphora to the complement set (the paper's (47), CompsetAccessible, compsetAccessible_sieve). The paper's minimal pair (43a) ~ (44): few and a few share their condition, but a few carries a reference individual, so its denotation lacks the empty-reference bipartition and the complement set is inaccessible whatever the condition (compsetAccessible_few, not_compsetAccessible_refind).

Implementation notes

An ordered bipartition of S (the paper's (15)) is determined by its reference set R ⊆ S, the complement set being S \ R, so a denotation is a Finset (Finset α) of reference sets and the bipartitions of S are its powerset. A condition on the cardinalities of the complement and reference sets is a NumberTree, whose coordinates are |A \ B| and |A ∩ B|, in the order of the paper's (18), so the paper's every, no and some are the tree's all, no and some. Few takes the proportional sense of (38a), its much smaller weakened to a strict comparison; the cardinal sense of (38b), few against a contextual standard, is not represented. The contextual standard of many is a parameter. Anti-predication, the negation of a plural type on the complement set, is read distributively as the paper's gloss of (55b) does. The quantifier perspective is derived from the denotation as the proposition that the empty reference set is in it, where the paper carries it as a lexical feature; its third value for degenerate denotations collapses into inaccessibility, which gates anaphora identically. The count of §4.8 is read off the paper's enumeration for two individuals, the non-empty selections of cardinality types; the paper's own gloss of the subtraction speaks of the empty set. Negation of a noun phrase, which the paper's (49) shows to flip accessibility, the dialogue and gesture data, the clarification-request diagnostics, and the type-theoretic encoding are not represented.

TODO

Read as the cardinal condition |refset| < 100, fewer than 100 in the paper's (43d) keeps the empty reference set, so the derived perspective makes the complement set accessible where the paper marks the anaphora bad; the paper's lexical feature can stipulate its way past the case.

The paper's count of 63 quantifiers on a two-element domain (§4.8) multiplies the per-noun count over the subsets of the domain rather than over their sizes, so it distinguishes the two singletons, against its own restriction to quantitative quantifiers in the same section.

References

• [LG22]
• [BC81]
• [vB84]
• [KS86]

The sieve

def LuckingGinzburg2022.sieve {α : Type u_1} [DecidableEq α] (q : Quantifier.NumberTree) [DecidableRel q] (S : Finset α) : Finset (Finset α)

The ordered bipartitions of the head noun's extension S (the paper's (15)) sifted by the condition q on the sizes of the complement set and the reference set: the reference sets R ⊆ S with q |S \ R| |R|.

Equations

• LuckingGinzburg2022.sieve q S = {R ∈ S.powerset | q (S \ R).card R.card}

@[simp]

theorem LuckingGinzburg2022.mem_sieve {α : Type u_1} [DecidableEq α] {q : Quantifier.NumberTree} [DecidableRel q] {S R : Finset α} : R ∈ sieve q S ↔ R ⊆ S ∧ q (S \ R).card R.card

theorem LuckingGinzburg2022.sieve_congr {α : Type u_1} [DecidableEq α] {q : Quantifier.NumberTree} [DecidableRel q] {S : Finset α} {q' : Quantifier.NumberTree} [DecidableRel q'] (h : ∀ (a b : ℕ), a + b = S.card → (q a b ↔ q' a b)) : sieve q S = sieve q' S

The sieve reads only the row of the tree at the size of the noun.

Descriptive quantifier conditions

def LuckingGinzburg2022.many (θ : ℕ) : Quantifier.NumberTree

The condition of many (the paper's (39)), a reference set exceeding a contextual standard θ; a cardinal quantifier.

Equations

• LuckingGinzburg2022.many θ = Quantifier.NumberTree.cardinal (Set.Ioi θ)

@[instance_reducible]

instance LuckingGinzburg2022.instDecidableRelNatMany (θ : ℕ) : DecidableRel (many θ)

Equations

• LuckingGinzburg2022.instDecidableRelNatMany θ x✝ b = { decide := θ.succ.ble b, reflects_decide := ⋯ }

Quantifier perspective and complement-set anaphora

def LuckingGinzburg2022.CompsetAccessible {α : Type u_1} (D : Finset (Finset α)) : Prop

The complement set of a denotation is available to anaphora (the paper's (47)) when the bipartition with an empty reference set is in the denotation, the value refset = ∅ of the quantifier perspective (48).

Equations

• LuckingGinzburg2022.CompsetAccessible D = (∅ ∈ D)

@[instance_reducible]

instance LuckingGinzburg2022.instDecidableCompsetAccessible {α : Type u_1} [DecidableEq α] (D : Finset (Finset α)) : Decidable (CompsetAccessible D)

Equations

• LuckingGinzburg2022.instDecidableCompsetAccessible D = LuckingGinzburg2022.instDecidableCompsetAccessible._aux_1 D

theorem LuckingGinzburg2022.compsetAccessible_sieve {α : Type u_1} [DecidableEq α] {q : Quantifier.NumberTree} [DecidableRel q] {S : Finset α} : CompsetAccessible (sieve q S) ↔ q S.card 0

The empty reference set survives the sieve exactly when the condition holds at the point (|S|, 0) of the tree.

theorem LuckingGinzburg2022.not_compsetAccessible_all {α : Type u_1} [DecidableEq α] {S : Finset α} (hS : S.Nonempty) : ¬CompsetAccessible (sieve Quantifier.NumberTree.all S)

Every N makes the complement set inaccessible, the noun being nonempty, as in the paper's (49a), All music lovers admire Reger. #They love Mozart.

theorem LuckingGinzburg2022.compsetAccessible_no {α : Type u_1} [DecidableEq α] {S : Finset α} : CompsetAccessible (sieve Quantifier.NumberTree.no S)

No N makes the complement set accessible, the empty reference set being its denotation (§4.3).

theorem LuckingGinzburg2022.not_compsetAccessible_many {α : Type u_1} [DecidableEq α] {S : Finset α} (θ : ℕ) : ¬CompsetAccessible (sieve (many θ) S)

Many N makes the complement set inaccessible, as in the paper's (43b), Many music lovers admire Reger. #They prefer Mozart.

theorem LuckingGinzburg2022.compsetAccessible_few {α : Type u_1} [DecidableEq α] {S : Finset α} (hS : S.Nonempty) : CompsetAccessible (sieve Quantifier.NumberTree.few S)

Few N makes the complement set accessible, the noun being nonempty, as in the paper's (43a), Few music lovers admire Reger. They prefer Mozart.

def LuckingGinzburg2022.refind {α : Type u_1} [DecidableEq α] (D : Finset (Finset α)) : Finset (Finset α)

The reference individual of a few (the paper's (46)) requires a nonempty reference set, which removes the empty-reference bipartition from a denotation.

Equations

• LuckingGinzburg2022.refind D = D.erase ∅

theorem LuckingGinzburg2022.not_compsetAccessible_refind {α : Type u_1} [DecidableEq α] (D : Finset (Finset α)) : ¬CompsetAccessible (refind D)

A denotation carrying a reference individual never makes its complement set accessible, whatever the condition: a few shares the condition of few and blocks the anaphora, the paper's (44), A few music lovers admire Reger. #They prefer Mozart.

Predication and anti-predication

def LuckingGinzburg2022.AntiPredication {α : Type u_1} [DecidableEq α] (B : α → Prop) (S R : Finset α) : Prop

Two-headed predication (§4.5): the verb phrase holds throughout the reference set and fails throughout the complement set.

Equations

• LuckingGinzburg2022.AntiPredication B S R = ((∀ a ∈ R, B a) ∧ ∀ a ∈ S \ R, ¬B a)

theorem LuckingGinzburg2022.antiPredication_iff {α : Type u_1} [DecidableEq α] {S R : Finset α} {B : α → Prop} [DecidablePred B] (hR : R ⊆ S) : AntiPredication B S R ↔ R = Finset.filter B S

A reference set within S is anti-predicated exactly when it is the part of S where the verb phrase holds.

theorem LuckingGinzburg2022.exists_antiPredication_iff {α : Type u_1} [DecidableEq α] {q : Quantifier.NumberTree} [DecidableRel q] {S : Finset α} {B : α → Prop} [DecidablePred B] : (∃ R ∈ sieve q S, AntiPredication B S R) ↔ q (S \ Finset.filter B S).card (Finset.filter B S).card

The truth conditions of q N VP (§4.5): some surviving bipartition is anti-predicated exactly when the condition holds of the sizes of N \ VP and N ∩ VP.

theorem LuckingGinzburg2022.exists_antiPredication_iff_toGQ {α : Type u_1} [DecidableEq α] {q : Quantifier.NumberTree} [DecidableRel q] {S : Finset α} {B : α → Prop} [DecidablePred B] : (∃ R ∈ sieve q S, AntiPredication B S R) ↔ q.toGQ (fun (x : α) => x ∈ S) B

Referential transparency has the truth conditions of the tree quantifier of its condition, a conservative, permutation-invariant generalized quantifier on the head noun.

theorem LuckingGinzburg2022.livesOn_toGQ {α : Type u_1} {q : Quantifier.NumberTree} {S : Finset α} : Quantifier.NP.LivesOn (q.toGQ fun (x : α) => x ∈ S) fun (x : α) => x ∈ S

Conservativity holds by construction: the quantifier lives on the head noun.

Witness sets

theorem LuckingGinzburg2022.mem_sieve_iff_witness {α : Type u_1} [DecidableEq α] {q : Quantifier.NumberTree} [DecidableRel q] {S R : Finset α} : R ∈ sieve q S ↔ Quantifier.NP.Witness (q.toGQ fun (x : α) => x ∈ S) (fun (x : α) => x ∈ S) fun (x : α) => x ∈ R

The witness of a quantified noun phrase is a surviving reference set (the paper's (17)), and these are exactly the witness sets of [BC81] of the tree quantifier on the head noun.

Complexity

def LuckingGinzburg2022.row (q : Quantifier.NumberTree) [DecidableRel q] (k : ℕ) : Finset (ℕ × ℕ)

The points of row k of the tree a condition selects, the denotation on a noun with k instances up to the choice of reference sets.

Equations

• LuckingGinzburg2022.row q k = {p ∈ Finset.antidiagonal k | q p.1 p.2}

theorem LuckingGinzburg2022.sieve_eq_iff {α : Type u_1} [DecidableEq α] {q : Quantifier.NumberTree} [DecidableRel q] {S : Finset α} {q' : Quantifier.NumberTree} [DecidableRel q'] : sieve q S = sieve q' S ↔ row q S.card = row q' S.card

Two conditions sieve a noun alike exactly when they select the same points of its row.

theorem LuckingGinzburg2022.card_Ioc_antidiagonal (k : ℕ) : (Finset.Ioc ∅ (Finset.antidiagonal k)).card = 2 ^ (k + 1) - 1

A condition selects one of 2 ^ (k + 1) sets of points of row k, so the paper's 2 ^ (k + 1) - 1 combinatorially possible denotations over a noun with k instances (§4.8) are the nonempty ones.

def LuckingGinzburg2022.domainCount {α : Type u_1} (M : Finset α) : ℕ

The paper's count of quantifiers on a domain M (§4.8): a nonempty selection of a row for each subset of the domain, taken as a head noun's extension.

Equations

• LuckingGinzburg2022.domainCount M = ∏ R ∈ M.powerset, (2 ^ (R.card + 1) - 1)