Strawson-relativized soundness

This file relativizes the soundness layer of Logic/Natural/Soundness.lean to presuppositions ([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.

Main declarations

• Relation.HoldsOn: the lattice content of a relation, relativized to a region; at ⊤ it is Relation.Holds.
• Signature.StrawsonSoundFor: Signature.SoundFor with every projected relation read on the symmetric definedness region defined x ⊓ defined y of [Gaj11]'s Strawson anti-additivity.
• strawsonSoundFor_top_iff, Signature.SoundFor.strawsonSoundFor: classical soundness is the trivial-definedness case, and implies the Strawson form at any definedness.
• strawsonSoundFor_anti_of_isStrawsonDE and the operator instances: onlyFull, sorryFull, superlativeAssert, and sinceFull realize the .anti row Strawson-ly while failing it classically.

Implementation notes

The operator instances are the semantic content of the classicalSignature = none rows of Polarity.LicensingContext.properties. Composing definedness along a path is presupposition projection and is deliberately not attempted here; its home is a bridge to Semantics/Presupposition/.

References

• [vF99a] — the Strawson move.
• [Gaj11] — the symmetric definedness gate.

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

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

Equations

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

@[simp]

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

At trivial definedness, relativized content is plain content.

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

Plain content implies relativized content on any region.

def NaturalLogic.Signature.StrawsonSoundFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (σ : Signature) (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

• σ.StrawsonSoundFor f defined = ∀ (R : NaturalLogic.Relation) (x y : α), R.Holds x y → NaturalLogic.Relation.HoldsOn (defined x ⊓ defined y) (NaturalLogic.Signature.project R σ) (f x) (f y)

theorem NaturalLogic.Signature.SoundFor.strawsonSoundFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ : Signature} {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 β] {σ : Signature} {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 : IsStrawsonDE f defined) : Signature.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) : Signature.anti.StrawsonSoundFor (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) : Signature.anti.StrawsonSoundFor (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) : Signature.anti.StrawsonSoundFor (superlativeAssert a) fun (restriction : Set W) => {w : W | 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) : Signature.anti.StrawsonSoundFor (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).