Two-dimensional semantics for conventional implicatures

[Pot05] [Wan25a]

Following [Pot05], a TwoDimProp splits a meaning into two independent predicates over worlds: at-issue content (truth-conditional, composes normally) and conventional implicature content (use-conditional, projecting to the root). CIs project through the truth-functional connectives and are blocked only by pure quotation ([KG24]; see pureQuote).

The at-issue tier carries the Heyting algebra of W → Prop (ᶜ/⊓/⊔/⇨); the CI tier always takes the meet ⊓ — CIs conjoin through every connective rather than tracking the at-issue operation — and ciStrongerThan is the strict order < on that tier. ciLift ([Wan25a]) bridges Semantics.Presupposition.PartialProp into this type.

Main definitions

• TwoDimProp — a two-dimensional meaning (at-issue and CI predicates over worlds).
• neg, and, or, imp — the connectives (at-issue Heyting op, CI meet).
• SecondaryMeaningProperties — the [Pot07] expressive diagnostics, plus two fields distinguishing outlook markers ([Kub26]).

References

[Pot05] [Pot07] [Wan25a] [KG24]

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

A two-dimensional meaning ([Pot05]): two predicates over worlds, the at-issue (truth-conditional) content atIssue and the conventional-implicature (use-conditional) content ci. E.g. "that bastard John is late" has atIssue "John is late" and ci "the speaker disdains 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.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_ci {W : Type u_1} (p c : W → Prop) (a✝ : W) : (withCI p c).ci a✝ = c a✝

@[simp]

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

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

Pure quotation strips CI content to ⊤, preserving only at-issue content: a quoted expressive does not project ([KG24]). E.g. in "He said 'that bastard Jones left'" the expressive 'bastard' is frozen inside the quotation and not attributed to the speaker.

Equations

• p.pureQuote = { atIssue := p.atIssue, ci := ⊤ }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.pureQuote_ci {W : Type u_1} (p : TwoDimProp W) (a✝ : W) : p.pureQuote.ci a✝ = ⊤ a✝

@[simp]

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

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

Connectives

Both dimensions are W → Prop, so each connective is built from that type's order structure: the at-issue tier carries the full Heyting algebra (ᶜ, ⊓, ⊔, ⇨), while the CI tier always takes the meet ⊓ — CIs project by conjunction through every connective rather than tracking the at-issue operation.

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 := p.atIssueᶜ, 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 := p.atIssue ⊓ q.atIssue, ci := p.ci ⊓ q.ci }

@[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 := p.atIssue ⊔ q.atIssue, ci := p.ci ⊓ q.ci }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.or_atIssue {W : Type u_1} (p q : TwoDimProp W) (w : W) : (p.or q).atIssue w ↔ p.atIssue w ∨ q.atIssue w

Disjunction's at-issue dimension.

@[simp]

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

Disjunction propagates both CIs.

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 := p.atIssue ⇨ q.atIssue, ci := p.ci ⊓ q.ci }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.imp_atIssue {W : Type u_1} (p q : TwoDimProp W) (w : W) : (p.imp q).atIssue w ↔ p.atIssue w → q.atIssue w

Implication's at-issue dimension.

@[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.

@[simp]

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)

structure Pragmatics.Expressives.SecondaryMeaningProperties : Type

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

Extends [Pot07]'s six expressive diagnostics with two additional properties needed to distinguish outlook markers ([Kub26]) 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 }

@[implicit_reducible]

instance Pragmatics.Expressives.instDecidableEqSecondaryMeaningProperties : DecidableEq SecondaryMeaningProperties

Equations

• Pragmatics.Expressives.instDecidableEqSecondaryMeaningProperties = Pragmatics.Expressives.instDecidableEqSecondaryMeaningProperties.decEq

def Pragmatics.Expressives.instDecidableEqSecondaryMeaningProperties.decEq (x✝ x✝¹ : SecondaryMeaningProperties) : Decidable (x✝ = x✝¹)

Equations

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

def Pragmatics.Expressives.expressiveProperties : SecondaryMeaningProperties

Expressives satisfy all six [Pot07] 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.ciStrongerThan {W : Type u_1} (φ ψ : TwoDimProp W) : Prop

CI informativeness ordering: φ has a stronger CI than ψ when φ's CI strictly entails ψ's — i.e. φ.ci < ψ.ci in the pointwise entailment order that W → Prop inherits from Prop. Concretely, φ.ci implies ψ.ci at every world, but some world satisfies ψ.ci and not φ.ci.

Example:

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

Equations

• Pragmatics.Expressives.ciStrongerThan φ ψ = (φ.ci < ψ.ci)

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

CI equivalence: same CI content.

Equations

• Pragmatics.Expressives.ciEquiv φ ψ = (φ.ci = ψ.ci)

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

CI-stronger-than is irreflexive (the strict entailment order on W → Prop).

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.

CI Lift: Presupposition → Two-Dimensional Meaning ([Wan25a])

[Wan25a] analyze de re presupposition by bifurcating a [Gut15] presuppositional meaning into two dimensions using [Pot05]'s CI type system:

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

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

Bridge: PartialProp ↔ TwoDimProp

This provides a new cross-module connection between:

• Semantics.Presupposition.PartialProp (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 (universally projecting) CI content, the assertion becomes at-issue content. The ⟦CI⟧ operator of [Wan25a].

Equations

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

@[simp]

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

@[simp]

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

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 CommonGround entails the presupposition, the CI dimension is satisfied at all CommonGround worlds. This means the presupposition is resolved against the CommonGround 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.