Pragmatic competition operators

Source-agnostic competition principles: do not use φ if there is a competitor φ' drawn from an Alternatives.Source that is stronger along the relevant content dimension. The competitor set is supplied as a Source S parameter, so the same operators work for Katzir alternatives (Structural.katzirSource lex), indirect alternatives (indirectFrom (katzirSource lex) …, [JBG+25]), Horn scales, or any other source — over any carrier S, not just parse trees.

Main definitions

• violatesMaximize — the generic "maximize content" principle along a Prop-valued content dimension ([Kat07]).
• violatesConversationalPrinciple — at-issue content instantiation (scalar implicature, [Kat07]).
• violatesMP — Maximize Presupposition ([Hei91], [Sch12b]): same assertive content, stronger presupposition.
• violatesMCIs — Maximize Conventional Implicatures ([LG25]): CI-content instantiation.

Main results

• violatesMaximize_of_violatesMP / violatesMP_of_violatesMaximize_sameAssertion — relate violatesMP to violatesMaximize on the presuppositional axis.

def Alternatives.violatesMaximize {S : Type u_1} {World : Type u_2} (src : Source S) (contentFn : S → World → Prop) (φ : S) (weaklyAssertable : S → Prop) : Prop

Generic "maximize content" principle parameterized over content dimension.

Scalar inferences arise from comparing a sentence φ with formal alternatives φ' that are more informative along some content dimension. The same reasoning applies to three dimensions:

• At-issue content → Scalar Implicatures (Conversational Principle, [Kat07])
• Presuppositional content → Antipresuppositions (Maximize Presupposition, [Sch12b])
• CI content → Anti-Conventional Implicatures (MCIs!, [LG25])

contentFn maps each expression to its content along the relevant dimension, a Prop-valued predicate (felicity, entailment, or CI satisfaction).

Equations

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

@[reducible, inline]

abbrev Alternatives.violatesConversationalPrinciple {S : Type u_1} {World : Type u_2} (src : Source S) (meaning : S → World → Prop) (φ : S) (weaklyAssertable : S → Prop) : Prop

The neo-Gricean conversational principle: violatesMaximize applied to at-issue (truth-conditional) content ([Kat07]).

Equations

• Alternatives.violatesConversationalPrinciple src meaning φ weaklyAssertable = Alternatives.violatesMaximize src meaning φ weaklyAssertable

def Alternatives.violatesMP {S : Type u_1} {World : Type u_2} (src : Source S) (presupFn assertionFn : S → World → Prop) (φ : S) (weaklyAssertable : S → Prop) : Prop

Maximize Presupposition (the principle: [Hei91]; reconstructed from Gricean reasoning by [Sch12b]): violatesMaximize applied to presuppositional content. Do not use φ if there is a competitor φ' (from src) with the same assertive content but stronger presupposition.

Modeling note on the same-assertion clause. assertionFn φ' w ↔ assertionFn φ w is required at every world. This is the right notion when assertionFn is the total at-issue content with presupposition factored out. If instead assertionFn were partial (undefined where φ's stronger presupposition fails), the standard antipresupposition condition asks for assertion-agreement only *where φ' is defined*, i.e. ∀ w, presupFn φ' w → (assertionFn φ' w ↔ assertionFn φ w). The unconditional form here is retained because the consumer Studies/JereticEtAl2025.lean (tous_violatesMP_via_indirect) supplies total Prop-valued content; switch to the guarded form if a partial assertionFn` is ever used.

Equations

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

@[reducible, inline]

abbrev Alternatives.violatesMCIs {S : Type u_1} {World : Type u_2} (src : Source S) (ciContentFn : S → World → Prop) (φ : S) (weaklyAssertable : S → Prop) : Prop

Maximize Conventional Implicatures ([LG25]): violatesMaximize applied to CI content. Unlike MP!, does NOT require the same assertive content — CI content is independent of truth conditions. UNVERIFIED: the specific numbered definition in [LG25] (was cited as "def 15" from memory) is not checked against the PDF.

Equations

• Alternatives.violatesMCIs src ciContentFn φ weaklyAssertable = Alternatives.violatesMaximize src ciContentFn φ weaklyAssertable

Structural relationships between MP and Maximize

violatesMP differs from violatesMaximize on the same presupFn only by the additional same-assertion clause. The two theorems below make the relationship Lean-checkable, discharging the diagnostic prose in [LG25] §4 that "ACIs do not require same assertive content, unlike antipresuppositions."

theorem Alternatives.violatesMaximize_of_violatesMP {S : Type u_1} {World : Type u_2} {src : Source S} {presupFn assertionFn : S → World → Prop} {φ : S} {weaklyAssertable : S → Prop} (h : violatesMP src presupFn assertionFn φ weaklyAssertable) : violatesMaximize src presupFn φ weaklyAssertable

Every violatesMP violation is also a violatesMaximize violation on the presuppositional axis (drops the same-assertion clause).

theorem Alternatives.violatesMP_of_violatesMaximize_sameAssertion {S : Type u_1} {World : Type u_2} {src : Source S} {presupFn assertionFn : S → World → Prop} {φ : S} {weaklyAssertable : S → Prop} (h_max : violatesMaximize src presupFn φ weaklyAssertable) (h_assert : ∀ (φ' : S), φ' ∈ src φ → ∀ (w : World), assertionFn φ' w ↔ assertionFn φ w) : violatesMP src presupFn assertionFn φ weaklyAssertable

Conversely, a violatesMaximize violation on presupFn combined with same-assertion at every alternative gives a violatesMP violation.