Mixed Quotation

@cite{kirk-giannini-2024}

Formal apparatus for overt and covert mixed quotation, following Kirk-Giannini 2024 "Covert mixed quotation" (Semantics & Pragmatics 17).

Core Idea

Mixed quotation is a compositional interaction between pure quotation and a covert mixed quotation operator 𝔐. A mixed-quoted expression simultaneously:

1. Used: contributes its at-issue semantic value to composition
2. Mentioned: peripherally entails that some salient speaker produced an utterance of that expression

The theory introduces four covert operators:

• 𝔐 (mixed quotation): at-issue ⟨*⟩ meaning + peripheral R attribution
• ↓ (shunting): moves peripheral content to the at-issue dimension
• † (diagonalizer): shifts ⟨*⟩ to evaluate at the world of evaluation
• 𝔄 (appropriateness): modalizes peripheral content via ◆

These operators unify five phenomena: CI projection failure, c-monsters, metalinguistic negation, metalinguistic negotiation, and "in a sense" constructions.

Connection to Existing Infrastructure

The TwoDimProp type from @cite{potts-2005} provides the at-issue × peripheral carrier. pureQuote (added to TwoDimProp) blocks CI projection under quotation. The operators here compose over TwoDimProp.

The quotative interpretation function ⟨⟩ — implemented as QuotInterp below — is from @cite{shan-2010}. K-G writes (paper p.12, p.15): "Drawing on Shan, I implement this proposal about the at-issue contribution of mixed-quoted items using a purpose-built quotative interpretation function ⟨⟩." (∗) is therefore Shan's; K-G's contribution is the covert apparatus 𝔐, ↓, †, 𝔄 layered on top.

Flat (TwoDimProp) vs. Layered (MQProp) Model

Two carriers are exposed:

• Flat TwoDimProp (at-issue × ci): Potts 2005's original bi-dimensional architecture. applyApprop REPLACES the ci dimension with appropriateness content — the original R-attribution from 𝔐 is overwritten when 𝔄 fires. Sufficient for at-issue truth-conditional predictions; cannot record that the utterance attribution survives embedding.

• Layered MQProp (at-issue × R-content × appropContent): refines the peripheral dimension into two distinct layers. applyMQ writes to R; applyApprop writes to ◆; shunt moves ◆ to at-issue; neg preserves both peripheral layers. Crown theorem full_chain_preserves_rContent: R survives the full 𝔐 → 𝔄 → ↓ → ¬ chain.

When to use which. Flat for at-issue-truth-conditional predictions where R is irrelevant (e.g. LoGuercio2025's CI work). Layered when the prediction is about R-survival or when both peripheral dimensions matter independently (K-G §3 metalinguistic negation, §1 strip-then-mix observation that 𝔐 introduces R-attribution while 𝔄 leaves it intact).

Bridge: MQProp.toFlat projects the layered model down by discarding R-content and using ◆-content as the flat ci. flat_agreement_atIssue and flat_loses_rContent quantify the agreement and the information loss of the projection.

@[reducible, inline]

abbrev Semantics.Quotation.QuotInterp (Expr Speaker W : Type) : Type

The quotative interpretation function ⟨*⟩.

Maps an expression q, a world of utterance w₁, and a speaker s to the extension of q as uttered by s at w₁, evaluated at world of evaluation w₂.

⟦⟨*⟩⟧(q, w₁, s, w₂) = χ where χ is the extension at w₂ of the intension contributed by an utterance of q by s at w₁.

Equations

• Semantics.Quotation.QuotInterp Expr Speaker W = (Expr → W → Speaker → W → Prop)

@[reducible, inline]

abbrev Semantics.Quotation.UttRel (Speaker Utt Expr W : Type) : Type

The utterance relation R.

R(s, u, q, w) holds iff speaker s produced utterance u of expression q at world w. Introduced peripherally by 𝔐 and resolved as a discourse anaphor.

Equations

• Semantics.Quotation.UttRel Speaker Utt Expr W = (Speaker → Utt → Expr → W → Prop)

structure Semantics.Quotation.MQContext (W Expr Speaker Utt : Type) : Type

A mixed quotation context: the discourse-anaphoric parameters and interpretation functions needed to evaluate mixed quotation.

The speaker sx and utterance ux are free variables resolved by discourse anaphora — they pick out the salient individual who produced the quoted material and the utterance event in which they did so.

• interp : QuotInterp Expr Speaker W

  Quotative interpretation function ⟨*⟩

• uttRel : UttRel Speaker Utt Expr W

  Utterance relation R

• sx : Speaker

  Anaphorically retrieved speaker

• ux : Utt

  Anaphorically retrieved utterance

• wc : W

  World of context

def Semantics.Quotation.MQContext.applyMQ {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) : Pragmatics.Expressives.TwoDimProp W

Apply the mixed quotation operator 𝔐 to an expression.

Returns a TwoDimProp with:

• at-issue: ⟨q⟩(wc)(sx) — the extension as used by the speaker at the world of context
• peripheral: R(sx, ux, q) — the speaker produced this utterance

This is the core of the theory: mixed quotation arises compositionally from these two semantic contributions of 𝔐.

Equations

• ctx.applyMQ q = { atIssue := ctx.interp q ctx.wc ctx.sx, ci := ctx.uttRel ctx.sx ctx.ux q }

@[simp]

theorem Semantics.Quotation.MQContext.applyMQ_atIssue {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) : (ctx.applyMQ q).atIssue = ctx.interp q ctx.wc ctx.sx

Projection of applyMQ onto the at-issue dimension: ⟨*⟩(q)(wc)(sx).

@[simp]

theorem Semantics.Quotation.MQContext.applyMQ_ci {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) : (ctx.applyMQ q).ci = ctx.uttRel ctx.sx ctx.ux q

Projection of applyMQ onto the peripheral dimension: R(sx, ux, q).

def Semantics.Quotation.shunt {W : Type} (p : Pragmatics.Expressives.TwoDimProp W) : Pragmatics.Expressives.TwoDimProp W

The shunting operator ↓: moves peripheral content to the at-issue dimension by conjoining it with at-issue content.

After shunting, the at-issue content becomes p.atIssue ∧ p.ci and peripheral content becomes trivial.

This operator is independently motivated (@cite{potts-2007}, McCready 2010) and is what allows peripheral content from mixed quotation to interact with higher at-issue operators like negation and conditionals. In the Writer monad architecture for CI effects (see Theories.Semantics.Composition.Effects.twoDimToWriter), shunting corresponds to running the Writer by folding the CI log into the value via conjunction (see runCIWriter and runCIWriter_twoDim in Theories.Semantics.Composition.Effects).

Equations

• Semantics.Quotation.shunt p = { atIssue := fun (w : W) => p.atIssue w ∧ p.ci w, ci := fun (x : W) => True }

@[simp]

theorem Semantics.Quotation.shunt_atIssue {W : Type} (p : Pragmatics.Expressives.TwoDimProp W) (w : W) : (shunt p).atIssue w ↔ p.atIssue w ∧ p.ci w

Shunting conjoins both dimensions into at-issue.

@[simp]

theorem Semantics.Quotation.shunt_ci {W : Type} (p : Pragmatics.Expressives.TwoDimProp W) (w : W) : (shunt p).ci w

Shunting trivializes peripheral content.

theorem Semantics.Quotation.shunt_atIssue_idempotent {W : Type} (p : Pragmatics.Expressives.TwoDimProp W) (w : W) : (shunt (shunt p)).atIssue w ↔ (shunt p).atIssue w

Shunting is idempotent on the at-issue dimension: once peripheral content has been consumed, shunting again has no effect.

def Semantics.Quotation.diagonalize {W Expr Speaker : Type} (interp : QuotInterp Expr Speaker W) (s : Speaker) (q : Expr) : W → Prop

The diagonalizer †: shifts the quotative interpretation so that at the world of evaluation w, the expression's meaning is what it would be as uttered by the speaker at w (rather than at wc).

This captures c-monstrous behavior without positing actual context monsters. "If Pluto were a planet" accesses the meaning 'planet' would have if conventions were different — because the diagonalizer evaluates ⟨planet⟩(w)(s) at the counterfactual world w where conventions still classify Pluto as a planet.

Formally: †(f) = f* where f*(q)(w) = ⟨q⟩(w)(s)(w) — the world of utterance and world of evaluation collapse.

Equations

• Semantics.Quotation.diagonalize interp s q w = interp q w s w

@[simp]

theorem Semantics.Quotation.diag_collapses_worlds {W Expr Speaker : Type} (interp : QuotInterp Expr Speaker W) (s : Speaker) (q : Expr) (w : W) : diagonalize interp s q w = interp q w s w

Diagonalization collapses world of utterance and evaluation.

def Semantics.Quotation.diagonalizeKG {W Expr Speaker : Type} (interp : QuotInterp Expr Speaker W) (q : Expr) : W → Prop

K-G's diagonalizer † with the ∃-over-speakers.

The bare diagonalize above is parameterized on a single speaker — it captures only the world-collapse half of K-G's footnote 22 definition (paper p.26):

† ⤳ λf. ∃s : f = λq. ⟨⟩(q)(w_c)(s).f

The ∃s quantifies over speakers/communities producing the variant function f* (the world-of-evaluation form f*(s) := λq. ⟨*⟩(q)(w)(s)). This existential is what makes c-monsters work: "Pluto could have been a planet" is true when there EXISTS a speaker whose use of 'planet' includes Pluto under the diagonalized reading — not just when the actual speaker's use does.

The bare diagonalize is the per-speaker witness; diagonalizeKG adds the existential. Bridge: diagonalizeKG_iff_exists_diagonalize.

Equations

• Semantics.Quotation.diagonalizeKG interp q w = ∃ (s : Speaker), interp q w s w

@[simp]

theorem Semantics.Quotation.diagonalizeKG_iff_exists_diagonalize {W Expr Speaker : Type} (interp : QuotInterp Expr Speaker W) (q : Expr) (w : W) : diagonalizeKG interp q w ↔ ∃ (s : Speaker), diagonalize interp s q w

diagonalizeKG is the existential closure of diagonalize over speakers.

def Semantics.Quotation.QuotInterp.fn22Wellformed {W Expr Speaker : Type} (interp : QuotInterp Expr Speaker W) (wc : W) : Prop

K-G's footnote 22 well-definedness condition.

For f* to be well-defined as a function (rather than a relation), no two speakers may agree on extensions of all expressions at the world of context wc while disagreeing on extensions at some other world.

Paper p.26 footnote: "I assume here that there are no two speakers or linguistic communities which assign the same extensions to all expressions in w_c but assign different extensions to some expressions in other worlds."

This is a global structural property of interp — it's about how speakers relate across worlds. Without it, the existential in diagonalizeKG overgenerates (any two speakers can act as witnesses for incompatible diagonal contents at the same world). K-G accepts this assumption to keep the semantics deterministic; it is independently violable.

Equations

• interp.fn22Wellformed wc = ∀ (s s' : Speaker), (∀ (q : Expr) (w : W), interp q wc s w ↔ interp q wc s' w) → ∀ (q : Expr) (w : W), interp q w s w ↔ interp q w s' w

theorem Semantics.Quotation.diagonalizeKG_deterministic_under_fn22 {W Expr Speaker : Type} (interp : QuotInterp Expr Speaker W) (wc : W) (h : interp.fn22Wellformed wc) (s s' : Speaker) (hAgree : ∀ (q : Expr) (w : W), interp q wc s w ↔ interp q wc s' w) (q : Expr) (w : W) : diagonalize interp s q w ↔ diagonalize interp s' q w

Under fn22-wellformedness, speakers who agree on extensions at wc across the entire vocabulary agree on diagonal extensions everywhere. This is the substantive use of fn22Wellformed: it lifts wc-extensional agreement to global agreement, which is what makes the existential in diagonalizeKG deterministic.

@[reducible, inline]

abbrev Semantics.Quotation.AppropStandard (Speaker Expr W : Type) : Type

An appropriateness standard: given a speaker and expression at a world, whether it is or would be appropriate for that speaker to use that expression.

This is the semantic content of the appropriateness modal ◆ in Kirk-Giannini's system. The modal quantifies over an accessibility relation, but for finite models we represent the result directly.

Equations

• Semantics.Quotation.AppropStandard Speaker Expr W = (Speaker → Expr → W → Prop)

def Semantics.Quotation.applyApprop {W Expr Speaker : Type} (approp : AppropStandard Speaker Expr W) (sx : Speaker) (q : Expr) (p : Pragmatics.Expressives.TwoDimProp W) : Pragmatics.Expressives.TwoDimProp W

The appropriateness operator 𝔄: replaces the peripheral content of a mixed-quoted expression with appropriateness content.

In the paper's compositional chain, 𝔄 operates on 𝔐's output: 𝔐(q) → 𝔄 → ↓ → ¬. The at-issue content from 𝔐 passes through unchanged; only the peripheral dimension is replaced with the proposition that the verbatim use of the expression is or would be appropriate. This is the key ingredient for metalinguistic negation: when ↓ shunts this appropriateness content to at-issue and negation scopes over the result, we get "not (p ∧ appropriate-to-say-q)".

Equations

• Semantics.Quotation.applyApprop approp sx q p = { atIssue := p.atIssue, ci := approp sx q }

@[simp]

theorem Semantics.Quotation.approp_preserves_atIssue {W Expr Speaker : Type} (approp : AppropStandard Speaker Expr W) (sx : Speaker) (q : Expr) (p : Pragmatics.Expressives.TwoDimProp W) : (applyApprop approp sx q p).atIssue = p.atIssue

𝔄 preserves at-issue content: it only replaces the peripheral dimension.

@[simp]

theorem Semantics.Quotation.applyApprop_ci {W Expr Speaker : Type} (approp : AppropStandard Speaker Expr W) (sx : Speaker) (q : Expr) (p : Pragmatics.Expressives.TwoDimProp W) : (applyApprop approp sx q p).ci = approp sx q

𝔄 replaces the peripheral dimension with appropriateness content.

theorem Semantics.Quotation.metalinguistic_neg_truth_conditions {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (approp : AppropStandard Speaker Expr W) (q : Expr) (w : W) : (shunt (applyApprop approp ctx.sx q (ctx.applyMQ q))).neg.atIssue w ↔ ¬(ctx.interp q ctx.wc ctx.sx w ∧ approp ctx.sx q w)

Metalinguistic negation truth conditions.

Negating a shunted appropriateness-enhanced mixed quotation yields: ¬(at-issue-meaning ∧ appropriate-to-use-expression).

This is the core prediction for metalinguistic negation: "I didn't manage to trap two MONGEESE" is true iff it's not the case that (I managed to trap two mongooses AND it's appropriate to call them 'mongeese'). Since the second conjunct is false (it's not appropriate), the negation is true even though I did manage to trap two mongooses.

theorem Semantics.Quotation.metalinguistic_neg_targets_appropriateness {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (approp : AppropStandard Speaker Expr W) (q : Expr) (w : W) (h_true : ctx.interp q ctx.wc ctx.sx w) (h_inapprop : ¬approp ctx.sx q w) : (shunt (applyApprop approp ctx.sx q (ctx.applyMQ q))).neg.atIssue w

The affirmed conjunct in metalinguistic negation.

In "I didn't trap two MONGEESE — I trapped two MONGOOSES", the second clause entails the at-issue content of the first. So the negation is understood as targeting the appropriateness conjunct: it's not appropriate to use 'mongeese'.

theorem Semantics.Quotation.mixed_quot_strips_original_ci {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) (originalCI : W → Prop) (w : W) : have quoted := (Pragmatics.Expressives.TwoDimProp.withCI (ctx.interp q ctx.wc ctx.sx) originalCI).pureQuote; quoted.ci w

Pure quotation composes with 𝔐: the expression is first purely quoted (stripping its original CI content), then 𝔐 re-introduces peripheral content attributing the utterance to the speaker.

This explains why CI items (expressives, slurs, NRRCs) don't project out of indirect speech reports: the material is first pure-quoted (stripping CIs) before being mixed-quoted (adding speaker attribution).

Two-Layer Peripheral Content

The flat TwoDimProp model has a single peripheral dimension, which forces 𝔄 to replace the R-content with ◆-content. This breaks Writer monotonicity: the log is overwritten rather than appended.

The non-monotonicity is an artifact of collapsing two genuinely distinct peripheral layers into one field:

• R-peripheral: utterance attribution R(s,u,q). Always projects to the discourse root. Never shunted. Never targeted by negation. Resolved as a discourse anaphor.
• ◆-peripheral: appropriateness ◆(s,q). Can be shunted by ↓ into the at-issue dimension. Targetable by negation after shunting.

In the two-layer model, 𝔐 writes to the R-layer and 𝔄 writes to the ◆-layer. No replacement — both layers are independently append-only. The key structural results:

1. Layer preservation: each operator preserves the layer it doesn't target (R persists through 𝔄, ↓, ¬)
2. Shunting conservation: ↓ is information-conservative — total content across all layers is invariant under shunting
3. Flat agreement: the flat TwoDimProp model is a projection of the two-layer model that agrees on at-issue content
4. Per-layer monotonicity: each layer satisfies Writer-style append-only behavior

structure Semantics.Quotation.MQProp (W : Type) : Type

• atIssue : W → Prop

  At-issue (truth-conditional) content

• rContent : W → Prop

  R-peripheral: utterance attribution. Projects universally.

• appropContent : W → Prop

  ◆-peripheral: appropriateness. Shuntable into at-issue.

@[reducible]

def Semantics.Quotation.MQProp.applyMQ {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) : MQProp W

𝔐 on the two-layer type: at-issue ← ⟨*⟩(q), R-layer ← R(s,u,q), ◆-layer trivial (no appropriateness content yet).

Equations

• Semantics.Quotation.MQProp.applyMQ ctx q = { atIssue := ctx.interp q ctx.wc ctx.sx, rContent := ctx.uttRel ctx.sx ctx.ux q, appropContent := fun (x : W) => True }

@[reducible]

def Semantics.Quotation.MQProp.applyApprop {W Expr Speaker : Type} (approp : AppropStandard Speaker Expr W) (sx : Speaker) (q : Expr) (p : MQProp W) : MQProp W

𝔄 on the two-layer type: writes to the ◆-layer only. R-content and at-issue are preserved — no log replacement.

Equations

• Semantics.Quotation.MQProp.applyApprop approp sx q p = { atIssue := p.atIssue, rContent := p.rContent, appropContent := fun (w : W) => p.appropContent w ∧ approp sx q w }

@[reducible]

def Semantics.Quotation.MQProp.shunt {W : Type} (p : MQProp W) : MQProp W

↓ on the two-layer type: conjoins ◆-content into at-issue. R-content is preserved — shunting is selective.

Equations

• p.shunt = { atIssue := fun (w : W) => p.atIssue w ∧ p.appropContent w, rContent := p.rContent, appropContent := fun (x : W) => True }

@[reducible]

def Semantics.Quotation.MQProp.neg {W : Type} (p : MQProp W) : MQProp W

Negation on the two-layer type: negates at-issue only. Both peripheral layers are preserved.

Equations

• p.neg = { atIssue := fun (w : W) => ¬p.atIssue w, rContent := p.rContent, appropContent := p.appropContent }

@[simp]

theorem Semantics.Quotation.MQProp.applyApprop_preserves_rContent {W Expr Speaker : Type} (approp : AppropStandard Speaker Expr W) (sx : Speaker) (q : Expr) (p : MQProp W) : (applyApprop approp sx q p).rContent = p.rContent

𝔄 preserves R-content.

@[simp]

theorem Semantics.Quotation.MQProp.applyApprop_preserves_atIssue {W Expr Speaker : Type} (approp : AppropStandard Speaker Expr W) (sx : Speaker) (q : Expr) (p : MQProp W) : (applyApprop approp sx q p).atIssue = p.atIssue

𝔄 preserves at-issue content.

@[simp]

theorem Semantics.Quotation.MQProp.applyApprop_appropContent {W Expr Speaker : Type} (approp : AppropStandard Speaker Expr W) (sx : Speaker) (q : Expr) (p : MQProp W) (w : W) : (applyApprop approp sx q p).appropContent w ↔ p.appropContent w ∧ approp sx q w

𝔄 appends appropriateness to ◆-content (no replacement).

@[simp]

theorem Semantics.Quotation.MQProp.shunt_preserves_rContent {W : Type} (p : MQProp W) : p.shunt.rContent = p.rContent

↓ preserves R-content: shunting is selective.

@[simp]

theorem Semantics.Quotation.MQProp.shunt_atIssue {W : Type} (p : MQProp W) (w : W) : p.shunt.atIssue w ↔ p.atIssue w ∧ p.appropContent w

↓ conjoins ◆-content into at-issue.

@[simp]

theorem Semantics.Quotation.MQProp.shunt_appropContent {W : Type} (p : MQProp W) (w : W) : p.shunt.appropContent w

↓ trivializes ◆-content (the layer is "drained").

@[simp]

theorem Semantics.Quotation.MQProp.neg_preserves_rContent {W : Type} (p : MQProp W) : p.neg.rContent = p.rContent

¬ preserves R-content.

@[simp]

theorem Semantics.Quotation.MQProp.neg_preserves_appropContent {W : Type} (p : MQProp W) : p.neg.appropContent = p.appropContent

¬ preserves ◆-content.

theorem Semantics.Quotation.MQProp.neg_preserves_both_peripherals {W : Type} (p : MQProp W) : p.neg.rContent = p.rContent ∧ p.neg.appropContent = p.appropContent

¬ preserves both peripheral dimensions (combined ergonomic lemma bundling neg_preserves_rContent and neg_preserves_appropContent).

@[simp]

theorem Semantics.Quotation.MQProp.neg_atIssue {W : Type} (p : MQProp W) (w : W) : p.neg.atIssue w ↔ ¬p.atIssue w

¬ negates the at-issue dimension.

@[simp]

theorem Semantics.Quotation.MQProp.applyMQ_atIssue {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) : (applyMQ ctx q).atIssue = ctx.interp q ctx.wc ctx.sx

𝔐 produces ⟨*⟩(q)(wc)(sx) on the at-issue dimension.

@[simp]

theorem Semantics.Quotation.MQProp.applyMQ_rContent {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) : (applyMQ ctx q).rContent = ctx.uttRel ctx.sx ctx.ux q

𝔐 produces R(sx, ux, q) on the R-layer.

@[simp]

theorem Semantics.Quotation.MQProp.applyMQ_appropContent {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (q : Expr) (w : W) : (applyMQ ctx q).appropContent w

𝔐 leaves the ◆-layer trivial — appropriateness has not been written yet.

theorem Semantics.Quotation.MQProp.full_chain_preserves_rContent {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (approp : AppropStandard Speaker Expr W) (q : Expr) : (applyApprop approp ctx.sx q (applyMQ ctx q)).shunt.neg.rContent = ctx.uttRel ctx.sx ctx.ux q

R-content persists through the full metalinguistic negation chain 𝔐 → 𝔄 → ↓ → ¬. The utterance attribution is never lost.

theorem Semantics.Quotation.MQProp.metalinguistic_neg_truth_conditions {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (approp : AppropStandard Speaker Expr W) (q : Expr) (w : W) : (applyApprop approp ctx.sx q (applyMQ ctx q)).shunt.neg.atIssue w ↔ ¬(ctx.interp q ctx.wc ctx.sx w ∧ approp ctx.sx q w)

Metalinguistic negation truth conditions in the layered model. The MQProp-side counterpart of the flat-model Semantics.Quotation.metalinguistic_neg_truth_conditions (line 219 above). At-issue content of the full chain is ¬(at-issue ∧ appropriate), identical to the flat model — but the layered model ALSO retains the R-attribution (per full_chain_preserves_rContent), which the flat model discards.

theorem Semantics.Quotation.MQProp.shunt_conserves {W : Type} (p : MQProp W) (w : W) : p.shunt.atIssue w ∧ p.shunt.rContent w ∧ p.shunt.appropContent w ↔ p.atIssue w ∧ p.rContent w ∧ p.appropContent w

Shunting conservation. The total information content — the conjunction of all three layers — is invariant under ↓.

Shunting doesn't destroy ◆-content; it relocates it from the ◆-layer to the at-issue layer. The ◆-layer becomes trivial, but the information is preserved in the at-issue conjunction. No content is created or destroyed — only moved.

This is the crown theorem of the two-layer analysis: it shows that the apparent non-monotonicity of the flat model is an illusion. When the layers are properly separated, every operation preserves total information (negation inverts at-issue, but that's intentional semantic content, not information loss).

def Semantics.Quotation.MQProp.toFlat {W : Type} (p : MQProp W) : Pragmatics.Expressives.TwoDimProp W

Project the two-layer model to the flat TwoDimProp by discarding R-content and using ◆-content as the CI dimension.

This projection is exact after 𝔄: the flat model's "replaced" CI is the ◆-layer of the two-layer model. The R-content, discarded here, is the information that the flat model loses.

Equations

• p.toFlat = { atIssue := p.atIssue, ci := p.appropContent }

@[simp]

theorem Semantics.Quotation.MQProp.toFlat_atIssue {W : Type} (p : MQProp W) : p.toFlat.atIssue = p.atIssue

The flat projection preserves at-issue content.

@[simp]

theorem Semantics.Quotation.MQProp.toFlat_ci {W : Type} (p : MQProp W) : p.toFlat.ci = p.appropContent

The flat projection uses ◆-content as the CI dimension (R-content discarded).

theorem Semantics.Quotation.MQProp.flat_agreement_atIssue {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (approp : AppropStandard Speaker Expr W) (q : Expr) (w : W) : (applyApprop approp ctx.sx q (applyMQ ctx q)).shunt.neg.atIssue w ↔ (Quotation.shunt (Quotation.applyApprop approp ctx.sx q (ctx.applyMQ q))).neg.atIssue w

The full chain on the two-layer model agrees with the flat model on at-issue content. The two models diverge only in what happens to R-content: the layered model preserves it, the flat model discards it.

theorem Semantics.Quotation.MQProp.flat_loses_rContent {W Expr Speaker Utt : Type} (ctx : MQContext W Expr Speaker Utt) (approp : AppropStandard Speaker Expr W) (q : Expr) : (applyApprop approp ctx.sx q (applyMQ ctx q)).shunt.neg.rContent = ctx.uttRel ctx.sx ctx.ux q ∧ (Quotation.shunt (Quotation.applyApprop approp ctx.sx q (ctx.applyMQ q))).neg.ci = (Quotation.shunt (Quotation.applyApprop approp ctx.sx q (ctx.applyMQ q))).ci

What the flat model loses: R-content is present in the layered model but absent in the flat projection.

After metalinguistic negation ("I didn't trap two MONGEESE"), the layered model records that the utterance 'mongeese' was produced (R is true). The flat model has no trace of this — the R-content was overwritten by ◆-content when 𝔄 was applied.