von Fintel (1999): NPI licensing, Strawson entailment, and context dependency

Von Fintel defends the Fauconnier–Ladusaw theory of negative polarity licensing against four licensers that are not downward entailing, focus only, the adversative attitudes, superlatives and conditional antecedents: each is downward entailing once the inference is checked only where the presuppositions hold. The notion is in Logic/Natural/Strawson.lean and the operators live with their owners, Iatridou's temporal since among them; this file carries the paper's arguments around them, and its licensing judgments are the rows of Data/Examples/VonFintel1999.json.

Want and glad are upward entailing in the Strawson sense, on the best-worlds semantics and on the set comparison alike. On the best-worlds semantics wanting and believing p makes one glad that p, which the Honda Civic scenario refutes for the set comparison. The set-comparison sorry is not Strawson downward entailing, which is why the paper keeps the best-worlds one. Of two entries for propositional only, the one that admits the prejacent's entailments as alternatives is Strawson downward entailing and the one that bars them assesses no downward inference at all; a conditional antecedent under a genuine ordering source is not downward entailing; and a superlative inside a definite description is not even Strawson downward entailing.

Main results

• isStrawsonUE_gladBetter, isStrawsonUE_regretBetter: the set-comparison glad and sorry are Strawson upward entailing, like the best-worlds want and glad.
• glad_eq_one_of_want_eq_one, not_gladBetter_of_want: wanting and believing gives gladness on the best-worlds semantics, not on the set comparison.
• not_isStrawsonDE_regretBetter: the set-comparison sorry would not license.
• only68b_eq_zero: the rejected entry for propositional only can assess no downward inference within one set of alternatives.
• not_antitone_conditionalNecessity, not_isStrawsonDE_theSuperlativeExceeds: the conditional under an ordering source and the superlative description fail downward inference.

TODO

• The shifted-context readings of §3.4 and the expansion of the modal horizon in §4.3 need von Fintel's later context-change operator; the static horizon semantics of (81)–(83) is Conditional.horizonCounterfactual.

References

• [vF99a]
• [KL93]
• [Roo92]
• [Kra86]
• [vF00a]

Want and glad

def VonFintel1999.Better {W : Type u_1} (A : Set (W → Prop)) (X Y : Set W) : Prop

X is better than Y when every X-world is strictly better than every Y-world under the ordering source A.

Equations

• VonFintel1999.Better A X Y = ∀ x ∈ X, ∀ y ∈ Y, x < y

noncomputable def VonFintel1999.gladBetter {W : Type u_1} (dox rel : W → Set W) (g : W → Set (W → Prop)) (p : Set W) : W → SignType

The set-comparison glad (52) has the presupposition of the best-worlds one and asserts that the belief worlds are strictly better than every relevant non-p world.

Equations

• VonFintel1999.gladBetter dox rel g p = (Function.support (Desire.BestWorlds.glad dox rel g p)).indicator fun (w : W) => SignType.ofProp (VonFintel1999.Better (g w) (dox w) (rel w \ p))

theorem VonFintel1999.isStrawsonUE_gladBetter {W : Type u_1} (dox rel : W → Set W) (g : W → Set (W → Prop)) : NaturalLogic.IsStrawsonUE (gladBetter dox rel g)

The set-comparison glad is still Strawson upward entailing in its complement (§3.3).

theorem VonFintel1999.glad_eq_one_of_want_eq_one {W : Type u_1} (dox rel : W → Set W) (g : W → Set (W → Prop)) (p : Set W) {w : W} (hd : dox w ⊆ rel w) (hb : dox w ⊆ p) (hw : Desire.BestWorlds.want rel g p w = 1) : Desire.BestWorlds.glad dox rel g p w = 1

On the best-worlds glad, a wants p and believes p entails a is glad that p, the inference [KL93] draw, when the modal base contains the belief worlds.

theorem VonFintel1999.not_gladBetter_of_want : ∃ (dox : Fin 3 → Set (Fin 3)) (rel : Fin 3 → Set (Fin 3)) (g : Fin 3 → Set (Fin 3 → Prop)) (p : Set (Fin 3)) (w : Fin 3), dox w ⊆ p ∧ Desire.BestWorlds.want rel g p w = 1 ∧ gladBetter dox rel g p w = -1

The Honda Civic scenario refutes that inference on the set-comparison glad. World 0 is the actual one, where the Civic bought is a lemon, 1 is where a good Civic is bought, and 2 where none is; the subject believes 0, wants the good Civic, and is not glad that a Civic was bought, since 0 is no better than 2.

noncomputable def VonFintel1999.regretBetter {W : Type u_1} (dox rel : W → Set W) (g : W → Set (W → Prop)) (p : Set W) : W → SignType

The set-comparison sorry (54) has the presupposition of glad and asserts that every relevant non-p world is strictly better than every belief world.

Equations

• VonFintel1999.regretBetter dox rel g p = (Function.support (Desire.BestWorlds.glad dox rel g p)).indicator fun (w : W) => SignType.ofProp (VonFintel1999.Better (g w) (rel w \ p) (dox w))

theorem VonFintel1999.isStrawsonUE_regretBetter {W : Type u_1} (dox rel : W → Set W) (g : W → Set (W → Prop)) : NaturalLogic.IsStrawsonUE (regretBetter dox rel g)

The set-comparison sorry is Strawson upward entailing in its complement.

theorem VonFintel1999.not_isStrawsonDE_regretBetter : ¬NaturalLogic.IsStrawsonDE (regretBetter (fun (x : Fin 3) => {0}) (fun (x : Fin 3) => Set.univ) fun (x : Fin 3) => {fun (x : Fin 3) => x = 2})

The set-comparison sorry is not Strawson downward entailing, so it would not license; the paper keeps the best-worlds regret. World 2 is the preferred one; the subject believes 0 and is sorry about {0, 1} but not about {0}, since 1 is no better than 0.

Propositional only, §3.4

Of the two entries for propositional only von Fintel compares, (68a) presupposes the prejacent and asserts that every true alternative is entailed by it; it is the substrate's Focus.Particles.only (· ⊆ ·) (Focus.Particles.only_subset_eq), Strawson downward entailing with the alternatives held fixed (Focus.Particles.isStrawsonDE_only_subset). (68b) bars the prejacent's entailments from the alternatives and asserts that every true alternative is the prejacent.

noncomputable def VonFintel1999.only68b {W : Type u_1} (C : Set (Set W)) (p : Set W) : W → SignType

Only in the entry (68b) presupposes the prejacent and that no alternative is entailed by it, and asserts that every true alternative is the prejacent.

Equations

• VonFintel1999.only68b C p = {w : W | w ∈ p ∧ ¬∃ r ∈ C, p ⊆ r}.indicator fun (w : W) => SignType.ofProp (w ∈ Focus.Particles.atMost (fun (x1 x2 : Set W) => x1 = x2) C p)

theorem VonFintel1999.only68b_eq_zero {W : Type u_1} (C : Set (Set W)) (p : Set W) {q : Set W} (hp : p ∈ C) (hqp : q ⊆ p) (w : W) : only68b C q w = 0

With (68b) no downward inference can be assessed within one set of alternatives, since when the premise's prejacent is an alternative the conclusion's presupposition fails (p. 134).

Conditional antecedents under an ordering source

theorem VonFintel1999.not_antitone_conditionalNecessity : ¬Antitone fun (α : Fin 2 → Prop) => {w : Fin 2 | Conditional.Restrictor.conditionalNecessity (fun (x : Fin 2) => ∅) (fun (x : Fin 2) => {fun (x : Fin 2) => x = 0}) α (fun (x : Fin 2) => x = 0) w}

With a genuine ordering source the antecedent position of Kratzer's conditional necessity is not downward entailing (73). The best strike-worlds are dry and the match lights, while the best dip and strike-worlds do not light; world 0 strikes a dry match, world 1 dips it first.

The superlative inside a definite description

noncomputable def VonFintel1999.theSuperlativeExceeds {W : Type u_1} {ι : Type u_2} {D : Type u_3} [Preorder D] (μ : ι → D) (C : W → Set ι) (d : D) : W → SignType

The μ-est C exceeds d presupposes a superlative individual and asserts that every such individual exceeds d.

Equations

• VonFintel1999.theSuperlativeExceeds μ C d = {w : W | ∃ (a : ι), Degree.superlative μ C a w = 1}.indicator fun (w : W) => SignType.ofProp (∀ (a : ι), Degree.superlative μ C a w = 1 → d < μ a)

theorem VonFintel1999.not_isStrawsonDE_theSuperlativeExceeds : ¬NaturalLogic.IsStrawsonDE fun (x : Unit → Set Bool) => theSuperlativeExceeds (fun (b : Bool) => if b = true then 3 else 5) x 4

The definite-description use is not even Strawson-valid (80). The tallest girl in the school is over four feet does not Strawson-entail the tallest girl in the class is over four feet, since the class's tallest girl need not be the school's; individual false is five feet, true three feet, and the class is {true}.