structure Pragmatics.Expressives.TwoDimProp (W : Type u_1) : Type u_1

A two-dimensional meaning following @cite{potts-2005}.

The key insight: linguistic expressions contribute to TWO independent dimensions of meaning that compose by different rules.

• atIssue: Truth-conditional content (what is said)
• ci: Conventional implicature (use-conditional content)

Example: "That bastard John is late"

• atIssue: John is late
• ci: Speaker has negative attitude toward John

• atIssue : W → Prop

  At-issue (truth-conditional) content

• ci : W → Prop

  Conventional implicature (use-conditional) content

theorem Pragmatics.Expressives.TwoDimProp.ext {W : Type u_1} {x y : TwoDimProp W} (atIssue : x.atIssue = y.atIssue) (ci : x.ci = y.ci) : x = y

theorem Pragmatics.Expressives.TwoDimProp.ext_iff {W : Type u_1} {x y : TwoDimProp W} : x = y ↔ x.atIssue = y.atIssue ∧ x.ci = y.ci

def Pragmatics.Expressives.TwoDimProp.ofAtIssue {W : Type u_1} (p : W → Prop) : TwoDimProp W

Create a proposition with no CI content.

Most ordinary expressions have trivial CI content (always satisfied).

Equations

• Pragmatics.Expressives.TwoDimProp.ofAtIssue p = { atIssue := p, ci := fun (x : W) => True }

def Pragmatics.Expressives.TwoDimProp.pureCI {W : Type u_1} (c : W → Prop) : TwoDimProp W

Create a pure CI (no at-issue contribution).

Some expressions ONLY contribute CI content. Example: "damn" in "the damn dog" doesn't change truth conditions.

Equations

• Pragmatics.Expressives.TwoDimProp.pureCI c = { atIssue := fun (x : W) => True, ci := c }

def Pragmatics.Expressives.TwoDimProp.withCI {W : Type u_1} (p c : W → Prop) : TwoDimProp W

Combine at-issue content with CI content.

Equations

• Pragmatics.Expressives.TwoDimProp.withCI p c = { atIssue := p, ci := c }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.withCI_atIssue {W : Type u_1} (p c : W → Prop) : (withCI p c).atIssue = p

withCI projects to its at-issue argument.

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.withCI_ci {W : Type u_1} (p c : W → Prop) : (withCI p c).ci = c

withCI projects to its CI argument.

def Pragmatics.Expressives.TwoDimProp.pureQuote {W : Type u_1} (p : TwoDimProp W) : TwoDimProp W

Pure quotation: strips CI content, preserving only at-issue content.

When an expression is purely quoted, its CI content (expressives, slurs, NRRCs) does not project. The quoted material is "frozen" — its peripheral content is blocked from passing up the tree.

This operation is the semantic reflex of pure quotation blocking peripheral content passage (@cite{kirk-giannini-2024}, Appendix Remark 6).

Example: In "He said 'that bastard Jones left'", the expressive 'bastard' is inside pure quotation and does not project to the speaker.

Equations

• p.pureQuote = { atIssue := p.atIssue, ci := fun (x : W) => True }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.pureQuote_strips_ci {W : Type u_1} (p : TwoDimProp W) (w : W) : p.pureQuote.ci w

Pure quotation neutralizes CI content.

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.pureQuote_preserves_atIssue {W : Type u_1} (p : TwoDimProp W) : p.pureQuote.atIssue = p.atIssue

Pure quotation preserves at-issue content.

structure Pragmatics.Expressives.TwoDimProp.PureQuoted (W : Type u_2) : Type u_2

Pure quotation with strip witness.

pureQuote is information-losing — once the CI is flattened to λ _ => True, the original CI cannot be recovered from the result alone. PureQuoted records both the stripped result AND the original, so downstream operators (in particular MQContext.applyMQ for the strip-then-mix pattern of @cite{kirk-giannini-2024} §3) can refer to what was discarded.

This is the substrate K-G's CI-projection-failure theorems need: rather than proving (pureQuote p).ci w := trivial (which is vacuously true regardless of input), they can compare the stripped output against the recorded original.

• result : TwoDimProp W

  The stripped output: at-issue preserved, CI flattened.

• original : TwoDimProp W

  The original input, retained for downstream comparison.

• is_strip : self.result = self.original.pureQuote

  The result is the original with CI stripped via pureQuote.

def Pragmatics.Expressives.TwoDimProp.pureQuoteRich {W : Type u_1} (p : TwoDimProp W) : PureQuoted W

Build a PureQuoted witness from an input proposition.

Bundles the existing pureQuote p with a record of the original p and a trivial proof of the strip relation.

Equations

• p.pureQuoteRich = { result := p.pureQuote, original := p, is_strip := ⋯ }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.pureQuoteRich_result {W : Type u_1} (p : TwoDimProp W) : p.pureQuoteRich.result = p.pureQuote

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.pureQuoteRich_original {W : Type u_1} (p : TwoDimProp W) : p.pureQuoteRich.original = p

theorem Pragmatics.Expressives.TwoDimProp.pureQuoteRich_atIssue_preserved {W : Type u_1} (p : TwoDimProp W) : p.pureQuoteRich.result.atIssue = p.pureQuoteRich.original.atIssue

The rich operator preserves at-issue between original and result.

theorem Pragmatics.Expressives.TwoDimProp.pureQuoteRich_ci_stripped {W : Type u_1} (p : TwoDimProp W) (w : W) : p.pureQuoteRich.result.ci w

The rich operator strips the original CI: result.ci is constantly True.

theorem Pragmatics.Expressives.TwoDimProp.pureQuote_loses_ci_info : ∃ (p₁ : TwoDimProp Unit) (p₂ : TwoDimProp Unit), p₁.ci ≠ p₂.ci ∧ p₁.pureQuote = p₂.pureQuote

Pure quotation is information-losing.

Two propositions with identical at-issue content but different CI dimensions produce identical results under pureQuote. This is the substantive non-trivial fact about the operator: the original CI is unrecoverable from the result. Constructive witness: λ _ => True and λ _ => False for the CI dimension, with at-issue trivial — pureQuote collapses both to the same { atIssue := True, ci := True }.

This theorem is what quotation_blocks_ci_projection should be, instead of the vacuous := trivial. After pureQuote, no CI information remains; any downstream peripheral content must be re-introduced (by applyMQ's R).

def Pragmatics.Expressives.TwoDimProp.neg {W : Type u_1} (p : TwoDimProp W) : TwoDimProp W

Negation: negates at-issue content; CI projects unchanged.

"John didn't see that bastard Pete"

• atIssue: ¬(John saw Pete)
• ci: Speaker thinks Pete is a bastard (unchanged)

This distinguishes CIs from presuppositions.

Equations

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

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.neg_atIssue {W : Type u_1} (p : TwoDimProp W) (w : W) : p.neg.atIssue w ↔ ¬p.atIssue w

Negation flips the at-issue dimension.

def Pragmatics.Expressives.TwoDimProp.and {W : Type u_1} (p q : TwoDimProp W) : TwoDimProp W

Conjunction: at-issue content conjoins; both CIs project.

"That bastard John met that jerk Pete"

• atIssue: John met Pete
• ci: Speaker thinks John is bastard and Pete is jerk

Equations

• p.and q = { atIssue := fun (w : W) => p.atIssue w ∧ q.atIssue w, ci := fun (w : W) => p.ci w ∧ q.ci w }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.and_atIssue {W : Type u_1} (p q : TwoDimProp W) (w : W) : (p.and q).atIssue w ↔ p.atIssue w ∧ q.atIssue w

Conjunction's at-issue dimension.

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.and_ci {W : Type u_1} (p q : TwoDimProp W) (w : W) : (p.and q).ci w ↔ p.ci w ∧ q.ci w

Conjunction propagates both CIs.

def Pragmatics.Expressives.TwoDimProp.or {W : Type u_1} (p q : TwoDimProp W) : TwoDimProp W

Disjunction: at-issue content disjoins; both CIs project.

CIs project through disjunction rather than being disjoined.

Equations

• p.or q = { atIssue := fun (w : W) => p.atIssue w ∨ q.atIssue w, ci := fun (w : W) => p.ci w ∧ q.ci w }

def Pragmatics.Expressives.TwoDimProp.imp {W : Type u_1} (p q : TwoDimProp W) : TwoDimProp W

Implication: at-issue content forms conditional; both CIs project.

"If that bastard John calls, I'll leave"

• atIssue: John calls → I leave
• ci: Speaker thinks John is bastard (projects from antecedent)

Equations

• p.imp q = { atIssue := fun (w : W) => p.atIssue w → q.atIssue w, ci := fun (w : W) => p.ci w ∧ q.ci w }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.ci_projects_through_neg {W : Type u_1} (p : TwoDimProp W) : p.neg.ci = p.ci

CI projects through negation.

Presuppositions can be filtered by antecedents; CIs cannot.

theorem Pragmatics.Expressives.TwoDimProp.ci_projects_from_antecedent {W : Type u_1} (p q : TwoDimProp W) (w : W) : (p.imp q).ci w ↔ p.ci w ∧ q.ci w

CI projects through conditional antecedent.

Unlike presuppositions, CIs in the antecedent of a conditional are not filtered; they project to the root.

"If the king of France is bald,..." - presupposes king exists (filtered) "If that bastard calls,..." - CI projects (speaker thinks he's bastard)

theorem Pragmatics.Expressives.TwoDimProp.ci_double_neg {W : Type u_1} (p : TwoDimProp W) : p.neg.neg.ci = p.ci

Double negation preserves CI.

CIs are unaffected by truth-functional operators.

theorem Pragmatics.Expressives.TwoDimProp.ci_independent_of_atIssue {W : Type u_1} (p : TwoDimProp W) (w : W) (h_ci : p.ci w) : (p.atIssue w → p.ci w) ∧ (¬p.atIssue w → p.ci w)

At-issue independence: CI content is independent of at-issue truth value.

The at-issue content can be true, false, or unknown; CI still holds.

structure Pragmatics.Expressives.SecondaryMeaningProperties : Type

Properties of secondary (non-at-issue) meaning expressions.

Extends @cite{potts-2007}'s six expressive diagnostics with two additional properties needed to distinguish outlook markers (@cite{kubota-2026}) from pure expressives and pure presuppositions.

• independent : Bool

  CI contributes to a dimension separate from at-issue content

• nondisplaceable : Bool

  Predicates something of the utterance situation (not the described situation)

• perspectiveDependent : Bool

  Evaluated from a particular perspective (usually the speaker's)

• descriptivelyIneffable : Bool

  Cannot be fully paraphrased by descriptive, non-expressive terms

• immediate : Bool

  Achieves its effect simply by being uttered (like a performative)

• repeatable : Bool

  Repetition strengthens rather than creating redundancy

• allowsPerspectiveShift : Bool

  Allows perspective shift to a non-speaker attitude holder under embedding

• requiresDiscourseAntecedent : Bool

  Requires a salient issue/counterstance in prior discourse

def Pragmatics.Expressives.instReprSecondaryMeaningProperties.repr : SecondaryMeaningProperties → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pragmatics.Expressives.instReprSecondaryMeaningProperties : Repr SecondaryMeaningProperties

Equations

• Pragmatics.Expressives.instReprSecondaryMeaningProperties = { reprPrec := Pragmatics.Expressives.instReprSecondaryMeaningProperties.repr }

def Pragmatics.Expressives.expressiveProperties : SecondaryMeaningProperties

Expressives satisfy all six @cite{potts-2007} properties and do NOT typically allow perspective shift or require discourse antecedents.

Equations

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

def Pragmatics.Expressives.appositiveProperties : SecondaryMeaningProperties

Appositives share most expressive properties but are not repeatable and ARE descriptively paraphrasable ("Laura, a doctor" → "Laura is a doctor").

Equations

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

def Pragmatics.Expressives.comma {W : Type u_1} (pred entity : W → Prop) : TwoDimProp W

The comma feature type-shifts at-issue content to CI content.

This is Potts' mechanism for appositives:

• "Laura, a doctor, recommended aspirin"
• "a doctor" is at-issue predicate
• comma shifts it to CI: "Laura is a doctor" becomes CI content

Formally: comma : ⟨⟨eᵃ,tᵃ⟩, ⟨eᵃ,tᶜ⟩⟩

Equations

• Pragmatics.Expressives.comma pred entity = { atIssue := entity, ci := pred }

def Pragmatics.Expressives.supplementaryAdverb {W : Type u_1} (adverbMeaning : (W → Prop) → W → Prop) (prop : W → Prop) : TwoDimProp W

Supplementary adverb application.

"Luckily, John won" = John won + CI(speaker considers it lucky)

Formally: comma₂ : ⟨⟨tᵃ,tᵃ⟩, ⟨tᵃ,tᶜ⟩⟩

Equations

• Pragmatics.Expressives.supplementaryAdverb adverbMeaning prop = { atIssue := prop, ci := adverbMeaning prop }

def Pragmatics.Expressives.ciStrongerThan {W : Type u_1} (φ ψ : TwoDimProp W) : Prop

CI informativeness ordering.

φ has stronger CI than ψ iff the contexts where φ is felicitous are a proper subset of contexts where ψ is felicitous.

⟦φ⟧ᵘ ⊂ ⟦ψ⟧ᵘ

Example:

• "That bastard John" is CI-stronger than "John"
• "That fucking bastard John" is CI-stronger than "That bastard John"

Equations

• Pragmatics.Expressives.ciStrongerThan φ ψ = ((∀ (w : W), φ.ci w → ψ.ci w) ∧ ∃ (w : W), ψ.ci w ∧ ¬φ.ci w)

def Pragmatics.Expressives.ciEquiv {W : Type u_1} (φ ψ : TwoDimProp W) : Prop

CI equivalence: same CI content.

Equations

• Pragmatics.Expressives.ciEquiv φ ψ = ∀ (w : W), φ.ci w ↔ ψ.ci w

theorem Pragmatics.Expressives.ciStrongerThan_irrefl {W : Type u_1} (φ : TwoDimProp W) : ¬ciStrongerThan φ φ

CI-stronger-than is irreflexive: no proposition is strictly CI-stronger than itself.

theorem Pragmatics.Expressives.ciStrongerThan_trans {W : Type u_1} (φ ψ χ : TwoDimProp W) (h1 : ciStrongerThan φ ψ) (h2 : ciStrongerThan ψ χ) : ciStrongerThan φ χ

CI-stronger-than is transitive.

theorem Pragmatics.Expressives.ciStrongerThan_asymm {W : Type u_1} (φ ψ : TwoDimProp W) (h : ciStrongerThan φ ψ) : ¬ciStrongerThan ψ φ

CI-stronger-than is asymmetric: if φ is CI-stronger than ψ, ψ is not CI-stronger than φ.

CI Lift: Presupposition → Two-Dimensional Meaning

@cite{wang-2025} analyze de re presupposition by bifurcating a @cite{gutzmann-2015} presuppositional meaning into two dimensions using @cite{potts-2005}'s CI type system:

• At-issue: the assertion component (identity function on the propositional content)
• CI: the presupposition (projects to root, evaluated against CG)

This derives de re readings: when a presuppositional expression appears under an attitude verb, the presupposition can be evaluated against the common ground (CG) rather than the attitude holder's beliefs, because it projects as CI content.

Bridge: PrProp ↔ TwoDimProp

This provides a new cross-module connection between:

• Core.Presupposition.PrProp (presupposition + assertion)
• Pragmatics.Expressives.TwoDimProp (at-issue + CI)

def Pragmatics.Expressives.ciLift {W : Type u_1} (presup assertion : W → Prop) : TwoDimProp W

CI lift: type-shift a presupposition/assertion pair into a two-dimensional meaning.

The presupposition becomes CI content (projects universally), while the assertion becomes at-issue content (composes truth-functionally).

This is the ⟦CI⟧ operator from @cite{wang-2025}.

Equations

• Pragmatics.Expressives.ciLift presup assertion = { atIssue := assertion, ci := presup }

theorem Pragmatics.Expressives.ciLift_atIssue {W : Type u_1} (presup assertion : W → Prop) : (ciLift presup assertion).atIssue = assertion

CI lift preserves the assertion as at-issue content.

theorem Pragmatics.Expressives.ciLift_ci {W : Type u_1} (presup assertion : W → Prop) : (ciLift presup assertion).ci = presup

CI lift maps presupposition to CI dimension.

theorem Pragmatics.Expressives.deRe_from_ciLift {W : Type u_1} (presup assertion cg : W → Prop) (h : ∀ (w : W), cg w → presup w) (w : W) : cg w → (ciLift presup assertion).ci w

De re reading: when CG entails the presupposition, the CI dimension is satisfied at all CG worlds. This means the presupposition is resolved against the CG regardless of what is embedded under an attitude verb.

theorem Pragmatics.Expressives.ciLift_neg_preserves_presup {W : Type u_1} (presup assertion : W → Prop) : (ciLift presup assertion).neg.ci = presup

CI lift composes with negation: negating a CI-lifted meaning negates the at-issue content but preserves the presupposition (as CI).

This matches both Potts' CI projection and standard presupposition projection through negation.

theorem Pragmatics.Expressives.ciLift_roundtrip {W : Type u_1} (presup assertion : W → Prop) : (ciLift presup assertion).ci = presup ∧ (ciLift presup assertion).atIssue = assertion

Round-trip: CI lift then extract components recovers the original predicates.