Spector (2026): Trivalence and transparency: a non-dynamic approach to anaphora

Spector interprets a first-order language statically at world–assignment pairs with partial assignments. A predicate of an unvalued variable is undefined, the connectives follow the Middle Kleene tables, and an existential is true only when the assignment already values its variable with a witness. A free variable presupposes that it is valued, and a sentence is felicitous in a context when Schlenker's symmetric Transparency holds at every occurrence of every free variable. The full system evaluates at plural assignments, where a free variable presupposes that its value is atomic; it restores covariation, captures quantificational subordination and the weak reading of donkey sentences, and a strong-truth operator internalizes universal readings.

Main statements

• felicitous_forward_conj, felicitous_bathroom, not_felicitous_reverse_conj: anaphora across conjunction and in bathroom sentences, and its sensitivity to order.
• trueAtP_notExNotEx_iff, trueAtP_qs_iff, felicitousP_qs: covariation and quantificational subordination in the full system.
• trueAtP_donkey_iff, felicitousP_donkey: the weak reading of donkey sentences, and Transparency for their pronoun.
• stronglyTrueAt_ex_and_iff: under Strong Truth, there is a bathroom and it is upstairs says that every bathroom is upstairs.

Implementation notes

• One language serves both systems: valued is the paper's U(x) in the simplified system and atomic(x) in the full one, and the simplified evaluation leaves the universal and the strong-truth operator undefined.
• Formula.occurrences lists the free arguments of each atom with the presupposition the Transparency Condition tests there, valued(x) for each and valued(x) ∧ valued(y) when both arguments of a relation are free.
• The language has no individual constants, so Sue's owning and beating in (40) are one-place predicates.
• The functional variables of the appendix, which (35) and (61) need, are not formalized, nor is Stone disjunction, which the paper leaves open (fn. 15).

References

• [Spe26]
• [Sch07]
• [Sch08d]
• [Man22]
• [Pet79]
• [BK01]

The language

inductive Spector2026.Formula (P : Type u_1) (R : Type u_2) : Type (max u_1 u_2)

The language has one- and two-place predicates on variables, the valuedness predicate that Transparency introduces, the connectives, and the quantifiers.

• pred {P : Type u_1} {R : Type u_2} (p : P) (x : ℕ) : Formula P R
• rel {P : Type u_1} {R : Type u_2} (r : R) (x y : ℕ) : Formula P R
• valued {P : Type u_1} {R : Type u_2} (x : ℕ) : Formula P R
• not {P : Type u_1} {R : Type u_2} (φ : Formula P R) : Formula P R
• and {P : Type u_1} {R : Type u_2} (φ ψ : Formula P R) : Formula P R
• or {P : Type u_1} {R : Type u_2} (φ ψ : Formula P R) : Formula P R
• ex {P : Type u_1} {R : Type u_2} (x : ℕ) (φ : Formula P R) : Formula P R
• all {P : Type u_1} {R : Type u_2} (x : ℕ) (φ : Formula P R) : Formula P R
• strong {P : Type u_1} {R : Type u_2} (φ : Formula P R) : Formula P R

structure Spector2026.Model (W : Type u_1) (D : Type u_2) (P : Type u_3) (R : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A model gives the extensions of the predicates at each world.

• pred : P → W → Set D
• rel : R → W → Set (D × D)

def Spector2026.Formula.binders {P : Type u_1} {R : Type u_2} : Formula P R → List ℕ

The variables an existential binds, for the Novelty Condition.

Equations

• (Spector2026.Formula.pred p x_1).binders = []
• (Spector2026.Formula.rel r x_1 y).binders = []
• (Spector2026.Formula.valued x_1).binders = []
• φ.not.binders = φ.binders
• (φ.and ψ).binders = φ.binders ++ ψ.binders
• (φ.or ψ).binders = φ.binders ++ ψ.binders
• (Spector2026.Formula.ex x_1 φ).binders = x_1 :: φ.binders
• (Spector2026.Formula.all x_1 φ).binders = φ.binders
• φ.strong.binders = φ.binders

def Spector2026.Novel {P : Type u_1} {R : Type u_2} (S : List (Formula P R)) : Prop

The Novelty Condition requires that no existential bind the same variable twice across a discourse.

Equations

• Spector2026.Novel S = (List.flatMap Spector2026.Formula.binders S).Nodup

The simplified system: partial assignments

theorem Spector2026.conj_transparency_parametric (E presup φ : SignType) (hw : E = 1 → presup = 1) : E.meetMiddle (presup.meetMiddle φ) = E.meetMiddle φ

Whenever the first conjunct's truth guarantees the presupposition, the presupposition can be dropped from the second conjunct, the parametric core of Transparency for conjunction.

theorem Spector2026.disj_transparency_parametric (negE presup φ : SignType) (hw : negE = -1 → presup = 1) : negE.joinMiddle (presup.meetMiddle φ) = negE.joinMiddle φ

Whenever the first disjunct's falsity guarantees the presupposition, the presupposition can be dropped from the second disjunct, the parametric core of Transparency for disjunction.

noncomputable def Spector2026.eval {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} (M : Model W D P R) : Formula P R → W → PartialAssign ℕ D → SignType

Evaluation at a world and a partial assignment. A predicate of an unvalued variable is undefined; the existential is true when its scope is, false when every value falsifies the scope, undefined otherwise. The universal and the strong-truth operator belong to the full system and are left undefined here.

Equations

• Spector2026.eval M (Spector2026.Formula.pred p x_3) x✝¹ x✝ = match x✝ x_3 with | none => 0 | some d => SignType.ofProp (d ∈ M.pred p x✝¹)
• Spector2026.eval M (Spector2026.Formula.rel r x_3 y) x✝¹ x✝ = match x✝ x_3, x✝ y with | some a, some b => SignType.ofProp ((a, b) ∈ M.rel r x✝¹) | x, x_1 => 0
• Spector2026.eval M (Spector2026.Formula.valued x_3) x✝¹ x✝ = match x✝ x_3 with | none => -1 | some val => 1
• Spector2026.eval M φ.not x✝¹ x✝ = -Spector2026.eval M φ x✝¹ x✝
• Spector2026.eval M (φ.and ψ) x✝¹ x✝ = (Spector2026.eval M φ x✝¹ x✝).meetMiddle (Spector2026.eval M ψ x✝¹ x✝)
• Spector2026.eval M (φ.or ψ) x✝¹ x✝ = (Spector2026.eval M φ x✝¹ x✝).joinMiddle (Spector2026.eval M ψ x✝¹ x✝)
• Spector2026.eval M (Spector2026.Formula.ex x_3 φ) x✝¹ x✝ = if Spector2026.eval M φ x✝¹ x✝ = 1 then 1 else if ∀ (a : D), Spector2026.eval M φ x✝¹ (x✝.update x_3 a) = -1 then -1 else 0
• Spector2026.eval M (Spector2026.Formula.all x_3 φ) x✝¹ x✝ = 0
• Spector2026.eval M φ.strong x✝¹ x✝ = 0

def Spector2026.TrueAt {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} (M : Model W D P R) (φ : Formula P R) (w : W) : Prop

A sentence is true at a world when some assignment makes it true.

Equations

• Spector2026.TrueAt M φ w = ∃ (g : PartialAssign ℕ D), Spector2026.eval M φ w g = 1

theorem Spector2026.eval_pred_of_eq_bot {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {g : PartialAssign ℕ D} (h : g x = ⊥) : eval M (Formula.pred p x) w g = 0

theorem Spector2026.eval_pred_of_eq_coe {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {g : PartialAssign ℕ D} {d : D} (h : g x = ↑d) : eval M (Formula.pred p x) w g = SignType.ofProp (d ∈ M.pred p w)

theorem Spector2026.eval_pred_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {g : PartialAssign ℕ D} : eval M (Formula.pred p x) w g = 1 ↔ ∃ (d : D), g x = ↑d ∧ d ∈ M.pred p w

theorem Spector2026.eval_pred_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {g : PartialAssign ℕ D} : eval M (Formula.pred p x) w g = -1 ↔ ∃ (d : D), g x = ↑d ∧ d ∉ M.pred p w

theorem Spector2026.eval_valued_of_ne_bot {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {g : PartialAssign ℕ D} (h : g x ≠ ⊥) : eval M (Formula.valued x) w g = 1

theorem Spector2026.eval_valued_of_eq_bot {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {g : PartialAssign ℕ D} (h : g x = ⊥) : eval M (Formula.valued x) w g = -1

@[simp]

theorem Spector2026.eval_valued_bot {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (x : ℕ) (w : W) : eval M (Formula.valued x) w ⊥ = -1

theorem Spector2026.eval_not {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ : Formula P R} {w : W} {g : PartialAssign ℕ D} : eval M φ.not w g = -eval M φ w g

theorem Spector2026.eval_and {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ ψ : Formula P R} {w : W} {g : PartialAssign ℕ D} : eval M (φ.and ψ) w g = (eval M φ w g).meetMiddle (eval M ψ w g)

theorem Spector2026.eval_or {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ ψ : Formula P R} {w : W} {g : PartialAssign ℕ D} : eval M (φ.or ψ) w g = (eval M φ w g).joinMiddle (eval M ψ w g)

theorem Spector2026.eval_ex_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {φ : Formula P R} {w : W} {g : PartialAssign ℕ D} : eval M (Formula.ex x φ) w g = 1 ↔ eval M φ w g = 1

The existential is true exactly when its scope is, since the assignment supplies the witness.

theorem Spector2026.eval_ex_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {φ : Formula P R} {w : W} {g : PartialAssign ℕ D} : eval M (Formula.ex x φ) w g = -1 ↔ eval M φ w g ≠ 1 ∧ ∀ (a : D), eval M φ w (g.update x a) = -1

The existential is false exactly when its scope is not true and every value falsifies it, the classical falsity condition.

theorem Spector2026.ne_bot_of_eval_ex_pred {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {g : PartialAssign ℕ D} (h : eval M (Formula.ex x (Formula.pred p x)) w g = 1) : g x ≠ ⊥

A true existential over a predicate values its variable.

Truth conditions

theorem Spector2026.trueAt_conj_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (T Q : P) (x : ℕ) (w : W) : TrueAt M ((Formula.ex x (Formula.pred T x)).and (Formula.pred Q x)) w ↔ ∃ d ∈ M.pred T w, d ∈ M.pred Q w

A table is in the room and it is purple is true at a world exactly when some individual is both, the classical reading of ∃x(T(x) ∧ P(x)).

theorem Spector2026.trueAt_bathroom_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (B F : P) (x : ℕ) (w : W) : TrueAt M ((Formula.ex x (Formula.pred B x)).not.or (Formula.pred F x)) w ↔ (∀ (d : D), d ∉ M.pred B w) ∨ ∃ d ∈ M.pred B w, d ∈ M.pred F w

The bathroom sentence ¬∃xB(x) ∨ F(x) is true at a world exactly when either no individual is a bathroom or some bathroom is upstairs, the classical reading of ¬∃xB(x) ∨ ∃x(B(x) ∧ F(x)).

Contexts and Transparency

Contexts are sets of pairs of a world and an assignment, singular in the simplified system and plural in the full one; update, Transparency and felicity are defined once over the evaluation ev of either system.

def Spector2026.nullCtx {W : Type u_1} {A : Type u_5} : Set (W × A)

The null context, all world–assignment pairs.

Equations

• Spector2026.nullCtx = Set.univ

def Spector2026.update {W : Type u_1} {P : Type u_3} {R : Type u_4} {A : Type u_5} (ev : Formula P R → W → A → SignType) (C : Set (W × A)) (φ : Formula P R) : Set (W × A)

Stalnakerian update keeps the pairs of the context at which the accepted sentence is true.

Equations

• Spector2026.update ev C φ = {p : W × A | p ∈ C ∧ ev φ p.1 p.2 = 1}

theorem Spector2026.isClassical_update {W : Type u_1} {P : Type u_3} {R : Type u_4} {A : Type u_5} (ev : Formula P R → W → A → SignType) (φ : Formula P R) : DynamicSemantics.CCP.IsClassical fun (x : Set (W × A)) => update ev x φ

Update intersects the context with the sentence's truth set, so it eliminates points and does so point by point.

@[reducible, inline]

abbrev Spector2026.Frame (P : Type u_6) (R : Type u_7) : Type (max u_7 u_6)

A frame is a sentence with the occurrence under test as a hole.

Equations

• Spector2026.Frame P R = (Spector2026.Formula P R → Spector2026.Formula P R)

def Spector2026.Transparent {W : Type u_1} {P : Type u_3} {R : Type u_4} {A : Type u_5} (ev : Formula P R → W → A → SignType) (C : Set (W × A)) (F : Frame P R) (π : Formula P R) : Prop

The occurrence at the hole of F is transparent in C for the presupposition π when filling the hole with π ∧ φ and with φ gives the same value throughout C, for every φ (§2.2.2; in the full system §6.3, where π reads as atomic(x)).

Equations

• Spector2026.Transparent ev C F π = ∀ (φ : Spector2026.Formula P R), ∀ p ∈ C, ev (F (π.and φ)) p.1 p.2 = ev (F φ) p.1 p.2

theorem Spector2026.not_transparent_id_null {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty W] (x : ℕ) : ¬Transparent (eval M) nullCtx id (Formula.valued x)

A bare pronoun is not transparent in the null context, since where the variable is unvalued valued(x) ∧ φ is false while φ may be true.

theorem Spector2026.transparent_id_of_valued {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {C : Set (W × PartialAssign ℕ D)} {x : ℕ} (hC : ∀ p ∈ C, p.2 x ≠ ⊥) : Transparent (eval M) C id (Formula.valued x)

A bare pronoun is transparent wherever the context values its variable.

theorem Spector2026.ne_bot_of_mem_update_ex {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {C : Set (W × PartialAssign ℕ D)} {T : P} {x : ℕ} {p : W × PartialAssign ℕ D} (hp : p ∈ update (eval M) C (Formula.ex x (Formula.pred T x))) : p.2 x ≠ ⊥

Accepting ∃xT(x) leaves x valued throughout the updated context.

theorem Spector2026.transparent_id_of_update_ex {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PartialAssign ℕ D)) (T : P) (x : ℕ) : Transparent (eval M) (update (eval M) C (Formula.ex x (Formula.pred T x))) id (Formula.valued x)

In A table is in the room. It is purple. the pronoun is transparent after the accepted existential.

theorem Spector2026.transparent_forward_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PartialAssign ℕ D)) (T : P) (x : ℕ) : Transparent (eval M) C (fun (ψ : Formula P R) => (Formula.ex x (Formula.pred T x)).and ψ) (Formula.valued x)

∃xT(x) ∧ P(x) is transparent in every context, because a true first conjunct values x.

theorem Spector2026.not_transparent_reverse_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty W] (T : P) (x : ℕ) : ¬Transparent (eval M) nullCtx (fun (ψ : Formula P R) => ψ.and (Formula.ex x (Formula.pred T x))) (Formula.valued x)

P(x) ∧ ∃xT(x) is not transparent in the null context, because with φ = P(x) at an unvalued variable the plain sentence is undefined and the presuppositional one false.

theorem Spector2026.transparent_bathroom {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PartialAssign ℕ D)) (B : P) (x : ℕ) : Transparent (eval M) C (fun (ψ : Formula P R) => (Formula.ex x (Formula.pred B x)).not.or ψ) (Formula.valued x)

The bathroom sentence ¬∃xB(x) ∨ H(x) is transparent in every context, because a false first disjunct is a true existential, which values x.

theorem Spector2026.not_transparent_reverse_bathroom {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (B : P) (x : ℕ) (hw : ∃ (w : W) (d : D), d ∈ M.pred B w) : ¬Transparent (eval M) nullCtx (fun (ψ : Formula P R) => ψ.or (Formula.ex x (Formula.pred B x)).not) (Formula.valued x)

The reversed bathroom sentence H(x) ∨ ¬∃xB(x) is not transparent in the null context, since with a tautological φ and an unvalued variable, at a world with a bathroom the plain sentence is true and the presuppositional one undefined.

The Transparency Condition for sentences and discourses

def Spector2026.Formula.occurrences {P : Type u_5} {R : Type u_6} : List ℕ → Formula P R → List (Frame P R × Formula P R)

The occurrences of free variables in the atoms of a formula, below the variables B bound above them. Each is the frame holing the atom, paired with the presupposition tested there, which is valued(x) for each free argument and valued(x) ∧ valued(y) for a relation whose two arguments are free (§2.2.2, items 1–2).

Equations

• One or more equations did not get rendered due to their size.
• Spector2026.Formula.occurrences x✝ (Spector2026.Formula.pred p x_2) = if x_2 ∈ x✝ then [] else [(id, Spector2026.Formula.valued x_2)]
• Spector2026.Formula.occurrences x✝ (Spector2026.Formula.valued x_3) = []

def Spector2026.Felicitous {W : Type u_1} {P : Type u_3} {R : Type u_4} {A : Type u_5} (ev : Formula P R → W → A → SignType) (C : Set (W × A)) (S : Formula P R) : Prop

A sentence is felicitous in C when Transparency holds in C at every occurrence of every free variable (§2.2.2, item 4; §6.3).

Equations

• Spector2026.Felicitous ev C S = ∀ o ∈ Spector2026.Formula.occurrences [] S, Spector2026.Transparent ev C o.1 o.2

def Spector2026.FelicitousDiscourse {W : Type u_1} {P : Type u_3} {R : Type u_4} {A : Type u_5} (ev : Formula P R → W → A → SignType) (C : Set (W × A)) : List (Formula P R) → Prop

A discourse is felicitous in C when each sentence is felicitous in the context updated with the sentences before it (§2.2.1, fn. 21).

Equations

• Spector2026.FelicitousDiscourse ev C [] = True
• Spector2026.FelicitousDiscourse ev C (S :: Ss) = (Spector2026.Felicitous ev C S ∧ Spector2026.FelicitousDiscourse ev (Spector2026.update ev C S) Ss)

theorem Spector2026.not_felicitous_pred_null {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty W] (Q : P) (x : ℕ) : ¬Felicitous (eval M) nullCtx (Formula.pred Q x)

It is purple out of the blue is infelicitous (§3.1).

theorem Spector2026.felicitousDiscourse_ex_pred {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PartialAssign ℕ D)) (T Q : P) (x : ℕ) : FelicitousDiscourse (eval M) C [Formula.ex x (Formula.pred T x), Formula.pred Q x]

A table is in the room. It is purple. is felicitous in every context (§3.1).

theorem Spector2026.felicitous_forward_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PartialAssign ℕ D)) (T Q : P) (x : ℕ) : Felicitous (eval M) C ((Formula.ex x (Formula.pred T x)).and (Formula.pred Q x))

A table is in the room and it is purple is felicitous in every context ((9)).

theorem Spector2026.not_felicitous_reverse_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty W] (T Q : P) (x : ℕ) : ¬Felicitous (eval M) nullCtx ((Formula.pred Q x).and (Formula.ex x (Formula.pred T x)))

It is purple and a table is in the room is infelicitous in the null context ((10)).

theorem Spector2026.felicitous_bathroom {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PartialAssign ℕ D)) (B H : P) (x : ℕ) : Felicitous (eval M) C ((Formula.ex x (Formula.pred B x)).not.or (Formula.pred H x))

The bathroom sentence is felicitous in every context ((11)).

theorem Spector2026.not_felicitous_reverse_bathroom {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (B H : P) (x : ℕ) (hw : ∃ (w : W) (d : D), d ∈ M.pred B w) : ¬Felicitous (eval M) nullCtx ((Formula.pred H x).or (Formula.ex x (Formula.pred B x)).not)

The reversed bathroom sentence is infelicitous in the null context, where there could be a bathroom ((12)).

Novelty

theorem Spector2026.eval_and_ex_ex_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (p q : P) (x : ℕ) (w : W) (g : PartialAssign ℕ D) : eval M ((Formula.ex x (Formula.pred p x)).and (Formula.ex x (Formula.pred q x))) w g = 1 ↔ eval M (Formula.ex x ((Formula.pred p x).and (Formula.pred q x))) w g = 1

A repeated existential means the same as one existential over the conjunction, which is never the reading of someone smokes; someone drinks.

theorem Spector2026.not_novel_repeat {P : Type u_3} {R : Type u_4} (p q : P) (x : ℕ) : ¬Novel [Formula.ex x (Formula.pred p x), Formula.ex x (Formula.pred q x)]

The Novelty Condition rules the repeated existential out.

theorem Spector2026.novel_fresh {P : Type u_3} {R : Type u_4} (p q : P) {x y : ℕ} (hxy : x ≠ y) : Novel [Formula.ex x (Formula.pred p x), Formula.ex y (Formula.pred q y)]

Existentials over fresh variables satisfy the Novelty Condition.

theorem Spector2026.not_novel_of_mem_binders {P : Type u_3} {R : Type u_4} {S₁ S₂ : Formula P R} {x : ℕ} (h₁ : x ∈ S₁.binders) (h₂ : x ∈ S₂.binders) : ¬Novel [S₁, S₂]

A variable bound by an existential in two sentences of a discourse violates Novelty.

theorem Spector2026.not_novel_16 {P : Type u_3} {R : Type u_4} (L φ ψ : Formula P R) (x : ℕ) : ¬Novel [L.or (Formula.ex x φ), Formula.ex x ψ]

Either the room is locked, or a female guitarist is playing. A woman is singing. cannot reuse the indefinite's variable ((16)).

theorem Spector2026.not_novel_stone {P : Type u_3} {R : Type u_4} (T A E : P) (x : ℕ) : ¬Novel [(Formula.ex x (Formula.pred T x)).or (Formula.ex x (Formula.pred A x)), Formula.pred E x]

A Stone disjunction with one variable, Matt bought a train ticket or an airplane ticket. It was expensive., violates Novelty (fn. 15).

The failure of covariation

theorem Spector2026.trueAt_notExNotEx_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty D] (S : R) {x y : ℕ} (hxy : x ≠ y) (w : W) : TrueAt M (Formula.ex x (Formula.ex y (Formula.rel S x y)).not).not w ↔ ∃ (b : D), ∀ (a : D), (a, b) ∈ M.rel S w

In the simplified system ¬∃x¬∃yS(x, y) is true at a world exactly when some one individual is spoken to by everyone, so the embedded existential takes wide scope.

The full system: plural assignments

noncomputable def Spector2026.evalP {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} (M : Model W D P R) : Formula P R → W → PluralAssign ℕ D → SignType

Evaluation at a world and a plural assignment. A predicate of a variable is defined when the assignments valuing the variable agree, and valued now reads as the paper's atomic; the existential is false only when the plural assignment covers the domain and every restriction falsifies the scope; the universal is true under that coverage when every restriction verifies the scope; the strong-truth operator is true when its argument is true here and false at no plural assignment, false when its argument is false here and true at no plural assignment.

Equations

• One or more equations did not get rendered due to their size.
• Spector2026.evalP M (Spector2026.Formula.pred p x_3) x✝¹ x✝ = if ∃ (d : D), x✝.SingularAt x_3 d ∧ d ∈ M.pred p x✝¹ then 1 else if ∃ (d : D), x✝.SingularAt x_3 d ∧ d ∉ M.pred p x✝¹ then -1 else 0
• Spector2026.evalP M (Spector2026.Formula.valued x_3) x✝¹ x✝ = SignType.ofProp (x✝.Singular x_3)
• Spector2026.evalP M φ.not x✝¹ x✝ = -Spector2026.evalP M φ x✝¹ x✝
• Spector2026.evalP M (φ.and ψ) x✝¹ x✝ = (Spector2026.evalP M φ x✝¹ x✝).meetMiddle (Spector2026.evalP M ψ x✝¹ x✝)
• Spector2026.evalP M (φ.or ψ) x✝¹ x✝ = (Spector2026.evalP M φ x✝¹ x✝).joinMiddle (Spector2026.evalP M ψ x✝¹ x✝)

def Spector2026.TrueAtP {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} (M : Model W D P R) (φ : Formula P R) (w : W) : Prop

A sentence is weakly true at a world when some plural assignment makes it true.

Equations

• Spector2026.TrueAtP M φ w = ∃ (G : PluralAssign ℕ D), Spector2026.evalP M φ w G = 1

def Spector2026.StronglyTrueAt {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} (M : Model W D P R) (φ : Formula P R) (w : W) : Prop

A sentence is strongly true at a world when some plural assignment makes it true and none makes it false.

Equations

• Spector2026.StronglyTrueAt M φ w = (Spector2026.TrueAtP M φ w ∧ ∀ (G : PluralAssign ℕ D), Spector2026.evalP M φ w G ≠ -1)

theorem Spector2026.StronglyTrueAt.trueAtP {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ : Formula P R} {w : W} (h : StronglyTrueAt M φ w) : TrueAtP M φ w

theorem Spector2026.evalP_pred_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.pred p x) w G = 1 ↔ ∃ (d : D), G.SingularAt x d ∧ d ∈ M.pred p w

theorem Spector2026.evalP_pred_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.pred p x) w G = -1 ↔ ∃ (d : D), G.SingularAt x d ∧ d ∉ M.pred p w

theorem Spector2026.evalP_rel_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {r : R} {x y : ℕ} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.rel r x y) w G = 1 ↔ ∃ (a : D) (b : D), G.SingularAt x a ∧ G.SingularAt y b ∧ (a, b) ∈ M.rel r w

theorem Spector2026.evalP_rel_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {r : R} {x y : ℕ} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.rel r x y) w G = -1 ↔ ∃ (a : D) (b : D), G.SingularAt x a ∧ G.SingularAt y b ∧ (a, b) ∉ M.rel r w

theorem Spector2026.evalP_valued_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.valued x) w G = 1 ↔ G.Singular x

theorem Spector2026.evalP_valued_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.valued x) w G = -1 ↔ ¬G.Singular x

theorem Spector2026.evalP_not {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M φ.not w G = -evalP M φ w G

theorem Spector2026.evalP_and {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ ψ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M (φ.and ψ) w G = (evalP M φ w G).meetMiddle (evalP M ψ w G)

theorem Spector2026.evalP_or {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ ψ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M (φ.or ψ) w G = (evalP M φ w G).joinMiddle (evalP M ψ w G)

theorem Spector2026.evalP_ex_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {φ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.ex x φ) w G = 1 ↔ evalP M φ w G = 1

theorem Spector2026.evalP_ex_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {φ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.ex x φ) w G = -1 ↔ evalP M φ w G ≠ 1 ∧ ∀ (a : D), Set.Nonempty (G.restrict x a) ∧ evalP M φ w (G.restrict x a) = -1

theorem Spector2026.evalP_all_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {φ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.all x φ) w G = 1 ↔ ∀ (a : D), Set.Nonempty (G.restrict x a) ∧ evalP M φ w (G.restrict x a) = 1

theorem Spector2026.evalP_all_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {φ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M (Formula.all x φ) w G = -1 ↔ (∀ (a : D), Set.Nonempty (G.restrict x a)) ∧ ∃ (a : D), evalP M φ w (G.restrict x a) = -1

theorem Spector2026.evalP_strong_eq_true_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M φ.strong w G = 1 ↔ evalP M φ w G = 1 ∧ ∀ (G' : PluralAssign ℕ D), evalP M φ w G' ≠ -1

theorem Spector2026.singular_of_evalP_ex_pred {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {p : P} {x : ℕ} {w : W} {G : PluralAssign ℕ D} (h : evalP M (Formula.ex x (Formula.pred p x)) w G = 1) : G.Singular x

A true existential over a predicate makes its variable atomic.

theorem Spector2026.evalP_strong_eq_false_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ : Formula P R} {w : W} {G : PluralAssign ℕ D} : evalP M φ.strong w G = -1 ↔ evalP M φ w G = -1 ∧ ∀ (G' : PluralAssign ℕ D), evalP M φ w G' ≠ 1

Transparency in the full system

theorem Spector2026.transparentP_forward_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PluralAssign ℕ D)) (T : P) (x : ℕ) : Transparent (evalP M) C (fun (ψ : Formula P R) => (Formula.ex x (Formula.pred T x)).and ψ) (Formula.valued x)

∃xT(x) ∧ P(x) is transparent in every context of the full system.

theorem Spector2026.transparentP_bathroom {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (C : Set (W × PluralAssign ℕ D)) (B : P) (x : ℕ) : Transparent (evalP M) C (fun (ψ : Formula P R) => (Formula.ex x (Formula.pred B x)).not.or ψ) (Formula.valued x)

The bathroom sentence is transparent in every context of the full system.

theorem Spector2026.not_singular_of_covers {D : Type u_2} {G : PluralAssign ℕ D} {x : ℕ} {a b : D} (hab : a ≠ b) (hcov : ∀ (a : D), Set.Nonempty (G.restrict x a)) : ¬G.Singular x

A plural assignment covering a domain with two individuals is not atomic at the covered variable.

theorem Spector2026.not_transparentP_forall_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {a b : D} (hab : a ≠ b) {C : Set (W × PluralAssign ℕ D)} {P₀ : P} {x : ℕ} {w : W} {G : PluralAssign ℕ D} (hC : (w, G) ∈ C) (hall : evalP M (Formula.all x (Formula.pred P₀ x)) w G = 1) : ¬Transparent (evalP M) C (fun (ψ : Formula P R) => (Formula.all x (Formula.pred P₀ x)).and ψ) (Formula.valued x)

A universal does not license a singular pronoun in ∀xP(x) ∧ Q(x). In a context containing a pair at which ∀xP(x) is true, over a domain with two individuals, the occurrence Q(x) is not transparent, because ∀xP(x) ∧ (atomic(x) ∧ φ) is never true there while ∀xP(x) ∧ φ is for a tautological φ.

def Spector2026.covering (D : Type u_2) (x : ℕ) : PluralAssign ℕ D

The plural assignment mapping x to every individual, one row each.

Equations

• Spector2026.covering D x = Set.range (PartialAssign.single x)

theorem Spector2026.restrict_covering_nonempty {D : Type u_2} (x : ℕ) (a : D) : Set.Nonempty ((covering D x).restrict x a)

theorem Spector2026.not_transparentP_forall_conj_univ {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {a b : D} (hab : a ≠ b) {P₀ : P} (x : ℕ) (hw : ∃ (w : W), ∀ (d : D), d ∈ M.pred P₀ w) : ¬Transparent (evalP M) Set.univ (fun (ψ : Formula P R) => (Formula.all x (Formula.pred P₀ x)).and ψ) (Formula.valued x)

The null context contains such a pair whenever some world makes the universal true.

theorem Spector2026.evalP_ex_and_all_ne_true {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {a b : D} (hab : a ≠ b) (P₀ Q : P) (x : ℕ) (w : W) (G : PluralAssign ℕ D) : evalP M ((Formula.ex x (Formula.pred P₀ x)).and (Formula.all x (Formula.pred Q x))) w G ≠ 1

∃xP(x) ∧ ∀xQ(x) is never true over a domain with two individuals, because the existential makes the variable atomic and the universal requires it to cover the domain.

Truth conditions in the full system

theorem Spector2026.trueAtP_bathroom_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (B F : P) (x : ℕ) (w : W) : TrueAtP M ((Formula.ex x (Formula.pred B x)).not.or (Formula.pred F x)) w ↔ (∀ (d : D), d ∉ M.pred B w) ∨ ∃ d ∈ M.pred B w, d ∈ M.pred F w

The bathroom sentence keeps its classical truth conditions in the full system.

def Spector2026.pairing {D : Type u_2} (x y : ℕ) (f : D → D) : PluralAssign ℕ D

The plural assignment pairing each individual a at x with f a at y.

Equations

• Spector2026.pairing x y f = Set.range fun (a : D) => (PartialAssign.single x a).update y (f a)

theorem Spector2026.restrict_pairing {D : Type u_2} {x y : ℕ} (hxy : x ≠ y) (f : D → D) (a : D) : Set.Nonempty ((pairing x y f).restrict x a) ∧ ((pairing x y f).restrict x a).SingularAt y (f a)

A restriction of the pairing to x = a is nonempty and atomic at y with value f a.

theorem Spector2026.trueAtP_notExNotEx_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty D] (S : R) {x y : ℕ} (hxy : x ≠ y) (w : W) : TrueAtP M (Formula.ex x (Formula.ex y (Formula.rel S x y)).not).not w ↔ ∀ (a : D), ∃ (b : D), (a, b) ∈ M.rel S w

In the full system ¬∃x¬∃yS(x, y) is true exactly when everyone spoke to someone, because the embedded existential is evaluated at each restriction, which restores covariation.

theorem Spector2026.trueAtP_allEx_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (S : R) {x y : ℕ} (hxy : x ≠ y) (w : W) : TrueAtP M (Formula.all x (Formula.ex y (Formula.rel S x y))) w ↔ ∀ (a : D), ∃ (b : D), (a, b) ∈ M.rel S w

∀x∃yS(x, y) is true exactly when everyone spoke to someone.

theorem Spector2026.trueAtP_allEx_iff_notExNotEx {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty D] (S : R) {x y : ℕ} (hxy : x ≠ y) (w : W) : TrueAtP M (Formula.all x (Formula.ex y (Formula.rel S x y))) w ↔ TrueAtP M (Formula.ex x (Formula.ex y (Formula.rel S x y)).not).not w

Everybody spoke to someone and not a single person failed to speak to someone are true at the same worlds.

Weak and strong truth

theorem Spector2026.stronglyTrueAt_ex_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (P₀ : P) (x : ℕ) (w : W) : StronglyTrueAt M (Formula.ex x (Formula.pred P₀ x)) w ↔ TrueAtP M (Formula.ex x (Formula.pred P₀ x)) w

On a simple existential, strong truth and weak truth coincide.

theorem Spector2026.trueAtP_not_stronglyTrueAt_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (B F : P) (x : ℕ) (w : W) {b₁ b₂ : D} (h₁ : b₁ ∈ M.pred B w) (h₂ : b₂ ∈ M.pred B w) (hF₁ : b₁ ∈ M.pred F w) (hF₂ : b₂ ∉ M.pred F w) : TrueAtP M ((Formula.ex x (Formula.pred B x)).and (Formula.pred F x)) w ∧ ¬StronglyTrueAt M ((Formula.ex x (Formula.pred B x)).and (Formula.pred F x)) w

There is a bathroom and it is upstairs is weakly but not strongly true at a world with a bathroom upstairs and a bathroom that is not.

theorem Spector2026.trueAtP_strong_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (φ : Formula P R) (w : W) : TrueAtP M φ.strong w ↔ StronglyTrueAt M φ w

Weak truth of O(S) is strong truth of S.

theorem Spector2026.evalP_strong_congr {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {φ ψ : Formula P R} {w : W} (h : ∀ (G : PluralAssign ℕ D), evalP M φ w G = evalP M ψ w G) (G : PluralAssign ℕ D) : evalP M φ.strong w G = evalP M ψ.strong w G

Logically equivalent sentences stay equivalent under O.

theorem Spector2026.evalP_strong_valued {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} [Nonempty D] (x : ℕ) (w : W) (G : PluralAssign ℕ D) : evalP M (Formula.valued x).strong w G = 0

O(atomic(x)) is undefined everywhere, since a singleton plural assignment makes atomic(x) true and the empty one makes it false.

theorem Spector2026.trueAtP_ex_and_strong_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} (S H : P) (x : ℕ) (w : W) : TrueAtP M ((Formula.ex x (Formula.pred S x)).and (Formula.pred H x).strong) w ↔ (∃ (d : D), d ∈ M.pred S w) ∧ ∀ (d : D), d ∈ M.pred H w

∃xS(x) ∧ O(H(x)) means that something is an S and everything is an H.

theorem Spector2026.not_transparentP_ex_and_strong {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {C : Set (W × PluralAssign ℕ D)} {S : P} {x : ℕ} {w : W} {G : PluralAssign ℕ D} (hC : (w, G) ∈ C) (hS : evalP M (Formula.ex x (Formula.pred S x)) w G = 1) : ¬Transparent (evalP M) C (fun (ψ : Formula P R) => (Formula.ex x (Formula.pred S x)).and ψ.strong) (Formula.valued x)

∃xS(x) ∧ O(H(x)) violates Transparency, since at a pair where ∃xS(x) is true a tautological φ makes ∃xS(x) ∧ O(φ) true but ∃xS(x) ∧ O(atomic(x) ∧ φ) undefined.

The Transparency Condition in the full system

theorem Spector2026.evalP_all_congr {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {φ ψ : Formula P R} {G : PluralAssign ℕ D} (h : ∀ (a : D), evalP M φ w (G.restrict x a) = evalP M ψ w (G.restrict x a)) : evalP M (Formula.all x φ) w G = evalP M (Formula.all x ψ) w G

A universal is fixed by the values of its scope at the restrictions.

theorem Spector2026.trueAtP_qs_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x y : ℕ} {w : W} (Rd L : R) (hxy : x ≠ y) : TrueAtP M ((Formula.all x (Formula.ex y (Formula.rel Rd x y))).and (Formula.all x (Formula.rel L x y))) w ↔ ∀ (a : D), ∃ (b : D), (a, b) ∈ M.rel Rd w ∧ (a, b) ∈ M.rel L w

Everyone read something and everyone liked it is true at a world exactly when everyone read something they liked ((27)).

theorem Spector2026.felicitousP_qs {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x y : ℕ} (C : Set (W × PluralAssign ℕ D)) (Rd L : R) (hxy : x ≠ y) : Felicitous (evalP M) C ((Formula.all x (Formula.ex y (Formula.rel Rd x y))).and (Formula.all x (Formula.rel L x y)))

The pronoun of quantificational subordination satisfies Transparency in every context ((28)).

theorem Spector2026.not_felicitousP_forall_conj {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {a b : D} (hab : a ≠ b) {P₀ Q : P} (hw : ∃ (w : W), ∀ (d : D), d ∈ M.pred P₀ w) : ¬Felicitous (evalP M) Set.univ ((Formula.all x (Formula.pred P₀ x)).and (Formula.pred Q x))

Over a domain with two individuals every student came. He … is infelicitous in the null context, because a universal does not license a singular pronoun ((21)–(22)).

theorem Spector2026.evalP_ex_and_not_all_ne_true {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {a b : D} (hab : a ≠ b) (P₀ Q : P) (G : PluralAssign ℕ D) : evalP M ((Formula.ex x (Formula.pred P₀ x)).and (Formula.all x (Formula.pred Q x)).not) w G ≠ 1

A linguist came and not every linguist smiled, with one variable, is never true over a domain with two individuals ((23)).

theorem Spector2026.evalP_all_false_and_not_ex_not_indet {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {a b : D} (hab : a ≠ b) (P₀ : P) (hd : ∃ (d : D), d ∉ M.pred P₀ w) : evalP M (Formula.all x (Formula.pred P₀ x)) w (covering D x) = -1 ∧ evalP M (Formula.ex x (Formula.pred P₀ x).not).not w (covering D x) = 0

∀x P(x) and ¬∃x¬P(x) differ in falsity. Where x covers a domain with two individuals, one of which is not a P, the universal is false and the negated existential undefined (Remark 4).

theorem Spector2026.not_felicitousDiscourseP_not_all {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} {a b : D} (hab : a ≠ b) (P₀ Q : P) (hd : ∃ (d : D), d ∉ M.pred P₀ w) : ¬FelicitousDiscourse (evalP M) Set.univ [(Formula.all x (Formula.pred P₀ x)).not, Formula.pred Q x]

Not every male student came. He stayed home. is infelicitous, because the negated universal makes x cover the domain, so the pronoun's atomicity fails (fn. 19).

Restrictors, donkey sentences, and strong truth

theorem Spector2026.restrict_iUnion_rows {D : Type u_2} {x : ℕ} {rows : D → PluralAssign ℕ D} (h : ∀ (e : D), ∀ g ∈ rows e, g x = ↑e) (e : D) : PluralAssign.restrict (⋃ (e : D), rows e) x e = rows e

Restricting a union of rows, the rows of e all sending x to e, to x = e gives the rows of e.

theorem Spector2026.update_single_apply_left {D : Type u_2} {x y : ℕ} (hxy : x ≠ y) (e v : D) : (PartialAssign.single x e).update y v x = ↑e

theorem Spector2026.trueAtP_qs_restricted_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x y : ℕ} {w : W} [Nonempty D] (S B : P) (Rd L : R) (hxy : x ≠ y) : TrueAtP M ((Formula.all x ((Formula.pred S x).not.or (Formula.ex y ((Formula.pred B y).and (Formula.rel Rd x y))))).and (Formula.all x ((Formula.pred S x).not.or (Formula.rel L x y)))) w ↔ ∀ a ∈ M.pred S w, ∃ b ∈ M.pred B w, (a, b) ∈ M.rel Rd w ∧ (a, b) ∈ M.rel L w

Every student read a book and every student liked it is true at a world exactly when every student read a book they liked ((31)).

theorem Spector2026.felicitousP_qs_restricted {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x y : ℕ} (C : Set (W × PluralAssign ℕ D)) (S B : P) (Rd L : R) (hxy : x ≠ y) : Felicitous (evalP M) C ((Formula.all x ((Formula.pred S x).not.or (Formula.ex y ((Formula.pred B y).and (Formula.rel Rd x y))))).and (Formula.all x ((Formula.pred S x).not.or (Formula.rel L x y))))

The pronoun of every student read a book and every student liked it satisfies Transparency in every context ((32)).

theorem Spector2026.not_felicitousP_qs_everyone {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x y : ℕ} {w : W} {c d : D} (hcd : c ≠ d) (S B : P) (Rd L : R) (hxy : x ≠ y) {e₀ : D} (he₀ : e₀ ∉ M.pred S w) (hS : ∀ s ∈ M.pred S w, ∃ b ∈ M.pred B w, (s, b) ∈ M.rel Rd w) : ¬Felicitous (evalP M) Set.univ ((Formula.all x ((Formula.pred S x).not.or (Formula.ex y ((Formula.pred B y).and (Formula.rel Rd x y))))).and (Formula.all x (Formula.rel L x y)))

The pronoun of every student read a book and everyone liked it fails Transparency in the null context at a world with a non-student where every student read a book, since a plural assignment can leave the non-student's book unsettled ((33)–(34)).

theorem Spector2026.trueAtP_donkey_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x y : ℕ} {w : W} [Nonempty D] (F Dn : P) (O Bt : R) (hxy : x ≠ y) : TrueAtP M (Formula.all x (((Formula.pred F x).and (Formula.ex y ((Formula.pred Dn y).and (Formula.rel O x y)))).not.or (Formula.rel Bt x y))) w ↔ ∀ a ∈ M.pred F w, (∃ d ∈ M.pred Dn w, (a, d) ∈ M.rel O w) → ∃ d ∈ M.pred Dn w, (a, d) ∈ M.rel O w ∧ (a, d) ∈ M.rel Bt w

Every farmer who owns a donkey beats it is weakly true at a world exactly when every farmer who owns a donkey beats a donkey they own, the weak existential reading ((36), §6.7.1).

theorem Spector2026.felicitousP_donkey {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x y : ℕ} (C : Set (W × PluralAssign ℕ D)) (F Dn : P) (O Bt : R) (hxy : x ≠ y) : Felicitous (evalP M) C (Formula.all x (((Formula.pred F x).and (Formula.ex y ((Formula.pred Dn y).and (Formula.rel O x y)))).not.or (Formula.rel Bt x y)))

The pronoun of the donkey sentence satisfies Transparency in every context ((37)–(38), §6.7.2).

theorem Spector2026.trueAtP_not_ex_and_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} (Dk OS BS : P) : TrueAtP M ((Formula.ex x ((Formula.pred Dk x).and (Formula.pred OS x))).and (Formula.pred BS x)).not w ↔ (∀ (d : D), ¬(d ∈ M.pred Dk w ∧ d ∈ M.pred OS w)) ∨ ∃ d ∈ M.pred Dk w, d ∈ M.pred OS w ∧ d ∉ M.pred BS w

It is not true that Sue has a donkey and that she beats it is weakly true at a world exactly when Sue has no donkey or has one she does not beat ((39)–(40)). Sue's owning and beating are rendered as one-place predicates.

theorem Spector2026.stronglyTrueAt_ex_and_iff {W : Type u_1} {D : Type u_2} {P : Type u_3} {R : Type u_4} {M : Model W D P R} {x : ℕ} {w : W} (B F : P) : StronglyTrueAt M ((Formula.ex x (Formula.pred B x)).and (Formula.pred F x)) w ↔ (∃ (d : D), d ∈ M.pred B w) ∧ ∀ d ∈ M.pred B w, d ∈ M.pred F w

Under Strong Truth, there is a bathroom and it is upstairs says that there is a bathroom and every bathroom is upstairs ((47a)).