Content layers

This file defines the three layers of a semantic contribution — presupposition, at-issue content, and implicature — the propositions carrying content at each layer, and the layers of such a proposition that a correction makes offensive, which a denial targets. The layers are [van-der-sandt-maier-2003]'s labels pr, fr, and imp of Layered DRT; PartialProp is the two-layer case, and BiLayered collapses the two backgrounded layers into one not-at-issue layer for analyses that only separate proffered from backgrounded content ([anderbois-brasoveanu-henderson-2015]).

Main definitions

• ContentLayer — the three layers.
• LayeredProp — content at each layer, with get, toPartialProp, ofPartialProp, and toBiLayered.
• LayeredProp.IsOffensive, LayeredProp.offensiveLayers — the layers inconsistent with a correction.
• BiLayered — at-issue and not-at-issue content, with ofProp.

References

• [van-der-sandt-maier-2003]
• [tonhauser-beaver-roberts-simons-2013]
• [anderbois-brasoveanu-henderson-2015]

inductive Presupposition.ContentLayer : Type

The layer of a semantic contribution: a backgrounded precondition, the proffered content, or an enrichment beyond the truth conditions.

• presupposition : ContentLayer
• atIssue : ContentLayer
• implicature : ContentLayer

@[instance_reducible]

instance Presupposition.instDecidableEqContentLayer : DecidableEq ContentLayer

Equations

• Presupposition.instDecidableEqContentLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Presupposition.instFintypeContentLayer : Fintype ContentLayer

Equations

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

def Presupposition.instReprContentLayer.repr : ContentLayer → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Presupposition.instReprContentLayer : Repr ContentLayer

Equations

• Presupposition.instReprContentLayer = { reprPrec := Presupposition.instReprContentLayer.repr }

structure Presupposition.LayeredProp (W : Type u_1) : Type u_1

Content at each of the three layers; the implicature layer is trivial by default.

• presupposition : W → Prop
• atIssue : W → Prop
• implicature : W → Prop

theorem Presupposition.LayeredProp.ext_iff {W : Type u_1} {x y : LayeredProp W} : x = y ↔ x.presupposition = y.presupposition ∧ x.atIssue = y.atIssue ∧ x.implicature = y.implicature

theorem Presupposition.LayeredProp.ext {W : Type u_1} {x y : LayeredProp W} (presupposition : x.presupposition = y.presupposition) (atIssue : x.atIssue = y.atIssue) (implicature : x.implicature = y.implicature) : x = y

structure Presupposition.BiLayered (W : Type u_1) : Type u_1

At-issue and not-at-issue content; the not-at-issue layer is trivial by default.

• atIssue : W → Prop
• notAtIssue : W → Prop

theorem Presupposition.BiLayered.ext {W : Type u_1} {x y : BiLayered W} (atIssue : x.atIssue = y.atIssue) (notAtIssue : x.notAtIssue = y.notAtIssue) : x = y

theorem Presupposition.BiLayered.ext_iff {W : Type u_1} {x y : BiLayered W} : x = y ↔ x.atIssue = y.atIssue ∧ x.notAtIssue = y.notAtIssue

def Presupposition.BiLayered.ofProp {W : Type u_1} (p : W → Prop) : BiLayered W

A proposition with no not-at-issue content.

Equations

• Presupposition.BiLayered.ofProp p = { atIssue := p }

@[simp]

theorem Presupposition.BiLayered.ofProp_atIssue {W : Type u_1} (p : W → Prop) : (ofProp p).atIssue = p

@[simp]

theorem Presupposition.BiLayered.ofProp_notAtIssue {W : Type u_1} (p : W → Prop) : (ofProp p).notAtIssue = fun (x : W) => True

def Presupposition.LayeredProp.get {W : Type u_1} (φ : LayeredProp W) : ContentLayer → W → Prop

The content at a layer.

Equations

• φ.get Presupposition.ContentLayer.presupposition = φ.presupposition
• φ.get Presupposition.ContentLayer.atIssue = φ.atIssue
• φ.get Presupposition.ContentLayer.implicature = φ.implicature

@[instance_reducible]

instance Presupposition.LayeredProp.instDecidablePredGetOfPresuppositionOfAtIssueOfImplicature {W : Type u_1} (φ : LayeredProp W) [DecidablePred φ.presupposition] [DecidablePred φ.atIssue] [DecidablePred φ.implicature] (l : ContentLayer) : DecidablePred (φ.get l)

Equations

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

def Presupposition.LayeredProp.toPartialProp {W : Type u_1} (φ : LayeredProp W) : PartialProp W

The two-layer proposition, discarding the implicature.

Equations

• φ.toPartialProp = { presup := φ.presupposition, assertion := φ.atIssue }

def Presupposition.LayeredProp.ofPartialProp {W : Type u_1} (p : PartialProp W) : LayeredProp W

A two-layer proposition, with no implicature.

Equations

• Presupposition.LayeredProp.ofPartialProp p = { presupposition := p.presup, atIssue := p.assertion }

@[simp]

theorem Presupposition.LayeredProp.toPartialProp_ofPartialProp {W : Type u_1} (p : PartialProp W) : (ofPartialProp p).toPartialProp = p

def Presupposition.LayeredProp.toBiLayered {W : Type u_1} (φ : LayeredProp W) : BiLayered W

The backgrounded layers collapsed into the not-at-issue layer.

Equations

• φ.toBiLayered = { atIssue := φ.atIssue, notAtIssue := fun (w : W) => φ.presupposition w ∧ φ.implicature w }

def Presupposition.LayeredProp.IsOffensive {W : Type u_1} (φ : LayeredProp W) (l : ContentLayer) (K : Set W) : Prop

Layer l is offensive against the correction K when no K-world satisfies its content — the layers a denial with correction K targets.

Equations

• φ.IsOffensive l K = ∀ w ∈ K, ¬φ.get l w

theorem Presupposition.LayeredProp.isOffensive_iff_disjoint {W : Type u_1} (φ : LayeredProp W) (l : ContentLayer) (K : Set W) : φ.IsOffensive l K ↔ Disjoint {w : W | φ.get l w} K

@[instance_reducible]

instance Presupposition.LayeredProp.instDecidableIsOffensiveOfFintypeOfMemSetOfDecidablePredGet {W : Type u_1} (φ : LayeredProp W) [Fintype W] (l : ContentLayer) (K : Set W) [DecidablePred fun (x : W) => x ∈ K] [DecidablePred (φ.get l)] : Decidable (φ.IsOffensive l K)

Equations

• φ.instDecidableIsOffensiveOfFintypeOfMemSetOfDecidablePredGet l K = Presupposition.LayeredProp.instDecidableIsOffensiveOfFintypeOfMemSetOfDecidablePredGet._aux_1 φ l K

def Presupposition.LayeredProp.offensiveLayers {W : Type u_1} (φ : LayeredProp W) (K : Set W) [(l : ContentLayer) → Decidable (φ.IsOffensive l K)] : Finset ContentLayer

The layers offensive against the correction K.

Equations

• φ.offensiveLayers K = {x : Presupposition.ContentLayer | φ.IsOffensive x K}