Content Layers

[MvdS03]

Semantic content is stratified into layers that determine its discourse behavior: how it projects, what denial can target, and whether it addresses the QUD.

[MvdS03] propose Layered DRT (LDRT), where every DRS condition carries a label — pr (presupposition), fr (at-issue), or imp (implicature) — that determines how it behaves in denial. This module extracts the layer system as a standalone type that unifies several existing linglib distinctions:

• PartialProp (presup + assertion) is the 2-layer special case (pr + fr)
• AtIssueness (atIssue vs notAtIssue) classifies content by whether it addresses the QUD — correlating with fr vs pr/imp

The Three Layers

Layer	Label	Denial example
Presupposition	pr	"The king of France is NOT bald — there is no king" (30b)
At-issue	fr	"Mary is NOT happy — she's miserable" (5)
Implicature	imp	"It's not POSSIBLE — it's NECESSARY" (29b)

Design Note

ContentLayer lives in Semantics/ because it generalizes PartialProp. The diagnostic SCF/OLE taxonomy of projective content ([TBRS13]) lives in Semantics/Presupposition/ProjectiveContent.lean.

Scope

This module captures the layer taxonomy and the Off function (which layers are offensive = inconsistent with a correction). The directed reverse anaphora (RA*) mechanism that uses Off to selectively retract conditions is defined in Studies/VanDerSandtMaier2003.lean as LDRS.directedRA.

See also: Semantics/Composition/Layered.BiLayered

Semantics/Composition/Layered.lean defines a 2-layer Prop-valued sibling BiLayered W (atIssue / notAtIssue, both W → Prop) with [MV26]'s composition rules I/II/III. Use LayeredProp when LDRT's offensive-layer machinery is needed; use BiLayered when the analysis only distinguishes at-issue from not-at-issue and operates over Set W (verum, evidential illocution, biased polar questions). A future Layered n parameterised refactor would consolidate the two.

inductive Semantics.ContentLayer.ContentLayer : Type

The layer of a semantic contribution, determining its discourse behavior.

[MvdS03] introduce this three-way distinction in Layered DRT, but the classification is framework-independent: it captures a difference in how content projects, how it can be challenged, and what denial can target.

• presupposition : ContentLayer

  Backgrounded precondition. Projects past negation, questions, modals. Targeted by "Hey wait a minute!" challenge. Example: "stop" presupposes prior state; "the king" presupposes existence.

• atIssue : ContentLayer

  Free/assertoric content. Addresses the QUD directly. Targeted by direct denial ("No, that's not true"). Example: "The king is bald" asserts baldness.

• implicature : ContentLayer

  Enrichment beyond literal truth conditions. Covers both scalar implicature (category D: "possible" implicates "not necessary") and connotation/register (category E: "steed" connotes formality). The paper groups both under imp as non-truth-conditional material targetable by denial. Example: "It's not POSSIBLE — it's NECESSARY" (29b).

@[implicit_reducible]

instance Semantics.ContentLayer.instDecidableEqContentLayer : DecidableEq ContentLayer

Equations

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

@[implicit_reducible]

instance Semantics.ContentLayer.instReprContentLayer : Repr ContentLayer

Equations

• Semantics.ContentLayer.instReprContentLayer = { reprPrec := Semantics.ContentLayer.instReprContentLayer.repr }

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

Equations

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

@[implicit_reducible]

instance Semantics.ContentLayer.instInhabitedContentLayer : Inhabited ContentLayer

Equations

• Semantics.ContentLayer.instInhabitedContentLayer = { default := Semantics.ContentLayer.instInhabitedContentLayer.default }

structure Semantics.ContentLayer.LayeredProp (W : Type u_1) : Type u_1

A full layered proposition: content at each layer.

Generalizes PartialProp from 2 layers to 3. When implicature is trivially true, a LayeredProp degenerates to a PartialProp.

• presupposition : W → Bool

  Presuppositional content (must hold for definedness).

• atIssue : W → Bool

  At-issue/assertoric content.

• implicature : W → Bool

  Implicature content (enrichment beyond truth conditions). Trivially true by default: most utterances carry no relevant implicature, just as PartialProp.ofProp sets presupposition to λ _ => True.

def Semantics.ContentLayer.LayeredProp.get {W : Type u_1} (lp : LayeredProp W) : ContentLayer → W → Bool

Access a layer's content by its tag.

Equations

• lp.get Semantics.ContentLayer.ContentLayer.presupposition = lp.presupposition
• lp.get Semantics.ContentLayer.ContentLayer.atIssue = lp.atIssue
• lp.get Semantics.ContentLayer.ContentLayer.implicature = lp.implicature

def Semantics.ContentLayer.LayeredProp.toPartialProp {W : Type u_1} (lp : LayeredProp W) : Presupposition.PartialProp W

Project a LayeredProp to a PartialProp by discarding the implicature layer.

This is the canonical projection: PartialProp is the 2-layer special case where implicature is invisible.

Equations

• lp.toPartialProp = { presup := fun (w : W) => lp.presupposition w = true, assertion := fun (w : W) => lp.atIssue w = true }

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

Lift a PartialProp to a LayeredProp with trivially true implicature.

This is the canonical embedding: every PartialProp is a LayeredProp with no implicature content. Noncomputable because Prop → Bool requires classical decidability.

Equations

• Semantics.ContentLayer.LayeredProp.ofPartialProp p = { presupposition := fun (w : W) => if p.presup w then true else false, atIssue := fun (w : W) => if p.assertion w then true else false }

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

The round-trip PartialProp → LayeredProp → PartialProp is the identity.

This confirms that PartialProp embeds faithfully into LayeredProp: no information is lost or added in the embedding.

def Semantics.ContentLayer.isOffensive {W : Type u_1} (φ : LayeredProp W) (l : ContentLayer) (correction : W → Bool) (worlds : List W) : Bool

Layer l of φ is offensive with respect to a correction when no world satisfies both the layer's content and the correction.

Off(φ, K) from [MvdS03]: the offensive layers are those whose content is inconsistent with the correction context. In propositional denial, only fr is offensive; in presuppositional denial, pr (and fr) are offensive; in implicature denial, imp is offensive.

Equations

• Semantics.ContentLayer.isOffensive φ l correction worlds = !worlds.any fun (w : W) => φ.get l w && correction w

def Semantics.ContentLayer.offensiveLayers {W : Type u_1} (φ : LayeredProp W) (correction : W → Bool) (worlds : List W) : List ContentLayer

Collect all offensive layers of φ with respect to a correction.

Equations

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

def Semantics.ContentLayer.isConsistent {W : Type u_1} (φ : LayeredProp W) (l : ContentLayer) (correction : W → Bool) (worlds : List W) : Bool

A non-offensive layer's content is consistent with the correction: some world satisfies both.

Equations

• Semantics.ContentLayer.isConsistent φ l correction worlds = worlds.any fun (w : W) => φ.get l w && correction w

theorem Semantics.ContentLayer.consistent_iff_not_offensive {W : Type u_1} (φ : LayeredProp W) (l : ContentLayer) (correction : W → Bool) (worlds : List W) : isConsistent φ l correction worlds = !isOffensive φ l correction worlds

Consistency is the negation of offensiveness.

Example 1: King of France (30)

"The king of France is bald" has:

• pr: France has a king (definite presupposition)
• fr: The king is bald (at-issue content)
• imp: trivially true (no implicature)

Two corrections disambiguate the denial:

• "He has a full head of hair" → propositional denial (only fr offensive)
• "France does not have a king" → presuppositional denial (pr and fr both offensive)

@[implicit_reducible]

instance Semantics.ContentLayer.instDecidableEqKFWorld : DecidableEq Semantics.ContentLayer.KFWorld✝

Equations

• Semantics.ContentLayer.instDecidableEqKFWorld x✝ y✝ = if h : Semantics.ContentLayer.KFWorld.ctorIdx✝ x✝ = Semantics.ContentLayer.KFWorld.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

def Semantics.ContentLayer.instReprKFWorld.repr : Semantics.ContentLayer.KFWorld✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.ContentLayer.instReprKFWorld : Repr Semantics.ContentLayer.KFWorld✝

Equations

• Semantics.ContentLayer.instReprKFWorld = { reprPrec := Semantics.ContentLayer.instReprKFWorld.repr }

theorem Semantics.ContentLayer.kf_propositional_denial : offensiveLayers Semantics.ContentLayer.kfProp✝ (fun (w : Semantics.ContentLayer.KFWorld✝) => w == Semantics.ContentLayer.KFWorld.kingHairy✝) Semantics.ContentLayer.kfWorlds✝ = [ContentLayer.atIssue]

Propositional denial: correction "he has hair" conflicts with fr only.

The presupposition (king exists) is consistent with the correction (world kingHairy satisfies both), so pr is NOT offensive. But no world is both bald and hairy, so fr IS offensive.

Corresponds to the standard propositional-denial reading of (30).

theorem Semantics.ContentLayer.kf_presuppositional_denial : offensiveLayers Semantics.ContentLayer.kfProp✝ (fun (w : Semantics.ContentLayer.KFWorld✝) => w == Semantics.ContentLayer.KFWorld.noKing1✝ || w == Semantics.ContentLayer.KFWorld.noKing2✝) Semantics.ContentLayer.kfWorlds✝ = [ContentLayer.presupposition, ContentLayer.atIssue]

Presuppositional denial: correction "no king exists" conflicts with both pr and fr.

No world has both "king exists" and "no king exists," so pr is offensive. No world is both "bald" and "no king," so fr is ALSO offensive — the assertion "falls with" the presupposition.

Corresponds to (30b): "The king of France is NOT bald — France does not have a king."

Example 2: Possibility → Necessity (29)

"It is possible that the pope is right" has:

• pr: trivially true
• fr: ◇p (it is possible)
• imp: ¬□p (not necessary — the scalar implicature of "possible")

Correction: "It is NECESSARY that the pope is right" (□p). Only imp is offensive: ◇p is consistent with □p (necessity entails possibility), but ¬□p contradicts □p.

@[implicit_reducible]

instance Semantics.ContentLayer.instDecidableEqModalW : DecidableEq Semantics.ContentLayer.ModalW✝

Equations

• Semantics.ContentLayer.instDecidableEqModalW x✝ y✝ = if h : Semantics.ContentLayer.ModalW.ctorIdx✝ x✝ = Semantics.ContentLayer.ModalW.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.ContentLayer.instReprModalW : Repr Semantics.ContentLayer.ModalW✝

Equations

• Semantics.ContentLayer.instReprModalW = { reprPrec := Semantics.ContentLayer.instReprModalW.repr }

def Semantics.ContentLayer.instReprModalW.repr : Semantics.ContentLayer.ModalW✝ → ℕ → Std.Format

Equations

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

theorem Semantics.ContentLayer.modal_implicature_denial : offensiveLayers Semantics.ContentLayer.modalProp✝ (fun (w : Semantics.ContentLayer.ModalW✝) => w == Semantics.ContentLayer.ModalW.nec✝) Semantics.ContentLayer.modalWorlds✝ = [ContentLayer.implicature]

Implicature denial: correction "it is necessary" conflicts with imp only.

The presupposition (trivially true) and at-issue content (◇p) are both consistent with the correction (□p entails ◇p). Only the scalar implicature (¬□p) conflicts.

Corresponds to (29b): "It is not POSSIBLE, it is NECESSARY that the pope is right."

BiLayered: 2-layer ⟨A, N⟩ Prop-valued sibling

A Prop-valued 2-layer sibling of LayeredProp ([MV26], inheriting the percolation discipline of [Pot05] and the at-issue proposal / appositive imposition split of [ABBH15]): the at-issue layer is the proffered content, the not-at-issue layer backgrounds presuppositions, conventional implicatures, and evidential commitments — collapsing LayeredProp's presupposition and implicature layers into a single notAtIssue. The substrate stays propositional (W → Prop) because the consumers (verum studies, evidential illocution, biased polar questions) operate over Set W.

Rule	When to use	At-issue layer	Not-at-issue layer
I	β has trivial NAI; α brings NAI	α.A β.A	α.N β.A
II	both α and β bring NAI	α.A β.A	α.N β.A ∧ β.N
III	α is illocutionary, takes the full ⟨A, N⟩ pair	(full pair handed to α)	(full pair handed to α)

structure Semantics.ContentLayer.BiLayered (W : Type u_1) : Type u_1

A 2-layer ⟨A, N⟩ proposition. Trivially-true notAtIssue is the default — most expressions add no not-at-issue content, so the empty case should be cheap to construct.

• atIssue : W → Prop

  Proffered, at-issue content.

• notAtIssue : W → Prop

  Backgrounded, not-at-issue content. Defaults to trivially true.

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

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

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

Lift a single proposition to a BiLayered with trivial NAI.

Equations

• Semantics.ContentLayer.BiLayered.ofProp p = { atIssue := p }

@[simp]

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

@[simp]

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

def Semantics.ContentLayer.composeI {W : Type u_1} (atFn naiFn : (W → Prop) → W → Prop) (β : BiLayered W) : BiLayered W

[MV26] Composition rule I: β has empty NAI; α brings NAI. The new at-issue layer is α.A β.A; the new NAI is α.N β.A.

Equations

• Semantics.ContentLayer.composeI atFn naiFn β = { atIssue := atFn β.atIssue, notAtIssue := naiFn β.atIssue }

def Semantics.ContentLayer.composeII {W : Type u_1} (atFn naiFn : (W → Prop) → W → Prop) (β : BiLayered W) : BiLayered W

[MV26] Composition rule II: both α and β bring NAI. The new NAI accumulates α.N β.A ∧ β.N.

Equations

• Semantics.ContentLayer.composeII atFn naiFn β = { atIssue := atFn β.atIssue, notAtIssue := fun (w : W) => naiFn β.atIssue w ∧ β.notAtIssue w }

def Semantics.ContentLayer.composeIII {W : Type u_1} (op : BiLayered W → BiLayered W) (β : BiLayered W) : BiLayered W

[MV26] Composition rule III: an illocutionary operator takes the full ⟨A, N⟩ pair from β and returns a new pair.

Equations

• Semantics.ContentLayer.composeIII op β = op β

@[simp]

theorem Semantics.ContentLayer.composeI_atIssue {W : Type u_1} (atFn naiFn : (W → Prop) → W → Prop) (β : BiLayered W) : (composeI atFn naiFn β).atIssue = atFn β.atIssue

@[simp]

theorem Semantics.ContentLayer.composeI_notAtIssue {W : Type u_1} (atFn naiFn : (W → Prop) → W → Prop) (β : BiLayered W) : (composeI atFn naiFn β).notAtIssue = naiFn β.atIssue

@[simp]

theorem Semantics.ContentLayer.composeII_atIssue {W : Type u_1} (atFn naiFn : (W → Prop) → W → Prop) (β : BiLayered W) : (composeII atFn naiFn β).atIssue = atFn β.atIssue

@[simp]

theorem Semantics.ContentLayer.composeII_notAtIssue {W : Type u_1} (atFn naiFn : (W → Prop) → W → Prop) (β : BiLayered W) : (composeII atFn naiFn β).notAtIssue = fun (w : W) => naiFn β.atIssue w ∧ β.notAtIssue w

@[simp]

theorem Semantics.ContentLayer.composeIII_apply {W : Type u_1} (op : BiLayered W → BiLayered W) (β : BiLayered W) : composeIII op β = op β

theorem Semantics.ContentLayer.composeI_eq_composeII_on_trivial_naiFn {W : Type u_2} (atFn naiFn : (W → Prop) → W → Prop) (β : BiLayered W) (hβ : β.notAtIssue = fun (x : W) => True) : composeI atFn naiFn β = composeII atFn naiFn β

Composition I subsumes Composition II when β.N is trivially true: the extra ∧ True conjunct collapses. The formal sense in which rule II generalises rule I.