Conventional implicature

This file defines two-dimensional meanings, the carrier of Potts's logic of conventional implicatures (CIs). A two-dimensional meaning has an at-issue value, which composes as usual, and not-at-issue content, a proposition the speaker contributes without putting it at issue; TwoDim W α pairs an at-issue value of type α with not-at-issue content over worlds W. Not-at-issue content only accumulates, so TwoDim W is the writer monad over propositions under meet. Applying an at-issue operator with f <$> p passes the not-at-issue content up (map_notAtIssue), and binding with p >>= f lets at-issue content feed later not-at-issue content but never the reverse (bind_atIssue). Potts's rule of CI application, which applies a CI functor f to an at-issue argument and returns the argument unmodified, is p >>= fun a ↦ ⟨a, f a⟩. The connectives neg, and, or and imp act on at-issue propositions and meet the not-at-issue content of their parts, so CIs project from under every connective.

Potts collects the CIs of a parsetree at its root, and Giorgolo and Asudeh recast that collection as a writer monad whose log lists the CIs. The map ofWriter conjoins such a log. It is a monad morphism (ofWriter_pure, ofWriter_bind), so composing two-dimensional meanings node by node predicts what collecting at the root does. Conjoining forgets how the log was itemized, for instance how often a CI was contributed (ofWriter_not_injective).

Karttunen and Peters treat presupposition the same way, as not-at-issue content. A two-dimensional proposition evaluates to a trivalent one (toTrivalent), undefined where its not-at-issue content fails, and the connectives here then evaluate to the Weak Kleene ones (toTrivalent_and). The two part at Karttunen's filtering: a filtering conditional presupposes at most what the unfiltered one does (imp_notAtIssue_subset_support), and less in general, because its antecedent's at-issue content can satisfy its consequent's presupposition, which no at-issue operator on two-dimensional meanings allows (exists_notAtIssue_ne_support). Two operations read the at-issue content where the not-at-issue content fails, and so are no trivalent operations: Karttunen and Peters's symmetric disjunction (orKPSymmetric_not_trivalent) and embedding under a negative factive (negFactive).

Main definitions

• TwoDim: an at-issue value and not-at-issue content, with its Monad instance.
• TwoDim.neg, TwoDim.and, TwoDim.or, TwoDim.imp: the connectives on propositions.
• TwoDim.ofWriter: the conjunction of a writer's log of CIs.
• TwoDim.toTrivalent: the trivalent proposition, undefined where the not-at-issue content fails.
• TwoDim.orKPSymmetric, TwoDim.negFactive: the symmetric two-dimensional disjunction and embedding under a negative factive.

Implementation notes

The not-at-issue dimension is the meet of the collected content rather than the collection, so a repeated CI adds nothing. That suits content whose repetition is redundant, but not the strengthening Potts reports for repeated expressives, which needs graded expressive content. The dimension also carries not-at-issue content that is not a CI in Potts's sense, such as the appositive impositions of AnderBois, Brasoveanu and Henderson and evidential content. How an utterance updates the context with each kind is not modelled here.

References

• [Pot05]
• [Pot07b]
• [GA12]
• [Kar73]
• [ABBH15]
• [KP79]
• [Yag25]
• [KS21a]
• [Hei92]
• [DPBS24]

structure ConventionalImplicature.TwoDim (W α : Type u) : Type u

A two-dimensional meaning pairs an at-issue value with the not-at-issue proposition it carries ([Pot05]). That bastard John is late has at-issue content "John is late" and not-at-issue content "the speaker disdains John".

• atIssue : α

  The at-issue value.

• notAtIssue : W → Prop

  The not-at-issue content.

theorem ConventionalImplicature.TwoDim.ext_iff {W α : Type u} {x y : TwoDim W α} : x = y ↔ x.atIssue = y.atIssue ∧ x.notAtIssue = y.notAtIssue

theorem ConventionalImplicature.TwoDim.ext {W α : Type u} {x y : TwoDim W α} (atIssue : x.atIssue = y.atIssue) (notAtIssue : x.notAtIssue = y.notAtIssue) : x = y

The monad

@[instance_reducible]

instance ConventionalImplicature.TwoDim.instMonad {W : Type u} : Monad (TwoDim W)

Two-dimensional meanings form the writer monad over propositions under meet. A pure value contributes no not-at-issue content, and composition meets the not-at-issue content of its parts.

Equations

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

@[simp]

theorem ConventionalImplicature.TwoDim.pure_atIssue {W α : Type u} (a : α) : (pure a).atIssue = a

@[simp]

theorem ConventionalImplicature.TwoDim.pure_notAtIssue {W α : Type u} (a : α) : (pure a).notAtIssue = ⊤

@[simp]

theorem ConventionalImplicature.TwoDim.map_atIssue {W α β : Type u} (f : α → β) (p : TwoDim W α) : (f <$> p).atIssue = f p.atIssue

@[simp]

theorem ConventionalImplicature.TwoDim.map_notAtIssue {W α β : Type u} (f : α → β) (p : TwoDim W α) : (f <$> p).notAtIssue = p.notAtIssue

@[simp]

theorem ConventionalImplicature.TwoDim.seq_atIssue {W α β : Type u} (f : TwoDim W (α → β)) (p : TwoDim W α) : (f <*> p).atIssue = f.atIssue p.atIssue

@[simp]

theorem ConventionalImplicature.TwoDim.seq_notAtIssue {W α β : Type u} (f : TwoDim W (α → β)) (p : TwoDim W α) : (f <*> p).notAtIssue = f.notAtIssue ⊓ p.notAtIssue

@[simp]

theorem ConventionalImplicature.TwoDim.bind_atIssue {W α β : Type u} (p : TwoDim W α) (f : α → TwoDim W β) : (p >>= f).atIssue = (f p.atIssue).atIssue

The at-issue value of a composition depends on the input's at-issue value alone, so not-at-issue content never flows into the at-issue dimension ([Pot05]).

@[simp]

theorem ConventionalImplicature.TwoDim.bind_notAtIssue {W α β : Type u} (p : TwoDim W α) (f : α → TwoDim W β) : (p >>= f).notAtIssue = p.notAtIssue ⊓ (f p.atIssue).notAtIssue

instance ConventionalImplicature.TwoDim.instLawfulMonad {W : Type u} : LawfulMonad (TwoDim W)

Connectives

def ConventionalImplicature.TwoDim.neg {W : Type u} (p : TwoDim W (W → Prop)) : TwoDim W (W → Prop)

Negation complements the at-issue proposition and passes the not-at-issue content up.

Equations

• p.neg = compl <$> p

def ConventionalImplicature.TwoDim.and {W : Type u} (p q : TwoDim W (W → Prop)) : TwoDim W (W → Prop)

Conjunction conjoins the at-issue propositions.

Equations

• p.and q = (fun (x1 x2 : W → Prop) => x1 ⊓ x2) <$> p <*> q

def ConventionalImplicature.TwoDim.or {W : Type u} (p q : TwoDim W (W → Prop)) : TwoDim W (W → Prop)

Disjunction disjoins the at-issue propositions.

Equations

• p.or q = (fun (x1 x2 : W → Prop) => x1 ⊔ x2) <$> p <*> q

def ConventionalImplicature.TwoDim.imp {W : Type u} (p q : TwoDim W (W → Prop)) : TwoDim W (W → Prop)

Implication takes the conditional of the at-issue propositions.

Equations

• p.imp q = (fun (x1 x2 : W → Prop) => x1 ⇨ x2) <$> p <*> q

@[simp]

theorem ConventionalImplicature.TwoDim.neg_atIssue {W : Type u} (p : TwoDim W (W → Prop)) : p.neg.atIssue = p.atIssueᶜ

@[simp]

theorem ConventionalImplicature.TwoDim.neg_notAtIssue {W : Type u} (p : TwoDim W (W → Prop)) : p.neg.notAtIssue = p.notAtIssue

@[simp]

theorem ConventionalImplicature.TwoDim.neg_neg {W : Type u} (p : TwoDim W (W → Prop)) : p.neg.neg = p

@[simp]

theorem ConventionalImplicature.TwoDim.and_atIssue {W : Type u} (p q : TwoDim W (W → Prop)) : (p.and q).atIssue = p.atIssue ⊓ q.atIssue

@[simp]

theorem ConventionalImplicature.TwoDim.and_notAtIssue {W : Type u} (p q : TwoDim W (W → Prop)) : (p.and q).notAtIssue = p.notAtIssue ⊓ q.notAtIssue

@[simp]

theorem ConventionalImplicature.TwoDim.or_atIssue {W : Type u} (p q : TwoDim W (W → Prop)) : (p.or q).atIssue = p.atIssue ⊔ q.atIssue

@[simp]

theorem ConventionalImplicature.TwoDim.or_notAtIssue {W : Type u} (p q : TwoDim W (W → Prop)) : (p.or q).notAtIssue = p.notAtIssue ⊓ q.notAtIssue

@[simp]

theorem ConventionalImplicature.TwoDim.imp_atIssue {W : Type u} (p q : TwoDim W (W → Prop)) : (p.imp q).atIssue = p.atIssue ⇨ q.atIssue

@[simp]

theorem ConventionalImplicature.TwoDim.imp_notAtIssue {W : Type u} (p q : TwoDim W (W → Prop)) : (p.imp q).notAtIssue = p.notAtIssue ⊓ q.notAtIssue

Collecting at the root

def ConventionalImplicature.TwoDim.ofWriter {W α : Type u} (m : Writer (List (W → Prop)) α) : TwoDim W α

ofWriter m reads a computation that logs its CIs ([GA12]) as a two-dimensional meaning, conjoining the log.

Equations

• ConventionalImplicature.TwoDim.ofWriter m = { atIssue := m.val, notAtIssue := fun (w : W) => ∀ c ∈ m.log, c w }

@[simp]

theorem ConventionalImplicature.TwoDim.ofWriter_atIssue {W α : Type u} (m : Writer (List (W → Prop)) α) : (ofWriter m).atIssue = m.val

@[simp]

theorem ConventionalImplicature.TwoDim.ofWriter_notAtIssue {W α : Type u} (m : Writer (List (W → Prop)) α) (w : W) : (ofWriter m).notAtIssue w ↔ ∀ c ∈ m.log, c w

@[simp]

theorem ConventionalImplicature.TwoDim.ofWriter_pure {W α : Type u} (a : α) : ofWriter (pure a) = pure a

theorem ConventionalImplicature.TwoDim.ofWriter_bind {W α β : Type u} (m : Writer (List (W → Prop)) α) (f : α → Writer (List (W → Prop)) β) : ofWriter (m >>= f) = do let a ← ofWriter m ofWriter (f a)

Composing node by node and collecting at the root agree, since ofWriter is a monad morphism.

theorem ConventionalImplicature.TwoDim.ofWriter_mk_cons_self {W α : Type u} (a : α) (c : W → Prop) (l : List (W → Prop)) : ofWriter (Writer.mk a (c :: c :: l)) = ofWriter (Writer.mk a (c :: l))

A CI logged twice contributes what it contributes logged once.

theorem ConventionalImplicature.TwoDim.ofWriter_not_injective {W α : Type u} [Nonempty α] : ¬Function.Injective ofWriter

Conjoining the log forgets how often a CI was contributed.

Presuppositions as not-at-issue content

noncomputable def ConventionalImplicature.TwoDim.toTrivalent {W : Type u} (p : TwoDim W (W → Prop)) : W → SignType

A two-dimensional proposition evaluates to the trivalent proposition undefined where its not-at-issue content fails and the classical value of its at-issue content elsewhere.

Equations

• p.toTrivalent = {w : W | p.notAtIssue w}.indicator fun (w : W) => SignType.ofProp (p.atIssue w)

@[simp]

theorem ConventionalImplicature.TwoDim.toTrivalent_eq_one_iff {W : Type u} (p : TwoDim W (W → Prop)) {w : W} : p.toTrivalent w = 1 ↔ p.notAtIssue w ∧ p.atIssue w

@[simp]

theorem ConventionalImplicature.TwoDim.toTrivalent_eq_neg_one_iff {W : Type u} (p : TwoDim W (W → Prop)) {w : W} : p.toTrivalent w = -1 ↔ p.notAtIssue w ∧ ¬p.atIssue w

@[simp]

theorem ConventionalImplicature.TwoDim.toTrivalent_eq_zero_iff {W : Type u} (p : TwoDim W (W → Prop)) {w : W} : p.toTrivalent w = 0 ↔ ¬p.notAtIssue w

theorem ConventionalImplicature.TwoDim.toTrivalent_neg {W : Type u} (p : TwoDim W (W → Prop)) : p.neg.toTrivalent = -p.toTrivalent

Negation evaluates to Kleene's negation.

theorem ConventionalImplicature.TwoDim.toTrivalent_and {W : Type u} (p q : TwoDim W (W → Prop)) {w : W} : (p.and q).toTrivalent w = (p.toTrivalent w).meetWeak (q.toTrivalent w)

Conjunction evaluates to Weak Kleene conjunction.

theorem ConventionalImplicature.TwoDim.toTrivalent_or {W : Type u} (p q : TwoDim W (W → Prop)) {w : W} : (p.or q).toTrivalent w = (p.toTrivalent w).joinWeak (q.toTrivalent w)

Disjunction evaluates to Weak Kleene disjunction.

theorem ConventionalImplicature.TwoDim.toTrivalent_imp {W : Type u} (p q : TwoDim W (W → Prop)) {w : W} : (p.imp q).toTrivalent w = (-p.toTrivalent w).joinWeak (q.toTrivalent w)

Implication evaluates to the Weak Kleene material conditional.

theorem ConventionalImplicature.TwoDim.imp_notAtIssue_subset_support {W : Type u} (p q : TwoDim W (W → Prop)) : {w : W | (p.imp q).notAtIssue w} ⊆ Function.support fun (w : W) => (-p.toTrivalent w).joinMiddle (q.toTrivalent w)

A filtering conditional presupposes at most what the antecedent and consequent presuppose together.

theorem ConventionalImplicature.TwoDim.exists_notAtIssue_ne_support {W : Type u} [Nonempty W] : ∃ (p : TwoDim W (W → Prop)) (q : TwoDim W (W → Prop)), ∀ (f : (W → Prop) → (W → Prop) → W → Prop), {w : W | (f <$> p <*> q).notAtIssue w} ≠ Function.support fun (w : W) => (-p.toTrivalent w).joinMiddle (q.toTrivalent w)

Filtering is no composition of two-dimensional meanings. A filtering conditional's presupposition depends on its antecedent's at-issue content, which no at-issue operator passes to the not-at-issue dimension ([Kar73]).

def ConventionalImplicature.TwoDim.orKPSymmetric {W : Type u} (p q : TwoDim W (W → Prop)) : TwoDim W (W → Prop)

The symmetric two-dimensional disjunction of the [KP79] tradition projects (A(ψ) ∨ Π(φ)) ∧ (A(φ) ∨ Π(ψ)) and asserts A(φ) ∨ A(ψ). The literal 1979 formulation was asymmetric, projecting the first disjunct's presupposition unconditionally; this is the symmetric variant of [Yag25]'s Definition 2, for whose symmetry [KS21a] give experimental support.

Equations

• p.orKPSymmetric q = { atIssue := p.atIssue ⊔ q.atIssue, notAtIssue := fun (w : W) => (q.atIssue w ∨ p.notAtIssue w) ∧ (p.atIssue w ∨ q.notAtIssue w) }

theorem ConventionalImplicature.TwoDim.orKPSymmetric_comm {W : Type u} (p q : TwoDim W (W → Prop)) : p.orKPSymmetric q = q.orKPSymmetric p

The symmetric disjunction is invariant under swapping its disjuncts.

theorem ConventionalImplicature.TwoDim.orKPSymmetric_atIssue_of_conflict {W : Type u} (p q : TwoDim W (W → Prop)) {w : W} (h : ¬(p.notAtIssue w ∧ q.notAtIssue w)) (hp : (p.orKPSymmetric q).notAtIssue w) : (p.orKPSymmetric q).atIssue w

When the disjuncts' presuppositions conflict, a defined symmetric disjunction is true, so it is never both defined and false there ([Yag25] §2.2).

theorem ConventionalImplicature.TwoDim.orKPSymmetric_not_trivalent {W : Type u} (w : W) : ¬∃ (f : SignType → SignType → SignType), ∀ (p q : TwoDim W (W → Prop)), (p.orKPSymmetric q).toTrivalent w = f (p.toTrivalent w) (q.toTrivalent w)

The symmetric disjunction is no trivalent operation. No binary operation on SignType computes its value from its disjuncts' values, since its presupposition reads their at-issue content where their presuppositions fail.

def ConventionalImplicature.TwoDim.negFactive {W : Type u} (p : TwoDim W (W → Prop)) (believes : (W → Prop) → W → Prop) : TwoDim W (W → Prop)

Embedding under a negative factive, x is unaware that p, presupposes that the complement holds and asserts that x does not believe its at-issue content. Presupposing that the complement holds, rather than only its at-issue content as [Hei92] does for atomic complements, is [DPBS24]'s treatment; the two part when the complement has its own presupposition.

Equations

• p.negFactive believes = { atIssue := fun (w : W) => ¬believes p.atIssue w, notAtIssue := fun (w : W) => p.notAtIssue w ∧ p.atIssue w }