Strawson-DE (@cite{von-fintel-1999}, Definition 14).
A function f : BProp World → BProp World 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 must accommodate factive attitudes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strawson-valid inference (@cite{von-fintel-1999}, Definition 19).
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
- One or more equations did not get rendered due to their size.
Instances For
Every classically DE function is Strawson-DE (for any definedness predicate).
Proof: the defined p w hypothesis is simply ignored; the Antitone proof
gives us f(q) ≤ f(p) unconditionally.
This establishes: DE ⊆ Strawson-DE.
Every anti-additive function is Strawson-DE.
Via: AA → DE → Strawson-DE.
Every anti-morphic function is Strawson-DE.
Via: AM → AA → DE → Strawson-DE.
The full hierarchy chain: AM → AA → DE → Strawson-DE.
Given an anti-morphic proof, we can derive all weaker properties.
- am : AntiAdditivity.IsAntiMorphic f
- de : Polarity.IsDownwardEntailing f
- strawsonDE : IsStrawsonDE f defined
Instances For
Negation satisfies the full hierarchy.
Equations
- ⋯ = ⋯
Instances For
"Only" #
@cite{von-fintel-1999} @cite{strawson-1952}
Horn's analysis: "Only x VP" decomposes into:
- Presupposition (positive): x VP (the focused individual satisfies VP)
- Assertion (negative): no y ≠ x satisfies VP
Von Fintel's key observation: "Only" is NOT classically DE, but IS Strawson-DE.
Counterexample to classical DE (ex 11): "Only John ate vegetables" does NOT entail "Only John ate kale" (Even though kale ⊆ vegetables: the presupposition that John ate kale may fail)
But with presupposition satisfied: If John ate kale (presup), then "Only John ate vegetables" DOES entail "Only John ate kale" — because if no one else ate vegetables, and kale ⊆ vegetables, then no one else ate kale.
"Only x VP" as a PrProp: Horn's asymmetric decomposition.
- Presupposition: the focused individual x satisfies VP
- Assertion: no y ≠ x satisfies VP
Uses Core.Presupposition.PrProp directly, making the presupposition/assertion
split structural rather than ad-hoc.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full "only" meaning: presupposition + assertion combined.
"Only x VP" is true at w iff x satisfies VP AND no one else does.
Equivalent to (onlyPrProp x scope).presup w && (onlyPrProp x scope).assertion w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
onlyFull equals the conjunction of onlyPrProp's components.
"Only" (full meaning) is not classically DE (von Fintel ex 11).
Counterexample: kale ⊆ vegetables, but "Only J ate vegetables" ⊬ "Only J ate kale" because J may have eaten vegetables but not kale.
The assertion component of "only" IS Strawson-DE.
When the presupposition is satisfied (the focused individual x satisfies the scope P), then: if P ⊆ Q, "no y≠x satisfies Q" implies "no y≠x satisfies P" — because P ⊆ Q.
This is von Fintel's central insight for "only" (Theorem 1 / ex 18).
The definedness predicate is world-independent (existential presupposition), so the extra world argument is unused.
Adversative/Factive Attitudes #
@cite{von-fintel-1999} @cite{heim-1992}
Von Fintel's analysis (§3): "sorry", "surprised", "regret" license NPIs in their complement position. The full denotation includes the factivity presupposition: "sorry that p" = "p holds AND the agent's preferred worlds have ¬p" (the agent wishes p weren't true).
Key insight: the full operator is NOT classically DE — narrowing p to p' ⊆ p may fail because the factivity presupposition (p' holds at the evaluation world) isn't guaranteed. But with Strawson-DE, adding the factivity presupposition of the conclusion makes the DE inference go through: if p' holds at w, then q(w) → p(w) for the factivity part, and ¬q → ¬p by contraposition for the preference part.
Contrast: "glad that p" = "p holds AND the agent's preferred worlds have p." This is UE in the complement — so "glad" does NOT license NPIs.
The bestOf parameter corresponds to bestWorlds f g from
Modality/Kratzer.lean (Kratzer's modal base + ordering source).
The two modules use different World types, so the connection is
structural rather than via direct import.
sorry denotation: adversative factive attitude (full operator).
"α is sorry that p" = p holds at w (factivity) AND in α's preferred worlds, p is NOT true (adversative preference).
bestOf w returns the "best" accessible worlds from w — intended to be
instantiated with Kratzer.bestWorlds f g from Modality/Kratzer.lean.
Unlike the assertion-only version (which would be trivially DE by contraposition), this full operator includes the positive factivity component, which is what blocks classical DE.
Equations
- Semantics.Entailment.StrawsonEntailment.sorryFull bestOf p w = (p w && (bestOf w).all fun (w' : Semantics.Entailment.World) => !p w')
Instances For
glad denotation: non-adversative factive attitude (full operator).
"α is glad that p" = p holds at w (factivity) AND in α's preferred worlds, p IS true (congruent preference).
Equations
- Semantics.Entailment.StrawsonEntailment.gladFull bestOf p w = (p w && (bestOf w).all fun (w' : Semantics.Entailment.World) => p w')
Instances For
sorry (full meaning) is NOT classically DE.
The factivity presupposition (positive component p w) blocks DE:
narrowing the scope from q to p ⊆ q may fail because p w = true is
not guaranteed by q w = true.
Counterexample: p = ∅, q = {w0}. sorry(q)(w0) = true (w0 satisfies q, and best worlds have ¬q). sorry(p)(w0) = false (w0 doesn't satisfy p). DE would require true ≤ false.
sorry IS Strawson-DE in its complement.
The definedness condition is factivity at the evaluation world:
p w = true (p holds at the world where we're checking the inference).
Given factivity (p w = true) and p ⊆ q:
q w = truefollows from p ≤ q — factivity of q is inherited- For all best worlds w': if ¬q(w') (from sorry(q)), then ¬p(w') by contraposition of p ≤ q
So sorry(q)(w) = true implies sorry(p)(w) = true, when p(w) = true.
sorry is Strawson-DE but NOT DE — the canonical adversative example.
glad is NOT Strawson-DE — it is upward entailing (UE).
If p ⊆ q: p(w) = true → q(w) = true, and all preferred worlds satisfying
p also satisfy q. So glad preserves entailment direction — it does NOT
license NPIs.
This is the adversative/non-adversative asymmetry that von Fintel §3.3 identifies as the key to NPI licensing in attitude complements.
Superlatives #
"The tallest girl who ___" is Strawson-DE in the relative clause position.
- "Emma is the tallest girl who ever won" ✓ (ex 75)
- But not classically DE: "tallest girl in her class ⇏ tallest to learn the alphabet" (ex 76), because the presupposition that Emma learned the alphabet may not hold.
Presupposition of superlative: subject satisfies the domain predicate.
"The tallest girl who VP" presupposes the subject is a girl who VP'd.
The world argument is unused: this presupposition is world-independent (it's about whether the subject satisfies the restriction at any world).
Equations
- Semantics.Entailment.StrawsonEntailment.superlativePresup subject restriction _w = ∃ (w' : Semantics.Entailment.World), subject w' = true ∧ restriction w' = true
Instances For
Superlative assertion: subject has the highest degree among those satisfying the restriction.
Simplified model: the "tallest who VP" at w checks that no one else in the restriction exceeds the subject.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Superlatives are Strawson-DE in the restriction position (ex 77).
When the presupposition is met (subject satisfies the restriction P), if P ⊆ Q, then "tallest who Q" entails "tallest who P" — the subject's rank can only improve by narrowing the comparison class.
Proof strategy: Part 1 (existential) follows from the presupposition.
Part 2 (universal) case-splits on whether any non-subject satisfies P:
if not, the disjunct ¬C(P) is trivially true; if so, monotonicity
gives C(Q), and the pointwise fact for Q transfers to P via p ≤ q.
Conditional Antecedents #
@cite{von-fintel-1999} @cite{kratzer-1986}
If-clauses license NPIs: "If you've ever been to Paris, you know the Louvre." Under the restrictor analysis (@cite{kratzer-1986}), "if α, must β" = necessity over the α-restricted modal base. The antecedent position is classically DE: strengthening the antecedent can only shrink the domain, making the universal check easier to satisfy.
condNecessity corresponds to conditionalNecessity f emptyBackground α β
from Conditionals/Restrictor.lean (with empty ordering source, where
best worlds = accessible worlds). The two modules use different World
types, so the correspondence is structural.
Conditional necessity via domain restriction.
"If α, must β" is true at w iff β holds at all α-worlds accessible from w.
domain w returns accessible worlds — intended to be instantiated with
Kratzer.accessibleWorlds f from Modality/Kratzer.lean.
Equations
- Semantics.Entailment.StrawsonEntailment.condNecessity domain α β w = (List.filter α (domain w)).all β
Instances For
The antecedent position of condNecessity is classically DE.
If α₁ ⊆ α₂, then "if α₂, must β" entails "if α₁, must β": the α₁-worlds
are a subset of the α₂-worlds, so the .all β check passes on the smaller
set whenever it passes on the larger.
Conditional antecedent is Strawson-DE (trivially, since it is classically DE).
Connections to Existing Infrastructure #
Bridge theorems linking IsStrawsonDE to:
IsDownwardEntailing = Antitone(fromPolarity.lean)IsAntiAdditive(fromAntiAdditivity.lean)PrProp.strawsonEntails(fromCore/Presupposition.lean)
Bridge: IsDE (= Antitone) implies IsStrawsonDE for any definedness.
This is just de_implies_strawsonDE but using the IsDE abbreviation
from Polarity.lean.
Negation is Strawson-DE (trivially, since it's anti-morphic).
"No student" is Strawson-DE (trivially, since it's anti-additive → DE).
"At most 2 students" is Strawson-DE (trivially, since it's DE).
Strawson-DE is strictly weaker than DE: there exist functions that are Strawson-DE but not DE. "Only" is the canonical example.