Structurally-Defined Alternatives

@cite{katzir-2007}

Katzir, R. (2007). Structurally-defined alternatives. Linguistics and Philosophy, 30(6), 669–690.

Scalar alternatives are not stipulated via Horn scales but generated structurally. The alternatives to a sentence φ are all parse trees obtainable from φ by three operations — deletion, contraction, and substitution — using items from the substitution source L(φ).

Key Definitions

• Substitution source (def 41): L(φ) = lexicon ∪ subtrees(φ)
• Structural complexity (def 19): ψ ≲ φ iff φ can be transformed to ψ by deletion, contraction, and substitution with items from L(φ). Also: φ ∼ ψ (equal complexity) and ψ < φ (strictly less complex).
• Structural alternatives (def 20): A_str(φ) := {ψ : ψ ≲ φ}
• Conversational principle (def 21): do not assert φ if ∃ φ' ∈ A_str(φ) with ⟦φ'⟧ ⊂ ⟦φ⟧ and φ' weakly assertable

The Symmetry Problem

The naïve conversational principle says: don't assert φ if there is a stronger alternative φ'. The symmetry problem (Kroch 1972; von Fintel & Heim class notes; see p. 673) is that for any stronger φ', there exists a symmetric alternative φ'' = φ ∧ ¬φ' which is also stronger, licensing the opposite inference.

Katzir's solution: restrict alternatives to those obtainable by structural operations. For φ = "John ate some of the cake":

• φ' = "John ate all of the cake" ∈ A_str(φ) — by substituting the Det leaf "some" with "all" (both in the lexicon, same category)
• φ'' = "John ate some but not all" ∉ A_str(φ) — requires ConjP/NegP structure not available in L(φ)

Tree Type

Uses the unified Tree C W from Core.Tree. All definitions are parameterized over the category type C, so they work with UD-grounded Cat, framework-specific categories, or any C with BEq/DecidableEq.

Connection to Linglib

• Horn scales subsumed: Lexical substitution of same-category items is a special case of structural alternatives (§8)
• Fills truthmaker gap: Phenomena/Conditionals/Studies/Santorio2018.lean's IsTruthmaker requires ALT_S computed via structural alternative generation
• Economy connection: @cite{katzir-singh-2015}'s complexity ordering in KatzirSingh2015.lean is based on structural complexity (def 19)

def Alternatives.Structural.substitutionSource {C W : Type} (lexicon : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) : List (Core.Tree.Tree C W)

The substitution source for φ (def 41, final version): the union of the lexicon of the language with the set of all subtrees of φ. The revised definition (adding subtrees) is needed to handle Matsumoto's examples (§5) where a complex sub-constituent of φ serves as a substitution source for a simpler constituent elsewhere in φ.

The initial definition (def 18) used only the lexicon; def 41 adds subtrees of φ to derive the inference in examples like: "It was warm yesterday, and it is a little bit more than warm today" where "a little bit more than warm" (a subtree of φ) substitutes for "warm" in the left conjunct.

Equations

• Alternatives.Structural.substitutionSource lexicon φ = lexicon ++ φ.subtrees

inductive Alternatives.Structural.StructOp {C W : Type} (source : List (Core.Tree.Tree C W)) : Core.Tree.Tree C W → Core.Tree.Tree C W → Prop

One structural operation on parse trees (p. 678). StructOp source φ ψ means ψ is obtained from φ by one application of deletion, contraction, or substitution with items from source.

The three operations:

• Deletion: remove a subtree (a child from a node)
• Contraction: remove an edge and identify endpoints (replace a node with one of its same-category children)
• Substitution: replace any constituent with a same-category item from the substitution source L(φ)

The inBind constructor extends Katzir's original PF-only operations to handle binding structures, allowing structural operations inside the body of a λ-binder.

• subst {C W : Type} {source : List (Core.Tree.Tree C W)} {φ ψ : Core.Tree.Tree C W} (h_cat : ψ.cat = φ.cat) (h_src : ψ ∈ source) : StructOp source φ ψ

  Substitute: replace tree with a same-category item from source.

• delete {C W : Type} {source : List (Core.Tree.Tree C W)} {cat : C} {cs : List (Core.Tree.Tree C W)} (i : Fin cs.length) : StructOp source (Core.Tree.Tree.node cat cs) (Core.Tree.Tree.node cat (cs.eraseIdx ↑i))

  Delete: remove the i-th child from a node.

• contract {C W : Type} {source : List (Core.Tree.Tree C W)} {cat : C} {cs : List (Core.Tree.Tree C W)} {child : Core.Tree.Tree C W} (h_mem : child ∈ cs) (h_cat : child.cat = cat) : StructOp source (Core.Tree.Tree.node cat cs) child

  Contract: replace a node with one of its same-category children.

• inChild {C W : Type} {source : List (Core.Tree.Tree C W)} {cat : C} {cs : List (Core.Tree.Tree C W)} (i : Fin cs.length) {ψ_child : Core.Tree.Tree C W} (h_step : StructOp source (cs.get i) ψ_child) : StructOp source (Core.Tree.Tree.node cat cs) (Core.Tree.Tree.node cat (cs.set (↑i) ψ_child))

  Recursive: apply an operation inside one child of a node.

• inBind {C W : Type} {source : List (Core.Tree.Tree C W)} {n : ℕ} {cat : C} {body body' : Core.Tree.Tree C W} (h_step : StructOp source body body') : StructOp source (Core.Tree.Tree.bind n cat body) (Core.Tree.Tree.bind n cat body')

  Recursive: apply an operation inside a binder body.

def Alternatives.Structural.atMostAsComplex {C W : Type} (source : List (Core.Tree.Tree C W)) (ψ φ : Core.Tree.Tree C W) : Prop

Structural complexity ordering (def 19): ψ ≲ φ iff φ can be transformed into ψ by a finite chain of structural operations using items from source.

Formally: the reflexive-transitive closure of StructOp source.

Equations

• Alternatives.Structural.atMostAsComplex source ψ φ = Relation.ReflTransGen (Alternatives.Structural.StructOp source) φ ψ

def Alternatives.Structural.equalComplexity {C W : Type} (source : List (Core.Tree.Tree C W)) (φ ψ : Core.Tree.Tree C W) : Prop

Equal complexity (def 19): φ ∼ ψ iff φ ≲ ψ ∧ ψ ≲ φ.

Equations

• Alternatives.Structural.equalComplexity source φ ψ = (Alternatives.Structural.atMostAsComplex source φ ψ ∧ Alternatives.Structural.atMostAsComplex source ψ φ)

def Alternatives.Structural.strictlyLessComplex {C W : Type} (source : List (Core.Tree.Tree C W)) (ψ φ : Core.Tree.Tree C W) : Prop

Strictly less complex (def 19): ψ < φ iff ψ ≲ φ ∧ ¬(φ ≲ ψ).

Equations

• Alternatives.Structural.strictlyLessComplex source ψ φ = (Alternatives.Structural.atMostAsComplex source ψ φ ∧ ¬Alternatives.Structural.atMostAsComplex source φ ψ)

def Alternatives.Structural.structuralAlternatives {C W : Type} (lex : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) : Set (Core.Tree.Tree C W)

Structural alternatives (def 20): A_str(φ) := {ψ : ψ ≲ φ}, where ≲ uses L(φ) = lexicon ∪ subtrees(φ).

Equations

• Alternatives.Structural.structuralAlternatives lex φ = {ψ : Core.Tree.Tree C W | Alternatives.Structural.atMostAsComplex (Alternatives.Structural.substitutionSource lex φ) ψ φ}

def Alternatives.Structural.katzirSource {C W : Type} (lex : List (Core.Tree.Tree C W)) : AlternativeSource (Core.Tree.Tree C W)

The Katzir source as an AlternativeSource. Pragmatic competition operators (violatesMP, violatesMaximize, violatesMCIs) accept any AlternativeSource (Tree C W); pass katzirSource lex to recover the classical Katzir 2007 competition. Other sources include Indirect.indirectFrom (Jeretič et al. 2025).

Equations

• Alternatives.Structural.katzirSource lex = Alternatives.Structural.structuralAlternatives lex

theorem Alternatives.Structural.self_is_alternative {C W : Type} (lex : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) : φ ∈ structuralAlternatives lex φ

φ is always a structural alternative to itself (reflexivity of ≲).

theorem Alternatives.Structural.self_mem_katzirSource {C W : Type} (lex : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) : φ ∈ katzirSource lex φ

theorem Alternatives.Structural.equalComplexity.refl {C W : Type} {source : List (Core.Tree.Tree C W)} (φ : Core.Tree.Tree C W) : equalComplexity source φ φ

theorem Alternatives.Structural.equalComplexity.symm {C W : Type} {source : List (Core.Tree.Tree C W)} {a b : Core.Tree.Tree C W} (h : equalComplexity source a b) : equalComplexity source b a

theorem Alternatives.Structural.equalComplexity.trans {C W : Type} {source : List (Core.Tree.Tree C W)} {a b c : Core.Tree.Tree C W} (h₁ : equalComplexity source a b) (h₂ : equalComplexity source b c) : equalComplexity source a c

theorem Alternatives.Structural.equalComplexity_terminal_subst {C W : Type} (source : List (Core.Tree.Tree C W)) (cat : C) (oldW newW : W) (h_old : Core.Tree.Tree.terminal cat oldW ∈ source) (h_new : Core.Tree.Tree.terminal cat newW ∈ source) : equalComplexity source (Core.Tree.Tree.terminal cat oldW) (Core.Tree.Tree.terminal cat newW)

A single same-category terminal substitution gives equal complexity, provided BOTH terminals are in the source (so the substitution is reversible). The standard atom for any equalComplexity chain.

inductive Alternatives.Structural.ExWord : Type

Vocabulary for the worked examples.

• john : ExWord
• ate : ExWord
• some_ : ExWord
• all_ : ExWord
• cake : ExWord
• apple : ExWord
• pear : ExWord
• or_ : ExWord
• and_ : ExWord
• tall : ExWord
• man : ExWord
• but_ : ExWord
• not_ : ExWord

@[implicit_reducible]

instance Alternatives.Structural.instDecidableEqExWord : DecidableEq ExWord

Equations

• Alternatives.Structural.instDecidableEqExWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Alternatives.Structural.instReprExWord.repr : ExWord → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.Structural.instReprExWord : Repr ExWord

Equations

• Alternatives.Structural.instReprExWord = { reprPrec := Alternatives.Structural.instReprExWord.repr }

def Alternatives.Structural.exLexicon : List (Core.Tree.Tree Core.Tree.Cat ExWord)

Minimal lexicon: terminal items available for substitution.

Equations

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

def Alternatives.Structural.someSentence : Core.Tree.Tree Core.Tree.Cat ExWord

φ = "John ate some cake" (simplified parse tree).

Equations

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

def Alternatives.Structural.allSentence : Core.Tree.Tree Core.Tree.Cat ExWord

φ' = "John ate all cake" — the scalar alternative.

Equations

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

theorem Alternatives.Structural.leafSubst_some_all : Core.Tree.Tree.leafSubst ExWord.some_ ExWord.all_ Core.Tree.Cat.Det someSentence = allSentence

Leaf substitution of "some" → "all" produces the expected tree.

theorem Alternatives.Structural.all_is_alternative_to_some : allSentence ∈ structuralAlternatives exLexicon someSentence

φ' is a structural alternative to φ: substitute Det leaf "some" with "all" from the lexicon (both Det, same category).

This is the paper's ex. (25): φ = "John ate some of the cake", φ' = "John ate all of the cake". Since "all" and "some" are both in the lexicon and both Det, substitution yields φ' ∼ φ, so φ' ∈ A_str(φ).

theorem Alternatives.Structural.some_all_equal_complexity : equalComplexity (substitutionSource exLexicon someSentence) someSentence allSentence

Equal complexity: "some" ↔ "all" by mutual substitution (same number of operations in each direction). φ' ∼ φ in the sense of def 19: both φ ≲ φ' and φ' ≲ φ hold (each obtained from the other by one leaf substitution).

def Alternatives.Structural.someButNotAllSentence : Core.Tree.Tree Core.Tree.Cat ExWord

φ'' = "John ate some but not all cake" — the symmetric alternative that the naïve principle cannot exclude.

Under the naïve principle, φ'' is stronger than φ (⟦φ''⟧ ⊂ ⟦φ⟧) and should block assertion of φ. But it licenses the inference that John ate ALL of the cake — the opposite of the correct implicature. Katzir's structural approach excludes φ'' because it requires ConjP and NegP structure not derivable from L(φ).

Equations

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

theorem Alternatives.Structural.symmetric_has_conjp : Core.Tree.Tree.containsCat Core.Tree.Cat.ConjP someButNotAllSentence = true

φ'' contains ConjP — a category absent from φ and L(φ).

theorem Alternatives.Structural.some_lacks_conjp : Core.Tree.Tree.containsCat Core.Tree.Cat.ConjP someSentence = false

φ does not contain ConjP.

theorem Alternatives.Structural.source_lacks_conjp : ((substitutionSource exLexicon someSentence).all fun (t : Core.Tree.Tree Core.Tree.Cat ExWord) => !Core.Tree.Tree.containsCat Core.Tree.Cat.ConjP t) = true

No item in L(someSentence) contains ConjP: the lexicon consists of terminal leaves (which have no internal structure) and the subtrees of φ are {S[...], N(john), VP[...], V(ate), Det(some), N(cake)} — none contain ConjP.

theorem Alternatives.Structural.category_preservation {C W : Type} [BEq C] (source : List (Core.Tree.Tree C W)) (c : C) (φ ψ : Core.Tree.Tree C W) (h_source : ∀ s ∈ source, Core.Tree.Tree.containsCat c s = false) (h_φ : Core.Tree.Tree.containsCat c φ = false) (h_reach : atMostAsComplex source ψ φ) : Core.Tree.Tree.containsCat c ψ = false

Key invariant: structural operations preserve absence of a category when that category does not appear in the substitution source.

If no item in source contains category c, and tree φ does not contain c, then no tree reachable from φ by structural operations contains c. This is because:

• Substitution can only introduce material from source (which lacks c)
• Deletion removes material (can't introduce c)
• Contraction promotes a subtree (which also lacks c by hypothesis)

Proof by induction on ReflTransGen, reducing to the single-step structOp_preserves_no_cat which case-splits on the five StructOp constructors.

theorem Alternatives.Structural.symmetry_problem_solved : someButNotAllSentence ∉ structuralAlternatives exLexicon someSentence

The symmetric alternative φ'' is NOT a structural alternative to φ.

Proof sketch: L(φ) contains no item with category ConjP (source_lacks_conjp), and φ itself lacks ConjP (some_lacks_conjp), so by category_preservation every tree in A_str(φ) lacks ConjP. But φ'' contains ConjP (symmetric_has_conjp) — contradiction.

This is the paper's central result: structure alone excludes the symmetric alternative, solving the symmetry problem without lexical stipulation of which alternatives are "good."

def Alternatives.Structural.orSentence : Core.Tree.Tree Core.Tree.Cat ExWord

φ = "John ate the apple or the pear" (ex. 26a).

Equations

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

def Alternatives.Structural.andSentence : Core.Tree.Tree Core.Tree.Cat ExWord

φ' = "John ate the apple and the pear" (ex. 26b). Obtained by substituting Conj "or" with "and".

Equations

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

theorem Alternatives.Structural.leafSubst_or_and : Core.Tree.Tree.leafSubst ExWord.or_ ExWord.and_ Core.Tree.Cat.Conj orSentence = andSentence

Leaf substitution of "or" → "and" produces the conjunction.

theorem Alternatives.Structural.and_is_alternative_to_or : andSentence ∈ structuralAlternatives exLexicon orSentence

"and" alternative obtainable by one substitution step.

def Alternatives.Structural.leftDisjunct : Core.Tree.Tree Core.Tree.Cat ExWord

The left disjunct "John ate the apple" is an alternative to the disjunction — obtainable by deletion of the right disjunct and the conjunction.

This derives the effect of Sauerland's L operator (which returns the left argument of a binary connective) from structural operations alone, without stipulating L as a primitive. The paper (p. 683) notes that L and R are "somewhat stipulative" and that structural alternatives derive the same predictions.

Equations

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

theorem Alternatives.Structural.left_disjunct_is_alternative : leftDisjunct ∈ structuralAlternatives exLexicon orSentence

def Alternatives.Structural.rightDisjunct : Core.Tree.Tree Core.Tree.Cat ExWord

The right disjunct is also an alternative (Sauerland's R operator).

Equations

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

theorem Alternatives.Structural.right_disjunct_is_alternative : rightDisjunct ∈ structuralAlternatives exLexicon orSentence

def Alternatives.Structural.tallMan : Core.Tree.Tree Core.Tree.Cat ExWord

"A tall man" parse tree (ex. 29a).

Equations

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

def Alternatives.Structural.justMan : Core.Tree.Tree Core.Tree.Cat ExWord

"A man" — obtained by deleting the Adj modifier (ex. 29b).

Equations

• Alternatives.Structural.justMan = Core.Tree.Tree.node Core.Tree.Cat.NP [Core.Tree.Tree.terminal Core.Tree.Cat.N Alternatives.Structural.ExWord.man]

theorem Alternatives.Structural.deletion_produces_alternative : justMan ∈ structuralAlternatives exLexicon tallMan

Deletion produces a simpler alternative: "a man" ∈ A_str("a tall man").

Under the structural approach, any modifier can be deleted to produce an alternative. Since the modified NP entails the bare NP ("a tall man came" → "a man came"), the bare NP is a stronger alternative in upward-entailing contexts, triggering no implicature. In DE contexts, entailment reverses and deletion alternatives generate inferences (§4.3, exx. 30–32).

theorem Alternatives.Structural.deletion_reduces_size : justMan.size < tallMan.size

Deletion reduces tree size.

theorem Alternatives.Structural.horn_alternatives_are_structural {C W : Type} [BEq C] [LawfulBEq C] [BEq W] (lex : List (Core.Tree.Tree C W)) (φ : Core.Tree.Tree C W) (α β : W) (c : C) (_h_α_in_lex : Core.Tree.Tree.terminal c α ∈ lex) (_h_β_in_lex : Core.Tree.Tree.terminal c β ∈ lex) : Core.Tree.Tree.leafSubst α β c φ ∈ structuralAlternatives lex φ

Horn scale alternatives are a special case of structural alternatives.

If two words α and β are on the same Horn scale (and therefore have the same syntactic category), then for any sentence tree φ containing α, the tree φ[β/α] obtained by leaf substitution is a structural alternative to φ. This is because:

1. β is in the lexicon (hence in L(φ))
2. β has the same category as α
3. Leaf substitution is a sequence of StructOp.subst steps (one per occurrence of α)

This means the scale-based approach to alternatives (listing Horn sets like ⟨some, most, all⟩) is not wrong — it is subsumed by the structural approach. Everything a Horn scale generates, structural operations generate too. But structural operations also generate alternatives that scales miss: deletion alternatives in DE contexts (§4.3), and sub-constituent alternatives for disjunction (§4.2).

def Alternatives.Structural.violatesMaximize {C W World : Type} (src : AlternativeSource (Core.Tree.Tree C W)) (contentFn : Core.Tree.Tree C W → World → Bool) (φ : Core.Tree.Tree C W) (weaklyAssertable : Core.Tree.Tree C W → Bool) : 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, @cite{katzir-2007})
• Presuppositional content → Antipresuppositions (Maximize Presupposition, @cite{schlenker-2012})
• CI content → Anti-Conventional Implicatures (MCIs!, @cite{lo-guercio-2025})

All three are instances of: do not use φ if there is a formal alternative φ' ∈ F(φ) such that (a) φ' is strictly more informative along the relevant content dimension, (b) φ' is contextually relevant, and (c) ¬φ' is innocently excludable.

contentFn maps each tree to its content along the relevant dimension.

The competitor set is supplied as an AlternativeSource parameter so that the same operator works for Katzir alternatives (katzirSource lex), indirect alternatives (Indirect.indirectFromKatzir, @cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}), or any other source.

Equations

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

@[reducible, inline]

abbrev Alternatives.Structural.violatesConversationalPrinciple {C W World : Type} (src : AlternativeSource (Core.Tree.Tree C W)) (meaning : Core.Tree.Tree C W → World → Bool) (φ : Core.Tree.Tree C W) (weaklyAssertable : Core.Tree.Tree C W → Bool) : Prop

The neo-Gricean conversational principle: violatesMaximize applied to at-issue (truth-conditional) content. @cite{katzir-2007} def 21.

Equations

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

def Alternatives.Structural.violatesMP {C W World : Type} (src : AlternativeSource (Core.Tree.Tree C W)) (presupFn assertionFn : Core.Tree.Tree C W → World → Bool) (φ : Core.Tree.Tree C W) (weaklyAssertable : Core.Tree.Tree C W → Bool) : Prop

Maximize Presupposition (@cite{schlenker-2012}): violatesMaximize applied to presuppositional content. Do not use φ if there is a competitor φ' (from src) with the same assertive content but stronger presupposition.

Pass katzirSource lex for Katzir alternatives; Indirect.indirectFromKatzir lex pron for indirect alternatives (@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}).

Equations

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

@[reducible, inline]

abbrev Alternatives.Structural.violatesMCIs {C W World : Type} (src : AlternativeSource (Core.Tree.Tree C W)) (ciContentFn : Core.Tree.Tree C W → World → Bool) (φ : Core.Tree.Tree C W) (weaklyAssertable : Core.Tree.Tree C W → Bool) : Prop

Maximize Conventional Implicatures (@cite{lo-guercio-2025} def 15): violatesMaximize applied to CI content. Unlike MP!, does NOT require the same assertive content — CI content is independent of truth conditions.

Do not use φ if there is a formal alternative φ' ∈ F(φ) such that: a. ⟦φ'⟧ᵘ ⊂ ⟦φ⟧ᵘ (CI-stronger) b. φ' ∈ C (contextually relevant) c. ¬⟦φ'⟧ᵘ doesn't contradict the negation of CI content of any element in C

Equations

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

def Alternatives.Structural.atLeastAsGoodAs {C W World : Type} (lex : List (Core.Tree.Tree C W)) (meaning : Core.Tree.Tree C W → World → Bool) (φ ψ : Core.Tree.Tree C W) : Prop

At-least-as-good-as relation (def 23, p. 680): φ ≲ ψ iff φ ≲_struct ψ ∧ ⟦φ⟧ ⊆ ⟦ψ⟧.

This combines structural complexity (from def 19) with semantic entailment. It is the relation that @cite{katzir-singh-2015} use as the basis for the Answer Condition in KatzirSingh2015.lean, where it appears as Scenario.atLeastAsGood.

The key insight: in KatzirSingh2015.lean, complexity is an abstract ℕ parameter. Here, structural complexity gives that parameter its intended content — the number of structural operations needed.

Equations

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