Docs / Semantics / Presupposition / Strawson

Strawson monotonicity

import Linglib.Semantics.Presupposition.Strawson · namespace Presupposition

Source

This file defines monotonicity under Strawson entailment for operators into trivalent propositions. An operator is Strawson downward entailing when shrinking its argument gives a conclusion that the original Strawson-entails, the inference being checked only where the presuppositions involved hold. Von Fintel introduces the notion to keep the Fauconnier–Ladusaw theory of negative polarity licensing for operators that are not downward entailing, and Gajewski adds Strawson anti-additivity. Each property holds as soon as the operator's values, where defined, follow an assertion with the classical property, whatever the presupposition, and without presuppositions the Strawson notions are the classical ones.

Implementation notes

Strawson entailment takes the presuppositions of premise and conclusion alike as premises, as in von Fintel's Strawson validity and Gajewski's own proofs, rather than the literal clause of Gajewski's cross-categorial definition at type t.

References

Strawson monotonicity

L48–51
L53–56
L58–61

An operator whose values, where defined, follow an antitone assertion is Strawson downward entailing, whatever the presupposition.

theorem IsStrawsonDE.of_antitoneL63–67
{α : Type u_1} {W : Type u_2} [Preorder α] {f : α → W → SignType} {a : α → W → Prop} (h : Antitone a) (hf : ∀ (p : α) (w : W), f p w ≠ 0 → (f p w = 1 ↔ a p w)) :
IsStrawsonDE f

Built from

L69–73
L75–77
L90–92
L94–96

Strawson anti-additivity

L106–111
L113–125