inductive Implicature.ConventionalImplicatures.CIAlternativeType : Type

Types of CI-bearing expressions that can form alternative sets.

Following Lo Guercio's examples from §3.2:

• Epithets and honorifics (§3.2.1)
• Nominal appositives (§3.2.3)
• Supplementary adverbs (§3.2.3)
• Emotive markers (§3.2.3)

• epithet : CIAlternativeType
• honorific : CIAlternativeType
• nominalAppositive : CIAlternativeType
• suppAdverb : CIAlternativeType
• emotiveMarker : CIAlternativeType

instance Implicature.ConventionalImplicatures.instReprCIAlternativeType : Repr CIAlternativeType

Equations

• Implicature.ConventionalImplicatures.instReprCIAlternativeType = { reprPrec := Implicature.ConventionalImplicatures.instReprCIAlternativeType.repr }

def Implicature.ConventionalImplicatures.instReprCIAlternativeType.repr : CIAlternativeType → ℕ → Std.Format

Equations

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

instance Implicature.ConventionalImplicatures.instDecidableEqCIAlternativeType : DecidableEq CIAlternativeType

Equations

• Implicature.ConventionalImplicatures.instDecidableEqCIAlternativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Implicature.ConventionalImplicatures.instBEqCIAlternativeType : BEq CIAlternativeType

Equations

• Implicature.ConventionalImplicatures.instBEqCIAlternativeType = { beq := Implicature.ConventionalImplicatures.instBEqCIAlternativeType.beq }

def Implicature.ConventionalImplicatures.instBEqCIAlternativeType.beq : CIAlternativeType → CIAlternativeType → Bool

Equations

• Implicature.ConventionalImplicatures.instBEqCIAlternativeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Implicature.ConventionalImplicatures.CIAlternativePair : Type

A CI alternative pair: weaker and stronger CI expressions.

Following @cite{fox-katzir-2011}, alternatives must be:

1. Formal alternatives (constructible by substitution)
2. At most as complex as the original
3. Contextually relevant

• altType : CIAlternativeType

  Type of CI expression

• weaker : String

  The weaker CI expression (used)

• stronger : String

  The stronger CI expression (alternative)

• strongerIsRelevant : Bool

  Is the stronger alternative contextually relevant?

instance Implicature.ConventionalImplicatures.instReprCIAlternativePair : Repr CIAlternativePair

Equations

• Implicature.ConventionalImplicatures.instReprCIAlternativePair = { reprPrec := Implicature.ConventionalImplicatures.instReprCIAlternativePair.repr }

def Implicature.ConventionalImplicatures.instReprCIAlternativePair.repr : CIAlternativePair → ℕ → Std.Format

Equations

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

def Implicature.ConventionalImplicatures.epithetPair (name : String) (relevant : Bool) : CIAlternativePair

Standard CI alternative pairs from Lo Guercio.

The stronger alternative is only a formal alternative if it is contextually relevant (mentioned, subconstituent, or lexical).

Equations

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

def Implicature.ConventionalImplicatures.honorificPair (name : String) (relevant : Bool) : CIAlternativePair

Equations

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

def Implicature.ConventionalImplicatures.appositivePair (name property : String) (relevant : Bool) : CIAlternativePair

Equations

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

structure Implicature.ConventionalImplicatures.MCIsResult : Type

Result of applying MCIs! (Maximize Conventional Implicatures).

Parallel to StandardRecipeResult from NeoGricean.Core.Basic.

• utterance : String

  The utterance analyzed

• ciAlternative : String

  The CI alternative considered

• alternativeIsCIStronger : Bool

  Is the alternative CI-stronger?

• alternativeIsFormal : Bool

  Is the alternative a formal alternative (contextually relevant)?

• aciArises : Bool

  Does an ACI arise?

• aciContent : Option String

  The inferred ACI content (if any)

instance Implicature.ConventionalImplicatures.instReprMCIsResult : Repr MCIsResult

Equations

• Implicature.ConventionalImplicatures.instReprMCIsResult = { reprPrec := Implicature.ConventionalImplicatures.instReprMCIsResult.repr }

def Implicature.ConventionalImplicatures.instReprMCIsResult.repr : MCIsResult → ℕ → Std.Format

Equations

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

def Implicature.ConventionalImplicatures.applyMCIs (pair : CIAlternativePair) : MCIsResult

Apply MCIs! to derive an ACI.

Following @cite{lo-guercio-2025} Definition 15:

• If speaker used φ with weaker CI
• And there's a formal alternative φ' with stronger CI
• Then infer speaker couldn't felicitously use φ'
• With competence: speaker believes ¬(CI content of φ')

Equations

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

def Implicature.ConventionalImplicatures.example_outOfBlue_noACI : MCIsResult

Example (18)-(19): Out of the blue, NO ACI arises.

"John arrived late" ⇝̸ ¬(John is a bastard) "Diego entró" ⇝̸ ¬(speaker respects Diego)

Because "that bastard John" is not a formal alternative; it is more complex.

Equations

• Implicature.ConventionalImplicatures.example_outOfBlue_noACI = Implicature.ConventionalImplicatures.applyMCIs (Implicature.ConventionalImplicatures.epithetPair "John" false)

def Implicature.ConventionalImplicatures.example_priorMention_ACI : MCIsResult

Example (20)-(21): With prior mention, an ACI arises.

"John arrived first, then that bastard Pedro arrived." Implicates: not(John is a bastard)

Because "that bastard" is now contextually relevant (mentioned), "that bastard John" is a formal alternative.

Equations

• Implicature.ConventionalImplicatures.example_priorMention_ACI = Implicature.ConventionalImplicatures.applyMCIs (Implicature.ConventionalImplicatures.epithetPair "John" true)

def Implicature.ConventionalImplicatures.example_honorific_ACI : MCIsResult

Example (22)-(23): Honorific parallel.

"Primero entró Donato. Después entró Don Pedro." ⇝ ¬(speaker respects Donato)

Equations

• Implicature.ConventionalImplicatures.example_honorific_ACI = Implicature.ConventionalImplicatures.applyMCIs (Implicature.ConventionalImplicatures.honorificPair "Donato" true)

def Implicature.ConventionalImplicatures.example_appositive_ACI : MCIsResult

Example (31)-(32): Appositive parallel.

"Diego recommended an aspirin. Laura, a doctor, recommended an antibiotic." ⇝ ¬(Diego is a doctor)

Equations

• Implicature.ConventionalImplicatures.example_appositive_ACI = Implicature.ConventionalImplicatures.applyMCIs (Implicature.ConventionalImplicatures.appositivePair "Diego" "a doctor" true)

theorem Implicature.ConventionalImplicatures.aci_independent_of_assertion : ∃ (pair : CIAlternativePair), pair.strongerIsRelevant = true ∧ (applyMCIs pair).aciArises = true

ACIs do not require the same assertive content.

Unlike antipresuppositions, ACIs can arise even when the utterance and alternative have different truth conditions.

Example (50): "Juan called Maria or that bastard Pedro"

• ACI: not(Maria is a bastard)
• Stronger alternative has different assertive content (and vs or)

CI content is independent of at-issue content.

def Implicature.ConventionalImplicatures.aciInDEContext (pair : CIAlternativePair) (_ctx : Core.NaturalLogic.ContextPolarity) : MCIsResult

ACIs are not affected by DE contexts.

Unlike scalar implicatures, ACIs arise in both UE and DE contexts.

Example (61): "I doubt that Juan or that bastard Pedro passed"

• SI blocked: does not implicate not(I doubt Juan and that bastard Pedro passed)
• ACI not blocked: implicates not(Juan is a bastard)

CI content does not interact with truth-conditional entailment.

Equations

• Implicature.ConventionalImplicatures.aciInDEContext pair _ctx = Implicature.ConventionalImplicatures.applyMCIs pair

theorem Implicature.ConventionalImplicatures.aci_polarity_insensitive (pair : CIAlternativePair) : aciInDEContext pair Core.NaturalLogic.ContextPolarity.upward = aciInDEContext pair Core.NaturalLogic.ContextPolarity.downward

structure Implicature.ConventionalImplicatures.ACIWithCancellation : Type

ACIs are cancellable.

Example (52): "Juan arrived first, then that bastard Pedro arrived (by the way, Juan is also a bastard)"

The parenthetical cancels the ACI.

• base : MCIsResult
• cancelled : Bool
• cancellationPhrase : Option String

instance Implicature.ConventionalImplicatures.instReprACIWithCancellation : Repr ACIWithCancellation

Equations

• Implicature.ConventionalImplicatures.instReprACIWithCancellation = { reprPrec := Implicature.ConventionalImplicatures.instReprACIWithCancellation.repr }

def Implicature.ConventionalImplicatures.instReprACIWithCancellation.repr : ACIWithCancellation → ℕ → Std.Format

Equations

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

def Implicature.ConventionalImplicatures.cancelACI (result : MCIsResult) (phrase : String) : ACIWithCancellation

Equations

• Implicature.ConventionalImplicatures.cancelACI result phrase = { base := result, cancelled := true, cancellationPhrase := some phrase }

def Implicature.ConventionalImplicatures.reinforceACI (result : MCIsResult) : MCIsResult

ACIs are reinforceable.

Example (63): Repeating the ACI content is not redundant.

"Juan arrived first, that bastard Pedro arrived second (by the way, Juan is not a bastard)"

The reinforcement is informative, not redundant (unlike presuppositions).

Equations

• Implicature.ConventionalImplicatures.reinforceACI result = result

structure Implicature.ConventionalImplicatures.ScalarInferenceComparison : Type

Summary of how ACIs differ from their "scalar cousins".

Property	SI	Antipresup	ACI
Same assertive content req	No	Yes	No
Affected by DE context	Yes	Varies	No
Cancellable	Yes	Yes	Yes
Reinforceable	Yes	No*	Yes
Embeddable	Yes	Yes	Yes

• Reinforcing a presupposition is redundant

• inferenceType : String
• requiresSameAssertion : Bool
• affectedByDE : Bool
• cancellable : Bool
• reinforceable : Bool

instance Implicature.ConventionalImplicatures.instReprScalarInferenceComparison : Repr ScalarInferenceComparison

Equations

• Implicature.ConventionalImplicatures.instReprScalarInferenceComparison = { reprPrec := Implicature.ConventionalImplicatures.instReprScalarInferenceComparison.repr }

def Implicature.ConventionalImplicatures.instReprScalarInferenceComparison.repr : ScalarInferenceComparison → ℕ → Std.Format

Equations

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

def Implicature.ConventionalImplicatures.siProperties : ScalarInferenceComparison

Equations

• Implicature.ConventionalImplicatures.siProperties = { inferenceType := "Scalar Implicature", requiresSameAssertion := false, affectedByDE := true, cancellable := true, reinforceable := true }

def Implicature.ConventionalImplicatures.antipresupProperties : ScalarInferenceComparison

Equations

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

def Implicature.ConventionalImplicatures.aciProperties : ScalarInferenceComparison

Equations

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

theorem Implicature.ConventionalImplicatures.aci_grounded_in_mcis {W : Type u_1} (φ ψ : Semantics.Lexical.Expressives.TwoDimProp W) (h_ci_stronger : Semantics.Lexical.Expressives.ciStrongerThan ψ φ) (_h_relevant : ∃ (w : W), ψ.ci w = true) : ∃ (w : W), φ.ci w = true ∧ ψ.ci w = false

The ACI mechanism is grounded in:

1. @cite{potts-2005}: CI content is independent of at-issue content
2. @cite{fox-katzir-2011}: Formal alternatives are structurally constrained
3. Gricean reasoning: Cooperative speakers maximize informativeness

Given these, MCIs! derives ACIs compositionally: if the speaker used φ when a CI-stronger formal alternative ψ was available and relevant, the hearer infers the speaker believes the CI of ψ does not hold. [sorry: need world-level formalization of speaker belief inference]