Referential Transparency Theory

@cite{lucking-ginzburg-2022} @cite{barwise-cooper-1981} @cite{cooper-2023}

@cite{lucking-ginzburg-2022} propose Referential Transparency Theory (RTT), replacing GQT's set-of-sets denotations for quantified noun phrases (QNPs) with sets of ordered set bipartitions. A bipartition ⟨refset, compset⟩ partitions the head noun's extension into a reference set and complement set; the union is the maxset. Quantifier words act as "sieves" on bipartitions via a descriptive quantifier condition (q-cond), and a quantifier perspective (q-persp) gates anaphora accessibility.

Core contributions formalized

1. Ordered set bipartitions as QNP denotations (§2.3, (15))
2. Descriptive quantifier conditions as cardinality relations (§4.2)
3. Quantifier perspective derived from bipartition structure (§4.3, (47))
4. few/a few contrast: same q-cond, different q-persp via refind (§4.3, (46))
5. Anti-predication: VP predicates on refset, ¬VP on compset (§4.5)
6. Structural conservativity: by construction (§1.3)
7. Complexity reduction: 2^(k+1) − 1 vs GQT's 2^(T(k)) (§4.8)
8. Bridges: RTT refsets = Cooper witness sets; compset predictions match

Thread map

• Ordered set bipartitions: defined here (BP)
• Witness sets: Theories.Semantics.TypeTheoretic.Quantification — WitnessSet, IsExistW, AnaphoraRef, anaphoraAvailable
• GQT properties: Theories.Semantics.Quantification.Quantifier — GQ, Conservative
• Conservative count: Core.Quantification.conservativeQuantifierCount
• Dog example: reuses DogWorld from TTR Ch. 7

§1. Ordered set bipartitions

An ordered set bipartition of a set s is a pair ⟨refset, compset⟩ of disjoint subsets whose union is s. The ordering matters: ⟨A, B⟩ ≠ ⟨B, A⟩ in general. These replace GQT's subset-of-powerset denotations.

structure LuckingGinzburg2022.BP (α : Type) : Type

An ordered set bipartition: a pair of Finsets. §2.3, (15): ⟨refset, compset⟩ where refset ∩ compset = ∅ and refset ∪ compset = maxset (the head noun's extension). Disjointness and union are verified extrinsically to enable decide.

• refset : Finset α
• compset : Finset α

def LuckingGinzburg2022.instDecidableEqBP.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : BP α✝) : Decidable (x✝ = x✝¹)

Equations

• LuckingGinzburg2022.instDecidableEqBP.decEq { refset := a, compset := a_1 } { refset := b, compset := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance LuckingGinzburg2022.instDecidableEqBP {α✝ : Type} [DecidableEq α✝] : DecidableEq (BP α✝)

Equations

• LuckingGinzburg2022.instDecidableEqBP = LuckingGinzburg2022.instDecidableEqBP.decEq

def LuckingGinzburg2022.BP.maxset {α : Type} [DecidableEq α] (b : BP α) : Finset α

The maxset (union of refset and compset).

Equations

• b.maxset = b.refset ∪ b.compset

def LuckingGinzburg2022.allBP {α : Type} [DecidableEq α] (S : Finset α) : Finset (BP α)

All ordered set bipartitions of S: for each R ⊆ S, form ⟨R, S \ R⟩.

Equations

• LuckingGinzburg2022.allBP S = Finset.map { toFun := fun (R : Finset α) => { refset := R, compset := S \ R }, inj' := ⋯ } S.powerset

theorem LuckingGinzburg2022.allBP_card {α : Type} [DecidableEq α] (S : Finset α) : (allBP S).card = 2 ^ S.card

The number of bipartitions of S equals 2^|S|. Each element independently goes to refset or compset.

theorem LuckingGinzburg2022.allBP_maxset {α : Type} [DecidableEq α] (S : Finset α) (b : BP α) (h : b ∈ allBP S) : b.maxset = S

Every bipartition in allBP has maxset = S.

theorem LuckingGinzburg2022.allBP_refset_sub {α : Type} [DecidableEq α] (S : Finset α) (b : BP α) (h : b ∈ allBP S) : b.refset ⊆ S

Refset of every bipartition in allBP is a subset of S.

§2. Descriptive quantifier conditions

A q-cond is a relation on |refset| and |compset|. Since RTT q-conds depend only on cardinalities (@cite{lucking-ginzburg-2022} §4.2), this is ℕ → ℕ → Bool — quantity invariance by construction.

@[reducible, inline]

abbrev LuckingGinzburg2022.QCond : Type

A descriptive quantifier condition: a decidable relation on the cardinalities of refset and compset. §4.2: the quantifier word's semantic contribution.

Equations

• LuckingGinzburg2022.QCond = (ℕ → ℕ → Bool)

def LuckingGinzburg2022.every_qcond : QCond

q-cond for every: |compset| = 0 (equivalently, |refset| = |maxset|). §4.7, (58).

Equations

• LuckingGinzburg2022.every_qcond _r c = (c == 0)

def LuckingGinzburg2022.no_qcond : QCond

q-cond for no: |refset| = 0 (all elements in compset).

Equations

• LuckingGinzburg2022.no_qcond r _c = (r == 0)

def LuckingGinzburg2022.some_qcond : QCond

q-cond for some: |refset| ≥ 1 (at least one witness).

Equations

• LuckingGinzburg2022.some_qcond r _c = decide (r ≥ 1)

def LuckingGinzburg2022.most_qcond : QCond

q-cond for most: |refset| > |compset|. §4.2: proportional, refset is the majority.

Equations

• LuckingGinzburg2022.most_qcond r c = decide (r > c)

def LuckingGinzburg2022.few_qcond : QCond

q-cond for few: |refset| < |compset|. §4.3, (46): refset is the minority. The paper uses |refset| ≪ |compset| with a contextual threshold; we simplify to strict less-than.

Equations

• LuckingGinzburg2022.few_qcond r c = decide (r < c)

def LuckingGinzburg2022.many_qcond (θ : ℕ) : QCond

q-cond for many: |refset| > θ (absolute threshold). §4.2, (39): evaluated against contextual standard.

Equations

• LuckingGinzburg2022.many_qcond θ r _c = decide (r > θ)

def LuckingGinzburg2022.sieve {α : Type} (qc : QCond) (bps : Finset (BP α)) : Finset (BP α)

Sieve: filter bipartitions by a quantifier condition. §2.3: quantifiers act as sieves on bipartition sets.

Equations

• LuckingGinzburg2022.sieve qc bps = {b ∈ bps | qc b.refset.card b.compset.card = true}

§3. Quantifier perspective (q-persp)

The q-persp feature is derived from the bipartition denotation (§4.3, (47)). It tracks whether the bipartition with an empty refset — ⟨∅, maxset⟩ — is included in the quantifier's denotation. If so, the compset is accessible for anaphoric reference.

The key empirical prediction: few and a few share the same q-cond (|refset| < |compset|) but differ in q-persp because a few includes a refind — an individual member of refset (§4.3, (46)). The refind forces refset ≠ ∅, excluding ⟨∅, maxset⟩ and blocking compset anaphora.

inductive LuckingGinzburg2022.QPerspective : Type

Quantifier perspective, derived from bipartition denotation. §4.3, (47)–(48): gates anaphoric accessibility of compset.

• refsetEmpty : QPerspective

  The empty-refset bipartition ⟨∅, maxset⟩ IS in the denotation. Compset is available for anaphora.

• refsetNonempty : QPerspective

  The empty-refset bipartition is NOT in the denotation. Compset is not available.

@[implicit_reducible]

instance LuckingGinzburg2022.instDecidableEqQPerspective : DecidableEq QPerspective

Equations

• LuckingGinzburg2022.instDecidableEqQPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LuckingGinzburg2022.instReprQPerspective.repr : QPerspective → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LuckingGinzburg2022.instReprQPerspective : Repr QPerspective

Equations

• LuckingGinzburg2022.instReprQPerspective = { reprPrec := LuckingGinzburg2022.instReprQPerspective.repr }

def LuckingGinzburg2022.deriveQPersp {α : Type} [DecidableEq α] (bps : Finset (BP α)) : QPerspective

Derive q-persp from a sieved set of bipartitions. §4.3, (47): check whether ⟨∅, _⟩ survives the sieve.

The paper also has a third value "none" for degenerate cases like every (sole bipartition ⟨maxset, ∅⟩), but this is functionally equivalent to refsetNonempty — compset not available in either case.

Equations

• LuckingGinzburg2022.deriveQPersp bps = if decide (∃ b ∈ bps, b.refset = ∅) = true then LuckingGinzburg2022.QPerspective.refsetEmpty else LuckingGinzburg2022.QPerspective.refsetNonempty

def LuckingGinzburg2022.QPerspective.compsetAvailable : QPerspective → Bool

Compset is available for anaphora iff q-persp = refsetEmpty. §4.3, (47b).

Equations

• LuckingGinzburg2022.QPerspective.refsetEmpty.compsetAvailable = true
• LuckingGinzburg2022.QPerspective.refsetNonempty.compsetAvailable = false

def LuckingGinzburg2022.refindFilter {α : Type} (bps : Finset (BP α)) : Finset (BP α)

Refind filter: exclude bipartitions with empty refset. §4.3, (46): a few includes a refind (an individual from refset), which requires refset ≠ ∅. This excludes ⟨∅, maxset⟩, changing q-persp from refsetEmpty to refsetNonempty.

Equations

• LuckingGinzburg2022.refindFilter bps = {b ∈ bps | decide (b.refset.card > 0) = true}

§4. Deriving compset anaphora from bipartition structure

The paper's central contribution: compset anaphora availability is derived from the bipartition denotation via q-persp, not stipulated per quantifier. This section proves per-quantifier q-persp derivations on a concrete domain and shows that the few/a few contrast follows structurally.

Note: the full @cite{cooper-2023} Ch. 7 anaphora table also depends on referentiality (refset in dgb-params vs q-params) and plurality — distinctions orthogonal to RTT's q-persp mechanism. RTT's novel prediction is specifically about compset accessibility, which we derive here.

def LuckingGinzburg2022.isDogB : Phenomena.Quantification.Studies.Cooper2023.DogWorld → Prop

Prop version of isDog for decidable sieving.

Equations

• LuckingGinzburg2022.isDogB Phenomena.Quantification.Studies.Cooper2023.DogWorld.fido = True
• LuckingGinzburg2022.isDogB Phenomena.Quantification.Studies.Cooper2023.DogWorld.rex = True
• LuckingGinzburg2022.isDogB Phenomena.Quantification.Studies.Cooper2023.DogWorld.spot = True
• LuckingGinzburg2022.isDogB Phenomena.Quantification.Studies.Cooper2023.DogWorld.luna = False

@[implicit_reducible]

instance LuckingGinzburg2022.instDecidablePredDogWorldIsDogB : DecidablePred isDogB

Equations

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

def LuckingGinzburg2022.doesBarkB : Phenomena.Quantification.Studies.Cooper2023.DogWorld → Bool

Bool version of doesBark.

Equations

• LuckingGinzburg2022.doesBarkB Phenomena.Quantification.Studies.Cooper2023.DogWorld.fido = true
• LuckingGinzburg2022.doesBarkB Phenomena.Quantification.Studies.Cooper2023.DogWorld.rex = false
• LuckingGinzburg2022.doesBarkB Phenomena.Quantification.Studies.Cooper2023.DogWorld.spot = true
• LuckingGinzburg2022.doesBarkB Phenomena.Quantification.Studies.Cooper2023.DogWorld.luna = false

def LuckingGinzburg2022.dogs : Finset Phenomena.Quantification.Studies.Cooper2023.DogWorld

The set of dogs (3 entities).

Equations

• LuckingGinzburg2022.dogs = {x : Phenomena.Quantification.Studies.Cooper2023.DogWorld | LuckingGinzburg2022.isDogB x}

theorem LuckingGinzburg2022.dogs_eq : dogs = {Phenomena.Quantification.Studies.Cooper2023.DogWorld.fido, Phenomena.Quantification.Studies.Cooper2023.DogWorld.rex, Phenomena.Quantification.Studies.Cooper2023.DogWorld.spot}

theorem LuckingGinzburg2022.dog_bipartitions_card : (allBP dogs).card = 8

2^3 = 8 bipartitions of the dog set.

theorem LuckingGinzburg2022.every_dog_qpersp : deriveQPersp (sieve every_qcond (allBP dogs)) = QPerspective.refsetNonempty

Every: sole bipartition ⟨dogs, ∅⟩ has refset = dogs ≠ ∅. Q-persp = refsetNonempty. Compset not available (compset = ∅).

theorem LuckingGinzburg2022.no_dog_qpersp : deriveQPersp (sieve no_qcond (allBP dogs)) = QPerspective.refsetEmpty

No: sole bipartition ⟨∅, dogs⟩ has refset = ∅. Q-persp = refsetEmpty. Compset available — but for no, compset = maxset, so it collapses with maxset anaphora.

theorem LuckingGinzburg2022.some_dog_qpersp : deriveQPersp (sieve some_qcond (allBP dogs)) = QPerspective.refsetNonempty

Some: ⟨∅, _⟩ excluded by |refset| ≥ 1. Q-persp = refsetNonempty.

theorem LuckingGinzburg2022.most_dog_qpersp : deriveQPersp (sieve most_qcond (allBP dogs)) = QPerspective.refsetNonempty

Most: ⟨∅, _⟩ excluded by |refset| > |compset|. Q-persp = refsetNonempty.

theorem LuckingGinzburg2022.few_dog_qpersp : deriveQPersp (sieve few_qcond (allBP dogs)) = QPerspective.refsetEmpty

Few: ⟨∅, dogs⟩ included (0 < 3). Q-persp = refsetEmpty. Compset IS available. "Few dogs barked. They [= non-barking dogs] slept through."

theorem LuckingGinzburg2022.aFew_dog_qpersp : deriveQPersp (refindFilter (sieve few_qcond (allBP dogs))) = QPerspective.refsetNonempty

A few: same q-cond as few, but refind excludes ⟨∅, dogs⟩. Q-persp = refsetNonempty. Compset NOT available. "#They [= non-barking dogs] slept through."

theorem LuckingGinzburg2022.few_compset_available : (deriveQPersp (sieve few_qcond (allBP dogs))).compsetAvailable = true

Compset available for few (derived from q-persp).

theorem LuckingGinzburg2022.aFew_compset_not_available : (deriveQPersp (refindFilter (sieve few_qcond (allBP dogs)))).compsetAvailable = false

Compset NOT available for a few (derived: refind changes q-persp).

theorem LuckingGinzburg2022.few_aFew_matches_cooper : Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef.compset ∈ Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable Phenomena.Quantification.Studies.Cooper2023.QuantName.few ∧ Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef.compset ∉ Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable Phenomena.Quantification.Studies.Cooper2023.QuantName.aFew

This matches @cite{cooper-2023} Ch. 7: .compset ∈ anaphoraAvailable .few but .compset ∉ anaphoraAvailable .aFew.

§5. RTT refsets are Cooper witness sets

@cite{cooper-2023} Ch. 7 defines WitnessSet P X as X ⊆ extension of P. RTT's refsets satisfy this by construction: every bipartition in allBP S has refset ⊆ S. When S = fullExtFinset P, this is exactly WitnessSet P.

theorem LuckingGinzburg2022.bp_refset_is_witnessSet {α : Type} [DecidableEq α] [Fintype α] (P : α → Prop) [DecidablePred P] (b : BP α) (h : b ∈ allBP (Phenomena.Quantification.Studies.Cooper2023.fullExtFinset P)) : Phenomena.Quantification.Studies.Cooper2023.WitnessSet P b.refset

Every RTT bipartition's refset is a Cooper witness set. Bridges RTT's bipartition denotations to the witness-set framework of @cite{cooper-2023} Ch. 7.

theorem LuckingGinzburg2022.dogs_eq_fullExt : dogs = Phenomena.Quantification.Studies.Cooper2023.fullExtFinset Phenomena.Quantification.Studies.Cooper2023.isDog

The dogs Finset equals Cooper's fullExtFinset isDog.

§6. Structural conservativity and complexity reduction

RTT's bipartitions partition only the restrictor (head noun extension). Conservativity is guaranteed by construction: the scope set never appears independently. §1.3, §4.8.

def LuckingGinzburg2022.qcondToGQ {α : Type} [DecidableEq α] (qc : QCond) [Fintype α] (N : α → Prop) [DecidablePred N] (Q : α → Prop) : Prop

Convert a QCond (bipartition sieve) to a classical GQ. The QNP ⟨q-cond, N⟩ applied to VP = Q is true iff some bipartition survives the sieve such that all refset members satisfy Q.

Equations

• LuckingGinzburg2022.qcondToGQ qc N Q = ∃ b ∈ LuckingGinzburg2022.allBP (Finset.filter N Finset.univ), qc b.refset.card b.compset.card = true ∧ ∀ a ∈ b.refset, Q a

theorem LuckingGinzburg2022.qcond_conservative {α : Type} [DecidableEq α] [Fintype α] (qc : QCond) (N Q : α → Prop) [DecidablePred N] : qcondToGQ qc N Q ↔ qcondToGQ qc N fun (x : α) => N x ∧ Q x

Conservativity holds for any QCond by construction. Every a ∈ b.refset satisfies N (since b.refset ⊆ filter N), so replacing Q with N ∧ Q doesn't change truth. @cite{lucking-ginzburg-2022} §1.3 @cite{barwise-cooper-1981}

def LuckingGinzburg2022.rttQuantifierCount (k : ℕ) : ℕ

RTT quantifier count: for a head noun extension of size k, there are 2^(k+1) − 1 possible QNP denotations (non-empty subsets of the 2^k bipartitions). §4.8.

Equations

• LuckingGinzburg2022.rttQuantifierCount k = 2 ^ (k + 1) - 1

theorem LuckingGinzburg2022.rtt_fewer_than_conservative_2 : rttQuantifierCount 2 < Core.Quantification.conservativeQuantifierCount 2

RTT's quantifier space is strictly smaller than GQT's conservative count (@cite{van-benthem-1984}). For n=2: RTT gives 7 vs GQT's 64.

theorem LuckingGinzburg2022.rtt_fewer_than_conservative_3 : rttQuantifierCount 3 < Core.Quantification.conservativeQuantifierCount 3

theorem LuckingGinzburg2022.rtt_fewer_than_conservative_4 : rttQuantifierCount 4 < Core.Quantification.conservativeQuantifierCount 4

§7. Anti-predication

A VP simultaneously predicates positively on refset members (the "nucl") and negatively on compset members (the "anti-nucl"). This two-headed predication is specific to RTT and absent from standard GQT. §4.5, Figure 5: the declarative plural head-subject rule has both nucl and anti-nucl.

def LuckingGinzburg2022.antiPredication {α : Type} (VP : α → Bool) (b : BP α) : Prop

Anti-predication: the VP holds for all refset members and fails for all compset members.

Equations

• LuckingGinzburg2022.antiPredication VP b = ((∀ a ∈ b.refset, VP a = true) ∧ ∀ a ∈ b.compset, VP a = false)

theorem LuckingGinzburg2022.antiPred_refset {α : Type} (VP : α → Bool) (b : BP α) (h : antiPredication VP b) (a : α) (ha : a ∈ b.refset) : VP a = true

Anti-predication implies the VP holds for every refset member.

theorem LuckingGinzburg2022.antiPred_compset {α : Type} (VP : α → Bool) (b : BP α) (h : antiPredication VP b) (a : α) (ha : a ∈ b.compset) : VP a = false

Anti-predication implies the VP fails for every compset member.

theorem LuckingGinzburg2022.every_truth_conditions {α : Type} [DecidableEq α] (S : Finset α) (VP : α → Bool) : (∃ b ∈ sieve every_qcond (allBP S), antiPredication VP b) ↔ ∀ a ∈ S, VP a = true

Truth conditions for "every N VP" via RTT: ∃ b in the sieved set with anti-predication ↔ ∀ a ∈ S, VP a = true. The unique bipartition ⟨S, ∅⟩ makes anti-predication equivalent to the VP holding on all of S (anti-nucl on ∅ is vacuous).

§8. Sieve cardinalities

Concrete verification that the q-cond sieves produce expected counts.

theorem LuckingGinzburg2022.every_dog_sieve_card : (sieve every_qcond (allBP dogs)).card = 1

theorem LuckingGinzburg2022.no_dog_sieve_card : (sieve no_qcond (allBP dogs)).card = 1

theorem LuckingGinzburg2022.few_dog_sieve_card : (sieve few_qcond (allBP dogs)).card = 4

4 few-bipartitions: ⟨∅, dogs⟩ plus 3 singletons.

theorem LuckingGinzburg2022.aFew_dog_sieve_card : (refindFilter (sieve few_qcond (allBP dogs))).card = 3

Refind removes the empty-refset bipartition, leaving 3.