structure Semantics.Lexical.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 → Bool

  At-issue (truth-conditional) content

• ci : W → Bool

  Conventional implicature (use-conditional) content

def Semantics.Lexical.Expressives.TwoDimProp.ofAtIssue {W : Type u_1} (p : BProp W) : TwoDimProp W

Create a proposition with no CI content.

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

Equations

• Semantics.Lexical.Expressives.TwoDimProp.ofAtIssue p = { atIssue := p, ci := fun (x : W) => true }

def Semantics.Lexical.Expressives.TwoDimProp.pureCI {W : Type u_1} (c : BProp W) : 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

• Semantics.Lexical.Expressives.TwoDimProp.pureCI c = { atIssue := fun (x : W) => true, ci := c }

def Semantics.Lexical.Expressives.TwoDimProp.withCI {W : Type u_1} (p c : BProp W) : TwoDimProp W

Combine at-issue content with CI content.

Equations

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

def Semantics.Lexical.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 }

def Semantics.Lexical.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 }

def Semantics.Lexical.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 Semantics.Lexical.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 }

theorem Semantics.Lexical.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 Semantics.Lexical.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 Semantics.Lexical.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 Semantics.Lexical.Expressives.TwoDimProp.ci_independent_of_atIssue {W : Type u_1} (p : TwoDimProp W) (w : W) (h_ci : p.ci w = true) : (p.atIssue w = true → p.ci w = true) ∧ (p.atIssue w = false → p.ci w = true)

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.

inductive Semantics.Lexical.Expressives.CIExprType : Type

Types of CI-contributing expressions.

Following Potts' taxonomy:

• Supplements: Appositives, parentheticals, supplementary relatives
• Expressives: Epithets, expressive adjectives, honorifics
• Utterance modifiers: Speech act adverbs (frankly, honestly)

• nominalAppositive : CIExprType
• clauseAppositive : CIExprType
• supplementaryAdverb : CIExprType
• epithet : CIExprType
• expressiveAdjective : CIExprType
• honorific : CIExprType
• emotiveMarker : CIExprType
• utteranceModifier : CIExprType

def Semantics.Lexical.Expressives.instReprCIExprType.repr : CIExprType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Expressives.instReprCIExprType : Repr CIExprType

Equations

• Semantics.Lexical.Expressives.instReprCIExprType = { reprPrec := Semantics.Lexical.Expressives.instReprCIExprType.repr }

instance Semantics.Lexical.Expressives.instDecidableEqCIExprType : DecidableEq CIExprType

Equations

• Semantics.Lexical.Expressives.instDecidableEqCIExprType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Expressives.instBEqCIExprType : BEq CIExprType

Equations

• Semantics.Lexical.Expressives.instBEqCIExprType = { beq := Semantics.Lexical.Expressives.instBEqCIExprType.beq }

def Semantics.Lexical.Expressives.instBEqCIExprType.beq : CIExprType → CIExprType → Bool

Equations

• Semantics.Lexical.Expressives.instBEqCIExprType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Semantics.Lexical.Expressives.CIExprProperties : Type

Properties of CI expressions (@cite{potts-2005} §2.5).

• speakerOriented : Bool

  CI is speaker-oriented (vs subject-oriented)

• repeatable : Bool

  CI can be repeated for emphasis without redundancy

• immediate : Bool

  CI is immediate (affects context just by being uttered)

• independent : Bool

  CI is independent of at-issue truth

instance Semantics.Lexical.Expressives.instReprCIExprProperties : Repr CIExprProperties

Equations

• Semantics.Lexical.Expressives.instReprCIExprProperties = { reprPrec := Semantics.Lexical.Expressives.instReprCIExprProperties.repr }

def Semantics.Lexical.Expressives.instReprCIExprProperties.repr : CIExprProperties → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Expressives.expressiveProperties : CIExprProperties

Expressives have all the characteristic CI properties.

Equations

• Semantics.Lexical.Expressives.expressiveProperties = { speakerOriented := true, repeatable := true, immediate := true, independent := true }

def Semantics.Lexical.Expressives.appositiveProperties : CIExprProperties

Appositives are slightly different (not repeatable in same way).

Equations

• Semantics.Lexical.Expressives.appositiveProperties = { speakerOriented := true, repeatable := false, immediate := true, independent := true }

def Semantics.Lexical.Expressives.comma {W : Type u_1} (pred entity : W → Bool) : 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

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

def Semantics.Lexical.Expressives.supplementaryAdverb {W : Type u_1} (adverbMeaning : BProp W → BProp W) (prop : BProp W) : TwoDimProp W

Supplementary adverb application.

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

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

Equations

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

def Semantics.Lexical.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

• Semantics.Lexical.Expressives.ciStrongerThan φ ψ = ((∀ (w : W), φ.ci w = true → ψ.ci w = true) ∧ ∃ (w : W), ψ.ci w = true ∧ φ.ci w = false)

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

CI equivalence: same CI content.

Equations

• Semantics.Lexical.Expressives.ciEquiv φ ψ = ∀ (w : W), φ.ci w = ψ.ci w

def Semantics.Lexical.Expressives.ciWeakerThan {W : Type u_1} (φ ψ : TwoDimProp W) : Prop

CI weaker than: inverse of stronger.

Equations

• Semantics.Lexical.Expressives.ciWeakerThan φ ψ = Semantics.Lexical.Expressives.ciStrongerThan ψ φ

structure Semantics.Lexical.Expressives.CIContext : Type

A context for evaluating CI felicity.

Following Kaplan/Gutzmann, CI meaning restricts the set of contexts in which an expression can be felicitously used.

• speakerAttitudes : String → ℤ

  Speaker's attitudes (who they like/dislike/respect)

• formality : ℚ

  Formality level of the context

• emotionalValence : ℤ

  Speaker's emotional state

def Semantics.Lexical.Expressives.isFelicitous (exprType : CIExprType) (target : String) (ctx : CIContext) : Bool

Check if a CI expression is felicitous in a context.

An epithet like "bastard" is felicitous iff speaker has negative attitude. An honorific like "don" is felicitous iff speaker has respect attitude.

Equations

• Semantics.Lexical.Expressives.isFelicitous Semantics.Lexical.Expressives.CIExprType.epithet target ctx = decide (ctx.speakerAttitudes target < -20)
• Semantics.Lexical.Expressives.isFelicitous Semantics.Lexical.Expressives.CIExprType.honorific target ctx = decide (ctx.speakerAttitudes target > 50)
• Semantics.Lexical.Expressives.isFelicitous Semantics.Lexical.Expressives.CIExprType.emotiveMarker target ctx = decide (ctx.emotionalValence.natAbs > 30)
• Semantics.Lexical.Expressives.isFelicitous exprType target ctx = true

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)
• Semantics.Lexical.Expressives.TwoDimProp (at-issue + CI)

def Semantics.Lexical.Expressives.ciLift {W : Type u_1} (p : Core.Presupposition.PrProp W) : TwoDimProp W

CI lift: type-shift a presuppositional proposition 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

• Semantics.Lexical.Expressives.ciLift p = { atIssue := p.assertion, ci := p.presup }

theorem Semantics.Lexical.Expressives.ciLift_atIssue {W : Type u_1} (p : Core.Presupposition.PrProp W) : (ciLift p).atIssue = p.assertion

CI lift preserves the assertion as at-issue content.

theorem Semantics.Lexical.Expressives.ciLift_ci {W : Type u_1} (p : Core.Presupposition.PrProp W) : (ciLift p).ci = p.presup

CI lift maps presupposition to CI dimension.

theorem Semantics.Lexical.Expressives.deRe_from_ciLift {W : Type u_1} (p : Core.Presupposition.PrProp W) (cg : BProp W) (h : ∀ (w : W), cg w = true → p.presup w = true) (w : W) : cg w = true → (ciLift p).ci w = true

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 Semantics.Lexical.Expressives.ciLift_neg_preserves_presup {W : Type u_1} (p : Core.Presupposition.PrProp W) : (ciLift p).neg.ci = p.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 Semantics.Lexical.Expressives.ciLift_roundtrip {W : Type u_1} (p : Core.Presupposition.PrProp W) : { presup := (ciLift p).ci, assertion := (ciLift p).atIssue } = p

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