Katzir 2007: Structurally-Defined Alternatives (End-to-End)

[Kat07]

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

Unified Tree Demonstration

This file demonstrates that a single Tree Cat String supports both:

• Structural operations (PF-level): leafSubst generates scalar alternatives by same-category word substitution
• Compositional interpretation (LF-level): evalTree computes truth conditions via FA, PM, and Predicate Abstraction

One tree, two interfaces — the Y-model made concrete.

The Argument

1. Build φ = "some student sleeps" as Tree Cat String with QR
2. Generate φ' = "every student sleeps" via leafSubst and prove it is a genuine structural alternative (φ' ∈ structuralAlternatives) through the Alternatives.Structural substrate
3. Interpret both: ⟦φ⟧ = true, ⟦φ'⟧ = false → asserting φ implicates ¬φ'
4. Prove the symmetric "some but not all" (a ConjP) is NOT a structural alternative via the substrate's category_preservation

This is Katzir's solution to the symmetry problem: structural constraints on alternatives prevent the symmetric alternative from being generated, licensing the scalar implicature. The alternative-generation and exclusion claims are stated about the canonical Alternatives.Structural operators, not re-derived locally.

def Katzir2007.φ : Syntax.Tree Syntax.Cat String

"Some student sleeps" after QR, with UD-grounded categories:

[S [DP [Det some] [N student]] [₁ [S [t₁:NP] [VP [V sleeps]]]]]

Equations

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

def Katzir2007.φ' : Syntax.Tree Syntax.Cat String

Scalar alternative: substitute "some" → "every" at Det position. This is Katzir's core operation (def 19, substitution): replace a terminal with a same-category item from the substitution source. Both "some" and "every" are Det terminals in the lexicon.

Equations

• Katzir2007.φ' = Syntax.Tree.leafSubst "some" "every" Syntax.Cat.Det Katzir2007.φ

def Katzir2007.katzirLex : List (Syntax.Tree Syntax.Cat String)

The lexicon for this fragment: the Det scale-mates plus the content words of φ, as Tree Cat String terminals. Feeds the substitution source L(φ) = katzirLex ∪ subtrees(φ).

Equations

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

theorem Katzir2007.φ'_is_structural_alternative : φ' ∈ Alternatives.Structural.structuralAlternatives katzirLex φ

φ' is a genuine structural alternative to φ, derived through the [Kat07] substrate (Alternatives.Structural): leaf substitution of the Det scale-mate "every" (in katzirLex) is a chain of StructOp.subst steps, so φ' ∈ A_str(φ) by horn_alternatives_are_structural. This states the study's alternative-generation claim about the canonical structuralAlternatives, not a local re-encoding.

theorem Katzir2007.some_student_sleeps : Quantification.some_sem Semantics.Montague.ToyLexicon.student_sem Semantics.Montague.ToyLexicon.sleeps_sem

"Some student sleeps" is true: John is a student and sleeps.

With interpTy .t = Prop, we state the truth condition directly at the Prop level rather than via evalTree (which requires a blanket Decidable instance for all propositions).

theorem Katzir2007.every_student_sleeps : ¬Quantification.every_sem Semantics.Montague.ToyLexicon.student_sem Semantics.Montague.ToyLexicon.sleeps_sem

The scalar alternative "every student sleeps" is false: Mary is a student but doesn't sleep.

theorem Katzir2007.readings_differ : Quantification.some_sem Semantics.Montague.ToyLexicon.student_sem Semantics.Montague.ToyLexicon.sleeps_sem ∧ ¬Quantification.every_sem Semantics.Montague.ToyLexicon.student_sem Semantics.Montague.ToyLexicon.sleeps_sem

The two readings differ: genuine scalar inference. Asserting "some" when "every" was available implicates ¬"every". The asymmetry is witnessed: "some" is satisfiable (John), while "every" is refuted (Mary is a student who doesn't sleep).

The symmetry problem: for any stronger alternative φ' = "every", there exists a symmetric alternative φ'' = "some but not all" which is also stronger. Naïve exhaustivity would predict no implicature.

Katzir's solution: φ'' requires ConjP and NegP structure, which cannot be generated from L(φ) = lexicon ∪ subtrees(φ) because the source tree φ contains neither category. We discharge this through the substrate's category_preservation, not by raw containsCat assertions — the same mechanism that proves Alternatives.Structural.symmetry_problem_solved, here on the QR-structured Tree Cat String.

def Katzir2007.φ'' : Syntax.Tree Syntax.Cat String

The symmetric alternative φ'' = "some but not all student sleeps", with the Det position filled by a ConjP.

Equations

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

theorem Katzir2007.no_conjp : ¬Syntax.Tree.ContainsCat Syntax.Cat.ConjP φ

φ contains no ConjP anywhere in its structure.

theorem Katzir2007.no_negp : ¬Syntax.Tree.ContainsCat Syntax.Cat.NegP φ

φ contains no NegP anywhere in its structure.

theorem Katzir2007.source_lacks_conjp (t : Syntax.Tree Syntax.Cat String) : t ∈ Alternatives.Structural.substitutionSource katzirLex φ → ¬Syntax.Tree.ContainsCat Syntax.Cat.ConjP t

No item in L(φ) = katzirLex ∪ subtrees(φ) contains ConjP: the lexicon is flat Det/N/V terminals and φ's subtrees are ConjP-free.

theorem Katzir2007.φ''_has_conjp : Syntax.Tree.ContainsCat Syntax.Cat.ConjP φ''

φ'' does contain ConjP.

theorem Katzir2007.symmetric_not_structural : φ'' ∉ Alternatives.Structural.structuralAlternatives katzirLex φ

The symmetry problem, solved through the substrate. φ'' is NOT a structural alternative to φ: by category_preservation, every tree in A_str(φ) lacks ConjP (no source item introduces it), but φ'' contains ConjP. So the scalar implicature ¬"every" is licensed — no symmetric alternative blocks it. This consumes Alternatives.Structural.category_preservation rather than re-deriving the argument from containsCat.