Strawson Entailment

@cite{von-fintel-1999} @cite{strawson-1952}

Strawson-DE: a weakened downward entailingness that checks DE inferences only when presuppositions of the conclusion are satisfied. This rescues the Fauconnier-Ladusaw analysis for four "recalcitrant" NPI licensors: only (§2), adversative attitude verbs (§3), superlatives (§4.2), and conditional antecedents (§4.1). These are not classically DE but do license NPIs; Strawson-DE explains why.

Polymorphism

The substrate is polymorphic over {W : Type*}. The operators (onlyFull, sorryFull, gladFull, superlativeAssert, condNecessity) take a polymorphic world type and the corresponding presupposition / ordering / modal-base parameters in their natural mathlib types (Set W, W → Set W, W → Prop). Concrete counterexamples (proofs of the form "X is not classically DE") are specialized to the 4-element World enum from Entailment/Basic.lean as a witness type, since non-DE-ness is an existence claim about some inhabited domain.

Hierarchy

AM ⊂ AA ⊂ DE ⊂ Strawson-DE (each strict — see strawsonDE_strictly_weaker_than_DE).

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

Strawson-DE (@cite{von-fintel-1999}, 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

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

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

Strawson-valid inference (@cite{von-fintel-1999}, 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

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

theorem Semantics.Entailment.StrawsonEntailment.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.

theorem Semantics.Entailment.StrawsonEntailment.de_implies_strawsonDE (f : Set World → Set World) (hDE : Polarity.IsDownwardEntailing f) (defined : Set World → World → Prop) : IsStrawsonDE f defined

Convenience: IsDownwardEntailing (the toy-World abbrev) implies Strawson-DE.

theorem Semantics.Entailment.StrawsonEntailment.antiAdditive_implies_strawsonDE (f : Set World → Set World) (hAA : AntiAdditivity.IsAntiAdditive f) (defined : Set World → World → Prop) : IsStrawsonDE f defined

Anti-additive ⇒ Strawson-DE.

theorem Semantics.Entailment.StrawsonEntailment.antiMorphic_implies_strawsonDE (f : Set World → Set World) (hAM : AntiAdditivity.IsAntiMorphic f) (defined : Set World → World → Prop) : IsStrawsonDE f defined

Anti-morphic ⇒ Strawson-DE.

def Semantics.Entailment.StrawsonEntailment.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"): @cite{gajewski-2011}, @cite{chierchia-2013} ch. 3, @cite{crnic-2014}.

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

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

theorem Semantics.Entailment.StrawsonEntailment.antiAdditive_implies_strawsonAA {α : Type u_1} {β : Type u_2} (f : Set α → Set β) (hAA : AntiAdditivity.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 Semantics.Entailment.StrawsonEntailment.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).

structure Semantics.Entailment.StrawsonEntailment.FullHierarchy (f : Set World → Set World) (defined : Set World → World → Prop) : Prop

The full hierarchy: AM → AA → DE → Strawson-DE.

• am : AntiAdditivity.IsAntiMorphic f
• aa : AntiAdditivity.IsAntiAdditive f
• de : Polarity.IsDownwardEntailing f
• strawsonDE : IsStrawsonDE f defined

def Semantics.Entailment.StrawsonEntailment.pnot_fullHierarchy (defined : Set World → World → Prop) : FullHierarchy pnot defined

Negation satisfies the full hierarchy.

Equations

• ⋯ = ⋯

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 Semantics.Entailment.StrawsonEntailment.onlyPrProp {W : Type u_1} (x : W → Prop) (scope : Set W) : Core.Presupposition.PrProp W

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

Equations

• Semantics.Entailment.StrawsonEntailment.onlyPrProp 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 Semantics.Entailment.StrawsonEntailment.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 ↔ (onlyPrProp x scope).presup w ∧ (onlyPrProp x scope).assertion w (Iff.rfl).

Equations

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

theorem Semantics.Entailment.StrawsonEntailment.onlyFull_eq_prprop {W : Type u_1} (x : W → Prop) (scope : Set W) (w : W) : onlyFull x scope w ↔ (onlyPrProp x scope).presup w ∧ (onlyPrProp x scope).assertion w

theorem Semantics.Entailment.StrawsonEntailment.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 Semantics.Entailment.StrawsonEntailment.onlyFull_isStrawsonAA {W : Type u_1} (x : W → Prop) : IsStrawsonAntiAdditive (onlyFull x) fun (scope : Set W) (_w : W) => ∃ (w' : W), x w' ∧ scope w'

@cite{gajewski-2011} Appendix 1 / eqs. 37-38: onlyFull is Strawson-AA.

This is the load-bearing puzzle of @cite{gajewski-2011}: 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 Semantics.Entailment.StrawsonEntailment.onlyFull_not_de : ¬Polarity.IsDownwardEntailing (onlyFull fun (x : World) => x = World.w0)

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

Concrete counterexample over the toy 4-element World: 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/Factive Attitudes

Polymorphic over world type W and two parameters:

• dox : W → Set W — the agent's doxastic accessibility (DOX in @cite{heim-1992} / 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 Semantics.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 Semantics.Entailment.StrawsonEntailment.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

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

def Semantics.Entailment.StrawsonEntailment.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

• Semantics.Entailment.StrawsonEntailment.gladFull dox bestOf p w = ((∀ w' ∈ dox w, p w') ∧ ∀ w' ∈ bestOf w, p w')

def Semantics.Entailment.StrawsonEntailment.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

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

theorem Semantics.Entailment.StrawsonEntailment.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 Semantics.Entailment.StrawsonEntailment.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'

@cite{gajewski-2011} 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 Semantics.Entailment.StrawsonEntailment.sorryFull_not_de : ¬Polarity.IsDownwardEntailing (sorryFull (fun (w : World) => {w}) fun (x : World) => {World.w1})

Ex. 30 (p. 111): sorry is NOT classically DE. Concrete witness over toy World: 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 Semantics.Entailment.StrawsonEntailment.sorryFull_strictly_strawsonDE : (IsStrawsonDE (sorryFull (fun (w : World) => {w}) fun (x : World) => {World.w1}) fun (p : Set World) (w : World) => ∀ w' ∈ {w}, p w') ∧ ¬Polarity.IsDownwardEntailing (sorryFull (fun (w : World) => {w}) fun (x : World) => {World.w1})

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

theorem Semantics.Entailment.StrawsonEntailment.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.

theorem Semantics.Entailment.StrawsonEntailment.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.

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 Semantics.Entailment.StrawsonEntailment.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

• Semantics.Entailment.StrawsonEntailment.superlativePresup α restriction _w = restriction α

def Semantics.Entailment.StrawsonEntailment.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

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

theorem Semantics.Entailment.StrawsonEntailment.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 Semantics.Entailment.StrawsonEntailment.superlative_isStrawsonAA {W : Type u_1} (α : W) : IsStrawsonAntiAdditive (superlativeAssert α) (superlativePresup α)

@cite{gajewski-2011} 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

@cite{kratzer-1986}

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 Theories/Semantics/Conditionals/Restrictor.lean::conditionalNecessity and is not monotone in its antecedent — that is the §4 puzzle vF addresses via dynamic context shifts in @cite{von-fintel-2000}. 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 Semantics.Entailment.StrawsonEntailment.condNecessity {W : Type u_1} (domain : W → Set W) (α β : Set W) : Set W

Conditional necessity via domain restriction (idle ordering source).

Equations

• Semantics.Entailment.StrawsonEntailment.condNecessity domain α β w = ∀ w' ∈ domain w, α w' → β w'

theorem Semantics.Entailment.StrawsonEntailment.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 Semantics.Entailment.StrawsonEntailment.conditional_antecedent_DE (domain : World → Set World) (β : Set World) : Polarity.IsDownwardEntailing fun (α : Set World) => condNecessity domain α β

Specialization of conditional_antecedent_antitone to the toy World for use with the IsDownwardEntailing abbrev.

theorem Semantics.Entailment.StrawsonEntailment.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 Semantics.Entailment.StrawsonEntailment.condNecessity_isAntiAdditive {W : Type u_1} (domain : W → Set W) (β : Set W) : AntiAdditivity.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 Semantics.Entailment.StrawsonEntailment.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 Semantics.Entailment.StrawsonEntailment.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'

@cite{gajewski-2011} 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.

theorem Semantics.Entailment.StrawsonEntailment.pnot_isStrawsonDE (defined : Set World → World → Prop) : IsStrawsonDE pnot defined

Negation is Strawson-DE.

theorem Semantics.Entailment.StrawsonEntailment.no_student_isStrawsonDE (defined : Set World → World → Prop) : IsStrawsonDE AntiAdditivity.no_student defined

"No student" is Strawson-DE.

theorem Semantics.Entailment.StrawsonEntailment.atMost2_isStrawsonDE (defined : Set World → World → Prop) : IsStrawsonDE AntiAdditivity.atMost2_student defined

"At most 2 students" is Strawson-DE.

theorem Semantics.Entailment.StrawsonEntailment.strawsonDE_strictly_weaker_than_DE : ∃ (f : Set World → Set World) (defined : Set World → World → Prop), IsStrawsonDE f defined ∧ ¬Polarity.IsDownwardEntailing f

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

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 Semantics.Entailment.StrawsonEntailment.sinceFull {W : Type u_1} (pastEvent sinceWindow : W → Set W) (p : Set W) : Set W

since(p) denotation.

Equations

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

theorem Semantics.Entailment.StrawsonEntailment.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 Semantics.Entailment.StrawsonEntailment.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

• Semantics.Entailment.StrawsonEntailment.regretFull = Semantics.Entailment.StrawsonEntailment.sorryFull

@[reducible, inline]

abbrev Semantics.Entailment.StrawsonEntailment.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

• Semantics.Entailment.StrawsonEntailment.amazedFull = Semantics.Entailment.StrawsonEntailment.sorryFull

@[reducible, inline]

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

surprised: expectation-based adversative attitude.

Equations

• Semantics.Entailment.StrawsonEntailment.surprisedFull = Semantics.Entailment.StrawsonEntailment.sorryFull

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 Semantics.Entailment.StrawsonEntailment.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

• Semantics.Entailment.StrawsonEntailment.wantFull bestOf p w = ∀ w' ∈ bestOf w, p w'

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

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

wish (Iatridou; vF Curveball #1, pp. 127-129)

α wishes p ≈ α thinks: if p were the case, α would be glad that p. Iatridou's analysis (eq. 59) embeds a counterfactual conditional inside the attitude, making wish non-monotonic in p. We do not formalize this analysis — its non-monotonicity is itself the puzzle vF flags as a threat to the K&L claim that wish that p ≡ sorry that ¬p.

A simpler "wish ≡ sorry-of-negation" placeholder is recoverable as fun p => sorryFull dox bestOf (compl p), which preserves DE-ness on the K&L side; this is what wishFull_simple below offers.

def Semantics.Entailment.StrawsonEntailment.wishFull_simple {W : Type u_1} (dox bestOf : W → Set W) (p : Set W) : Set W

A simplified wish(p) ≡ sorry(¬p) denotation (the K&L analysis vF discusses on p. 126; Iatridou's counterfactual analysis is more complex and breaks monotonicity — see module docstring).

Equations

• Semantics.Entailment.StrawsonEntailment.wishFull_simple dox bestOf p = Semantics.Entailment.StrawsonEntailment.sorryFull dox bestOf fun (w : W) => ¬p w

IsWDE — Asher 1987 Weakened Downward Entailment

@cite{asher-1987}

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 Semantics.Entailment.StrawsonEntailment.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

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

theorem Semantics.Entailment.StrawsonEntailment.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.