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 direct quotation ([Pot07]; see pureQuote, and Semantics.Quotation.Mixed for [KG24]'s mixed quotation).

The at-issue tier carries the Heyting algebra of W → Prop (ᶜ/⊓/⊔/⇨); the CI tier always takes the meet ⊓. TwoDimProp.ofPartialProp 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 six [Pot07] expressive diagnostics.

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: expressives are nondisplaceable outside of direct quotation ([Pot07]), so in "He said 'that bastard Jones left'" the expressive is frozen inside the quotation and not attributed to the speaker. [KG24]'s mixed quotation (used and mentioned at once) is the refinement in Semantics.Quotation.Mixed.

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 meanings with identical at-issue content but different CI collapse to the same pureQuote, so the original CI is unrecoverable.

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 ⊓. In [Pot05]'s logic CIs do not compose via connectives at all — they are split off and collected at the root, interpreted conjunctively; the per-connective meet flattens that root collection into a compositional rule (the projection predictions coincide).

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

The six expressive diagnostics of [Pot07]: a yes/no fingerprint a class of secondary-meaning items either matches or fails.

• 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

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

Equations

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

@[instance_reducible]

instance Pragmatics.Expressives.instReprSecondaryMeaningProperties : Repr SecondaryMeaningProperties

Equations

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

@[instance_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] diagnostics ("damn damn damn" strengthens). Speaker orientation is the default, not an absolute: [Pot07] adopts a shiftable contextual judge, and [HP09] document non-speaker-oriented readings even unembedded.

Equations

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

def Pragmatics.Expressives.appositiveProperties : SecondaryMeaningProperties

Appositives (supplements) share independence and perspective dependence with expressives but fail the expressive-specific diagnostics ([Pot07]): their content is ordinary propositional material — displaceable ("Ed, then a first-year resident, ..."), paraphrasable ("Laura, a doctor" ↔ "Laura is a doctor"), not performative-like, not repeatable.

Equations

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

def Pragmatics.Expressives.TwoDimProp.ofPartialProp {W : Type u_1} (p : Semantics.Presupposition.PartialProp W) : TwoDimProp W

A presupposition/assertion pair as a two-dimensional meaning: the presupposition becomes (universally projecting) CI content, the assertion at-issue content — [Wan25a]'s de re analysis. Deliberately discards presupposition filtering: a CI-tier presupposition projects through and/imp where a real presupposition would be filtered by its local context, which is the point — the de re presupposition is evaluated against the common ground instead.

Equations

• Pragmatics.Expressives.TwoDimProp.ofPartialProp p = { atIssue := p.assertion, ci := p.presup }

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.ofPartialProp_ci {W : Type u_1} (p : Semantics.Presupposition.PartialProp W) (a✝ : W) : (ofPartialProp p).ci a✝ = p.presup a✝

@[simp]

theorem Pragmatics.Expressives.TwoDimProp.ofPartialProp_atIssue {W : Type u_1} (p : Semantics.Presupposition.PartialProp W) (a✝ : W) : (ofPartialProp p).atIssue a✝ = p.assertion a✝