Strawson entailment

An operator into trivalent propositions is Strawson downward entailing when shrinking its argument gives a conclusion that the original Strawson-entails, the inference being checked only where the presuppositions involved hold. Von Fintel introduces the notion to keep the Fauconnier–Ladusaw theory of negative polarity licensing for focus only, the adversative attitudes, superlatives, temporal since and conditional antecedents, none of which is downward entailing in the classical sense. Gajewski defines Strawson anti-additivity, which the same operators also satisfy.

Strawson entailment adds presuppositions only as premises, so each Strawson property holds as soon as the operator's values, where defined, follow an assertion with the classical counterpart, whatever the presupposition; it is the presupposition that defeats the classical property.

Main definitions

• IsStrawsonDE, IsStrawsonUE: antitonicity and monotonicity under Strawson entailment.
• IsStrawsonAntiAdditive: f (p ⊔ q) is Strawson equivalent to f p conjoined with f q.
• only: von Fintel's only over a name.

Main results

• IsStrawsonDE.of_antitone, IsStrawsonUE.of_monotone, IsStrawsonAntiAdditive.of_isAntiAdditive: the classical property of an assertion that the defined values follow suffices.
• isStrawsonAntiAdditive_iff: Strawson anti-additivity is Strawson downward entailingness together with the Strawson form of Atlas's pseudo-anti-additivity.
• isStrawsonDE_ofProp_iff, isStrawsonAntiAdditive_ofProp_iff: without presuppositions the Strawson notions are the classical ones.
• isStrawsonAntiAdditive_only, not_antitone_posExt_only: only over a name is Strawson anti-additive and not classically downward entailing.
• not_isStrawsonUE_only, not_isStrawsonUE_since, Desire.BestWorlds.not_isStrawsonUE_regret, Degree.not_isStrawsonUE_superlative, Conditional.not_isStrawsonUE_horizonCounterfactual: none of the Strawson downward entailing operators is Strawson upward entailing as well.
• Degree.isStrawsonAntiAdditive_superlative, Conditional.isStrawsonAntiAdditive_horizonCounterfactual: the superlative in its class and the modal-horizon counterfactual in its antecedent are Strawson anti-additive, and neither is classically downward entailing.
• Desire.BestWorlds.isStrawsonUE_want, Desire.BestWorlds.isStrawsonUE_glad, Desire.BestWorlds.not_isStrawsonDE_glad, Desire.BestWorlds.isStrawsonAntiAdditive_regret: want and glad are Strawson upward entailing and glad is not Strawson downward entailing, while sorry is Strawson anti-additive.
• Focus.Particles.isStrawsonDE_only, Focus.Particles.isStrawsonAntiAdditive_only_subset, Focus.Particles.isStrawsonDE_only_apply: the propositional exclusive is Strawson downward entailing in its prejacent and, applied to an individual, in its predicate, on scales refining entailment; Focus.Particles.not_isStrawsonDE_only_superset fails it on the reversed scale.
• only_eq_only_range, only_ne_only_range: the name-based only is the exclusive over the alternatives the name generates exactly when no predication entails another's.

Implementation notes

• Strawson entailment takes the presuppositions of premise and conclusion alike as premises, as in von Fintel's Strawson validity and Gajewski's own proofs, rather than the literal clause of Gajewski's cross-categorial definition at type t.
• only is von Fintel's name-based only, which excludes individuals; the propositional exclusive of Coppock and Beaver, which excludes alternative propositions, is Focus.Particles.only, and its Strawson facts hold with the alternatives held fixed, as von Fintel requires. only presupposes that x is P; Horn's presupposition that something is P gives the same Strawson facts, as von Fintel notes.
• Want, glad and sorry are the best-worlds entries of Desire.BestWorlds; following Heim, the factivity of glad and sorry is doxastic, and with suitable ordering sources sorry also covers regret, amazed and surprised. Von Fintel calls glad upward entailing; its presupposition that the domain contains non-p worlds can fail at a larger argument, so Desire.BestWorlds.isStrawsonUE_glad is the Strawson form he states for want.
• The other operators live with their owners, the superlative in Degree.superlative and the conditional in Conditional.horizonCounterfactual, and their Strawson facts are proved here, as are those of Iatridou's temporal since, defined here.

References

• [Str52]
• [vF99a]
• [Gaj05]
• [Gaj11]
• [CB14]
• [Atl96]
• [Hor96]
• [Hei92]
• [Hei99]

Strawson monotonicity

def NaturalLogic.IsStrawsonDE {α : Type u_1} {W : Type u_3} [Preorder α] (f : α → W → SignType) : Prop

An operator into trivalent propositions is Strawson downward entailing if p ≤ q makes f q Strawson-entail f p ([vF99a]'s (14)).

Equations

• NaturalLogic.IsStrawsonDE f = ∀ ⦃p q : α⦄, p ≤ q → Presupposition.strawsonEntails (f q) (f p)

def NaturalLogic.IsStrawsonUE {α : Type u_1} {W : Type u_3} [Preorder α] (f : α → W → SignType) : Prop

An operator into trivalent propositions is Strawson upward entailing if p ≤ q makes f p Strawson-entail f q.

Equations

• NaturalLogic.IsStrawsonUE f = ∀ ⦃p q : α⦄, p ≤ q → Presupposition.strawsonEntails (f p) (f q)

theorem NaturalLogic.isStrawsonDE_iff {α : Type u_1} {W : Type u_3} [Preorder α] {f : α → W → SignType} : IsStrawsonDE f ↔ ∀ ⦃p q : α⦄, p ≤ q → ∀ (w : W), f p w ≠ 0 → f q w = 1 → f p w = 1

Von Fintel's own statement of Strawson downward entailingness asks that f p be true wherever it is defined and f q is true.

theorem NaturalLogic.IsStrawsonDE.of_antitone {α : Type u_1} {W : Type u_3} [Preorder α] {f : α → W → SignType} {a : α → W → Prop} (h : Antitone a) (hf : ∀ (p : α) (w : W), f p w ≠ 0 → (f p w = 1 ↔ a p w)) : IsStrawsonDE f

An operator whose values, where defined, follow an antitone assertion is Strawson downward entailing, whatever the presupposition.

theorem NaturalLogic.IsStrawsonUE.of_monotone {α : Type u_1} {W : Type u_3} [Preorder α] {f : α → W → SignType} {a : α → W → Prop} (h : Monotone a) (hf : ∀ (p : α) (w : W), f p w ≠ 0 → (f p w = 1 ↔ a p w)) : IsStrawsonUE f

An operator whose values, where defined, follow a monotone assertion is Strawson upward entailing, whatever the presupposition.

theorem NaturalLogic.IsStrawsonDE.of_antitone_posExt {α : Type u_1} {W : Type u_3} [Preorder α] {f : α → W → SignType} (h : Antitone fun (p : α) => Trivalent.posExt (f p)) : IsStrawsonDE f

Classical downward entailingness of the truth set implies the Strawson form.

theorem NaturalLogic.isStrawsonDE_ofProp_iff {α : Type u_1} {W : Type u_3} [Preorder α] {g : α → W → Prop} : (IsStrawsonDE fun (p : α) (w : W) => SignType.ofProp (g p w)) ↔ Antitone g

Without presuppositions, Strawson downward entailingness is antitonicity.

theorem NaturalLogic.isStrawsonUE_ofProp_iff {α : Type u_1} {W : Type u_3} [Preorder α] {g : α → W → Prop} : (IsStrawsonUE fun (p : α) (w : W) => SignType.ofProp (g p w)) ↔ Monotone g

Without presuppositions, Strawson upward entailingness is monotonicity.

theorem NaturalLogic.not_antitone_posExt {α : Type u_1} {W : Type u_3} [Preorder α] {f : α → W → SignType} {p q : α} {w : W} (hpq : p ≤ q) (hq : f q w = 1) (hp : f p w = 0) : ¬Antitone fun (p : α) => Trivalent.posExt (f p)

A presupposition failing at a smaller argument defeats classical downward entailingness.

theorem NaturalLogic.not_isStrawsonUE {α : Type u_1} {W : Type u_3} [Preorder α] {f : α → W → SignType} {p q : α} {w : W} (hpq : p ≤ q) (hp : f p w = 1) (hq : f q w = -1) : ¬IsStrawsonUE f

A larger argument false at a world where a smaller one is true defeats Strawson upward entailingness.

Strawson anti-additivity

def NaturalLogic.IsStrawsonAntiAdditive {α : Type u_1} {W : Type u_3} [SemilatticeSup α] (f : α → W → SignType) : Prop

An operator into trivalent propositions is Strawson anti-additive if f (p ⊔ q) is Strawson equivalent to f p conjoined with f q ([Gaj11]'s (36)), the conjunction being the classical one, defined where both conjuncts are.

Equations

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

theorem NaturalLogic.IsStrawsonAntiAdditive.of_isAntiAdditive {α : Type u_1} {W : Type u_3} [SemilatticeSup α] {f : α → W → SignType} {a : α → W → Prop} (h : IsAntiAdditive a) (hf : ∀ (p : α) (w : W), f p w ≠ 0 → (f p w = 1 ↔ a p w)) : IsStrawsonAntiAdditive f

An operator whose values, where defined, follow an anti-additive assertion is Strawson anti-additive, whatever the presupposition.

theorem NaturalLogic.IsStrawsonAntiAdditive.isStrawsonDE {α : Type u_1} {W : Type u_3} [SemilatticeSup α] {f : α → W → SignType} (h : IsStrawsonAntiAdditive f) : IsStrawsonDE f

theorem NaturalLogic.isStrawsonAntiAdditive_iff {α : Type u_1} {W : Type u_3} [SemilatticeSup α] {f : α → W → SignType} : IsStrawsonAntiAdditive f ↔ IsStrawsonDE f ∧ ∀ (p q : α), Presupposition.strawsonEntails (fun (w : W) => (f p w).meetWeak (f q w)) (f (p ⊔ q))

Strawson anti-additivity adds to Strawson downward entailingness the Strawson form of [Atl96]'s pseudo-anti-additivity, that f p and f q together entail f (p ⊔ q) ([vF99a]'s (25); [Gaj11], Appendix 1).

theorem NaturalLogic.isStrawsonAntiAdditive_ofProp_iff {α : Type u_1} {W : Type u_3} [SemilatticeSup α] {g : α → W → Prop} : (IsStrawsonAntiAdditive fun (p : α) (w : W) => SignType.ofProp (g p w)) ↔ IsAntiAdditive g

Without presuppositions, Strawson anti-additivity is anti-additivity.

Only

noncomputable def NaturalLogic.only {ι : Type u_2} {W : Type u_3} (x : ι) (P : ι → Set W) : W → SignType

Only x is P presupposes that x is P and asserts that nothing else is ([vF99a]'s (15)).

Equations

• NaturalLogic.only x P = (P x).indicator fun (w : W) => SignType.ofProp (∀ (y : ι), y ≠ x → w ∉ P y)

theorem NaturalLogic.isStrawsonAntiAdditive_only {ι : Type u_2} {W : Type u_3} (x : ι) : IsStrawsonAntiAdditive (only x)

theorem NaturalLogic.isStrawsonDE_only {ι : Type u_2} {W : Type u_3} (x : ι) : IsStrawsonDE (only x)

theorem NaturalLogic.not_antitone_posExt_only : ¬Antitone fun (P : Bool → Set Unit) => Trivalent.posExt (only true P)

Only John ate vegetables does not classically entail only John ate kale, whose presupposition may fail ([vF99a]'s (11)).

theorem NaturalLogic.not_isStrawsonUE_only : ¬IsStrawsonUE (only true)

Only John smokes does not Strawson-entail only John smokes or drinks, which is defined and false when someone else drinks, so only is not upward entailing.

theorem NaturalLogic.only_eq_only_range {ι : Type u_2} {W : Type u_3} (x : ι) (P : ι → Set W) (hP : ∀ (y : ι), P x ⊆ P y → y = x) : only x P = Focus.Particles.only (fun (x1 x2 : Set W) => x1 ⊆ x2) (Set.range P) (P x)

When distinct individuals yield alternatives none of which the prejacent entails, the name-based only is the propositional exclusive Focus.Particles.only applied to the predication of x, over the alternatives the name generates ([CB14]'s (93)).

theorem NaturalLogic.only_ne_only_range : (only true fun (x : Bool) => Set.univ) ≠ Focus.Particles.only (fun (x1 x2 : Set Unit) => x1 ⊆ x2) (Set.range fun (x : Bool) => Set.univ) Set.univ

Without that condition the two come apart, since two individuals with the same predication are one alternative, entailed by the prejacent, for the exclusive but two individuals for the name-based only.

Temporal since

noncomputable def NaturalLogic.since {T : Type u_5} [LinearOrder T] (ago : T → T) (p : Set T) : T → SignType

It has been five years since p presupposes that p held at the time ago t five years before the evaluation time t and asserts that it has not held since ([vF99a], after Iatridou).

Equations

• NaturalLogic.since ago p = {t : T | ago t ∈ p}.indicator fun (t : T) => SignType.ofProp (Disjoint (Set.Ioc (ago t) t) p)

theorem NaturalLogic.isStrawsonAntiAdditive_since {T : Type u_5} [LinearOrder T] (ago : T → T) : IsStrawsonAntiAdditive (since ago)

Since is Strawson anti-additive in its clause, as [Gaj11] finds von Fintel's Strawson downward entailing operators to be.

theorem NaturalLogic.isStrawsonDE_since {T : Type u_5} [LinearOrder T] (ago : T → T) : IsStrawsonDE (since ago)

Since is Strawson downward entailing.

theorem NaturalLogic.not_antitone_posExt_since : ¬Antitone fun (p : Set ℤ) => Trivalent.posExt (since (fun (x : ℤ) => x - 5) p)

It's been five years since I saw a bird of prey does not classically entail it's been five years since I saw an eagle, whose presupposition may fail.

theorem NaturalLogic.not_isStrawsonUE_since : ¬IsStrawsonUE (since fun (x : ℤ) => x - 5)

It's been five years since I saw an eagle does not Strawson-entail it's been five years since I saw a bird, defined and false when a sparrow was seen since.

The propositional exclusive

theorem Focus.Particles.isStrawsonDE_only {W : Type u_1} {S : Set W → Set W → Prop} (C : Set (Set W)) (hS : ∀ ⦃p q r : Set W⦄, p ⊆ q → S q r → S p r) : NaturalLogic.IsStrawsonDE (only S C)

On a scale refining entailment, only is Strawson downward entailing in its prejacent with the alternatives held fixed ([vF99a], §3.4; [CB14], fn. 22).

theorem Focus.Particles.isStrawsonAntiAdditive_only_subset {W : Type u_1} (C : Set (Set W)) : NaturalLogic.IsStrawsonAntiAdditive (only (fun (x1 x2 : Set W) => x1 ⊆ x2) C)

On the entailment scale only is Strawson anti-additive in its prejacent.

theorem Focus.Particles.isStrawsonDE_only_subset {W : Type u_1} (C : Set (Set W)) : NaturalLogic.IsStrawsonDE (only (fun (x1 x2 : Set W) => x1 ⊆ x2) C)

theorem Focus.Particles.isStrawsonDE_only_apply {W : Type u_1} {ι : Type u_2} {S : Set W → Set W → Prop} (C : Set (Set W)) (hS : ∀ ⦃p q r : Set W⦄, p ⊆ q → S q r → S p r) (x : ι) : NaturalLogic.IsStrawsonDE fun (P : ι → Set W) => only S C (P x)

Applied to the predication of an individual, only is Strawson downward entailing in the predicate with the alternatives held fixed, so NP-modifying only licenses negative polarity items in the verb phrase ([CB14]'s (93)).

theorem Focus.Particles.not_antitone_posExt_only_subset : ¬Antitone fun (p : Set Bool) => Trivalent.posExt (only (fun (x1 x2 : Set Bool) => x1 ⊆ x2) {{true}, Set.univ} p)

There only was precipitation in Medford does not classically entail there only was rain in Medford, whose presupposition, the premise [vF99a]'s (67) adds, may fail.

theorem Focus.Particles.not_isStrawsonDE_only_superset : ¬NaturalLogic.IsStrawsonDE (only (fun (x1 x2 : Set Bool) => x1 ⊇ x2) {{true}, Set.univ})

On a scale on which a weaker alternative outranks a stronger one, here reverse entailment, only is not Strawson downward entailing in its prejacent ([CB14], fn. 22). The two-world model is ours; the footnote states the claim without one.

Want, glad and sorry

theorem Desire.BestWorlds.isStrawsonUE_want {W : Type u_1} (base : W → Set W) (g : W → Set (W → Prop)) : NaturalLogic.IsStrawsonUE (want base g)

Want is Strawson upward entailing in its complement ([vF99a], §3.2).

theorem Desire.BestWorlds.isStrawsonUE_glad {W : Type u_1} (dox base : W → Set W) (g : W → Set (W → Prop)) : NaturalLogic.IsStrawsonUE (glad dox base g)

theorem Desire.BestWorlds.not_isStrawsonDE_glad : ¬NaturalLogic.IsStrawsonDE (glad (fun (x : Fin 3) => {0}) (fun (x : Fin 3) => Set.univ) fun (x : Fin 3) => {fun (x : Fin 3) => x = 1})

Glad is not Strawson downward entailing, so it licenses no negative polarity item ([vF99a], §3.3). The subject believes world 0 and prefers world 1, so is glad that 0 or 1 holds but not that 0 does.

theorem Desire.BestWorlds.isStrawsonAntiAdditive_regret {W : Type u_1} (dox base : W → Set W) (g : W → Set (W → Prop)) : NaturalLogic.IsStrawsonAntiAdditive (regret dox base g)

Sorry is Strawson anti-additive in its complement, since wanting a disjunction false is wanting each disjunct false.

theorem Desire.BestWorlds.isStrawsonDE_regret {W : Type u_1} (dox base : W → Set W) (g : W → Set (W → Prop)) : NaturalLogic.IsStrawsonDE (regret dox base g)

theorem Desire.BestWorlds.not_antitone_posExt_regret : ¬Antitone fun (p : Set Bool) => Trivalent.posExt (regret (fun (x : Bool) => {true}) (fun (x : Bool) => Set.univ) (fun (x : Bool) => {fun (x : Bool) => x = false}) p)

Sorry that Robin bought a car does not classically entail sorry that Robin bought a Honda Civic, whose factive presupposition may fail ([vF99a]'s (30)). The subject believes world true and prefers world false.

theorem Desire.BestWorlds.not_isStrawsonUE_regret : ¬NaturalLogic.IsStrawsonUE (regret (fun (x : Fin 3) => {0}) (fun (x : Fin 3) => Set.univ) fun (x : Fin 3) => {fun (x : Fin 3) => x = 1})

Sorry that Robin bought a Civic does not Strawson-entail sorry that Robin bought a Civic or a Golf, defined and false when the subject prefers the Golf. The subject believes world 0 and prefers world 1.

Superlatives

theorem Degree.isStrawsonAntiAdditive_superlative {α : Type u_1} {D : Type u_2} {W : Type u_3} [Preorder D] (μ : α → D) (x : α) : NaturalLogic.IsStrawsonAntiAdditive fun (x_1 : W → Set α) => superlative μ x_1 x

The superlative is Strawson anti-additive in its comparison class.

theorem Degree.isStrawsonDE_superlative {α : Type u_1} {D : Type u_2} {W : Type u_3} [Preorder D] (μ : α → D) (x : α) : NaturalLogic.IsStrawsonDE fun (x_1 : W → Set α) => superlative μ x_1 x

theorem Degree.not_antitone_posExt_superlative : ¬Antitone fun (C : Unit → Set Unit) => Trivalent.posExt (superlative (fun (x : Unit) => 0) C ())

Emma is the tallest girl in her class does not classically entail Emma is the tallest girl in her class to have learned the alphabet, whose presupposition may fail ([vF99a]'s (76)).

theorem Degree.not_isStrawsonUE_superlative : ¬NaturalLogic.IsStrawsonUE fun (x : Unit → Set Bool) => superlative (fun (x : Bool) => 0) x true

Emma is the tallest girl to have learned the alphabet does not Strawson-entail Emma is the tallest girl, defined and false when a taller girl has not learned it.

Conditional antecedents

theorem Conditional.isStrawsonAntiAdditive_horizonCounterfactual {I : Type u_1} {W : Type u_2} (horizon : I → Set W) (q : Set W) : NaturalLogic.IsStrawsonAntiAdditive fun (x : Set W) => horizonCounterfactual horizon x q

The modal-horizon counterfactual is Strawson anti-additive in its antecedent, since a strict conditional with a disjunctive antecedent is the conjunction of the conditionals of the disjuncts ([Gaj11], Appendix 1).

theorem Conditional.isStrawsonDE_horizonCounterfactual {I : Type u_1} {W : Type u_2} (horizon : I → Set W) (q : Set W) : NaturalLogic.IsStrawsonDE fun (x : Set W) => horizonCounterfactual horizon x q

theorem Conditional.not_antitone_posExt_horizonCounterfactual : ¬Antitone fun (p : Set Unit) => Trivalent.posExt (horizonCounterfactual (fun (x : Unit) => Set.univ) p Set.univ)

Strengthening the antecedent is not classically valid, since a strengthened antecedent can fall outside the horizon ([vF99a], §4.3).

theorem Conditional.not_isStrawsonUE_horizonCounterfactual : ¬NaturalLogic.IsStrawsonUE fun (p : Set Bool) => horizonCounterfactual (fun (x : Unit) => Set.univ) p {true}

Weakening the antecedent is not Strawson valid either, since the weaker antecedent can admit worlds the consequent excludes.