Strawson-relativized soundness

[vF99a]'s Strawson move, at signature level: a projection row holds modulo presuppositions when the projected relation holds on the region where the arguments' presuppositions are satisfied. NLRelation.HoldsOn D relativizes the lattice content of a relation to a region D; EntailmentSig.StrawsonSoundFor σ f defined is SoundFor with every projected relation read on defined x ⊓ defined y — the symmetric definedness gate of [Gaj11]'s Strawson anti-additivity. Classical soundness is the trivial-definedness case (strawsonSoundFor_top_iff) and implies the Strawson form at any definedness (EntailmentSig.SoundFor.strawsonSoundFor).

The operator instances are the semantic content of the classicalSignature = none rows of Semantics.Polarity.Licensing.contextProperties: onlyFull, sorryFull, superlativeAssert, and sinceFull realize the .anti row Strawson-ly while failing it classically.

Main declarations

• NLRelation.HoldsOn: relation content relativized to a region;
• EntailmentSig.StrawsonSoundFor: row soundness modulo presupposition;
• strawsonSoundFor_top_iff, EntailmentSig.SoundFor.strawsonSoundFor: the classical ↔ Strawson bridges;
• strawsonSoundFor_anti_of_isStrawsonDE and the four operator instances.

Composing definedness along a path is presupposition projection and is deliberately not attempted here — its home is a bridge to Semantics/Presupposition/, not an ad-hoc operator.

def NaturalLogic.NLRelation.HoldsOn {β : Type u_1} [Lattice β] [BoundedOrder β] (D : β) : NLRelation → β → β → Prop

The lattice content of a relation, relativized to a region D (the worlds where the relevant presuppositions are satisfied). At D = ⊤ this is NLRelation.Holds (holdsOn_top).

Equations

• NaturalLogic.NLRelation.HoldsOn D NaturalLogic.NLRelation.equiv = fun (u v : β) => u ⊓ D = v ⊓ D
• NaturalLogic.NLRelation.HoldsOn D NaturalLogic.NLRelation.forward = fun (u v : β) => u ⊓ D ≤ v
• NaturalLogic.NLRelation.HoldsOn D NaturalLogic.NLRelation.reverse = fun (u v : β) => v ⊓ D ≤ u
• NaturalLogic.NLRelation.HoldsOn D NaturalLogic.NLRelation.negation = fun (u v : β) => u ⊓ v ⊓ D = ⊥ ∧ D ≤ u ⊔ v
• NaturalLogic.NLRelation.HoldsOn D NaturalLogic.NLRelation.alternation = fun (u v : β) => u ⊓ v ⊓ D = ⊥
• NaturalLogic.NLRelation.HoldsOn D NaturalLogic.NLRelation.cover = fun (u v : β) => D ≤ u ⊔ v
• NaturalLogic.NLRelation.HoldsOn D NaturalLogic.NLRelation.independent = fun (x x_1 : β) => True

@[simp]

theorem NaturalLogic.NLRelation.holdsOn_top {β : Type u_1} [Lattice β] [BoundedOrder β] {R : NLRelation} {u v : β} : HoldsOn ⊤ R u v ↔ R.Holds u v

At trivial definedness, relativized content is plain content.

theorem NaturalLogic.NLRelation.Holds.holdsOn {β : Type u_1} [Lattice β] [BoundedOrder β] {R : NLRelation} {u v : β} (D : β) (h : R.Holds u v) : HoldsOn D R u v

Plain content implies relativized content on any region.

def NaturalLogic.EntailmentSig.StrawsonSoundFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (σ : EntailmentSig) (f defined : α → β) : Prop

σ's row is Strawson-sound for f relative to defined: every projected relation holds on the region where both arguments' presuppositions are satisfied — the symmetric gate of [Gaj11]'s IsStrawsonAntiAdditive.

Equations

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

theorem NaturalLogic.EntailmentSig.SoundFor.strawsonSoundFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ : EntailmentSig} {f : α → β} (h : σ.SoundFor f) (defined : α → β) : σ.StrawsonSoundFor f defined

Classical soundness implies Strawson soundness at any definedness.

theorem NaturalLogic.strawsonSoundFor_top_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ : EntailmentSig} {f : α → β} : (σ.StrawsonSoundFor f fun (x : α) => ⊤) ↔ σ.SoundFor f

Strawson soundness at trivial definedness is classical soundness.

The Strawson-DE operator zoo, at signature level

theorem NaturalLogic.strawsonSoundFor_anti_of_isStrawsonDE {W : Type u_1} {W' : Type u_2} {f : Set W → Set W'} {defined : Set W → W' → Prop} (h : Entailment.IsStrawsonDE f defined) : EntailmentSig.anti.StrawsonSoundFor f fun (p : Set W) => {w : W' | defined p w}

[vF99a]'s Strawson-DE, at signature level: a Strawson-DE operator realizes the .anti row relative to its definedness.

theorem NaturalLogic.onlyFull_strawsonSoundFor_anti {W : Type u_1} (x : W → Prop) : EntailmentSig.anti.StrawsonSoundFor (Entailment.onlyFull x) fun (scope : Set W) => {_w : W | ∃ (w' : W), x w' ∧ scope w'}

only realizes the .anti row Strawson-ly (definedness = its existence presupposition) while failing it classically (onlyFull_not_de).

theorem NaturalLogic.sorryFull_strawsonSoundFor_anti {W : Type u_1} (dox bestOf : W → Set W) : EntailmentSig.anti.StrawsonSoundFor (Entailment.sorryFull dox bestOf) fun (p : Set W) => {w : W | ∀ w' ∈ dox w, p w'}

Adversatives (sorry, regret, surprised) realize the .anti row Strawson-ly (definedness = doxastic factivity) while failing it classically (sorryFull_not_de).

theorem NaturalLogic.superlativeAssert_strawsonSoundFor_anti {W : Type u_1} (a : W) : EntailmentSig.anti.StrawsonSoundFor (Entailment.superlativeAssert a) fun (restriction : Set W) => {w : W | Entailment.superlativePresup a restriction w}

Superlatives realize the .anti row Strawson-ly in their restriction (definedness = the designated-subject presupposition).

theorem NaturalLogic.sinceFull_strawsonSoundFor_anti {W : Type u_1} (pastEvent sinceWindow : W → Set W) : EntailmentSig.anti.StrawsonSoundFor (Entailment.sinceFull pastEvent sinceWindow) fun (p : Set W) => {w : W | ∃ w' ∈ pastEvent w, p w'}

Temporal since realizes the .anti row Strawson-ly (definedness = the past-event presupposition).