Transparency and local contexts

Schlenker defines transparency and local contexts on syntactic environments. A syntactic environment is represented by the set of functions from the denotation of its gap to the sentence's truth set, one for each continuation of the string that the theory consults. A restriction x on the gap is transparent in a context set C when restricting any denotation of the gap by x changes the sentence's truth value at no world of C, for every such function (Transparent). The local context is the least transparent restriction (IsLocalContext), and a presupposition is satisfied when it is entailed by the local context (Satisfied).

A restriction is transparent iff at each world of the context, under each continuation, the sentence's truth value factors through restricting the gap by it (transparent_iff_factorsThrough). When the gap denotes a set of indices, worlds for a clause or world–individual pairs for a predicate, this is dependence: the truth value depends only on the gap's denotation within the restriction (transparent_iff_dependsOn). The local context is then the set of indices on which the truth value depends at some world of the context under some continuation, and it exists whenever each of these truth values depends on finitely many indices (isLocalContext_of_dependsOn). In the propositional case every environment is truth-functional, the truth value at a world depending only on the gap's value there (IsTruthFunctional), so the local context is the set of worlds of the context at which the truth value depends on the gap for some continuation (isLocalContext_of_isTruthFunctional).

A restriction is transparent at an assertion when it is transparent for the denotations of the gap that agree with that assertion on it (TransparentAt), the resolutions of a trigger that presupposes the restriction and asserts the assertion. Transparency at the trigger's own assertion is the trigger's definedness by supervaluation, every resolution giving the sentence the same truth value (transparentAt_iff), and transparency is transparency at every assertion (transparent_iff_forall_transparentAt).

A restriction is stably transparent when it never settles the truth value across a set of continuations unless the unrestricted gap settles it the same way (StablyTransparent), the condition Kalomoiros's Limited Symmetry imposes at each parsing point after a trigger. It is weaker than transparency, and the two coincide for a single continuation, so that transparency is stable transparency for each continuation alone (transparent_iff_forall_stablyTransparent_singleton). Transparency, unlike stability, is unchanged when the gap is negated (transparent_image_compl_iff).

Main definitions

• Presupposition.Transparent: a transparent restriction of a gap.
• Presupposition.IsLocalContext: the least transparent restriction.
• Presupposition.Satisfied: satisfaction of a presupposition in the local context.
• Presupposition.TransparentAt: transparency for the resolutions of a trigger.
• Presupposition.StablyTransparent: a restriction that settles no truth value the gap leaves open.

Main results

• Presupposition.transparent_iff_forall_transparentAt, Presupposition.transparentAt_iff: transparency is definedness by supervaluation at every assertion.
• Presupposition.transparent_iff_factorsThrough: the truth value factors through the restriction.
• Presupposition.transparent_iff_dependsOn: transparency is dependence.
• Presupposition.transparent_iff_forall_stablyTransparent_singleton: transparency is stable transparency for each continuation alone.
• Presupposition.isLocalContext_of_dependsOn: the local context is the set of indices the truth value depends on.
• Presupposition.IsLocalContext.satisfied_iff_transparent: where the local context exists, satisfaction is transparency.

Implementation notes

The paper states transparency for strings, quantifying over the expressions that may fill the gap; here the gap's denotation ranges over the whole type, which is the paper's Expressivity assumption and the reading that its existence proofs require. The local context is restricted to the context set, so a world outside it constrains nothing.

References

• [Sch09a]
• [Kal23]

def Presupposition.Transparent {W : Type u_1} {α : Type u_2} [SemilatticeInf α] (C : Set W) (env : Set (α → Set W)) (x : α) : Prop

A restriction x on the gap of the environment env is transparent in the context C when restricting any denotation d of the gap by x changes the truth value at no world of C, for every continuation in env.

Equations

• Presupposition.Transparent C env x = ∀ f ∈ env, ∀ (d : α), ∀ w ∈ C, w ∈ f (x ⊓ d) ↔ w ∈ f d

def Presupposition.IsLocalContext {W : Type u_1} {α : Type u_2} [SemilatticeInf α] (C : Set W) (env : Set (α → Set W)) (x : α) : Prop

The local context of the gap of env in C is its least transparent restriction.

Equations

• Presupposition.IsLocalContext C env x = IsLeast {x : α | Presupposition.Transparent C env x} x

theorem Presupposition.Transparent.anti {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env env' : Set (α → Set W)} {x : α} (h : env' ⊆ env) (hx : Transparent C env x) : Transparent C env' x

theorem Presupposition.transparent_iff_forall_singleton {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} : Transparent C env x ↔ ∀ w ∈ C, Transparent {w} env x

Transparency holds in a context iff it holds at each of its worlds.

theorem Presupposition.IsLocalContext.unique {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x y : α} (hx : IsLocalContext C env x) (hy : IsLocalContext C env y) : x = y

def Presupposition.Satisfied {W : Type u_1} {α : Type u_2} [SemilatticeInf α] (C : Set W) (env : Set (α → Set W)) (P : α) : Prop

A presupposition P on the gap of env is satisfied in C when the local context exists and entails it.

Equations

• Presupposition.Satisfied C env P = ∃ (x : α), Presupposition.IsLocalContext C env x ∧ x ≤ P

theorem Presupposition.satisfied_iff {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} (h : IsLocalContext C env x) (P : α) : Satisfied C env P ↔ x ≤ P

theorem Presupposition.transparent_iff_factorsThrough {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} : Transparent C env x ↔ ∀ f ∈ env, ∀ w ∈ C, Function.FactorsThrough (fun (d : α) => w ∈ f d) fun (x_1 : α) => x ⊓ x_1

A restriction is transparent iff at each world of the context, under each continuation, the sentence's truth value factors through restricting the gap by it.

theorem Presupposition.Transparent.mono {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x y : α} (hx : Transparent C env x) (hxy : x ≤ y) : Transparent C env y

A restriction weaker than a transparent one is transparent.

theorem Presupposition.Transparent.inf {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x y : α} (hx : Transparent C env x) (hy : Transparent C env y) : Transparent C env (x ⊓ y)

Transparent restrictions are closed under conjunction (C.13).

theorem Presupposition.IsLocalContext.satisfied_iff_transparent {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} (h : IsLocalContext C env x) (P : α) : Satisfied C env P ↔ Transparent C env P

Where the local context exists, a presupposition is satisfied iff it is transparent.

theorem Presupposition.Satisfied.transparent {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} (h : Satisfied C env x) : Transparent C env x

A satisfied presupposition is transparent.

Transparency at an assertion

def Presupposition.TransparentAt {W : Type u_1} {α : Type u_2} [SemilatticeInf α] (C : Set W) (env : Set (α → Set W)) (x a : α) : Prop

A restriction x on the gap of env is transparent in C at the assertion a when it is transparent for the denotations of the gap that agree with a on x. These are the resolutions of a trigger presupposing x and asserting a, which resolve its presupposition failure either way, so that transparency at a is the definedness of the trigger by supervaluation: every resolution gives the sentence the same truth value at each world of C (transparentAt_iff).

Equations

• Presupposition.TransparentAt C env x a = ∀ f ∈ env, ∀ (d : α), x ⊓ d = x ⊓ a → ∀ w ∈ C, w ∈ f (x ⊓ d) ↔ w ∈ f d

theorem Presupposition.Transparent.transparentAt {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} (h : Transparent C env x) (a : α) : TransparentAt C env x a

theorem Presupposition.transparent_iff_forall_transparentAt {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} : Transparent C env x ↔ ∀ (a : α), TransparentAt C env x a

Transparency is transparency at every assertion: it quantifies over the assertion that supervaluation holds fixed.

theorem Presupposition.transparentAt_iff {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x a : α} : TransparentAt C env x a ↔ ∀ f ∈ env, ∀ (d d' : α), x ⊓ d = x ⊓ a → x ⊓ d' = x ⊓ a → ∀ w ∈ C, w ∈ f d ↔ w ∈ f d'

Transparency at a says that the resolutions of the trigger give the sentence one truth value at each world of the context.

Transparency is dependence

theorem Presupposition.transparent_iff_dependsOn {W : Type u_1} {ι : Type u_3} {C : Set W} {env : Set (Set ι → Set W)} {x : Set ι} : Transparent C env x ↔ ∀ f ∈ env, ∀ w ∈ C, DependsOn (fun (d : Set ι) => w ∈ f d) x

A restriction is transparent iff at each world of the context, under each continuation, the sentence's truth value depends only on the gap's denotation within the restriction.

theorem Presupposition.isLocalContext_of_dependsOn {W : Type u_1} {ι : Type u_3} {C : Set W} {env : Set (Set ι → Set W)} (h : ∀ f ∈ env, ∀ w ∈ C, ∃ (s : Set ι), s.Finite ∧ DependsOn (fun (d : Set ι) => w ∈ f d) s) : IsLocalContext C env {i : ι | ∃ f ∈ env, ∃ w ∈ C, ¬DependsOn (fun (d : Set ι) => w ∈ f d) {i}ᶜ}

If the truth value at each world of the context, under each continuation, depends on finitely many indices, the local context exists: it is the set of indices on which the truth value depends at some world of the context under some continuation.

Negating the gap

theorem Presupposition.transparent_image_compl_iff {W : Type u_1} {β : Type u_3} [BooleanAlgebra β] {C : Set W} {env : Set (β → Set W)} {x : β} : Transparent C ((fun (f : β → Set W) (d : β) => f dᶜ) '' env) x ↔ Transparent C env x

Transparency is invariant under negating the gap. A restriction is transparent for a set of continuations iff it is transparent for the same continuations applied to the gap's negation.

Stable transparency

def Presupposition.StablyTransparent {W : Type u_1} {α : Type u_2} [SemilatticeInf α] (C : Set W) (env : Set (α → Set W)) (x : α) : Prop

A restriction x on the gap is stably transparent in C for a set of continuations when restricting a denotation d by x settles the truth value at a world of C across all of them only where d settles it the same way: wherever every continuation makes the sentence true (false) with x ⊓ d, every continuation makes it true (false) with d.

Equations

• Presupposition.StablyTransparent C env x = ∀ (d : α), ∀ w ∈ C, ((∀ f ∈ env, w ∈ f (x ⊓ d)) → ∀ f ∈ env, w ∈ f d) ∧ ((∀ f ∈ env, w ∉ f (x ⊓ d)) → ∀ f ∈ env, w ∉ f d)

theorem Presupposition.Transparent.stablyTransparent {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} (h : Transparent C env x) : StablyTransparent C env x

theorem Presupposition.stablyTransparent_singleton_iff {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {x : α} {f : α → Set W} : StablyTransparent C {f} x ↔ Transparent C {f} x

For a single continuation, stable transparency is transparency.

theorem Presupposition.transparent_iff_forall_stablyTransparent_singleton {W : Type u_1} {α : Type u_2} [SemilatticeInf α] {C : Set W} {env : Set (α → Set W)} {x : α} : Transparent C env x ↔ ∀ f ∈ env, StablyTransparent C {f} x

Transparency is stable transparency for each continuation alone.

Truth-functional environments

def Presupposition.IsTruthFunctional {W : Type u_1} (f : Set W → Set W) : Prop

A continuation is truth-functional when the sentence's truth value at a world depends only on the gap's truth value there.

Equations

• Presupposition.IsTruthFunctional f = ∀ (w : W) (d d' : Set W), (w ∈ d ↔ w ∈ d') → (w ∈ f d ↔ w ∈ f d')

def Presupposition.DependsAt {W : Type u_1} (f : Set W → Set W) (w : W) : Prop

The sentence's truth value at w depends on the gap of a continuation.

Equations

• Presupposition.DependsAt f w = ¬(w ∈ f Set.univ ↔ w ∈ f ∅)

theorem Presupposition.IsTruthFunctional.mem_iff_of_mem {W : Type u_1} {f : Set W → Set W} (hf : IsTruthFunctional f) {w : W} {d : Set W} (h : w ∈ d) : w ∈ f d ↔ w ∈ f Set.univ

theorem Presupposition.IsTruthFunctional.mem_iff_of_notMem {W : Type u_1} {f : Set W → Set W} (hf : IsTruthFunctional f) {w : W} {d : Set W} (h : w ∉ d) : w ∈ f d ↔ w ∈ f ∅

theorem Presupposition.transparent_iff_subset {W : Type u_1} {C x : Set W} {env : Set (Set W → Set W)} (henv : ∀ f ∈ env, IsTruthFunctional f) : Transparent C env x ↔ C ∩ {w : W | ∃ f ∈ env, DependsAt f w} ⊆ x

A restriction is transparent for truth-functional continuations iff it contains every world of the context at which the truth value depends on the gap for some continuation.

theorem Presupposition.isLocalContext_of_isTruthFunctional {W : Type u_1} {C : Set W} {env : Set (Set W → Set W)} (henv : ∀ f ∈ env, IsTruthFunctional f) : IsLocalContext C env (C ∩ {w : W | ∃ f ∈ env, DependsAt f w})

The local context of truth-functional continuations exists: it is the set of worlds of the context at which the truth value depends on the gap for some continuation.

theorem Presupposition.satisfied_iff_transparent {W : Type u_1} {C : Set W} {env : Set (Set W → Set W)} (henv : ∀ f ∈ env, IsTruthFunctional f) (P : Set W) : Satisfied C env P ↔ Transparent C env P

For truth-functional continuations, a presupposition is satisfied in its local context iff it is a transparent restriction.

theorem Presupposition.stablyTransparent_iff {W : Type u_1} {C x : Set W} {env : Set (Set W → Set W)} (henv : ∀ f ∈ env, IsTruthFunctional f) : StablyTransparent C env x ↔ ∀ w ∈ C, w ∉ x → ((∀ f ∈ env, w ∈ f ∅) → ∀ f ∈ env, w ∈ f Set.univ) ∧ ((∀ f ∈ env, w ∉ f ∅) → ∀ f ∈ env, w ∉ f Set.univ)

A restriction is stably transparent for truth-functional continuations iff at each world of the context outside it, whenever the continuations agree on the truth value with a false gap, they agree on it with a true gap.