def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.Presupposition (W : Type u_1) : Type u_1

A presupposition: a condition that must be satisfied for an expression to have a defined truth value.

Following @cite{heim-1983}, presuppositions are definedness conditions on the input context.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.Presupposition W = (W → Prop)

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.existentialPresup {W : Type u_1} {E : Type u_2} (restrictor : E → W → Prop) : Presupposition W

Existential presupposition: the restrictor of a quantifier is non-empty.

For "every book that Maria reads", this presupposes: ∃x. book(x) ∧ reads(maria, x)

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.existentialPresup restrictor w = ∃ (x : E), restrictor x w

inductive Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.QuantifierStrength : Type

Strong quantifier: quantifiers that carry existential presupposition.

• "every", "each", "both" presuppose non-empty domain
• "some", "a" do not (they assert existence)

• strong : QuantifierStrength
• weak : QuantifierStrength

instance Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instDecidableEqQuantifierStrength : DecidableEq QuantifierStrength

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instDecidableEqQuantifierStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instReprQuantifierStrength.repr : QuantifierStrength → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instReprQuantifierStrength : Repr QuantifierStrength

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instReprQuantifierStrength = { reprPrec := Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instReprQuantifierStrength.repr }

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.hasExistentialPresup : QuantifierStrength → Bool

Strong quantifiers presuppose non-empty restrictor.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.hasExistentialPresup Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.QuantifierStrength.strong = true
• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.hasExistentialPresup Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.QuantifierStrength.weak = false

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.indicativeRestrictor {W : Type u_1} {Time : Type u_2} {E : Type u_3} (restrictor : E → Situation W Time → Prop) (s : Situation W Time) : E → Prop

Indicative restrictor: evaluates the restrictor at the actual world.

"Every book that Maria reads.IND..." → Presupposes books exist that Maria reads in the actual world

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.indicativeRestrictor restrictor s x = restrictor x s

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.sfRestrictor {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (restrictor : E → Situation W Time → Prop) (s₀ : Situation W Time) : E → Prop

SF restrictor: quantifies over historical alternatives.

"Every book that Maria reads.SF..." → Quantifies over situations where Maria might read books → No presupposition that she actually reads any

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.sfRestrictor history restrictor s₀ x = ∃ s₁ ∈ Semantics.Tense.BranchingTime.historicalBase history s₀, restrictor x s₁

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.satisfiesPresup {W : Type u_1} {E : Type u_2} (c : IContext W E) (p : Presupposition W) : Prop

A context satisfies a presupposition if the presupposition holds throughout the context.

Following Heim's context change semantics: presuppositions are requirements on the input context.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.satisfiesPresup c p = ∀ gw ∈ c, p gw.2

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.locallySatisfied {W : Type u_1} (p : Presupposition W) (w : W) : Prop

A presupposition is locally satisfied if it holds at the evaluation world.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.locallySatisfied p w = p w

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.weakenedPresup {W : Type u_1} (p : Presupposition W) (condition : W → Prop) : Presupposition W

A presupposition is weakened to a conditional presupposition.

Weak(P) = "if there are relevant entities, then P"

This is what SF achieves: instead of presupposing existence, it makes the assertion conditional on existence.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.weakenedPresup p condition w = (condition w → p w)

theorem Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.indicative_preserves_presup {W : Type u_1} {Time : Type u_2} {E : Type u_3} (restrictor : E → Situation W Time → Prop) (s : Situation W Time) (h_presup : ∃ (x : E), indicativeRestrictor restrictor s x) : ∃ (x : E), restrictor x s

Indicative preserves existential presupposition.

With indicative mood in the restrictor, the strong quantifier's existential presupposition projects.

"Cada livro que Maria ler.IND será interessante" → Presupposes ∃x. book(x) ∧ reads(maria, x)

theorem Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.sf_weakens_presup {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (restrictor : E → Situation W Time → Prop) (s₀ : Situation W Time) (h_no_actual : ¬∃ (x : E), restrictor x s₀) (h_possible : ∃ s₁ ∈ Tense.BranchingTime.historicalBase history s₀, ∃ (x : E), restrictor x s₁) : ∃ (x : E), sfRestrictor history restrictor s₀ x

SF weakens existential presupposition.

With SF in the restrictor, existence is only presupposed conditionally on the relevant situation obtaining.

"Cada livro que Maria ler.SF será interessante" → No categorical presupposition; existence conditional on future

Quantifying over historical alternatives means we don't presuppose existence in any particular world.

theorem Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.sf_felicitous_under_uncertainty {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (restrictor : E → Situation W Time → Prop) (s₀ : Situation W Time) (h_uncertainty : (∃ s₁ ∈ Tense.BranchingTime.historicalBase history s₀, ∃ (x : E), restrictor x s₁) ∧ ∃ s₂ ∈ Tense.BranchingTime.historicalBase history s₀, ¬∃ (x : E), restrictor x s₂) : (∃ (x : E), sfRestrictor history restrictor s₀ x) ∧ ∃ s ∈ Tense.BranchingTime.historicalBase history s₀, ¬∃ (x : E), restrictor x s

SF makes strong quantifiers felicitous in uncertain contexts.

When the speaker is uncertain whether the restrictor will be satisfied, SF is felicitous but indicative is not.

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.relClauseIND {W : Type u_1} {Time : Type u_2} {E : Type u_3} (noun relClause : E → Situation W Time → Prop) (s : Situation W Time) : E → Prop

Relative clause with indicative.

"todo livro [que Maria ler.IND]" "every book [that Maria reads.IND]"

Structure: ∀x[book(x) ∧ reads(m,x,s₀)] →... Presupposes existence of books Maria reads at s₀.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.relClauseIND noun relClause s x = (noun x s ∧ relClause x s)

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.relClauseSF {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (noun relClause : E → Situation W Time → Prop) (s₀ : Situation W Time) : E → Prop

Relative clause with SF.

"todo livro [que Maria ler.SF]" "every book [that Maria reads.SF]"

Structure: ∀s₁∈hist(s₀): ∀x[book(x,s₁) ∧ reads(m,x,s₁)] →... No categorical existence presupposition.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.relClauseSF history noun relClause s₀ x = ∃ s₁ ∈ Semantics.Tense.BranchingTime.historicalBase history s₀, noun x s₁ ∧ relClause x s₁

theorem Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.relClause_sf_weakens_quantifier {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (noun relClause : E → Situation W Time → Prop) (s₀ : Situation W Time) (h_none_actual : ¬∃ (x : E), noun x s₀ ∧ relClause x s₀) (h_some_possible : ∃ s₁ ∈ Tense.BranchingTime.historicalBase history s₀, ∃ (x : E), noun x s₁ ∧ relClause x s₁) : ∃ (x : E), relClauseSF history noun relClause s₀ x

SF in relative clause weakens strong quantifier presupposition.

This is the formal version of the contrast in (17)-(18).

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.modalDisplacement {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (restrictor nuclear : E → Situation W Time → Prop) (s₀ : Situation W Time) : Prop

Modal displacement: SF introduces quantification over situations, which "displaces" the existential presupposition.

Without SF: ∃x.P(x) presupposed, ∀x.P(x) → Q(x) asserted With SF: ∀s∈hist. [∃x.P(x,s) presupposed within s, ∀x.P(x,s)→Q(x,s) asserted]

The presupposition is now local to each situation, not global.

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.sf_is_modal_displacement {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (restrictor nuclear : E → Situation W Time → Prop) (s₀ : Situation W Time) : modalDisplacement history restrictor nuclear s₀ ↔ ∀ s₁ ∈ Tense.BranchingTime.historicalBase history s₀, ∀ (x : E), restrictor x s₁ → nuclear x s₁

Modal displacement captures SF semantics.

The universal quantifier with SF is equivalent to modal displacement: quantifying over situations, with local existence conditions.

inductive Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.PresuppositionStrategy : Type

Accommodation vs modal displacement.

Presupposition accommodation: Adding the presupposition to the context. Modal displacement: Quantifying over situations where presupposition holds.

SF uses modal displacement, not accommodation.

• accommodation : PresuppositionStrategy
• localAccommodation : PresuppositionStrategy
• modalDisplacement : PresuppositionStrategy

instance Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instDecidableEqPresuppositionStrategy : DecidableEq PresuppositionStrategy

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instDecidableEqPresuppositionStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instReprPresuppositionStrategy : Repr PresuppositionStrategy

Equations

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

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.instReprPresuppositionStrategy.repr : PresuppositionStrategy → ℕ → Std.Format

Equations

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

def Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.sfStrategy : PresuppositionStrategy

SF employs modal displacement strategy.

Equations

• Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.sfStrategy = Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.PresuppositionStrategy.modalDisplacement

theorem Semantics.Dynamic.IntensionalCDRT.PresuppositionWeakening.modal_displacement_weaker_than_accommodation {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (history : Tense.BranchingTime.WorldHistory W Time) (restrictor : E → Situation W Time → Prop) (s₀ : Situation W Time) (h_global : ∀ s₁ ∈ Tense.BranchingTime.historicalBase history s₀, ∃ (x : E), restrictor x s₁) (h_nonempty : ∃ (s : Situation W Time), s ∈ Tense.BranchingTime.historicalBase history s₀) : ∃ s₁ ∈ Tense.BranchingTime.historicalBase history s₀, ∃ (x : E), restrictor x s₁

Modal displacement is weaker than global accommodation.

With modal displacement, we only require existence in some accessible situations, not in all of them.