Content Layers

@cite{van-der-sandt-maier-2003}

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

@cite{van-der-sandt-maier-2003} 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:

• PrProp (presup + assertion) is the 2-layer special case (pr + fr)
• Challengeability (directDenial vs hwamChallenge) identifies which layer is targeted by a discourse challenge
• AtIssueness (atIssue vs notAtIssue) classifies content by whether it addresses the QUD — correlating with fr vs pr/imp
• TraditionalCategory (presupposition vs conventionalImplicature vs supplementary) is a coarser, partially overlapping taxonomy

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 Core/Semantics/ because it generalizes PrProp. Bridges to Core/Discourse/AtIssueness and Phenomena/Presupposition/ ProjectiveContent.Challengeability live downstream in bridge files, preserving the independence of Core/Semantics/ and Core/Discourse/.

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 Theories.Semantics.Dynamic.DRT.Basic as LDRS.directedRA.

inductive Core.Semantics.ContentLayer.ContentLayer : Type

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

@cite{van-der-sandt-maier-2003} 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).

instance Core.Semantics.ContentLayer.instDecidableEqContentLayer : DecidableEq ContentLayer

Equations

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

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

Equations

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

instance Core.Semantics.ContentLayer.instReprContentLayer : Repr ContentLayer

Equations

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

def Core.Semantics.ContentLayer.instBEqContentLayer.beq : ContentLayer → ContentLayer → Bool

Equations

• Core.Semantics.ContentLayer.instBEqContentLayer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Semantics.ContentLayer.instBEqContentLayer : BEq ContentLayer

Equations

• Core.Semantics.ContentLayer.instBEqContentLayer = { beq := Core.Semantics.ContentLayer.instBEqContentLayer.beq }

def Core.Semantics.ContentLayer.instInhabitedContentLayer.default : ContentLayer

Equations

• Core.Semantics.ContentLayer.instInhabitedContentLayer.default = Core.Semantics.ContentLayer.ContentLayer.presupposition

instance Core.Semantics.ContentLayer.instInhabitedContentLayer : Inhabited ContentLayer

Equations

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

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

A full layered proposition: content at each layer.

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

• 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 PrProp.ofBProp sets presupposition to λ _ => true.

def Core.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 Core.Semantics.ContentLayer.ContentLayer.presupposition = lp.presupposition
• lp.get Core.Semantics.ContentLayer.ContentLayer.atIssue = lp.atIssue
• lp.get Core.Semantics.ContentLayer.ContentLayer.implicature = lp.implicature

def Core.Semantics.ContentLayer.LayeredProp.toPrProp {W : Type u_1} (lp : LayeredProp W) : Presupposition.PrProp W

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

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

Equations

• lp.toPrProp = { presup := lp.presupposition, assertion := lp.atIssue }

def Core.Semantics.ContentLayer.LayeredProp.ofPrProp {W : Type u_1} (p : Presupposition.PrProp W) : LayeredProp W

Lift a PrProp to a LayeredProp with trivially true implicature.

This is the canonical embedding: every PrProp is a LayeredProp with no implicature content.

Equations

• Core.Semantics.ContentLayer.LayeredProp.ofPrProp p = { presupposition := p.presup, atIssue := p.assertion }

theorem Core.Semantics.ContentLayer.LayeredProp.roundtrip_prprop {W : Type u_1} (p : Presupposition.PrProp W) : (ofPrProp p).toPrProp = p

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

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

def Core.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 @cite{van-der-sandt-maier-2003}: 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

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

def Core.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 Core.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

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

theorem Core.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)

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

Equations

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

def Core.Semantics.ContentLayer.instBEqKFWorld.beq : Core.Semantics.ContentLayer.KFWorld✝ → Core.Semantics.ContentLayer.KFWorld✝ → Bool

Equations

• Core.Semantics.ContentLayer.instBEqKFWorld.beq x✝ y✝ = (Core.Semantics.ContentLayer.KFWorld.ctorIdx✝ x✝ == Core.Semantics.ContentLayer.KFWorld.ctorIdx✝¹ y✝)

instance Core.Semantics.ContentLayer.instBEqKFWorld : BEq Core.Semantics.ContentLayer.KFWorld✝

Equations

• Core.Semantics.ContentLayer.instBEqKFWorld = { beq := Core.Semantics.ContentLayer.instBEqKFWorld.beq }

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

Equations

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

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

Equations

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

theorem Core.Semantics.ContentLayer.kf_propositional_denial : offensiveLayers Core.Semantics.ContentLayer.kfProp✝ (fun (w : Core.Semantics.ContentLayer.KFWorld✝) => w == Core.Semantics.ContentLayer.KFWorld.kingHairy✝) Core.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 Core.Semantics.ContentLayer.kf_presuppositional_denial : offensiveLayers Core.Semantics.ContentLayer.kfProp✝ (fun (w : Core.Semantics.ContentLayer.KFWorld✝) => w == Core.Semantics.ContentLayer.KFWorld.noKing1✝ || w == Core.Semantics.ContentLayer.KFWorld.noKing2✝) Core.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.

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

Equations

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

instance Core.Semantics.ContentLayer.instBEqModalW : BEq Core.Semantics.ContentLayer.ModalW✝

Equations

• Core.Semantics.ContentLayer.instBEqModalW = { beq := Core.Semantics.ContentLayer.instBEqModalW.beq }

def Core.Semantics.ContentLayer.instBEqModalW.beq : Core.Semantics.ContentLayer.ModalW✝ → Core.Semantics.ContentLayer.ModalW✝ → Bool

Equations

• Core.Semantics.ContentLayer.instBEqModalW.beq x✝ y✝ = (Core.Semantics.ContentLayer.ModalW.ctorIdx✝ x✝ == Core.Semantics.ContentLayer.ModalW.ctorIdx✝¹ y✝)

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

Equations

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

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

Equations

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

theorem Core.Semantics.ContentLayer.modal_implicature_denial : offensiveLayers Core.Semantics.ContentLayer.modalProp✝ (fun (w : Core.Semantics.ContentLayer.ModalW✝) => w == Core.Semantics.ContentLayer.ModalW.nec✝) Core.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."