Strawson entailment and NPI licensing (von Fintel 1999)

This file indexes [vF99a]'s defense of the Fauconnier-Ladusaw analysis of NPI licensing: four contexts that license NPIs without being classically downward entailing — only, adversative attitudes, superlatives, and conditional antecedents — are all Strawson-DE (his Definition 14). Each theorem is named after the paper's example number and discharged by specializing the corresponding substrate theorem from Logic/Natural/Strawson/Basic.lean. The NPI stimuli are typed rows in Data/Examples/VonFintel1999.json (Examples.ex10, …).

Main results

• ex11_only_not_DE, ex18_only_strawsonDE — the §2 separation: only is Strawson-DE but not classically DE.
• ex22_since_strawsonDE — §2.2: since (Iatridou's exs. 20-22).
• ex30_sorry_not_DE, ex28b_sorry_strawsonDE — the §3 adversative separation.
• ex45_want_isUE, ex50_gladKL_isUE, ex52_gladVF_isUE — §§3.2-3.3: want and glad are upward entailing, so NPIs are not licensed.
• ex72_conditional_antecedent_DE, conditional_antecedent_strawsonDE_under_restrictor — §4.1, the restrictor analysis.
• ex77_superlative_strawsonDE — §4.2 superlatives.
• onlyIndiv_eq_onlyVia — (15)'s individual-identity exclusion equals [Roo92]'s onlyVia over injective individual-generated families.
• bridge_lahiri_glad_settle_overgeneration, bridge_hoeksema_gtOverSet_strawsonDE — cross-framework bridges.

Discussed without formalization: §2.3 pseudo-anti-additivity (exs. 23-27), ex. 31, and the §3.4 shifting-context material (exs. 60-68).

References

• [vF99a], [KL93], [Lah98], [Hoe83], [Roo92], [Atl96].

glad, want, and Asher's weakened DE (single-consumer substrate)

def VonFintel1999.gladFullVF {W : Type u_1} (dox relevant : W → Set W) (lt : W → W → W → Prop) (p : Set W) : Set W

glad (von Fintel eq. 52, the replacement vF prefers over K&L eq. 50). α is glad that p at w iff every belief world is strictly preferred (under lt from the perspective of w) to every relevant non-p world: i.e., DOX(α, w) <_g (relevant w − p).

Both gladFull and gladFullVF are UE in p. They differ on cases like vF's Honda-Civic example (p. 124): when the agent buys a Honda Civic and discovers it's a lemon, the K&L version makes "I'm glad I bought a Honda Civic" automatic from "I wanted a Honda Civic and got one"; the vF version permits the reasonable "I wanted to but I'm not glad I did" because the actual world is now worse than the belief worlds at the time of evaluation.

Equations

• VonFintel1999.gladFullVF dox relevant lt p w = ∀ w₁ ∈ dox w, ∀ w₂ ∈ relevant w, ¬p w₂ → lt w w₂ w₁

theorem VonFintel1999.gladFullVF_isUE {W : Type u_1} (dox relevant : W → Set W) (lt : W → W → W → Prop) : Monotone (gladFullVF dox relevant lt)

glad (vF eq. 52) is UE in its complement.

want (vF §3.2 eq. 45, pp. 116-118)

α wants p iff in α's preferred worlds (drawn from a doxastic modal base dox), p holds. This is UE — the headline result vF defends in §3.2 against Asher (1987) / Heim (1992) non-monotonicity puzzles (Concorde, couch).

def VonFintel1999.wantFull {W : Type u_1} (bestOf : W → Set W) (p : Set W) : Set W

want(p) denotation: in α's preferred worlds among dox w, p holds.

Equations

• VonFintel1999.wantFull bestOf p w = ∀ w' ∈ bestOf w, p w'

theorem VonFintel1999.wantFull_isUE {W : Type u_1} (bestOf : W → Set W) : Monotone (wantFull bestOf)

want is upward entailing in its complement (vF §3.2 headline).

IsWDE — Asher 1987 Weakened Downward Entailment

[Ash87]

vF p. 112 (footnote 8) cites Asher's WDE as a sibling of Strawson-DE. Asher's schema:

α regrets that φ ⟦φ⟧ ⇒ ⟦ψ⟧ α believes that ψ ⊢ α regrets that ψ

This is the upward direction (φ → ψ) with a doxastic side condition on the conclusion's complement (believes ψ). Compare Strawson-DE, which is the downward direction with a presupposition side condition on the conclusion. The two schemas are not equivalent; vF (p. 112, footnote 8) writes "the intent of defining something like Strawson Entailment is clear" but the formal apparatus differs.

def VonFintel1999.IsWDE {W : Type u_1} (f : Set W → Set W) (believes : Set W → W → Prop) : Prop

Asher's WDE: f(p) plus belief in q implies f(q), when p ⊆ q.

Equations

• VonFintel1999.IsWDE f believes = ∀ (p q : Set W), p ⊆ q → ∀ (w : W), believes q w → f p w → f q w

theorem VonFintel1999.monotone_implies_WDE {W : Type u_1} (f : Set W → Set W) (hMono : Monotone f) (believes : Set W → W → Prop) : IsWDE f believes

Classical UE (Monotone) implies WDE: the doxastic side condition is redundant when monotonicity already holds.

only is Strawson-DE but not DE (§2)

The licensing datum is Examples.ex10; the separation fails classically because the conclusion's existence presupposition is not guaranteed by the premise.

def VonFintel1999.onlyJohn : Set (Fin 4) → Set (Fin 4)

Only John, with the focus individual modeled as · = (0 : Fin 4).

Equations

• VonFintel1999.onlyJohn = NaturalLogic.onlyFull fun (x : Fin 4) => x = 0

def VonFintel1999.onlyJohnDefined (scope : Set (Fin 4)) (_w : Fin 4) : Prop

Only John's existence presupposition.

Equations

• VonFintel1999.onlyJohnDefined scope _w = ∃ (w' : Fin 4), w' = 0 ∧ scope w'

theorem VonFintel1999.ex11_only_not_DE : ¬Antitone onlyJohn

Ex. 11 (p. 101): only is not classically downward entailing.

theorem VonFintel1999.ex18_only_strawsonDE : NaturalLogic.IsStrawsonDE onlyJohn onlyJohnDefined

Ex. 18 (p. 104): only is Strawson-DE relative to its existence presupposition.

since (§2.2)

Iatridou's examples; the licensing datum is Examples.ex21.

theorem VonFintel1999.ex22_since_strawsonDE (pastEvent sinceWindow : Fin 4 → Set (Fin 4)) : NaturalLogic.IsStrawsonDE (NaturalLogic.sinceFull pastEvent sinceWindow) fun (p : Set (Fin 4)) (w : Fin 4) => ∃ w' ∈ pastEvent w, p w'

Ex. 22 (p. 107): since is Strawson-DE in its complement, relative to the past-event presupposition.

Pseudo-anti-additivity (§2.3)

[Atl96]'s pseudo-anti-additivity is "useless for the analysis of NPI licensing" (p. 110): licensers and non-licensers share it alike (exs. 25-27).

Adversative attitudes (§3)

Factivity blocks classical DE in the complement (exs. 29-30); Strawson-DE restores the inference. The licensing data are Examples.ex28a and Examples.ex28b; [KL93]'s coherence challenge (ex. 31) is reanalyzed in §3.1 as a modal-base shift.

def VonFintel1999.sorryFrame : Set (Fin 4) → Set (Fin 4)

The substrate's DE-counterexample frame for sorryFull.

Equations

• VonFintel1999.sorryFrame = NaturalLogic.sorryFull (fun (w : Fin 4) => {w}) fun (x : Fin 4) => {1}

theorem VonFintel1999.ex30_sorry_not_DE : ¬Antitone sorryFrame

Ex. 30 (p. 111): sorry is not classically DE in its complement.

theorem VonFintel1999.ex28b_sorry_strawsonDE (dox bestOf : Fin 4 → Set (Fin 4)) : NaturalLogic.IsStrawsonDE (NaturalLogic.sorryFull dox bestOf) fun (p : Set (Fin 4)) (w : Fin 4) => ∀ w' ∈ dox w, p w'

Ex. 28b (p. 111): sorry is Strawson-DE relative to doxastic factivity.

want and glad are upward entailing (§§3.2-3.3)

The Asher/Heim apparent non-monotonicity of want is a modal-base shift; the sorry/glad monotonicity asymmetry tracks the NPI-licensing asymmetry (Examples.glad_any), in English and in Hindi ([Lah98] §4.5).

theorem VonFintel1999.ex45_want_isUE (bestOf : Fin 4 → Set (Fin 4)) : Monotone (wantFull bestOf)

Eq. 45 (§3.2): want is upward entailing in its complement.

theorem VonFintel1999.ex50_gladKL_isUE (dox bestOf : Fin 4 → Set (Fin 4)) : Monotone (NaturalLogic.gladFull dox bestOf)

Ex. 50 (p. 122): glad on the K&L semantics is upward entailing.

theorem VonFintel1999.ex52_gladVF_isUE (dox relevant : Fin 4 → Set (Fin 4)) (lt : Fin 4 → Fin 4 → Fin 4 → Prop) : Monotone (gladFullVF dox relevant lt)

Ex. 52 (p. 124): glad on vF's replacement semantics is likewise upward entailing.

Shifting contexts (§3.4)

The coherent glad…but sorry sequences (exs. 60-61) rest on modal-base shifts and need dynamic-context machinery not in the substrate; footnote 8's Weakened DE is the substrate's IsWDE; focus-only over a non-name (exs. 66-68) is subsumed by onlyFull.

Conditional antecedents (§4.1)

The restrictor analysis ([Kra86]) makes the antecedent position classically DE; on Stalnaker-Lewis ([Sta68], [Lew73b]) it is not, and vF §4.3 reduces those failures to context shifts via [vF00], an operator not in the substrate. The licensing datum is Examples.ex70a.

theorem VonFintel1999.ex72_conditional_antecedent_DE (domain : Fin 4 → Set (Fin 4)) (β : Set (Fin 4)) : Antitone fun (α : Set (Fin 4)) => NaturalLogic.condNecessity domain α β

Ex. 72 (p. 137): with an idle ordering source, condNecessity is classically DE in its antecedent.

theorem VonFintel1999.conditional_antecedent_strawsonDE_under_restrictor (domain : Fin 4 → Set (Fin 4)) (β : Set (Fin 4)) (defined : Set (Fin 4) → Fin 4 → Prop) : NaturalLogic.IsStrawsonDE (fun (α : Set (Fin 4)) => NaturalLogic.condNecessity domain α β) defined

Restrictor-style conditional antecedents are a fortiori Strawson-DE.

Superlatives (§4.2)

Adding a restriction can reorder the comparison class (ex. 76), so the position is not classically DE; predicative use only (Examples.ex75), the definite-description use (ex. 80) lacking local Strawson-DE.

theorem VonFintel1999.ex77_superlative_strawsonDE (α : Fin 4) : NaturalLogic.IsStrawsonDE (NaturalLogic.superlativeAssert α) (NaturalLogic.superlativePresup α)

Ex. 77 (p. 139): the superlative is Strawson-DE in its restriction position.

Cross-framework bridges

The four recalcitrants land at exactly Strawson-DE while glad sits outside the hierarchy (UE). K&L and vF derive the sorry/glad asymmetry from the same substrate theorems under different prose; the examples check the statement identity by discharging this file's statements with K&L's proof terms.

theorem VonFintel1999.bridge_lahiri_glad_settle_overgeneration : Lahiri1998.Examples.ex31b.judgment = Features.Judgment.acceptable ∧ KadmonLandman1993.settleGladAnybody.grammatical = true ∧ KadmonLandman1993.settleGladTickets.grammatical = true

The settle-for-less data ([Lah98] §4.5, [KL93]): glad + NPI is grammatical on a rescued reading that gladFull_isUE cannot capture.

theorem VonFintel1999.bridge_hoeksema_gtOverSet_strawsonDE {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (defined : Set D → Entity → Prop) : NaturalLogic.IsStrawsonDE (Core.Order.Comparison.gt.overSet μ) defined

[Hoe83]'s S-comparative is anti-additive, hence Strawson-DE with classical AA to spare (it licenses strong NPIs).

Individual-identity only and Rooth's strong theory

(15) (p. 104) excludes by individual identity, onlyVia by proposition identity; they coincide over an injective individual-generated family. (Fin 4)-constant propositions (the extensional onlyFull) fail injectivity wholesale, so the bridge is stated intensionally.

def VonFintel1999.onlyIndiv {W : Type u_1} {ι : Type u_2} (P : ι → Set W) (x : ι) : Set W

(15)'s assertion, intensionalized: no individual other than x satisfies P.

Equations

• VonFintel1999.onlyIndiv P x = {w : W | ∀ (y : ι), y ≠ x → w ∉ P y}

theorem VonFintel1999.onlyIndiv_eq_onlyVia {W : Type u_1} {ι : Type u_2} (P : ι → Set W) (x : ι) (hP : Function.Injective P) : onlyIndiv P x = Focus.onlyVia (Set.range P) (P x)

(15) coincides with onlyVia over an injective individual-generated alternative family.

theorem VonFintel1999.onlyIndiv_ne_onlyVia_of_collapse : onlyIndiv (fun (x : Bool) => Set.univ) true ≠ Focus.onlyVia (Set.range fun (x : Bool) => Set.univ) Set.univ

onlyVia cannot distinguish cotrue alternatives that (15) separates.