Maximize Presupposition

@cite{heim-1991}

Maximize Presupposition (MP) is a pragmatic principle: among competing expressions with the same assertive content, use the one with the strongest satisfied presupposition.

Three formulations unified

This module provides a general, domain-agnostic formulation of MP and connects it to existing domain-specific implementations:

1. OT formulation (mpConstraintOf): MP as a NamedConstraint C parameterized by a presuppositional strength function. Violation count = maxStrength − strength(c). Wang2023's mpConstraint is an instance (phiMP).

2. Structural alternatives (violatesMP in Theories.Semantics.Alternatives.Structural): MP defined over syntactic trees, parametric in an Alternatives.AlternativeSource (Tree C W). The classical Katzir 2007 source is katzirSource lex; the indirect-alternative source Alternatives.Indirect.indirectFrom (@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}) competes with unpronounceable Katzir witnesses (e.g. les deux NP competes with the silent tous les NP.dual via the Indirect Alternative construction). Bridge to the OT formulation is conceptual: both enforce "prefer the strongest presupposition" but over different candidate-generation mechanisms.

3. IC/FP/MP ranking (PragConstraint.MP in Phenomena/Presupposition/Studies/Wang2025.lean): MP as a violable constraint ranked below IC (Internal Coherence) and FP (Felicity Presupposition). Describes MP's position in the constraint hierarchy for presupposition obligatoriness (@cite{wang-2025}). Trigger typology lives in Semantics.Presupposition.TriggerTypology.

Core abstraction

MP competition requires three ingredients:

1. A candidate set — forms that can fill the same syntactic position
2. A presuppositional strength measure — strength : C → Nat
3. A same-assertion condition — all candidates have identical at-issue content (e.g., phiPresup_same_assertion)

MP penalizes failure to maximize strength: candidates with weaker presuppositions incur more violations. The key structural property: MP is antagonistic to markedness constraints, which penalize strength directly (mp_reverses_markedness).

Architecture

• §1: Abstract MP and markedness constraints (mpConstraintOf, markednessPenalty)
• §2: Structural properties (reversal, dominance)
• §3: Phi-feature instance (phiMP)
• §4: Presuppositional strict total order on well-formed cells

§1: Abstract Constraints

Two generic constraint constructors, parameterized by a presuppositional strength function strength : C → Nat:

• mpConstraintOf: penalizes failure to maximize presupposition. Violation count = maxStrength - strength c.
• markednessPenalty: penalizes presuppositional strength directly. Violation count = strength c.

These are antagonistic: for any candidate c, mpConstraintOf.eval c + markednessPenalty.eval c = maxStrength (when strength c ≤ maxStrength).

def Semantics.Presupposition.MaximizePresupposition.mpConstraintOf {C : Type} (maxStrength : ℕ) (strength : C → ℕ) : Core.Constraint.OT.NamedConstraint C

Build an MP constraint from a presuppositional strength function. Violation count = maxStrength - strength c: maximal presupposition → 0 violations, weaker presupposition → more.

Equations

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

def Semantics.Presupposition.MaximizePresupposition.markednessPenalty {C : Type} (strength : C → ℕ) : Core.Constraint.OT.NamedConstraint C

A markedness constraint penalizing presuppositional strength. Violation count = strength c: stronger presupposition → more violations. This is the generic form of Wang2023's todConstraint (Taboo of Directness).

Equations

• Semantics.Presupposition.MaximizePresupposition.markednessPenalty strength = { name := "Markedness", family := Core.Constraint.OT.ConstraintFamily.markedness, eval := strength }

theorem Semantics.Presupposition.MaximizePresupposition.mp_markedness_complementary {C : Type} (maxStrength : ℕ) (strength : C → ℕ) (c : C) (h : strength c ≤ maxStrength) : (mpConstraintOf maxStrength strength).eval c + (markednessPenalty strength).eval c = maxStrength

Violation counts sum to maxStrength for any candidate whose strength does not exceed the maximum.

§2: Structural Properties

The core algebraic facts about MP and markedness as OT constraints. These hold for any candidate type and strength function.

theorem Semantics.Presupposition.MaximizePresupposition.mp_zero_at_max {C : Type} (maxStrength : ℕ) (strength : C → ℕ) (c : C) (hMax : strength c = maxStrength) : (mpConstraintOf maxStrength strength).eval c = 0

MP assigns 0 violations to the maximally presupposing candidate.

theorem Semantics.Presupposition.MaximizePresupposition.markedness_zero_at_min {C : Type} (strength : C → ℕ) (c : C) (hMin : strength c = 0) : (markednessPenalty strength).eval c = 0

Markedness assigns 0 violations to the minimally presupposing candidate.

theorem Semantics.Presupposition.MaximizePresupposition.mp_reverses_markedness {C : Type} (maxStrength : ℕ) (strength : C → ℕ) (c₁ c₂ : C) (h₁ : strength c₁ ≤ maxStrength) (h₂ : strength c₂ ≤ maxStrength) : (markednessPenalty strength).eval c₁ < (markednessPenalty strength).eval c₂ ↔ (mpConstraintOf maxStrength strength).eval c₁ > (mpConstraintOf maxStrength strength).eval c₂

MP and markedness impose opposite orderings: fewer MP violations ↔ more markedness violations. This is the general form of Wang2023's tod_reverses_mp.

theorem Semantics.Presupposition.MaximizePresupposition.mp_selects_strongest {C : Type} [DecidableEq C] (candidates : List C) (maxStrength : ℕ) (strength : C → ℕ) (rest : List (Core.Constraint.OT.NamedConstraint C)) (hNE : candidates ≠ []) (hBound : ∀ c ∈ candidates, strength c ≤ maxStrength) (hExists : ∃ c₀ ∈ candidates, strength c₀ = maxStrength) (c : C) : c ∈ (Core.Constraint.OT.mkTableau candidates (mpConstraintOf maxStrength strength :: rest) hNE).optimal → strength c = maxStrength

MP dominant → strongest wins: when MP is the top-ranked constraint, all optimal candidates have maximal presuppositional strength. Proof via optimal_zero_first — a max-strength candidate has 0 MP violations, forcing all winners to have 0 as well.

theorem Semantics.Presupposition.MaximizePresupposition.markedness_selects_weakest {C : Type} [DecidableEq C] (candidates : List C) (strength : C → ℕ) (rest : List (Core.Constraint.OT.NamedConstraint C)) (hNE : candidates ≠ []) (hExists : ∃ c₀ ∈ candidates, strength c₀ = 0) (c : C) : c ∈ (Core.Constraint.OT.mkTableau candidates (markednessPenalty strength :: rest) hNE).optimal → strength c = 0

Markedness dominant → weakest wins: when a markedness constraint is the top-ranked constraint, all optimal candidates have zero presuppositional strength. This is the general form of Wang2023's tod_mp_only_minimal.

§3: Phi-Feature Instance

The phi-feature system (PrivativePair with presupStrength = specLevel) is a canonical instance of MP competition:

• Candidates: well-formed PrivativePair cells (3 cells)
• Strength: presupStrength (= specLevel: 0, 1, or 2)
• maxStrength: 2 (= PrivativePair.maximal.specLevel)
• Same assertion: phiPresup_same_assertion — all cells have identical (trivially true) at-issue content

This section defines phiMP (the instantiation) and proves bridges connecting the general theorems to phiPresup.

def Semantics.Presupposition.MaximizePresupposition.phiMP : Core.Constraint.OT.NamedConstraint Features.PrivativePair

The phi-feature MP constraint: mpConstraintOf instantiated with presupStrength over PrivativePair.

Equations

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

theorem Semantics.Presupposition.MaximizePresupposition.phiMP_eval (c : Features.PrivativePair) : phiMP.eval c = Features.PrivativePair.maximal.specLevel - PhiFeatures.presupStrength c

phiMP evaluates to maxSpec - presupStrength.

def Semantics.Presupposition.MaximizePresupposition.phiMarkedness : Core.Constraint.OT.NamedConstraint Features.PrivativePair

The phi-feature markedness constraint: markednessPenalty instantiated with presupStrength. This is the generic form of ToD.

Equations

• Semantics.Presupposition.MaximizePresupposition.phiMarkedness = Semantics.Presupposition.MaximizePresupposition.markednessPenalty Semantics.Presupposition.PhiFeatures.presupStrength

theorem Semantics.Presupposition.MaximizePresupposition.phiMarkedness_eval (c : Features.PrivativePair) : phiMarkedness.eval c = PhiFeatures.presupStrength c

phiMarkedness evaluates to presupStrength.

theorem Semantics.Presupposition.MaximizePresupposition.phi_same_assertion {E : Type u_1} (innerP outerP : E → Prop) (c₁ c₂ : Features.PrivativePair) (x : E) : (PhiFeatures.phiPresup innerP outerP c₁).assertion x ↔ (PhiFeatures.phiPresup innerP outerP c₂).assertion x

Phi-feature competitors satisfy the same-assertion condition: all cells of phiPresup have identical (trivially true) at-issue content. This is the prerequisite for MP to apply — if assertions differed, the competition would be at-issue (scalar implicature), not presuppositional.

theorem Semantics.Presupposition.MaximizePresupposition.phi_strength_nesting {E : Type u_1} {innerP outerP : E → Prop} (hContain : ∀ (x : E), innerP x → outerP x) {c₁ c₂ : Features.PrivativePair} (hw₁ : c₁.wellFormed = true) (hw₂ : c₂.wellFormed = true) (hSpec : PhiFeatures.presupStrength c₁ ≥ PhiFeatures.presupStrength c₂) (x : E) (h : Core.Presupposition.PrProp.defined x (PhiFeatures.phiPresup innerP outerP c₁)) : Core.Presupposition.PrProp.defined x (PhiFeatures.phiPresup innerP outerP c₂)

Phi-feature competitors satisfy the presuppositional nesting condition: stronger presupposition → smaller domain. This ensures the strength ordering corresponds to genuine set-theoretic containment of presuppositional domains.

theorem Semantics.Presupposition.MaximizePresupposition.phi_mp_selects_maximal (candidates : List Features.PrivativePair) (rest : List (Core.Constraint.OT.NamedConstraint Features.PrivativePair)) (hNE : candidates ≠ []) (hWF : ∀ c ∈ candidates, c.wellFormed = true) (hMax : Features.PrivativePair.maximal ∈ candidates) (c : Features.PrivativePair) : c ∈ (Core.Constraint.OT.mkTableau candidates (phiMP :: rest) hNE).optimal → PhiFeatures.presupStrength c = Features.PrivativePair.maximal.specLevel

MP over phi-features selects the maximal (most marked) cell when it is among the candidates. Instantiation of mp_selects_strongest to PrivativePair.

This is the normal-speech pattern: absent any politeness or context-sensitivity constraint, MP forces use of the form with the strongest presupposition (SG over PL, 1st over 3rd, DEF over INDEF). @cite{sauerland-2003} derives the preference for singular from exactly this principle.

theorem Semantics.Presupposition.MaximizePresupposition.phi_mp_reverses_markedness (c₁ c₂ : Features.PrivativePair) (hw₁ : c₁.wellFormed = true) (hw₂ : c₂.wellFormed = true) : phiMarkedness.eval c₁ < phiMarkedness.eval c₂ ↔ phiMP.eval c₁ > phiMP.eval c₂

MP and markedness reverse each other over phi-features. This is the algebraic core of tod_reverses_mp in Wang2023.

§4: presupWeakerThan is a Strict Total Order

presupWeakerThan (defined in PhiFeatures) inherits the strict total order structure of < on Nat via specLevel. We prove the standard order-theoretic properties on well-formed cells.

The key non-trivial result is totality: distinct well-formed cells always have different specLevels (specLevel_injective_wf), so presupWeakerThan is a strict linear order on the 3-element set of well-formed cells.

theorem Semantics.Presupposition.MaximizePresupposition.specLevel_injective_wf (a b : Features.PrivativePair) (ha : a.wellFormed = true) (hb : b.wellFormed = true) (h : a.specLevel = b.specLevel) : a = b

specLevel is injective on well-formed cells: two well-formed cells with the same specLevel are identical. This follows from the three well-formed cells having specLevels 0, 1, 2 — all distinct.

theorem Semantics.Presupposition.MaximizePresupposition.presupWeakerThan_irrefl (c : Features.PrivativePair) : PhiFeatures.presupWeakerThan c c = false

presupWeakerThan is irreflexive.

theorem Semantics.Presupposition.MaximizePresupposition.presupWeakerThan_trans (a b c : Features.PrivativePair) (h₁ : PhiFeatures.presupWeakerThan a b = true) (h₂ : PhiFeatures.presupWeakerThan b c = true) : PhiFeatures.presupWeakerThan a c = true

presupWeakerThan is transitive.

theorem Semantics.Presupposition.MaximizePresupposition.presupWeakerThan_asymm (a b : Features.PrivativePair) (h : PhiFeatures.presupWeakerThan a b = true) : PhiFeatures.presupWeakerThan b a = false

presupWeakerThan is asymmetric.

theorem Semantics.Presupposition.MaximizePresupposition.presupWeakerThan_total (a b : Features.PrivativePair) (ha : a.wellFormed = true) (hb : b.wellFormed = true) (hne : a ≠ b) : PhiFeatures.presupWeakerThan a b = true ∨ PhiFeatures.presupWeakerThan b a = true

presupWeakerThan is total on well-formed cells: for distinct well-formed cells, either a < b or b < a.

theorem Semantics.Presupposition.MaximizePresupposition.strongerThan_iff_not_weakerOrEq (a b : Features.PrivativePair) : PhiFeatures.presupStrongerThan a b = true ↔ PhiFeatures.presupWeakerThan b a = true

presupStrongerThan is the converse of presupWeakerThan.

theorem Semantics.Presupposition.MaximizePresupposition.strength_iff_specLevel (a b : Features.PrivativePair) : PhiFeatures.presupWeakerThan a b = true ↔ a.specLevel < b.specLevel

The presuppositional strength ordering is determined by specLevel: a is strictly weaker than b iff a.specLevel < b.specLevel.