inductive NeoGricean.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 NeoGricean.ConventionalImplicatures.instReprCIAlternativeType : Repr CIAlternativeType

Equations

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

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

Equations

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

instance NeoGricean.ConventionalImplicatures.instDecidableEqCIAlternativeType : DecidableEq CIAlternativeType

Equations

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

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

Equations

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

instance NeoGricean.ConventionalImplicatures.instBEqCIAlternativeType : BEq CIAlternativeType

Equations

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

structure NeoGricean.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 NeoGricean.ConventionalImplicatures.instReprCIAlternativePair : Repr CIAlternativePair

Equations

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

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

Equations

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

def NeoGricean.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 NeoGricean.ConventionalImplicatures.honorificPair (name : String) (relevant : Bool) : CIAlternativePair

Equations

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

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

Equations

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

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

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

Equations

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

instance NeoGricean.ConventionalImplicatures.instReprMCIsResult : Repr MCIsResult

Equations

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

def NeoGricean.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 NeoGricean.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

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

def NeoGricean.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

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

def NeoGricean.ConventionalImplicatures.example_honorific_ACI : MCIsResult

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

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

Equations

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

def NeoGricean.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

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

theorem NeoGricean.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 NeoGricean.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

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

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

structure NeoGricean.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

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

Equations

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

instance NeoGricean.ConventionalImplicatures.instReprACIWithCancellation : Repr ACIWithCancellation

Equations

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

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

Equations

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

def NeoGricean.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

• NeoGricean.ConventionalImplicatures.reinforceACI result = result

structure NeoGricean.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 NeoGricean.ConventionalImplicatures.instReprScalarInferenceComparison : Repr ScalarInferenceComparison

Equations

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

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

Equations

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

def NeoGricean.ConventionalImplicatures.siProperties : ScalarInferenceComparison

Equations

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

def NeoGricean.ConventionalImplicatures.antipresupProperties : ScalarInferenceComparison

Equations

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

def NeoGricean.ConventionalImplicatures.aciProperties : ScalarInferenceComparison

Equations

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

theorem NeoGricean.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]