Local contexts in quantified sentences

A quantifier on van Benthem's tree of numbers holds of a restrictor and a scope according to how many individuals of the restrictor are outside and inside the scope. A predicate in its scope or restrictor denotes a set of world–individual pairs, so the local context of that position is a set of such pairs (scopeTruth, restrictorTruth), and by isLocalContext_of_dependsOn it is the set of pairs on which the sentence's truth value depends. At a world, a quantifier depends on whether an individual is in its scope iff the individual is in the restrictor and the quantifier is not constant on the row of the restrictor's size (Quantifier.NumberTree.dependsOn_toGQ_compl_singleton_iff). So the local context of the nuclear scope is the restrictor's individuals at the worlds of the context where that row is not constant (isLocalContext_scopeTruth): a presupposition triggered in the scope projects universally over the restrictor, except at worlds where the sentence's truth value does not depend on its scope at all (transparent_scopeTruth_iff). A trigger in the scope is transparent at its own assertion iff the quantifier gives one value to every scope that resolves the trigger, at each world of the context (transparentAt_scopeTruth_iff). With every scope as a continuation, as the incremental theory has it, the local context of the restrictor is every individual unless the quantifier is constant on the whole triangle below the size of the universe, and a presupposition triggered in the restrictor projects universally over the domain (transparent_restrictorTruth_iff).

These are Schlenker's derivations of universal projection, in Anti-Dynamics and in Local Contexts, stated world by world. The conditions under which those papers prove them, that the restrictor and the domain have constant sizes across the context and that the quantifier is not constant on the relevant points of the tree there, become the condition at each world under which the presupposition is required.

Main results

• isLocalContext_scopeTruth, transparent_scopeTruth_iff: universal projection from the nuclear scope.
• transparentAt_scopeTruth_iff: definedness by supervaluation of a trigger in the nuclear scope.
• isLocalContext_restrictorTruth, transparent_restrictorTruth_iff: universal projection from the restrictor, with every scope as a continuation.

Implementation notes

The domain is a finite type, the same at every world, and the quantifier is the same at every world. A predicate's denotation is a set of world–individual pairs, the two-place intension of the appendix of Local Contexts.

References

• [vB84]
• [Sch07]
• [Sch09a]

def Presupposition.scopeTruth {W : Type u_1} {E : Type u_2} (q : Quantifier.NumberTree) (A : W → E → Prop) (d : Set (W × E)) : Set W

The truth set of (Q A. _), as a function of the denotation of its scope, is the set of worlds at which q holds of the restrictor and of the scope's individuals there.

Equations

• Presupposition.scopeTruth q A d = {w : W | q.toGQ (A w) fun (e : E) => (w, e) ∈ d}

def Presupposition.restrictorTruth {W : Type u_1} {E : Type u_2} (q : Quantifier.NumberTree) (B : W → E → Prop) (d : Set (W × E)) : Set W

The truth set of (Q _. B) as a function of the denotation of its restrictor.

Equations

• Presupposition.restrictorTruth q B d = {w : W | q.toGQ (fun (e : E) => (w, e) ∈ d) (B w)}

theorem Presupposition.dependsOn_slice_iff {W : Type u_1} {E : Type u_2} {w v : W} {e : E} {g : (E → Prop) → Prop} : DependsOn (fun (d : Set (W × E)) => g fun (x : E) => (w, x) ∈ d) {(v, e)}ᶜ ↔ v = w → DependsOn g {e}ᶜ

A truth value at w that is a function of the individuals at w depends on the pair (v, e) iff v is w and the function depends on e.

theorem Presupposition.dependsOn_slice {W : Type u_1} {E : Type u_2} [Finite E] (w : W) (g : (E → Prop) → Prop) : ∃ (s : Set (W × E)), s.Finite ∧ DependsOn (fun (d : Set (W × E)) => g fun (x : E) => (w, x) ∈ d) s

A truth value at w that is a function of the individuals at w depends on finitely many pairs.

theorem Presupposition.transparentAt_scopeTruth_iff {W : Type u_1} {E : Type u_2} {q : Quantifier.NumberTree} {A : W → E → Prop} {C : Set W} {P a : Set (W × E)} : TransparentAt C {scopeTruth q A} P a ↔ ∀ w ∈ C, ∀ (D D' : E → Prop), (∀ (e : E), (w, e) ∈ P → (D e ↔ (w, e) ∈ a)) → (∀ (e : E), (w, e) ∈ P → (D' e ↔ (w, e) ∈ a)) → (q.toGQ (A w) D ↔ q.toGQ (A w) D')

A trigger in the nuclear scope that presupposes P and asserts a is transparent at a iff at each world of the context the quantifier gives one value to every scope that agrees with a on the individuals that satisfy P there.

The nuclear scope

theorem Presupposition.isLocalContext_scopeTruth {W : Type u_1} {E : Type u_2} [Finite E] (q : Quantifier.NumberTree) (A : W → E → Prop) (C : Set W) : IsLocalContext C {scopeTruth q A} {p : W × E | p.1 ∈ C ∧ A p.1 p.2 ∧ ¬q.ConstantOnRow {x : E | A p.1 x}.ncard}

The local context of the nuclear scope of (Q A. _) is the individuals of the restrictor, at the worlds of the context where q is not constant on the row of the restrictor's size.

theorem Presupposition.transparent_scopeTruth_iff {W : Type u_1} {E : Type u_2} [Finite E] (q : Quantifier.NumberTree) {C : Set W} {A : W → E → Prop} {P : Set (W × E)} : Transparent C {scopeTruth q A} P ↔ ∀ w ∈ C, ¬q.ConstantOnRow {x : E | A w x}.ncard → ∀ (e : E), A w e → (w, e) ∈ P

A presupposition triggered in the nuclear scope projects universally over the restrictor. It is transparent iff at each world of the context where q is not constant on the row of the restrictor's size, every individual of the restrictor satisfies it.

The restrictor

theorem Presupposition.isLocalContext_restrictorTruth {W : Type u_1} {E : Type u_2} [Finite E] (q : Quantifier.NumberTree) (C : Set W) : IsLocalContext C (Set.range (restrictorTruth q)) {p : W × E | p.1 ∈ C ∧ ¬q.ConstantBelow (Nat.card E)}

With every scope as a continuation, the local context of the restrictor is every individual at every world of the context, unless q is constant below the size of the universe.

theorem Presupposition.transparent_restrictorTruth_iff {W : Type u_1} {E : Type u_2} [Finite E] (q : Quantifier.NumberTree) {C : Set W} {P : Set (W × E)} : Transparent C (Set.range (restrictorTruth q)) P ↔ ¬q.ConstantBelow (Nat.card E) → ∀ w ∈ C, ∀ (e : E), (w, e) ∈ P

A presupposition triggered in the restrictor, with every scope as a continuation, projects universally over the domain. It is transparent iff every individual satisfies it at each world of the context, unless q is constant below the size of the universe.