Quantified presupposition projection

Projection of presuppositions from the scope of quantifiers — the empirically contested corner of projection theory: [Che09a] supports universal projection, [MS15b] argue for existential semantic projection pragmatically strengthened, and [SS17] delimit when each reading surfaces.

Main declarations

• forallPartial — universal quantification, universal projection.
• existsPartialUniv / existsPartialExist — existential quantification with universal vs existential projection; consumers committing to a projection theory pick one explicitly.
• negExistsPartial — negated existential, universal projection.

def Semantics.Presupposition.PartialProp.forallPartial {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Universal presupposition projection: presuppositions project universally from the scope of a universal quantifier.

For ∀x ∈ S, φ(x) where φ(x) is a PartialProp:

• asserts: ∀x ∈ S, assertion(φ(x))
• presupposes: ∀x ∈ S, presup(φ(x))

[Che09a], [Fox13]: presuppositions triggered in the scope of a universal quantifier tend to project universally. ([MS15b] dissent: semantic projection is existential, pragmatically strengthened — cf. [SS17].)

Equations

• Semantics.Presupposition.PartialProp.forallPartial S φ = { presup := fun (w : W) => ∀ (x : α), S x → (φ x).presup w, assertion := fun (w : W) => ∀ (x : α), S x → (φ x).assertion w }

def Semantics.Presupposition.PartialProp.existsPartialUniv {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Existential presupposition projection — universal presup, existential assert.

For ∃x ∈ S, φ(x): presuppositions project universally, but the assertion is existential. This is the projection choice supported experimentally by [Che09a]; whether it is the right default is empirically contested — see [SS17] for conditions under which a non-universal (existential) reading is preferred. Consumers committing to a projection theory should pick existsPartialUniv or existsPartialExist explicitly.

Equations

• Semantics.Presupposition.PartialProp.existsPartialUniv S φ = { presup := fun (w : W) => ∀ (x : α), S x → (φ x).presup w, assertion := fun (w : W) => ∃ (x : α), S x ∧ (φ x).assertion w }

def Semantics.Presupposition.PartialProp.existsPartialExist {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Existential presupposition projection — existential presup, existential assert. The non-universal alternative to existsPartialUniv; see [SS17] for the empirical debate.

Equations

• Semantics.Presupposition.PartialProp.existsPartialExist S φ = { presup := fun (w : W) => ∃ (x : α), S x ∧ (φ x).presup w, assertion := fun (w : W) => ∃ (x : α), S x ∧ (φ x).assertion w }

def Semantics.Presupposition.PartialProp.negExistsPartial {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Negated existential with universal presupposition projection.

For ¬∃x ∈ S, φ(x): equivalent to ∀x ∈ S, ¬φ(x). Presuppositions project universally.

Equations

• Semantics.Presupposition.PartialProp.negExistsPartial S φ = { presup := fun (w : W) => ∀ (x : α), S x → (φ x).presup w, assertion := fun (w : W) => ¬∃ (x : α), S x ∧ (φ x).assertion w }

theorem Semantics.Presupposition.PartialProp.forallPartial_holds {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) (w : W) : holds w (forallPartial S φ) ↔ (∀ (x : α), S x → (φ x).presup w) ∧ ∀ (x : α), S x → (φ x).assertion w

forallPartial holds iff every member satisfies both presupposition and assertion.