Spector 2025: Trivalence and Transparency

@cite{spector-2025}

A non-dynamic approach to anaphora combining trivalent semantics (Middle Kleene, @cite{peters-1979}, @cite{beaver-krahmer-2001}) with Schlenker's Transparency Principle (@cite{schlenker-2007}, @cite{schlenker-2008a}).

Key Results Formalized

1. Forward anaphora in conjunction (§3.2): ∃xT(x) ∧ P(x̲) satisfies Transparency — the free variable in the second conjunct is licensed by the existential in the first.

2. Reverse conjunction fails (§3.2): P(x̲) ∧ ∃xT(x) does NOT satisfy Transparency in the null context — cataphora across conjunction is correctly predicted to be infelicitous.

3. Bathroom sentences (§3.3): ¬∃xB(x) ∨ H(x̲) satisfies Transparency — the classic "either there's no bathroom or it's upstairs" pattern is correctly predicted to be felicitous.

4. Reverse bathroom fails (§3.3): H(x̲) ∨ ¬∃xB(x) does NOT satisfy Transparency in the null context.

5. Semantic adequacy: The trivalent semantics delivers the correct truth-at-a-world conditions (§2.1).

Note on Middle Kleene conjunction

The paper's Table 1 shows 0 ∧ # = # for conjunction, but the paper's text (§2.1) states: "If φ is not undefined, then the truth values of φ ∧ ψ are the same as in the Strong Kleene truth-tables." Strong Kleene gives false ∧ # = false. The §3.2 proofs depend on this: the reverse conjunction counterexample requires meetMiddle false # = false. We follow the text and the proofs (Table 1 appears to contain an error in the conjunction column for 0 ∧ #).

Architecture

The trivalent semantics uses partial assignments (PartialAssign D) and plural assignments (PluralAssign D) from Core.Assignment. Predicate application yields # when the variable is unvalued. The existential quantifier uses @cite{mandelkern-2022}'s witness condition: ∃xφ is true at (w,g) only if g(x) witnesses φ, undefined if classically true but g(x) is not a witness.

@[reducible, inline]

abbrev Phenomena.Anaphora.Studies.Spector2025.Interp (W : Type u_2) (D : Type u) : Type (max u u_2)

Interpretation function: maps predicates to extensions at worlds.

Equations

• Phenomena.Anaphora.Studies.Spector2025.Interp W D = (W → D → Bool)

def Phenomena.Anaphora.Studies.Spector2025.evalPred {D : Type u} {W : Type u_1} (I : Interp W D) (g : Core.PartialAssign D) (x : ℕ) (w : W) : Core.Duality.Truth3

Evaluate a one-place predicate on a partial assignment. §2.1:

• 1 if g(x) ∈ I(P,w)
• 0 if g(x) ≠ # and g(x) ∉ I(P,w)
• # if g(x) = #

Equations

• Phenomena.Anaphora.Studies.Spector2025.evalPred I g x w = match g x with | some d => Core.Duality.Truth3.ofBool (I w d) | none => Core.Duality.Truth3.indet

def Phenomena.Anaphora.Studies.Spector2025.valuedT3 {D : Type u} (g : Core.PartialAssign D) (x : ℕ) : Core.Duality.Truth3

The U(x) predicate as a Truth3 value. Always bivalent: true if valued, false if not.

Equations

• Phenomena.Anaphora.Studies.Spector2025.valuedT3 g x = Core.Duality.Truth3.ofBool (g.valued x)

theorem Phenomena.Anaphora.Studies.Spector2025.valuedT3_defined {D : Type u} (g : Core.PartialAssign D) (x : ℕ) : (valuedT3 g x).isDefined = true

U(x) is never undefined.

theorem Phenomena.Anaphora.Studies.Spector2025.evalPred_valued {D : Type u} {W : Type u_1} (I : Interp W D) (g : Core.PartialAssign D) (x : ℕ) (w : W) (h : g.valued x = true) : (evalPred I g x w).isDefined = true

When g values x, evaluating a predicate at x is bivalent.

theorem Phenomena.Anaphora.Studies.Spector2025.evalPred_unvalued {D : Type u} {W : Type u_1} (I : Interp W D) (g : Core.PartialAssign D) (x : ℕ) (w : W) (h : g.valued x = false) : evalPred I g x w = Core.Duality.Truth3.indet

When g does not value x, evaluating a predicate at x is undefined.

def Phenomena.Anaphora.Studies.Spector2025.trueAtWorld {D : Type u} {W : Type u_1} (φ : W → Core.PartialAssign D → Core.Duality.Truth3) (w : W) : Prop

A sentence φ is true at a world w iff there is an assignment g such that ⟦φ⟧^{w,g} = 1.

§2.1: "A sentence φ is true at a world w if and only if there is an assignment function g such that ⟦φ⟧^{w,g} = 1." This bridges trivalent assignment-level semantics to world-level truth conditions.

Equations

• Phenomena.Anaphora.Studies.Spector2025.trueAtWorld φ w = ∃ (g : Core.PartialAssign D), φ w g = Core.Duality.Truth3.true

Parametric Transparency

§6.3 observes that the Transparency proofs are parametric in the assignment type — the same Middle Kleene reasoning works for individual assignments g and plural assignments G. We factor this out: the proofs below are stated over abstract Truth3 values, independent of assignment representation.

theorem Phenomena.Anaphora.Studies.Spector2025.conj_transparency_parametric (E presup φ : Core.Duality.Truth3) : (E = Core.Duality.Truth3.true → presup = Core.Duality.Truth3.true) → E.meetMiddle (presup.meetMiddle φ) = E.meetMiddle φ

Parametric forward conjunction Transparency: meetMiddle E (meetMiddle presup φ) = meetMiddle E φ whenever E = true → presup = true. Independent of assignment type — works for both individual and plural systems.

§3.2, §6.3: The three cases are:

• E = false: meetMiddle false _ = false (left zero)
• E = #: meetMiddle # _ = # (left absorbs)
• E = true: witness gives presup = true, so meetMiddle true φ = φ

theorem Phenomena.Anaphora.Studies.Spector2025.disj_transparency_parametric (negE presup φ : Core.Duality.Truth3) : (negE = Core.Duality.Truth3.false → presup = Core.Duality.Truth3.true) → negE.joinMiddle (presup.meetMiddle φ) = negE.joinMiddle φ

Parametric bathroom Transparency: joinMiddle negE (meetMiddle presup φ) = joinMiddle negE φ whenever negE = false → presup = true.

Forward anaphora: ∃xT(x) ∧ P(x̲)

Consider "A table is in the room and it is purple," translated as ∃xT(x) ∧ P(x̲). The Transparency question is: does ∃xT(x) ∧ (U(x) ∧ φ) always have the same truth value as ∃xT(x) ∧ φ?

The frame is F(ψ) = ∃xT(x) ∧ ψ, and the presupposition is U(x).

Proof (§3.2): Consider (w,g).

• If ∃xT(x) is false at (w,g): both sentences are false (Middle Kleene: false ∧ _ = false).
• If ∃xT(x) is # at (w,g): both sentences are # (Middle Kleene: # ∧ _ = #).
• If ∃xT(x) is true at (w,g): then g values x, so U(x) = true, so meetMiddle true φ = φ, so both sentences equal ∃xT(x) ∧ φ.

theorem Phenomena.Anaphora.Studies.Spector2025.forward_conj_transparency {D : Type u} {W : Type u_1} (E presup : W → Core.PartialAssign D → Core.Duality.Truth3) (hwitness : ∀ (w : W) (g : Core.PartialAssign D), E w g = Core.Duality.Truth3.true → presup w g = Core.Duality.Truth3.true) (C : Semantics.Presupposition.Transparency.Ctx W D) (φ : Semantics.Presupposition.Transparency.Sent W D) (w : W) (g : Core.PartialAssign D) : C w g → (E w g).meetMiddle ((presup w g).meetMiddle (φ w g)) = (E w g).meetMiddle (φ w g)

Forward conjunction Transparency: ∃xT(x) ∧ P(x̲) satisfies Transparency in every context.

§3.2: The abstract pattern is: if E = true implies presup = true (the witness connection), then the frame F(ψ) = meetMiddle E ψ satisfies Transparency for presup.

Derived from conj_transparency_parametric.

theorem Phenomena.Anaphora.Studies.Spector2025.reverse_conj_transparency_fails : ∃ (W : Type), ∃ (D : Type), ∃ (E : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (presup : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (φ : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (w : W), ∃ (g : Core.PartialAssign D), ((presup w g).meetMiddle (φ w g)).meetMiddle (E w g) ≠ (φ w g).meetMiddle (E w g)

Reverse conjunction Transparency FAILS: P(x̲) ∧ ∃xT(x) does NOT satisfy Transparency in the null context.

§3.2: Take φ = P(x). If g does not value x, then φ ∧ ∃xT(x) is # (left undefined absorbs), but (U(x) ∧ φ) ∧ ∃xT(x) is false ∧ ∃xT(x) = false (since U(x) = false and meetMiddle false # = false). The key asymmetry of Middle Kleene: meetMiddle false # = false but meetMiddle # _ = #.

Bathroom sentences: ¬∃xB(x) ∨ H(x̲)

"Either there is no bathroom, or it is hidden," translated as ¬∃xB(x) ∨ H(x̲). The Transparency question is: does ¬∃xB(x) ∨ (U(x) ∧ φ) always have the same truth value as ¬∃xB(x) ∨ φ?

The frame is F(ψ) = joinMiddle (¬∃xB(x)) ψ, and the presupposition is U(x).

Proof (§3.3): Consider (w,g).

• If ¬∃xB(x) is true at (w,g): joinMiddle true _ = true (SK).
• If ¬∃xB(x) is # at (w,g): joinMiddle # _ = # (left absorbs).
• If ¬∃xB(x) is false at (w,g): then ∃xB(x) is true, so g values x, so U(x) = true, so meetMiddle true φ = φ, and both disjunctions reduce to joinMiddle false φ.

theorem Phenomena.Anaphora.Studies.Spector2025.bathroom_transparency {D : Type u} {W : Type u_1} (negE presup : W → Core.PartialAssign D → Core.Duality.Truth3) (hwitness : ∀ (w : W) (g : Core.PartialAssign D), negE w g = Core.Duality.Truth3.false → presup w g = Core.Duality.Truth3.true) (C : Semantics.Presupposition.Transparency.Ctx W D) (φ : Semantics.Presupposition.Transparency.Sent W D) (w : W) (g : Core.PartialAssign D) : C w g → (negE w g).joinMiddle ((presup w g).meetMiddle (φ w g)) = (negE w g).joinMiddle (φ w g)

Bathroom sentence Transparency: ¬∃xB(x) ∨ H(x̲) satisfies Transparency in every context.

The key insight: ¬E being false means E is true, which (by the witness condition) means g values x, making U(x) redundant. Derived from disj_transparency_parametric.

theorem Phenomena.Anaphora.Studies.Spector2025.reverse_bathroom_transparency_fails : ∃ (W : Type), ∃ (D : Type), ∃ (negE : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (presup : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (φ : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (w : W), ∃ (g : Core.PartialAssign D), ((presup w g).meetMiddle (φ w g)).joinMiddle (negE w g) ≠ (φ w g).joinMiddle (negE w g)

Reverse bathroom Transparency FAILS: H(x̲) ∨ ¬∃xB(x) does NOT satisfy Transparency in the null context.

§3.3: Consider g that does not value x and a tautological φ. Then φ ∨ ¬∃xB(x) has φ = # (unvalued), so joinMiddle # (¬∃xB(x)) = #. But (U(x) ∧ φ) ∨ ¬∃xB(x) has U(x) = false, so meetMiddle false # = false, and joinMiddle false (¬∃xB(x)) can be true — a difference.

Bathroom truth-condition equivalence

§2.1 proves that the trivalent sentence ¬∃xB(x) ∨ F(x) is true at a world w (in the sense of definition (6): ∃g such that the sentence is .true at (w,g)) if and only if the classical sentence ¬∃xB(x) ∨ ∃x(B(x) ∧ F(x)) is true at w.

This is the key semantic adequacy result: the trivalent system delivers the correct truth conditions, not just correct felicity predictions.

Proof outline (two directions):

(8) classically true → (7) true at some (w,g):

• Case 1: ∃xB(x) classically false. Then for every g, ∃xB(x) is false at (w,g), so ¬∃xB(x) is true, and joinMiddle true _ = true.
• Case 2: ∃x(B(x) ∧ F(x)) classically true. Pick witness a, set g(x) = a. Then ¬∃xB(x) is false (since g(x) = a witnesses B), and F(x) is true. So joinMiddle false true = true.

(7) true at some (w,g) → (8) classically true:

• By Middle Kleene disjunction, either ¬∃xB(x) is true at (w,g) (→ ∃xB(x) classically false → first disjunct of (8)), or ¬∃xB(x) is false and F(x) is true. In the latter case, ∃xB(x) is true so g(x) ∈ I(B,w), and F(x) true means g(x) ∈ I(F,w), so g(x) witnesses B(x) ∧ F(x).

def Phenomena.Anaphora.Studies.Spector2025.bathroomSent {D W : Type} (B F : Interp W D) (dom : List D) (w : W) (g : Core.PartialAssign D) : Core.Duality.Truth3

The trivalent sentence ¬∃xB(x) ∨ F(x) evaluated at (w,g), where B and F are one-place predicates and x is variable 0.

Components:

• ∃xB(x): true if g(0) ∈ I(B,w), false if ∀d, d ∉ I(B,w), # if classically true but g(0) not a witness
• ¬∃xB(x): negation (flips true/false, preserves #)
• F(x): evalPred F g 0 w (true/false/# depending on g(0))
• Overall: joinMiddle (neg (∃xB(x))) (F(x))

Equations

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

def Phenomena.Anaphora.Studies.Spector2025.bathroomClassical {D W : Type} (B F : Interp W D) (dom : List D) (w : W) : Prop

Classical truth of ¬∃xB(x) ∨ ∃x(B(x) ∧ F(x)): either no element satisfies B, or some element satisfies both B and F.

Equations

• Phenomena.Anaphora.Studies.Spector2025.bathroomClassical B F dom w = ((dom.all fun (d : D) => B w d == false) = true ∨ ∃ (d : D), d ∈ dom ∧ B w d = true ∧ F w d = true)

theorem Phenomena.Anaphora.Studies.Spector2025.bathroom_classical_to_trivalent {D W : Type} (B F : Interp W D) (dom : List D) (w : W) (h : bathroomClassical B F dom w) : trueAtWorld (bathroomSent B F dom) w

Direction 1: If the classical bathroom disjunction holds, then the trivalent sentence is true at w.

§2.1: We construct a specific g that makes the trivalent sentence .true.

• If no bathrooms exist: any g works (¬∃xB(x) is true, joinMiddle true _ = true).
• If a bathroom a exists with F(a): set g(0) = a. Then ¬∃xB(x) is false (a witnesses B), F(x) = F(a) = true, and joinMiddle false true = true.

theorem Phenomena.Anaphora.Studies.Spector2025.bathroom_trivalent_to_classical {D W : Type} (B F : Interp W D) (dom : List D) (w : W) (hdom : ∀ (d : D), d ∈ dom) (h : trueAtWorld (bathroomSent B F dom) w) : bathroomClassical B F dom w

Direction 2: If the trivalent bathroom sentence is true at w, then the classical disjunction holds.

§2.1: By Middle Kleene disjunction, the sentence is .true at (w,g) only if either: (a) ¬∃xB(x) is .true → ∃xB(x) is .false → no bathrooms, or (b) ¬∃xB(x) is .false and F(x) is .true. In case (b), ∃xB(x) is .true, so g(0) ∈ I(B,w) (witness condition), and F(x) = true means g(0) ∈ I(F,w). So g(0) witnesses B(x) ∧ F(x).

Requires dom to list all elements of D (completeness).

theorem Phenomena.Anaphora.Studies.Spector2025.bathroom_truth_equiv {D W : Type} (B F : Interp W D) (dom : List D) (w : W) (hdom : ∀ (d : D), d ∈ dom) : trueAtWorld (bathroomSent B F dom) w ↔ bathroomClassical B F dom w

Bathroom truth-condition equivalence (the complete iff).

§2.1: The trivalent sentence ¬∃xB(x) ∨ F(x) is true at world w if and only if the classical sentence ¬∃xB(x) ∨ ∃x(B(x) ∧ F(x)) is classically true at w.

This is the key semantic adequacy result: the non-standard trivalent semantics with partial assignments delivers exactly the classical truth conditions for bathroom sentences.

theorem Phenomena.Anaphora.Studies.Spector2025.bare_pronoun_fails_null : ∃ (W : Type), ∃ (D : Type), ∃ (presup : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (φ : W → Core.PartialAssign D → Core.Duality.Truth3), ∃ (w : W), ∃ (g : Core.PartialAssign D), True ∧ (presup w g).meetMiddle (φ w g) ≠ φ w g

A bare pronoun P(x̲) is infelicitous in the null context.

§3.1: In the null context, Transparency requires that for every φ, U(x) ∧ φ and φ have the same truth value across all (w,g). But take g with g(x) = # and φ always true: meetMiddle false true = false ≠ true, so Transparency fails.

The identity frame F(ψ) = ψ represents a bare sentence.

theorem Phenomena.Anaphora.Studies.Spector2025.geach_has_bound_reading : DonkeyAnaphora.geachDonkey.boundReading = true

The Geach donkey sentence reports a bound reading — forward conjunction ∃xP(x) ∧ Q(x̲) is exactly this pattern. Spector's system predicts it is felicitous via forward_conj_transparency.

theorem Phenomena.Anaphora.Studies.Spector2025.conditional_donkey_has_bound_reading : DonkeyAnaphora.conditionalDonkey.boundReading = true

Conditional donkey (If a farmer owns a donkey, he beats it) also has a bound reading. In Spector's system, the conditional is ¬∃xF(x) ∨ B(x̲) — the bathroom sentence pattern.

theorem Phenomena.Anaphora.Studies.Spector2025.classic_bathroom_felicitous : BathroomSentences.classicBathroom.felicitous = true

The classic bathroom sentence is felicitous. Spector's system predicts this via bathroom_transparency: the frame F(ψ) = joinMiddle (¬∃xB(x)) ψ satisfies Transparency because ¬∃xB(x) = false implies ∃xB(x) = true implies g values x.

theorem Phenomena.Anaphora.Studies.Spector2025.standard_negation_infelicitous : BathroomSentences.standardNegation.felicitous = false

Standard negation across sentence boundary is infelicitous — consistent with Transparency failing for bare pronouns.

theorem Phenomena.Anaphora.Studies.Spector2025.conjunction_version_infelicitous : BathroomSentences.conjunctionVersion.felicitous = false

Conjunction doesn't license bathroom-pattern anaphora (wrong connective). Spector's system handles this: conjunction uses meetMiddle, not joinMiddle, so the mechanism is different.

theorem Phenomena.Anaphora.Studies.Spector2025.wrong_order_bathroom_infelicitous : BathroomSentences.wrongOrder.felicitous = false

Wrong-order bathroom sentence is infelicitous. This corresponds to reverse_bathroom_transparency_fails: H(x̲) ∨ ¬∃xB(x) fails Transparency because H(x̲) is in left position, and Middle Kleene left-absorbs #.

theorem Phenomena.Anaphora.Studies.Spector2025.bathroom_felicity_alignment : BathroomSentences.classicBathroom.felicitous = true ∧ BathroomSentences.conjunctionVersion.felicitous = false ∧ BathroomSentences.wrongOrder.felicitous = false ∧ BathroomSentences.standardNegation.felicitous = false

Summary: Spector's Transparency predictions align with all felicity judgments in the bathroom sentence dataset. Felicitous examples have the presupposition in the RIGHT disjunct (after the negated existential); infelicitous examples violate this pattern.

The plural assignment system

The preliminary system (§§2–5) fails on covariation: ¬∃x¬∃yS(x,y) ("everybody spoke to somebody") wrongly requires a single person everyone spoke to. The full system (§6) replaces individual partial assignments with plural assignments — sets of atomic assignments.

Key changes from the simplified system:

• Evaluation is relative to (w, G) where G : PluralAssign D
• U(x) is replaced by atomic(x): |G(x)| = 1 (all assignments in G that define x agree on its value)
• The universal quantifier ∀xφ is now well-defined
• Quantificational subordination works via inter-variable dependencies recorded in G

@[reducible, inline]

abbrev Phenomena.Anaphora.Studies.Spector2025.PSent (W : Type u_4) (D : Type u_5) : Type (max u_4 u_5)

Plural sentence: evaluated relative to a world and a plural assignment.

Equations

• Phenomena.Anaphora.Studies.Spector2025.PSent W D = (W → Core.PluralAssign D → Core.Duality.Truth3)

@[reducible, inline]

abbrev Phenomena.Anaphora.Studies.Spector2025.singularAt {D : Type u_2} (G : Core.PluralAssign D) (x : ℕ) (d : D) : Prop

Alias for PluralAssign.singularAt — G assigns x uniquely to d. §6.2: |G(x)| = 1 with G(x) = d.

Equations

• Phenomena.Anaphora.Studies.Spector2025.singularAt G x d = G.singularAt x d

noncomputable def Phenomena.Anaphora.Studies.Spector2025.evalPredPlural {D : Type u_2} {W : Type u_3} (I : Interp W D) (G : Core.PluralAssign D) (x : ℕ) (w : W) : Core.Duality.Truth3

Evaluate a one-place predicate relative to (w, G). §6.2:

• 1 if |G(x)| = 1 and G(x) ∈ I(P,w)
• 0 if |G(x)| = 1 and G(x) ∉ I(P,w)
• # if |G(x)| ≠ 1

Equations

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

noncomputable def Phenomena.Anaphora.Studies.Spector2025.atomicT3 {D : Type u_2} (G : Core.PluralAssign D) (x : ℕ) : Core.Duality.Truth3

The atomic(x) predicate as a Truth3 value. §6.3: ⟦atomic(x)⟧^{w,G} = 1 if |G(x)| = 1, 0 otherwise. Always bivalent (never #). Replaces U(x) from the simplified system.

Equations

• Phenomena.Anaphora.Studies.Spector2025.atomicT3 G x = if G.singular x then Core.Duality.Truth3.true else Core.Duality.Truth3.false

theorem Phenomena.Anaphora.Studies.Spector2025.atomicT3_defined {D : Type u_2} (G : Core.PluralAssign D) (x : ℕ) : (atomicT3 G x).isDefined = true

atomic(x) is always defined (bivalent).

noncomputable def Phenomena.Anaphora.Studies.Spector2025.existsPlural {D : Type u_2} {W : Type u_3} (x : ℕ) (φ : PSent W D) (dom : Set D) (w : W) (G : Core.PluralAssign D) : Core.Duality.Truth3

Plural existential quantifier with witness condition. §6.2:

• 1 if ⟦φ⟧^{w,G} = 1
• 0 if for every atomic a ∈ D, G_{x=a} ≠ ∅ and ⟦φ⟧^{w,G_{x=a}} = 0
• # otherwise

Equations

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

noncomputable def Phenomena.Anaphora.Studies.Spector2025.forallPlural {D : Type u_2} {W : Type u_3} (x : ℕ) (φ : PSent W D) (dom : Set D) (w : W) (G : Core.PluralAssign D) : Core.Duality.Truth3

Plural universal quantifier. §6.2:

• 1 if for every atomic a ∈ D, G_{x=a} ≠ ∅ and ⟦φ⟧^{w,G_{x=a}} = 1
• 0 if the coverage condition holds and some a gives ⟦φ⟧^{w,G_{x=a}} = 0
• # otherwise

Equations

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

theorem Phenomena.Anaphora.Studies.Spector2025.plural_forward_conj_transparency {D : Type u_2} {W : Type u_3} (E presup : W → Core.PluralAssign D → Core.Duality.Truth3) (hwitness : ∀ (w : W) (G : Core.PluralAssign D), E w G = Core.Duality.Truth3.true → presup w G = Core.Duality.Truth3.true) (φ : W → Core.PluralAssign D → Core.Duality.Truth3) (w : W) (G : Core.PluralAssign D) : (E w G).meetMiddle ((presup w G).meetMiddle (φ w G)) = (E w G).meetMiddle (φ w G)

Forward conjunction Transparency in the plural system, derived from the parametric version.

theorem Phenomena.Anaphora.Studies.Spector2025.plural_bathroom_transparency {D : Type u_2} {W : Type u_3} (negE presup : W → Core.PluralAssign D → Core.Duality.Truth3) (hwitness : ∀ (w : W) (G : Core.PluralAssign D), negE w G = Core.Duality.Truth3.false → presup w G = Core.Duality.Truth3.true) (φ : W → Core.PluralAssign D → Core.Duality.Truth3) (w : W) (G : Core.PluralAssign D) : (negE w G).joinMiddle ((presup w G).meetMiddle (φ w G)) = (negE w G).joinMiddle (φ w G)

Bathroom Transparency in the plural system, derived from the parametric version.

Universal doesn't introduce a discourse referent

§6.3 (pp.20–21): ∀xP(x) ∧ Q(x̲) does NOT satisfy Transparency in the null context. When ∀xP(x) is true at (w,G), G(x) contains all atomic individuals in D, so |G(x)| ≠ 1 (assuming |D| ≥ 2), and therefore atomic(x) is false. This means the universal quantifier cannot serve as the antecedent of a singular pronoun.

theorem Phenomena.Anaphora.Studies.Spector2025.universal_doesnt_license_anaphora : ∃ (D : Type), ∃ (presup : Core.PluralAssign D → Core.Duality.Truth3), ∃ (φ : Core.PluralAssign D → Core.Duality.Truth3), ∃ (G : Core.PluralAssign D), (presup G).meetMiddle (φ G) ≠ φ G

The universal quantifier does not license subsequent singular anaphora. For two-element domains: ∀xP(x) being true forces |G(x)| > 1, making atomic(x) false.

§6.3: the sentences ∀xP(x) ∧ (atomic(x) ∧ φ) and ∀xP(x) ∧ φ can differ — taking φ tautological, the first is false (since atomic(x) is false when |G(x)| > 1) while the second is true.

The covariation problem and its fix

§5: In the simplified (individual-assignment) system, ¬∃x¬∃yS(x,y) ("everybody spoke to somebody") is true at (w,g) iff for all a, (a, g(y)) ∈ I(S,w). This wrongly gives a constant-witness reading: "everyone spoke to g(y)" — a single person.

§6.4: With plural assignments, the innermost ∃y is evaluated relative to G_{x=a} for each a, so different a's can pair with different b's. The sentence now correctly means "for every a there exists b such that (a,b) ∈ S."

theorem Phenomena.Anaphora.Studies.Spector2025.covariation_fixed {D : Type u_2} {W : Type u_3} (S : W → D → D → Bool) (dom : List D) (w : W) (hcovar : ∀ (a : D), a ∈ dom → ∃ (b : D), b ∈ dom ∧ S w a b = true) : ∃ (G : Core.PluralAssign D), ∀ (a : D), a ∈ dom → ∃ (b : D), b ∈ dom ∧ ∃ (g : Core.PartialAssign D), g ∈ G ∧ g 0 = some a ∧ g 1 = some b ∧ S w a b = true

The covariation fix: with plural assignments, the universal-existential pattern is correctly expressible.

§6.4: If a world satisfies ∀x∃y S(x,y), we can build a plural assignment G that witnesses each a-b pair independently. This is impossible with individual assignments, where a single g(y) must work for all values of x.

theorem Phenomena.Anaphora.Studies.Spector2025.covariation_fails_individual : ∃ (D : Type), ∃ (W : Type), ∃ (S : W → D → D → Bool), ∃ (w : W), ∃ (x : ∀ (a : D), ∃ (b : D), S w a b = true), ¬∃ (g : Core.PartialAssign D), ∀ (a : D), ∃ (b : D), g 1 = some b ∧ S w a b = true

In contrast, with individual assignments the covariation reading fails: a single assignment can only provide one witness for y, which must work for ALL values of x.

Two notions of truth at a world

§7: Two modes of interpretation for donkey sentences:

• Weak Truth: S is weakly true at w if ∃G such that S is true at (w,G). Generates existential (weak) readings.

• Strong Truth: S is strongly true at w if ∃G true at (w,G) AND no G' makes S false at (w,G'). Generates universal (strong) readings. Similar to @cite{elliott-2023}'s strengthened reading and @cite{champollion-bumford-henderson-2019}'s homogeneity approach.

For simple existentials ∃xP(x), weak and strong truth coincide. They diverge for donkey sentences.

def Phenomena.Anaphora.Studies.Spector2025.weakTruthP {D : Type u_2} {W : Type u_3} (φ : PSent W D) (w : W) : Prop

Weak truth at a world: ∃G such that the sentence is true at (w,G). §7 (46a).

Equations

• Phenomena.Anaphora.Studies.Spector2025.weakTruthP φ w = ∃ (G : Core.PluralAssign D), φ w G = Core.Duality.Truth3.true

def Phenomena.Anaphora.Studies.Spector2025.strongTruthP {D : Type u_2} {W : Type u_3} (φ : PSent W D) (w : W) : Prop

Strong truth at a world: weakly true AND not weakly false. §7 (46b).

Equations

• Phenomena.Anaphora.Studies.Spector2025.strongTruthP φ w = ((∃ (G : Core.PluralAssign D), φ w G = Core.Duality.Truth3.true) ∧ ¬∃ (G : Core.PluralAssign D), φ w G = Core.Duality.Truth3.false)

theorem Phenomena.Anaphora.Studies.Spector2025.strongTruth_implies_weakTruth {D : Type u_2} {W : Type u_3} (φ : PSent W D) (w : W) (h : strongTruthP φ w) : weakTruthP φ w

Strong truth implies weak truth.

theorem Phenomena.Anaphora.Studies.Spector2025.spector_predicts_weak_donkey : DonkeyAnaphora.geachDonkey.weakReading = true

Connection to donkey reading data: Spector's system predicts weak readings by default (via Weak Truth).

theorem Phenomena.Anaphora.Studies.Spector2025.spector_allows_strong_donkey : DonkeyAnaphora.geachDonkey.strongReading = true

The system also allows strong readings via Strong Truth.

theorem Phenomena.Anaphora.Studies.Spector2025.kanazawa_negated_donkey : DonkeyAnaphora.negatedDonkey.strongReading = true ∧ DonkeyAnaphora.negatedDonkey.weakReading = false

@cite{kanazawa-1994}'s generalization: reading preference tracks quantifier monotonicity. The negated donkey has only strong readings (universal reading when the pronoun is in a DE context).

The Strong Truth Operator

§7 (55): The operator O internalizes Strong Truth as an embeddable operator in the object language:

⟦O(S)⟧^{w,G} = 1 if ⟦S⟧^{w,G} = 1 and ¬∃G'. ⟦S⟧^{w,G'} = 0
⟦O(S)⟧^{w,G} = 0 if ⟦S⟧^{w,G} = 0 and ¬∃G'. ⟦S⟧^{w,G'} = 1
⟦O(S)⟧^{w,G} = # otherwise

This allows Strong Truth to be applied at specific syntactic positions rather than globally. Key properties:

• If S₁ ≡ S₂ (logically equivalent), then O(S₁) ≡ O(S₂)
• O can violate Transparency when embedded, which is desirable: ∃xS(x) ∧ O(H(x̲)) is correctly predicted to be infelicitous

noncomputable def Phenomena.Anaphora.Studies.Spector2025.strongTruthOp {D : Type u_2} {W : Type u_3} (φ : PSent W D) (w : W) (G : Core.PluralAssign D) : Core.Duality.Truth3

The Strong Truth Operator O. §7 (55).

Equations

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

theorem Phenomena.Anaphora.Studies.Spector2025.strongTruthOp_preserves_equiv {D : Type u_2} {W : Type u_3} (φ₁ φ₂ : PSent W D) (hequiv : ∀ (w : W) (G : Core.PluralAssign D), φ₁ w G = φ₂ w G) (w : W) (G : Core.PluralAssign D) : strongTruthOp φ₁ w G = strongTruthOp φ₂ w G

O preserves logical equivalence: if φ₁ and φ₂ agree everywhere, O(φ₁) and O(φ₂) agree everywhere. §7 (57).

theorem Phenomena.Anaphora.Studies.Spector2025.strongTruthOp_true_implies {D : Type u_2} {W : Type u_3} (φ : PSent W D) (w : W) (G : Core.PluralAssign D) (h : strongTruthOp φ w G = Core.Duality.Truth3.true) : φ w G = Core.Duality.Truth3.true

O(S) is true at (w,G) implies S is true at (w,G).

theorem Phenomena.Anaphora.Studies.Spector2025.strongTruthOp_weakTruth_iff_strongTruth {D : Type u_2} {W : Type u_3} (φ : PSent W D) (w : W) : weakTruthP (strongTruthOp φ) w ↔ strongTruthP φ w

Strong truth at w ↔ weak truth of O(S) at w. Embedding O at matrix level recovers the Strong Truth interpretation.

Spector's static system vs. Dynamic Predicate Logic

positions the system as a non-dynamic alternative to DPL (@cite{groenendijk-stokhof-1991}). Key comparison:

Phenomenon	Spector	DPL
Forward conj ∃xP(x) ∧ Q(x)	✓ Transparency	✓ assignment persistence
Reverse conj Q(x) ∧ ∃xP(x)	✗ Middle Kleene	✗ x not yet bound
Bathroom ¬∃xB(x) ∨ F(x)	✓ Transparency	✗ negation is test
Neg blocks ¬∃xP(x). Q(x)	✗ no frame	✗ negation is test

The systems agree on 3/4 cases. The disagreement on bathroom sentences is significant: standard DPL cannot handle them because negation is a test that doesn't export assignments (@cite{krahmer-muskens-1996}), while Spector's Transparency-based approach handles them naturally via Middle Kleene disjunction.

theorem Phenomena.Anaphora.Studies.Spector2025.spector_handles_bathroom : BathroomSentences.classicBathroom.felicitous = true

Spector handles bathroom sentences; standard DPL does not. Middle Kleene disjunction + Transparency handles ¬∃xB(x) ∨ F(x̲) without any dynamic mechanism — the key empirical advantage.

theorem Phenomena.Anaphora.Studies.Spector2025.spector_dpl_agree_cataphora_blocked : BathroomSentences.wrongOrder.felicitous = false

Both systems correctly block cataphora (reverse conjunction).