The Transparency Principle

@cite{schlenker-2007} @cite{schlenker-2008a} @cite{spector-2025}

Schlenker's Transparency Principle states that a presupposition is felicitous iff it is semantically redundant at its syntactic position. @cite{spector-2025} applies this to anaphora: free variables presuppose they are valued, and Transparency governs whether this presupposition projects.

Core Idea

Given a sentence S containing a presuppositional element at some position, form two sentences:

• S1: replace the element with U(x) ∧ φ (presupposition conjoined)
• S2: replace the element with φ alone

Transparency is satisfied iff S1 and S2 have the same truth value at every world-assignment pair in the context, for every formula φ.

Middle Kleene Connection

The Transparency proofs rely on Middle Kleene truth tables:

• Left-undefined absorbs (both ∧ and ∨)
• Left-defined uses Strong Kleene

This asymmetry is what makes ∃xT(x) ∧ P(x̲) felicitous (Transparency holds) while P(x̲) ∧ ∃xT(x) is infelicitous (Transparency fails).

Assignment types

PartialAssign and PluralAssign are defined in Core.Assignment.

@[reducible, inline]

abbrev Semantics.Presupposition.Transparency.Ctx (W : Type u_2) (D : Type u) : Type (max u_2 u)

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

Equations

• Semantics.Presupposition.Transparency.Ctx W D = (W → Core.PartialAssign D → Prop)

def Semantics.Presupposition.Transparency.nullCtx {W : Type u_1} {D : Type u} : Ctx W D

The null context: all world-assignment pairs. @cite{spector-2025} §2.2.1: "the null context which contains all possible world-assignment pairs."

Equations

• Semantics.Presupposition.Transparency.nullCtx x✝¹ x✝ = True

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

Stalnakerian update: intersect context with sentence's truth set. @cite{spector-2025} §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

• Semantics.Presupposition.Transparency.stalnakerUpdate C S w g = (C w g ∧ S w g = Core.Duality.Truth3.true)

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

Two trivalent sentences agree throughout a context.

Equations

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

@[reducible, inline]

abbrev Semantics.Presupposition.Transparency.Sent (W : Type u_2) (D : Type u) : Type (max u_2 u)

A trivalent sentence over world-assignment pairs.

Equations

• Semantics.Presupposition.Transparency.Sent W D = (W → Core.PartialAssign D → Core.Duality.Truth3)

@[reducible, inline]

abbrev Semantics.Presupposition.Transparency.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

• Semantics.Presupposition.Transparency.Frame W D = (Semantics.Presupposition.Transparency.Sent W D → Semantics.Presupposition.Transparency.Sent W D)

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

The Transparency Principle (symmetric version).

@cite{spector-2025} §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

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

theorem Semantics.Presupposition.Transparency.transparent_of_presup_true {W : Type u_1} {D : Type u} (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 Semantics.Presupposition.Transparency.noveltyCondition (usedVars : List ℕ) (newVar : ℕ) : Prop

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

@cite{spector-2025} §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)).

Equations

• Semantics.Presupposition.Transparency.noveltyCondition usedVars newVar = ¬newVar ∈ usedVars