Strawson entailment

This file defines Strawson-DE — downward entailingness checked only where the conclusion's presuppositions are satisfied ([vF99a]) — and the presuppositional operators that motivate it: only, adversative attitude verbs, superlatives, and conditional antecedents license NPIs without being classically DE.

Main declarations

• IsStrawsonDE, IsStrawsonAntiAdditive, StrawsonValid: the DE notions and validity, relativized to a definedness predicate.
• antitone_implies_strawsonDE, antiAdditive_implies_strawsonAA: the classical notions imply their Strawson forms.
• onlyFull, sorryFull, gladFull, superlativeAssert, condNecessity, sinceFull: the operators, each Strawson-DE (or Strawson-anti-additive) but not classically DE.
• strawsonDE_strictly_weaker_than_DE: each step of AM ⊂ AA ⊂ DE ⊂ Strawson-DE is strict.

Implementation notes

The operators are polymorphic over a world type, taking their presupposition, ordering, and modal-base parameters at mathlib types (Set W, W → Set W, W → Prop). The concrete counterexamples ("not classically DE") are specialized to Fin 4: non-DE-ness is an existence claim about some inhabited domain.

References

• [vF99a] — Strawson entailment and the licensor case studies.
• [Str52] — the presuppositional notion of entailment.

Strawson entailment

def NaturalLogic.IsStrawsonDE {α : Type u_1} {β : Type u_2} (f : Set α → Set β) (defined : Set α → β → Prop) : Prop

Strawson-DE ([vF99a], Definition 14, p. 104).

A function f : Set W → Set W is Strawson-DE with respect to a world-relativized definedness predicate defined iff: for all p ⊆ q, at every world w where defined p w holds (i.e. the presupposition of f(p) is satisfied at w), we have f q w → f p w.

The definedness predicate is world-relativized because presuppositions are world-relative: "sorry that p" presupposes p at the evaluation world, not at all worlds. For "only" the presupposition happens to be world-independent, but the type accommodates factive attitudes.

Equations

• NaturalLogic.IsStrawsonDE f defined = ∀ (p q : Set α), p ⊆ q → ∀ (w : β), defined p w → f q w → f p w

def NaturalLogic.StrawsonValid {W : Type u_1} (premises : List (Set W)) (conclusion : Set W) (presupSatisfied : Prop) : Prop

Strawson-valid inference ([vF99a], Definition 19, p. 105).

An inference from premises to conclusion is Strawson-valid iff it is classically valid once we add the premise that all presuppositions of the conclusion are satisfied.

Equations

• NaturalLogic.StrawsonValid premises conclusion presupSatisfied = (presupSatisfied → ∀ (w : W), (∀ p ∈ premises, p w) → conclusion w)

The classical-to-Strawson hierarchy

theorem NaturalLogic.antitone_implies_strawsonDE {α : Type u_1} {β : Type u_2} (f : Set α → Set β) (hAnti : Antitone f) (defined : Set α → β → Prop) : IsStrawsonDE f defined

Classical DE implies Strawson-DE (for any definedness predicate). The defined p w hypothesis is simply ignored. Polymorphic over domain and codomain to match IsAntiAdditive's shape.

def NaturalLogic.IsStrawsonAntiAdditive {α : Type u_1} {β : Type u_2} (f : Set α → Set β) (defined : Set α → β → Prop) : Prop

Strawson anti-additive — the Strawson-relativized version of anti-additivity. Required by strong NPIs ("lift a finger", "in years"): [Gaj11], [Chi13] ch. 3, [Crn14].

f is Strawson-AA iff for all p, q and worlds w where both f p's and f q's presuppositions are satisfied, f (p ∪ q) w ↔ f p w ∧ f q w.

The Strawson move on AA is the same as on DE: the equality is checked "under the assumption that all presuppositions of the statements involved are satisfied" (vF Definition 19, p. 105). Strong NPIs are licensed in Strawson-AA contexts but not in mere-Strawson-DE contexts — this is the asymmetry that distinguishes "any" (weak, needs only DE) from "lift a finger" (strong, needs AA).

Equations

• NaturalLogic.IsStrawsonAntiAdditive f defined = ∀ (p q : Set α) (w : β), defined p w → defined q w → (f (p ∪ q) w ↔ f p w ∧ f q w)

theorem NaturalLogic.antiAdditive_implies_strawsonAA {α : Type u_1} {β : Type u_2} (f : Set α → Set β) (hAA : IsAntiAdditive f) (defined : Set α → β → Prop) : IsStrawsonAntiAdditive f defined

Classical anti-additivity ⇒ Strawson-AA (definedness is ignored). Polymorphic over {α β : Type*} to match IsStrawsonAntiAdditive's shape.

theorem NaturalLogic.strawsonAA_implies_strawsonDE {W : Type u_1} (f : Set W → Set W) (defined : Set W → W → Prop) (hAA : IsStrawsonAntiAdditive f defined) (hDefSubset : ∀ (p q : Set W), p ⊆ q → ∀ (w : W), defined p w → defined q w) : IsStrawsonDE f defined

Strawson-AA ⇒ Strawson-DE.

Anti-additivity is strictly stronger than DE classically; the same strict inclusion holds in the Strawson-relativized world (modulo suitable presupposition handling).

only (Horn's asymmetric analysis; [Hor96])

only

Horn's analysis: "Only x VP" decomposes into:

• Presupposition (positive): ∃ y, x y ∧ VP y — some witness exists (Horn's amended 1996/1997 version, vF footnote 2 p. 104).
• Assertion (negative): ∀ y, x y ∨ ¬ VP y — no y ≠ x satisfies VP.

Von Fintel's key observation: only is NOT classically DE (onlyFull_not_de below; vF ex. 11 p. 101) but IS Strawson-DE (onlyFull_isStrawsonDE; vF ex. 18 p. 104).

def NaturalLogic.onlyPartialProp {W : Type u_1} (x : W → Prop) (scope : Set W) : Semantics.Presupposition.PartialProp W

"Only x VP" as a PartialProp: Horn's asymmetric decomposition.

Equations

• NaturalLogic.onlyPartialProp x scope = { presup := fun (x_1 : W) => ∃ (y : W), x y ∧ scope y, assertion := fun (x_1 : W) => ∀ (y : W), x y ∨ ¬scope y }

def NaturalLogic.onlyFull {W : Type u_1} (x : W → Prop) (scope : Set W) : Set W

The full "only" meaning: presupposition + assertion combined.

"Only x VP" is true at w iff x satisfies VP AND no one else does. By construction, onlyFull x scope w ↔ (onlyPartialProp x scope).presup w ∧ (onlyPartialProp x scope).assertion w (Iff.rfl).

Equations

• NaturalLogic.onlyFull x scope _w = ((∃ (y : W), x y ∧ scope y) ∧ ∀ (y : W), x y ∨ ¬scope y)

theorem NaturalLogic.onlyFull_eq_prprop {W : Type u_1} (x : W → Prop) (scope : Set W) (w : W) : onlyFull x scope w ↔ (onlyPartialProp x scope).presup w ∧ (onlyPartialProp x scope).assertion w

theorem NaturalLogic.onlyFull_isStrawsonDE {W : Type u_1} (x : W → Prop) : IsStrawsonDE (onlyFull x) fun (scope : Set W) (_w : W) => ∃ (w' : W), x w' ∧ scope w'

Ex. 18 (p. 104): onlyFull is Strawson-DE in its scope.

When the presupposition is satisfied (the focused individual x satisfies the scope P), then P ⊆ Q, "no y ≠ x satisfies Q" implies "no y ≠ x satisfies P" — because P ⊆ Q makes the exclusion easier to satisfy.

The definedness predicate is world-independent (existential presupposition), so the world argument is unused.

theorem NaturalLogic.onlyFull_isStrawsonAA {W : Type u_1} (x : W → Prop) : IsStrawsonAntiAdditive (onlyFull x) fun (scope : Set W) (_w : W) => ∃ (w' : W), x w' ∧ scope w'

[Gaj11] Appendix 1 / eqs. 37-38: onlyFull is Strawson-AA.

This is the load-bearing puzzle of [Gaj11]: vF's recalcitrant Strawson-DE operators are also Strawson-AA, yet they don't license strong NPIs (either, in weeks, punctual until). So Strawson-AA is too weak as a characterization of strong-NPI licensors — Gajewski argues the operative property is DE assessed on the meaning enriched with the licenser's direct implicature, and the apparent AA-requirement is just "DE + scalar endpoint" in disguise (Conjecture 48).

Definedness predicate: existence of a witness for both p and q individually (the conjunctive form of Strawson biconditional definedness).

theorem NaturalLogic.onlyFull_not_de : ¬Antitone (onlyFull fun (x : Fin 4) => x = 0)

Ex. 11 (p. 101): onlyFull is NOT classically DE.

Concrete counterexample over the toy 4-element Fin 4: take p = ∅ and q = {w0} with focus on w0. Then p ⊆ q and onlyFull (· = w0) q w0 holds (w0 satisfies q and is the only such), but onlyFull (· = w0) p w0 fails (the existence presup that someone satisfies p is unmet). Classical DE would require the conclusion to hold.

Adversative attitudes ([Hei92], [KL93])

Adversative/Factive Attitudes

Polymorphic over world type W and two parameters:

• dox : W → Set W — the agent's doxastic accessibility (DOX in [Hei92] / vF eq. 41-50). dox w is the set of worlds compatible with what the agent at w believes.
• bestOf : W → Set W — the worlds in dox w that maximally satisfy the attitude's preference / expectation ordering. Intended to be instantiated with Modality.Kratzer.bestWorlds f g w.

Both sorryFull and gladFull use doxastic factivity (vF eq. 50/53): "α is sorry/glad that p" presupposes that the agent at w believes p, i.e. dox w ⊆ p. This is more faithful to vF §3.2-3.3 than the evaluation-world factivity p w an earlier draft used.

Two glad semantics are provided: gladFull (K&L eq. 50, the analysis vF cites), and gladFullVF (vF eq. 52, the analysis vF prefers). Both are UE in the complement (gladFull_isUE, gladFullVF_isUE), so the headline NPI-licensing prediction is the same; they differ on the factual content of the gladness claim (cf. vF p. 124's Honda Civic example). For sorry the analogous K&L vs vF distinction is collapsed in the substrate's sorryFull (both eq. 50/53 styles produce Strawson-DE; the substrate uses the simpler additive form).

def NaturalLogic.sorryFull {W : Type u_1} (dox bestOf : W → Set W) (p : Set W) : Set W

sorry denotation with doxastic factivity (vF eq. 50/53). α is sorry that p at w iff (i) the agent at w believes p (factivity through belief: dox w ⊆ p) AND (ii) in α's preferred worlds, p does NOT hold (adversative preference).

Equations

• NaturalLogic.sorryFull dox bestOf p w = ((∀ w' ∈ dox w, p w') ∧ ∀ w' ∈ bestOf w, ¬p w')

def NaturalLogic.gladFull {W : Type u_1} (dox bestOf : W → Set W) (p : Set W) : Set W

glad (K&L eq. 50): factivity + congruent preference. "α is glad that p" at w iff agent at w believes p AND in α's preferred worlds, p also holds.

Equations

• NaturalLogic.gladFull dox bestOf p w = ((∀ w' ∈ dox w, p w') ∧ ∀ w' ∈ bestOf w, p w')

theorem NaturalLogic.sorryFull_isStrawsonDE {W : Type u_1} (dox bestOf : W → Set W) : IsStrawsonDE (sorryFull dox bestOf) fun (p : Set W) (w : W) => ∀ w' ∈ dox w, p w'

Ex. 28b (p. 111): sorry IS Strawson-DE in its complement. Definedness is doxastic factivity (dox w ⊆ p). Given doxastic factivity of p and p ⊆ q: doxastic factivity of q is inherited (every dox-world satisfies q since it satisfies p); for all best worlds, ¬q w' (from sorry q) gives ¬p w' by contraposition of p ⊆ q.

theorem NaturalLogic.sorryFull_isStrawsonAA {W : Type u_1} (dox bestOf : W → Set W) : IsStrawsonAntiAdditive (sorryFull dox bestOf) fun (p : Set W) (w : W) => ∀ w' ∈ dox w, p w'

[Gaj11] Appendix 1: sorry is Strawson-AA. Definedness: doxastic factivity of both p and q. Forward direction needs definedness to extract the doxastic-factivity component for each conjunct; reverse direction needs only p ⊆ p ∪ q and the contraposition on best worlds.

theorem NaturalLogic.sorryFull_not_de : ¬Antitone (sorryFull (fun (w : Fin 4) => {w}) fun (x : Fin 4) => {1})

Ex. 30 (p. 111): sorry is NOT classically DE. Concrete witness over toy Fin 4: dox w := {w} (agent believes only actual world), bestOf w := {w1}, p = ∅, q = {w0}. Then sorry q w0 holds but sorry p w0 fails (doxastic factivity of empty p fails).

theorem NaturalLogic.sorryFull_strictly_strawsonDE : (IsStrawsonDE (sorryFull (fun (w : Fin 4) => {w}) fun (x : Fin 4) => {1}) fun (p : Set (Fin 4)) (w : Fin 4) => ∀ w' ∈ {w}, p w') ∧ ¬Antitone (sorryFull (fun (w : Fin 4) => {w}) fun (x : Fin 4) => {1})

sorry is Strawson-DE but NOT classically DE — the canonical adversative example.

theorem NaturalLogic.gladFull_isUE {W : Type u_1} (dox bestOf : W → Set W) : Monotone (gladFull dox bestOf)

glad (K&L eq. 50) is UE in its complement.

Superlatives

Superlatives

vF eq. 79 (p. 139) presupposes Q(α) = True — the designated subject α satisfies the restriction Q. The substrate parameterizes by the individual α : W directly (rather than by a predicate subject : W → Prop), so the presupposition is the literal restriction α. The assertion encodes "no other y in the restriction outranks α" via absence of a non-α witness in the restriction.

The substrate elides scales/degrees: a faithful eq. 79 formalization would need a Degree type and a relation α has_higher_P_than y at d. The current encoding tracks the Strawson-DE structure without the ordinal content, which suffices for the NPI-licensing prediction.

def NaturalLogic.superlativePresup {W : Type u_1} (α : W) (restriction : Set W) (_w : W) : Prop

Presupposition of superlative (vF eq. 79): the designated subject α satisfies the restriction. World-independent.

Equations

• NaturalLogic.superlativePresup α restriction _w = restriction α

def NaturalLogic.superlativeAssert {W : Type u_1} (α : W) (restriction : Set W) : Set W

Superlative assertion: the designated subject α satisfies the restriction, and no y ≠ α in the restriction "outranks" α (encoded here as absence of a non-α witness — placeholder for a real degree order).

Equations

• NaturalLogic.superlativeAssert α restriction _w = (restriction α ∧ ∀ (y : W), y = α ∨ ¬restriction y)

theorem NaturalLogic.superlative_isStrawsonDE {W : Type u_1} (α : W) : IsStrawsonDE (superlativeAssert α) (superlativePresup α)

Ex. 77 (p. 139): superlatives are Strawson-DE in the restriction position. Adding a restriction can only improve the subject's rank, given that α satisfies the new restriction.

theorem NaturalLogic.superlative_isStrawsonAA {W : Type u_1} (α : W) : IsStrawsonAntiAdditive (superlativeAssert α) (superlativePresup α)

[Gaj11] Appendix 1: superlatives are Strawson-AA in the restriction position. The "α is/isn't outranked" universal composes through union/intersection like onlyFull's "no other y satisfies the scope." Definedness: restriction α for both p and q.

Conditional antecedents

Conditional Antecedents

[Kra86]

condNecessity domain α β: "if α, must β" is true at w iff β holds at all α-worlds in domain w. This is the idle-ordering subcase of the Kratzer restrictor analysis. The full Kratzer conditional with a non-trivial preference ordering lives in Semantics/Conditionals/Restrictor.lean::conditionalNecessity and is not monotone in its antecedent — that is the §4 puzzle vF addresses via dynamic context shifts in [vF00]. The substrate's condNecessity here proves the easy idle case so consumer files have a stable handle.

For the genuine non-monotonicity counterexample (vF ex. 70-73), see Conditionals/Restrictor.lean::restrictor_monotone for the idle-base case and Conditionals/Counterfactual.lean for the Stalnaker-Lewis similarity-based operator.

def NaturalLogic.condNecessity {W : Type u_1} (domain : W → Set W) (α β : Set W) : Set W

Conditional necessity via domain restriction (idle ordering source).

Equations

• NaturalLogic.condNecessity domain α β w = ∀ w' ∈ domain w, α w' → β w'

theorem NaturalLogic.conditional_antecedent_antitone {W : Type u_1} (domain : W → Set W) (β : Set W) : Antitone fun (α : Set W) => condNecessity domain α β

The antecedent position of condNecessity is classically DE (Antitone in the polymorphic sense).

theorem NaturalLogic.conditional_antecedent_strawsonDE {W : Type u_1} (domain : W → Set W) (β : Set W) (defined : Set W → W → Prop) : IsStrawsonDE (fun (α : Set W) => condNecessity domain α β) defined

Conditional antecedents are a fortiori Strawson-DE.

theorem NaturalLogic.condNecessity_isAntiAdditive {W : Type u_1} (domain : W → Set W) (β : Set W) : IsAntiAdditive fun (α : Set W) => condNecessity domain α β

Conditional antecedents are classically anti-additive in the antecedent: (P ∪ Q)-restricted modal base = (P-restricted) ∪ (Q-restricted), so universal-over-restriction-implies-consequent distributes appropriately.

theorem NaturalLogic.condNecessity_isStrawsonAA {W : Type u_1} (domain : W → Set W) (β : Set W) : IsStrawsonAntiAdditive (fun (α : Set W) => condNecessity domain α β) fun (x : Set W) (x_1 : W) => True

Conditional antecedents are Strawson-AA with trivial definedness (since they are classically AA).

theorem NaturalLogic.wouldFull_isStrawsonAA {W : Type u_1} (domain : W → Set W) (q : Set W) : IsStrawsonAntiAdditive (fun (p : Set W) => condNecessity domain p q) fun (p : Set W) (w : W) => ∃ w' ∈ domain w, p w'

[Gaj11] Appendix 1's actual would SAA result.

vF's would has the same truth conditions as condNecessity but with the non-vacuity presupposition D_i(w) ∩ p ≠ ∅ (the modal base intersected with the antecedent is non-empty). The SAA proof is identical to the classical AA result; the non-vacuity is what matters for non-trivial Strawson reasoning, not for the AA equation itself.

Strictness

theorem NaturalLogic.strawsonDE_strictly_weaker_than_DE : ∃ (f : Set (Fin 4) → Set (Fin 4)) (defined : Set (Fin 4) → Fin 4 → Prop), IsStrawsonDE f defined ∧ ¬Antitone f

Strawson-DE is strictly weaker than DE: onlyFull is the canonical witness — Strawson-DE without classical DE.

Additional operators

since (Iatridou, vF §2.2 exs. 20-22)

"It's been five years since I saw a bird of prey in this area." Same dialectical structure as only: licenses NPIs but is not classically DE; adding the temporal presupposition (the bird-sighting) restores the inference.

pastEvent w is the set of past worlds (5 years ago); sinceWindow w is the set of intermediate worlds (between past event and now). The operator says: there was an event in pastEvent that satisfied p, and no sinceWindow world has satisfied p.

def NaturalLogic.sinceFull {W : Type u_1} (pastEvent sinceWindow : W → Set W) (p : Set W) : Set W

since(p) denotation.

Equations

• NaturalLogic.sinceFull pastEvent sinceWindow p w = ((∃ w' ∈ pastEvent w, p w') ∧ ∀ w' ∈ sinceWindow w, ¬p w')

theorem NaturalLogic.sinceFull_isStrawsonDE {W : Type u_1} (pastEvent sinceWindow : W → Set W) : IsStrawsonDE (sinceFull pastEvent sinceWindow) fun (p : Set W) (w : W) => ∃ w' ∈ pastEvent w, p w'

since is Strawson-DE in p. Definedness: there is a past p-event (the temporal presupposition). With p ⊆ q, the past p-event is a fortiori a past q-event; the no-since-then-q constraint contraposes to no-since-then-p.

regret, amazed, surprised (vF §3 siblings of sorry)

vF p. 114: "For attitudes like want, wish, glad, regret, sorry the ordering will be one of 'preference'. For attitudes like expect, amazed, surprised the ordering will be one of 'expectation/likelihood'."

The difference is in the ordering source supplied to bestOf, not in the operator's structure. We define regretFull, amazedFull, surprisedFull as aliases of sorryFull with the understanding that their bestOf will be instantiated with different ordering sources at the use site. The Strawson-DE proof is shared.

@[reducible, inline]

abbrev NaturalLogic.regretFull {W : Type u_1} (dox bestOf : W → Set W) (p : Set W) : Set W

regret: preference-based adversative attitude (vF §3 sibling of sorry). Same structure; bestOf carries the preference ordering source.

Equations

• NaturalLogic.regretFull = NaturalLogic.sorryFull

@[reducible, inline]

abbrev NaturalLogic.amazedFull {W : Type u_1} (dox bestOf : W → Set W) (p : Set W) : Set W

amazed: expectation-based adversative attitude. bestOf carries an expectation/likelihood ordering source.

Equations

• NaturalLogic.amazedFull = NaturalLogic.sorryFull

@[reducible, inline]

abbrev NaturalLogic.surprisedFull {W : Type u_1} (dox bestOf : W → Set W) (p : Set W) : Set W

surprised: expectation-based adversative attitude.

Equations

• NaturalLogic.surprisedFull = NaturalLogic.sorryFull