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 Spector2025.Interp (W : Type u_2) (D : Type u) : Type (max u u_2)

Interpretation function: maps predicates to extensions at worlds.

Equations

• Spector2025.Interp W D = (W → D → Bool)

def 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

• 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 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

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

theorem Spector2025.valuedT3_defined {D : Type u} (g : Core.PartialAssign D) (x : ℕ) : (valuedT3 g x).isDefined

U(x) is never undefined.

theorem 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

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

theorem 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 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

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

Abstract Transparency

Originally split out into Theories/Semantics/Presupposition/Transparency.lean, but Spector 2025 is the only consumer; per the project's N≥2 promotion discipline this co-locates the abstract API with its sole user until a second consumer (e.g., a future Mandelkern 2022 study file) lands.

Schlenker (2007, 2008a) introduced the Transparency Principle in a dynamic-with-local-contexts setting; Spector reuses the condition in a static partial-assignment setting (§2.2). The definitions below stay parametric in the assignment carrier so that the §6 plural-assignment variants can reuse the same shape.

@[reducible, inline]

abbrev Spector2025.Ctx (W : Type u_2) (D : Type u) : Type (max u_2 u)

A context is a set of world-assignment pairs. §2.2.1: "We view a context C as a set of world-assignment pairs (w,g)."

Equations

• Spector2025.Ctx W D = (W → Core.PartialAssign D → Prop)

def Spector2025.nullCtx {D : Type u} {W : Type u_1} : Ctx W D

The null context: all world-assignment pairs. §2.2.1: "the null context which contains all possible world-assignment pairs."

Equations

• Spector2025.nullCtx x✝¹ x✝ = True

def Spector2025.stalnakerUpdate {D : Type u} {W : Type u_1} (C : Ctx W D) (S : W → Core.PartialAssign D → Core.Duality.Truth3) : Ctx W D

Stalnakerian update: intersect context with sentence's truth set. §2.2.1: "if a sentence S is accepted as true in context C, then the resulting context is simply C intersected with the set of world-assignment pairs where S is true."

Equations

• Spector2025.stalnakerUpdate C S w g = (C w g ∧ S w g = Core.Duality.Truth3.true)

def Spector2025.agreeIn {D : Type u} {W : Type u_1} (C : Ctx W D) (S1 S2 : W → Core.PartialAssign D → Core.Duality.Truth3) : Prop

Two trivalent sentences agree throughout a context.

Equations

• Spector2025.agreeIn C S1 S2 = ∀ (w : W) (g : Core.PartialAssign D), C w g → S1 w g = S2 w g

@[reducible, inline]

abbrev Spector2025.Sent (W : Type u_2) (D : Type u) : Type (max u_2 u)

A trivalent sentence over world-assignment pairs.

Equations

• Spector2025.Sent W D = (W → Core.PartialAssign D → Core.Duality.Truth3)

@[reducible, inline]

abbrev Spector2025.Frame (W : Type u_2) (D : Type u) : Type (max u_2 u)

A sentence frame: a sentence with a hole for a sub-sentence.

Equations

• Spector2025.Frame W D = (Spector2025.Sent W D → Spector2025.Sent W D)

def Spector2025.transparent {D : Type u} {W : Type u_1} (C : Ctx W D) (frame : Frame W D) (presup : Sent W D) : Prop

The Transparency Principle (symmetric version).

§2.2.2 / §6.3: For a sentence S containing a free (underlined) variable x, form S1 by replacing P(x̲) with U(x) ∧ φ and S2 by replacing P(x̲) with φ. Transparency is satisfied in context C iff S1 and S2 agree throughout C for every formula φ.

We formalize this as: given a sentence-with-hole frame and a presupposition predicate presup, Transparency holds iff for every φ, frame (meetMiddle presup φ) and frame φ agree in C.

The frame represents the sentence with a hole where the presuppositional element occurs. The presupposition (e.g., U(x)) is conjoined via Middle Kleene conjunction.

Equations

• Spector2025.transparent C frame presup = ∀ (φ : Spector2025.Sent W D), Spector2025.agreeIn C (frame fun (w : W) (g : Core.PartialAssign D) => (presup w g).meetMiddle (φ w g)) (frame φ)

theorem Spector2025.transparent_of_presup_true {D : Type u} {W : Type u_1} (C : Ctx W D) (frame : Frame W D) (presup : Sent W D) (hframe : ∀ (φ₁ φ₂ : Sent W D), (∀ (w : W) (g : Core.PartialAssign D), C w g → φ₁ w g = φ₂ w g) → ∀ (w : W) (g : Core.PartialAssign D), C w g → frame φ₁ w g = frame φ₂ w g) (hpresup : ∀ (w : W) (g : Core.PartialAssign D), C w g → presup w g = Core.Duality.Truth3.true) : transparent C frame presup

Transparency holds trivially when the presupposition is always true in the context (since meetMiddle true v = v).

def Spector2025.noveltyCondition (usedVars : List ℕ) (newVar : ℕ) : Prop

The Novelty Condition: an existential quantifier introducing variable x can only occur once in a discourse.

§4 / @cite{heim-1982}: "If x is a variable, an occurrence of ∃x can only occur once in a whole discourse." This prevents ∃xP(x).∃xQ(x) from collapsing to ∃x(P(x) ∧ Q(x)).

Currently has no consumer in this file — see Deferred work at the end of the file.

Equations

• Spector2025.noveltyCondition usedVars newVar = ¬newVar ∈ usedVars

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 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 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 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 : Ctx W D) (φ : 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 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 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 : Ctx W D) (φ : 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 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 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 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

• 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 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 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 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 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.

Empirical coverage from §3

Spector's predictions cover the following items in adjacent files; the mapping is recorded here in prose so that future readers can find the relevant theorems without our duplicating the data file's stipulations in rfl-equality theorems.

forward_conj_transparency (above) handles forward intersentential anaphora across conjunction (∃xT(x) ∧ P(x̲)). It corresponds to Phenomena.Anaphora.DonkeyAnaphora.geachDonkey.boundReading and to the veridical-basic case of Studies.Anaphora.Hofmann2025.

reverse_conj_transparency_fails (above) corresponds to the cataphora side of the same data (Hofmann's negatedBasic).

bathroom_transparency (below) handles the bathroom-disjunction pattern (¬∃xB(x) ∨ H(x̲), Roberts 1989; Hofmann's bathroomDisjunction). It also covers the conditional-donkey pattern (¬∃xF(x) ∨ B(x̲), geachDonkey / conditionalDonkey).

reverse_bathroom_transparency_fails (below) accounts for the wrong-order bathroom (Hofmann's wrongOrderBathroom) and for separate-sentence configurations like negationBlocks and conjunctionBlocks where the mechanism is unavailable for distinct reasons (no joint frame; conjunction uses meetMiddle not joinMiddle).

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

Plural assignments are imported from Core.Assignment (open Core brings PluralAssign, singularAt, singular, restrict, defined, null, ofPred, singleton, sumDref into scope). Spector's static reuse is one consumer; the PPCDRT substrate (Theories/Semantics/Dynamic/PPCDRT/) is the other — once linglib has ≥2 consumers of plural-assignment machinery it belongs in Core.

@[reducible, inline]

abbrev 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

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

@[reducible, inline]

abbrev 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

• Spector2025.singularAt G x d = G.singularAt x d

noncomputable def 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

• Spector2025.evalPredPlural I G x w = if h : ∃ (d : D), Spector2025.singularAt G x d then Core.Duality.Truth3.ofBool (I w (Classical.choose h)) else Core.Duality.Truth3.indet

noncomputable def 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

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

theorem Spector2025.atomicT3_defined {D : Type u_2} (G : Core.PluralAssign D) (x : ℕ) : (atomicT3 G x).isDefined

atomic(x) is always defined (bivalent).

noncomputable def 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 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 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 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 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 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 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 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

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

def 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

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

theorem 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.

Reading preferences (§7) — empirical mapping

Spector argues (§7) that weakTruthP generates weak (existential) readings by default and that strongTruthP generates strong (universal) readings. Kanazawa's (1994) generalization picks one or the other based on the monotonicity profile of the surrounding quantifier: upward-entailing contexts (some) prefer weak; downward-entailing contexts (no, the negated donkey) prefer strong.

End-to-end derivations of these readings on a concrete toy world (corresponding to geachDonkey and negatedDonkey in Phenomena.Anaphora.DonkeyAnaphora) are deferred — see §6.7 entry in the Deferred work docstring at the end of this file.

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 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 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 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 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-1995}), while Spector's Transparency-based approach handles them naturally via Middle Kleene disjunction. The bathroom row is witnessed in Spector's favour by bathroom_transparency together with reverse_bathroom_transparency_fails; for an independent formalization of the ¬∃xB(x) ∨ F(x) truth conditions, see bathroom_truth_equiv.

Deferred work

Items from Spector (2025) that this file does not yet formalize. Each is a real piece of the paper; collected here so future work has explicit grep-able anchors.

• §5 covariation failure proof. covariation_fails_individual (above) proves a different statement (a single g cannot witness y for all x); the actual paper claim — that the simplified individual-assignment semantics produces a constant-witness reading for ¬∃x¬∃yS(x,y) — is not yet derived.

• §6.7 donkey sentence end-to-end. The classical donkey sentence ∀x(¬(F(x) ∧ ∃y(D(y) ∧ O(x,y))) ∨ B(x,y)) and its weak existential reading are summarized in prose but not proved on a concrete toy world. Spector's Tables 4–5 use 7 individuals; a 4-individual decide-checked variant would suffice.

• §7 Strong Truth examples (47), (54). The operator O is defined and proved equivalence-preserving (strongTruthOp_preserves_equiv, strongTruthOp_weakTruth_iff_strongTruth); the central motivating examples (Either it's not the case that Sue has a credit card and bought a cake with it…, the donkey-disjunction O parse of (54-c)) are not.

• Appendix functional variables. Spector's solution to quantificational subordination over indefinites (y_x(z) functional variables, paper (64)–(66)) is entirely deferred.

• Witness-condition substrate. The Mandelkern (2022) witness condition is currently inlined into existsT3 / existsPlural here (one-line stipulation each). A faithful Mandelkern 2022 study file would let those derive from the witness primitive instead. Deferred pending paper access; cite key mandelkern-2022 exists in references.bib with role cited, sources crossref. Per Spector p. 10, Mandelkern's system is quadrivalent + uses local-context bound clauses + uses individual (not plural) assignments — a substantive stub, not a quick one.

• noveltyCondition enforcement. The definition (in section AbstractTransparency above) has no consumer; §4 examples like (16) — ∃xP(x).∃xQ(x) collapsing to ∃x(P(x) ∧ Q(x)) — are not ruled out by any current theorem in this file.