Lo Guercio (2025): Maximize Conventional Implicatures!

This file formalizes Lo Guercio's anti-conventional implicatures: scalar inferences that arise from comparing the conventionally implicated content of formal alternatives, as scalar implicatures compare at-issue content and antipresuppositions presuppositional content. Conventionally implied meaning is a restriction on the contexts of felicitous use, so one sentence has stronger such content than another when its felicity set is a proper subset of the other's, and the principle Maximize Conventional Implicatures! forbids a sentence when a formal alternative in the sense of Katzir and of Fox and Katzir, one no more complex than it, has stronger content. All three principles are instances of the substrate's Competition.Blocked, here along conventional-implicature content.

The worked case is the epithet. Out of the blue, John arrived first carries no inference that John is no bastard, because that bastard John arrived first is not a formal alternative: the epithet construction is a determiner phrase with three daughters, which no chain of deletions, contractions, and substitutions from a source of lexical items and one-daughter phrases can build (outOfBlue_no_ACI, through Tree.subtree_preservation). Once that bastard Pedro has been mentioned, its phrase enters the substitution source, the epithet alternative is derived by substituting it for the subject and then John for Pedro, the paper's derivation (24) (epithet_alternative_priorMention), and the inference arises (priorMention_yes_ACI): the bare sentence is then used exactly where the speaker does not hold the attitude (unblocked_priorMention), where out of the blue it is used whatever the attitude (unblocked_outOfBlue).

Implementation notes

The felicity-set semantics of the paper's (12) is expressiveCI: a sentence is felicitous at a world unless it contains the epithet construction and the speaker does not hold the attitude there. The honorific don/doña of the paper's §3.2.1, the Japanese honorifics of its §3.2.2, the expressive adjectives of its §3.2.4, and the embeddability and oddness discussion of its §4 are rows of Data/Examples/LoGuercio2025.json and prose, not theorems.

References

• [LG25]
• [Kat07]
• [FK11]
• [Gut15]
• [Kap99]

The epithet as a structural alternative

inductive LoGuercio2025.EWord : Type

Vocabulary for the epithet example.

• john : EWord
• pedro : EWord
• arrived : EWord
• first : EWord
• andThen : EWord
• that_ : EWord
• bastard : EWord

@[instance_reducible]

instance LoGuercio2025.instDecidableEqEWord : DecidableEq EWord

Equations

• LoGuercio2025.instDecidableEqEWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LoGuercio2025.instReprEWord : Repr EWord

Equations

• LoGuercio2025.instReprEWord = { reprPrec := LoGuercio2025.instReprEWord.repr }

def LoGuercio2025.instReprEWord.repr : EWord → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• LoGuercio2025.instReprEWord.repr LoGuercio2025.EWord.john prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LoGuercio2025.EWord.john")).group prec✝
• LoGuercio2025.instReprEWord.repr LoGuercio2025.EWord.pedro prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LoGuercio2025.EWord.pedro")).group prec✝
• LoGuercio2025.instReprEWord.repr LoGuercio2025.EWord.first prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LoGuercio2025.EWord.first")).group prec✝
• LoGuercio2025.instReprEWord.repr LoGuercio2025.EWord.that_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LoGuercio2025.EWord.that_")).group prec✝

@[instance_reducible]

instance LoGuercio2025.instBEqEWord : BEq EWord

Equations

• LoGuercio2025.instBEqEWord = { beq := fun (a b : LoGuercio2025.EWord) => decide (a = b) }

instance LoGuercio2025.instLawfulBEqEWord : LawfulBEq EWord

def LoGuercio2025.epithetLex : Finset (PhraseStructure.Tree PhraseStructure.Cat EWord)

The lexical items, terminals only.

Equations

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

def LoGuercio2025.arrivedFirst : PhraseStructure.Tree PhraseStructure.Cat EWord

The predicate arrived first.

Equations

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

def LoGuercio2025.johnArrived : PhraseStructure.Tree PhraseStructure.Cat EWord

[DP John] arrived first, the first conjunct of the paper's (20a) as its (24) parses it.

Equations

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

def LoGuercio2025.bastardJohnArrived : PhraseStructure.Tree PhraseStructure.Cat EWord

[DP that bastard John] arrived first, the paper's (20b).

Equations

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

def LoGuercio2025.bastardPedroDP : PhraseStructure.Tree PhraseStructure.Cat EWord

[DP that bastard Pedro], mentioned in the second conjunct of (20a).

Equations

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

def LoGuercio2025.bastardPedroArrived : PhraseStructure.Tree PhraseStructure.Cat EWord

[DP that bastard Pedro] arrived first, the intermediate step of the derivation (24).

Equations

• LoGuercio2025.bastardPedroArrived = PhraseStructure.Tree.node PhraseStructure.Cat.S [LoGuercio2025.bastardPedroDP, LoGuercio2025.arrivedFirst]

def LoGuercio2025.priorContextLex : Finset (PhraseStructure.Tree PhraseStructure.Cat EWord)

After the mention the substitution source holds the lexical items and the contextually relevant epithet phrase ([FK11]).

Equations

• LoGuercio2025.priorContextLex = insert LoGuercio2025.bastardPedroDP LoGuercio2025.epithetLex

def LoGuercio2025.WideDP (t : PhraseStructure.Tree PhraseStructure.Cat EWord) : Prop

A determiner phrase with at least two daughters.

Equations

• LoGuercio2025.WideDP t = (t.cat = PhraseStructure.Cat.Det ∧ 2 ≤ (RoseTree.children t).length)

def LoGuercio2025.IsEpithet : PhraseStructure.Tree PhraseStructure.Cat EWord → Prop

The epithet construction is a determiner phrase that bastard X.

Equations

• One or more equations did not get rendered due to their size.
• LoGuercio2025.IsEpithet x✝ = False

@[instance_reducible]

instance LoGuercio2025.instDecidablePredTreeCatEWordWideDP : DecidablePred WideDP

Equations

• LoGuercio2025.instDecidablePredTreeCatEWordWideDP x✝ = { decide := decide (x✝.cat = PhraseStructure.Cat.Det) && decide (2 ≤ (RoseTree.children x✝).length), reflects_decide := ⋯ }

theorem LoGuercio2025.WideDP.of_isEpithet {t : PhraseStructure.Tree PhraseStructure.Cat EWord} (h : IsEpithet t) : WideDP t

def LoGuercio2025.HasEpithet (φ : PhraseStructure.Tree PhraseStructure.Cat EWord) : Prop

A tree contains the epithet construction.

Equations

• LoGuercio2025.HasEpithet φ = ∃ s ∈ RoseTree.subtrees φ, LoGuercio2025.IsEpithet s

@[instance_reducible]

instance LoGuercio2025.instDecidablePredTreeCatEWordHasEpithet : DecidablePred HasEpithet

Equations

• LoGuercio2025.instDecidablePredTreeCatEWordHasEpithet x✝ = LoGuercio2025.instDecidablePredTreeCatEWordHasEpithet._aux_1 x✝

theorem LoGuercio2025.no_wideDP_outOfBlue {ψ : PhraseStructure.Tree PhraseStructure.Cat EWord} (h : ψ ∈ PhraseStructure.Tree.structuralAlternatives epithetLex johnArrived) (t : RoseTree (PhraseStructure.Tree.Label PhraseStructure.Cat EWord)) : t ∈ RoseTree.subtrees ψ → ¬WideDP t

Out of the blue no structural alternative of the bare sentence contains a determiner phrase with two or more daughters, since no source item has one, the sentence has none, and the operations cannot widen a phrase.

theorem LoGuercio2025.epithet_not_alternative_outOfBlue : bastardJohnArrived ∉ PhraseStructure.Tree.structuralAlternatives epithetLex johnArrived

Out of the blue, the epithet sentence is not a structural alternative.

theorem LoGuercio2025.epithet_alternative_priorMention : bastardJohnArrived ∈ PhraseStructure.Tree.structuralAlternatives priorContextLex johnArrived

After the mention, the epithet sentence is a structural alternative, by the paper's derivation (24), in which the mentioned phrase replaces the subject and then John replaces Pedro.

Conventionally implicated content as felicity sets

@[reducible, inline]

abbrev LoGuercio2025.World : Type

The worlds settle whether the speaker believes that John is a bastard.

Equations

• LoGuercio2025.World = Bool

def LoGuercio2025.expressiveCI (φ : PhraseStructure.Tree PhraseStructure.Cat EWord) : Set World

Under the felicity-set content of the paper's (12), a sentence with the epithet construction is felicitous only where the speaker holds the attitude; any other sentence is felicitous everywhere.

Equations

• LoGuercio2025.expressiveCI φ = {w : LoGuercio2025.World | LoGuercio2025.HasEpithet φ → w = true}

theorem LoGuercio2025.epithet_ciStronger_than_bare : expressiveCI bastardJohnArrived ⊂ expressiveCI johnArrived

The epithet sentence has stronger content than the bare one, since its felicity set is a proper subset.

The inference

theorem LoGuercio2025.outOfBlue_no_ACI : ¬Competition.Blocked (PhraseStructure.Tree.structuralAlternatives epithetLex) expressiveCI johnArrived

Out of the blue the bare sentence does not violate the principle, since every formal alternative is free of the epithet construction, so none has stronger content.

theorem LoGuercio2025.priorMention_yes_ACI : Competition.Blocked (PhraseStructure.Tree.structuralAlternatives priorContextLex) expressiveCI johnArrived

After the mention the bare sentence violates the principle, since the epithet sentence is a formal alternative with stronger content.

theorem LoGuercio2025.unblocked_outOfBlue : Competition.unblocked (PhraseStructure.Tree.structuralAlternatives epithetLex) expressiveCI johnArrived = Set.univ

Out of the blue the bare sentence is used whatever the speaker's attitude, so it carries no anti-conventional implicature.

theorem LoGuercio2025.unblocked_priorMention : Competition.unblocked (PhraseStructure.Tree.structuralAlternatives priorContextLex) expressiveCI johnArrived = {false}

After the mention the bare sentence is used exactly where the speaker does not hold the attitude, the anti-conventional implicature that John is no bastard in the speaker's eyes.