@cite{blutner-2000} — Presupposition Projection via Bidirectional OT

@cite{blutner-2000} @cite{van-der-sandt-1992} @cite{geurts-1995}

Some Aspects of Optimality in Natural Language Interpretation. Journal of Semantics 17(3): 189–216.

Overview

Section 4 of @cite{blutner-2000} reconstructs @cite{van-der-sandt-1992}'s and @cite{geurts-1995}'s presupposition projection mechanism within bidirectional OT. The I-principle (interpretation optimality) selects the preferred accommodation site; the Q-principle (production optimality) blocks accommodation when a simpler expression alternative exists.

Two Constraints

• AvoidA (Avoid Accommodation): counts the number of discourse markers that require accommodation. Binding (resolving against existing context) is preferred over accommodation. This captures @cite{van-der-sandt-1992}'s and @cite{geurts-1995}'s first preference (binding > accommodation).

• BeStrong: ranks interpretations by logical strength (entailment). Stronger (more informative) outcomes are preferred. This captures @cite{geurts-1995}'s second preference (higher accommodation site yields stronger interpretation, ceteris paribus).

Ranking: AvoidA >> BeStrong.

Application

Example (18): "If Peter has a dog, then his cat is gray"

Three projection sites for the presupposition "Peter has a cat":

• τ₁ (local): accommodate in consequent — requires accommodation
• τ₂ (intermediate): accommodate in antecedent — requires accommodation
• τ₃ (global): accommodate globally — requires accommodation

All three violate AvoidA. BeStrong is decisive: global accommodation (τ₃) gives the strongest interpretation → selected.

Example (19): "If Peter has a cat, then his cat is gray"

Three projection sites:

• τ₁ (local): requires accommodation (AvoidA violated)
• τ₂ (intermediate): allows binding/factoring (AvoidA satisfied)
• τ₃ (global): requires accommodation (AvoidA violated)

AvoidA selects τ₂ (intermediate) — the only site where the presupposition is bound rather than accommodated.

Accommodation blocking (Q-principle)

@cite{blutner-2000} §4, example (25): accommodation of "the car" is blocked when a simpler expression "a car" achieves the same context change without triggering presupposition. This is Q-principle blocking: the presuppositional form is more complex than the non-presuppositional alternative.

inductive Phenomena.Presupposition.Studies.Blutner2000.ProjectionSite : Type

Presupposition projection sites, following @cite{van-der-sandt-1992}.

• local : ProjectionSite
• intermediate : ProjectionSite
• global : ProjectionSite

instance Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqProjectionSite : DecidableEq ProjectionSite

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqProjectionSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Blutner2000.instBEqProjectionSite.beq : ProjectionSite → ProjectionSite → Bool

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqProjectionSite.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Blutner2000.instBEqProjectionSite : BEq ProjectionSite

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqProjectionSite = { beq := Phenomena.Presupposition.Studies.Blutner2000.instBEqProjectionSite.beq }

def Phenomena.Presupposition.Studies.Blutner2000.instReprProjectionSite.repr : ProjectionSite → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Blutner2000.instReprProjectionSite : Repr ProjectionSite

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instReprProjectionSite = { reprPrec := Phenomena.Presupposition.Studies.Blutner2000.instReprProjectionSite.repr }

@[reducible, inline]

abbrev Phenomena.Presupposition.Studies.Blutner2000.AvoidA : Type

AvoidA (Avoid Accommodation): counts accommodated discourse markers. 0 = bound (no accommodation needed), n = n markers accommodated.

Captures @cite{van-der-sandt-1992}'s preference for binding over accommodation and @cite{geurts-1995}'s preference (i).

Equations

• Phenomena.Presupposition.Studies.Blutner2000.AvoidA = ℕ

@[reducible, inline]

abbrev Phenomena.Presupposition.Studies.Blutner2000.Strength : Type

BeStrong: ranks by logical strength of the resulting interpretation. Lower values = stronger interpretation.

Captures @cite{geurts-1995}'s preference (ii): prefer higher accommodation sites (which yield stronger interpretations).

Equations

• Phenomena.Presupposition.Studies.Blutner2000.Strength = ℕ

Presupposition: "Peter has a cat" (triggered by "his cat"). Context: empty (∅). No antecedent provides a cat. All three sites require accommodation (no binding possible).

inductive Phenomena.Presupposition.Studies.Blutner2000.Form18 : Type

The input form for example (18). Only one form (the presuppositional sentence). The competition is among interpretations (projection sites).

• sentence : Form18

instance Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqForm18 : DecidableEq Form18

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqForm18 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Blutner2000.instBEqForm18.beq : Form18 → Form18 → Bool

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqForm18.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Blutner2000.instBEqForm18 : BEq Form18

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqForm18 = { beq := Phenomena.Presupposition.Studies.Blutner2000.instBEqForm18.beq }

def Phenomena.Presupposition.Studies.Blutner2000.instReprForm18.repr : Form18 → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Blutner2000.instReprForm18 : Repr Form18

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instReprForm18 = { reprPrec := Phenomena.Presupposition.Studies.Blutner2000.instReprForm18.repr }

def Phenomena.Presupposition.Studies.Blutner2000.gen18 : List (Form18 × ProjectionSite)

Generator: one form, three projection sites.

Equations

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

def Phenomena.Presupposition.Studies.Blutner2000.profile18 : Form18 × ProjectionSite → List ℕ

Constraint profile: [AvoidA, BeStrong]. All three sites require accommodation (AvoidA = 1). Strength: global (0) > intermediate (1) > local (2).

Equations

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

theorem Phenomena.Presupposition.Studies.Blutner2000.ex18_global_wins : Core.ConstraintEvaluation.superoptimal gen18 profile18 = [(Form18.sentence, ProjectionSite.global)]

Example (18): AvoidA is tied (all sites accommodate), so BeStrong is decisive. Global accommodation wins (strongest interpretation).

Presupposition: "Peter has a cat" (triggered by "his cat"). Context: empty (∅), but the antecedent introduces "Peter has a cat". At the intermediate site, the presupposition can be BOUND (factored) against the antecedent — no accommodation needed.

inductive Phenomena.Presupposition.Studies.Blutner2000.Form19 : Type

Generator for example (19).

• sentence : Form19

instance Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqForm19 : DecidableEq Form19

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqForm19 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Blutner2000.instBEqForm19.beq : Form19 → Form19 → Bool

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqForm19.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Blutner2000.instBEqForm19 : BEq Form19

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqForm19 = { beq := Phenomena.Presupposition.Studies.Blutner2000.instBEqForm19.beq }

def Phenomena.Presupposition.Studies.Blutner2000.instReprForm19.repr : Form19 → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Blutner2000.instReprForm19 : Repr Form19

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instReprForm19 = { reprPrec := Phenomena.Presupposition.Studies.Blutner2000.instReprForm19.repr }

def Phenomena.Presupposition.Studies.Blutner2000.gen19 : List (Form19 × ProjectionSite)

Equations

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

def Phenomena.Presupposition.Studies.Blutner2000.profile19 : Form19 × ProjectionSite → List ℕ

Constraint profile for example (19): [AvoidA, BeStrong]. Intermediate: binding possible → AvoidA = 0. Local and global: accommodation required → AvoidA = 1. Strength: global (0) > intermediate (1) > local (2).

Equations

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

theorem Phenomena.Presupposition.Studies.Blutner2000.ex19_intermediate_wins : Core.ConstraintEvaluation.superoptimal gen19 profile19 = [(Form19.sentence, ProjectionSite.intermediate)]

Example (19): AvoidA is decisive — intermediate projection allows binding (0 violations) while local and global require accommodation. BeStrong is irrelevant since AvoidA already discriminates.

@cite{blutner-2000} example (25): "He had an accident. ??The car hit him." vs "He had an accident. A car hit him."

"The car" triggers the presupposition that there is a unique salient car.
"A car" does not trigger this presupposition.

Starting from a neutral context (no car introduced), both sentences
achieve the same context change — but "the car" requires accommodation
while "a car" does not. The Q-principle blocks accommodation of "the car"
because the simpler alternative "a car" achieves the same effect. 

inductive Phenomena.Presupposition.Studies.Blutner2000.DefForm : Type

Two forms: the presuppositional definite and the indefinite.

• definite : DefForm
• indefinite : DefForm

instance Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqDefForm : DecidableEq DefForm

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqDefForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Blutner2000.instBEqDefForm.beq : DefForm → DefForm → Bool

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqDefForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Blutner2000.instBEqDefForm : BEq DefForm

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqDefForm = { beq := Phenomena.Presupposition.Studies.Blutner2000.instBEqDefForm.beq }

def Phenomena.Presupposition.Studies.Blutner2000.instReprDefForm.repr : DefForm → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Blutner2000.instReprDefForm : Repr DefForm

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instReprDefForm = { reprPrec := Phenomena.Presupposition.Studies.Blutner2000.instReprDefForm.repr }

inductive Phenomena.Presupposition.Studies.Blutner2000.AccidentMeaning : Type

The shared meaning (same context change result).

• carHitHim : AccidentMeaning

instance Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqAccidentMeaning : DecidableEq AccidentMeaning

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instDecidableEqAccidentMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Blutner2000.instBEqAccidentMeaning.beq : AccidentMeaning → AccidentMeaning → Bool

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqAccidentMeaning.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Blutner2000.instBEqAccidentMeaning : BEq AccidentMeaning

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instBEqAccidentMeaning = { beq := Phenomena.Presupposition.Studies.Blutner2000.instBEqAccidentMeaning.beq }

instance Phenomena.Presupposition.Studies.Blutner2000.instReprAccidentMeaning : Repr AccidentMeaning

Equations

• Phenomena.Presupposition.Studies.Blutner2000.instReprAccidentMeaning = { reprPrec := Phenomena.Presupposition.Studies.Blutner2000.instReprAccidentMeaning.repr }

def Phenomena.Presupposition.Studies.Blutner2000.instReprAccidentMeaning.repr : AccidentMeaning → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.Studies.Blutner2000.genAccident : List (DefForm × AccidentMeaning)

Generator: both forms map to the same meaning.

Equations

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

def Phenomena.Presupposition.Studies.Blutner2000.profileAccident : DefForm × AccidentMeaning → List ℕ

Profile: [FormComplexity, AccommodationCost]. The definite requires accommodation (more complex pragmatically); the indefinite does not.

Equations

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

theorem Phenomena.Presupposition.Studies.Blutner2000.accommodation_blocked : Core.ConstraintEvaluation.superoptimal genAccident profileAccident = [(DefForm.indefinite, AccidentMeaning.carHitHim)]

Q-principle blocks the definite: the indefinite achieves the same meaning with fewer violations. The definite form is blocked (pragmatically anomalous) in neutral contexts.

theorem Phenomena.Presupposition.Studies.Blutner2000.accommodation_blocked_is_Q : Theories.Pragmatics.Bidirectional.satisfiesQ genAccident profileAccident (DefForm.definite, AccidentMeaning.carHitHim) = false

This is a Q-principle effect: the definite is blocked because a competing form (indefinite) with the same meaning is better.

theorem Phenomena.Presupposition.Studies.Blutner2000.indefinite_satisfies_both : Theories.Pragmatics.Bidirectional.satisfiesQ genAccident profileAccident (DefForm.indefinite, AccidentMeaning.carHitHim) = true ∧ Theories.Pragmatics.Bidirectional.satisfiesI genAccident profileAccident (DefForm.indefinite, AccidentMeaning.carHitHim) = true

The indefinite satisfies both Q and I.

@cite{blutner-2000}'s projection sites correspond to the accommodation levels in Semantics.Presupposition.Accommodation. The bridge makes explicit that Blutner's OT analysis operates over the same site taxonomy as the Heim/Lewis/van der Sandt tradition.

def Phenomena.Presupposition.Studies.Blutner2000.ProjectionSite.toAccommodationLevel : ProjectionSite → Semantics.Presupposition.Accommodation.AccommodationLevel

Map projection sites to the standard accommodation levels.

Equations

• Phenomena.Presupposition.Studies.Blutner2000.ProjectionSite.local.toAccommodationLevel = Semantics.Presupposition.Accommodation.AccommodationLevel.local
• Phenomena.Presupposition.Studies.Blutner2000.ProjectionSite.intermediate.toAccommodationLevel = Semantics.Presupposition.Accommodation.AccommodationLevel.intermediate 0
• Phenomena.Presupposition.Studies.Blutner2000.ProjectionSite.global.toAccommodationLevel = Semantics.Presupposition.Accommodation.AccommodationLevel.global

theorem Phenomena.Presupposition.Studies.Blutner2000.global_is_global_accommodation : ProjectionSite.global.toAccommodationLevel = Semantics.Presupposition.Accommodation.AccommodationLevel.global

Global projection corresponds to global accommodation.

theorem Phenomena.Presupposition.Studies.Blutner2000.local_is_local_accommodation : ProjectionSite.local.toAccommodationLevel = Semantics.Presupposition.Accommodation.AccommodationLevel.local

Local projection corresponds to local accommodation.