Fox & Katzir 2011: On the Characterization of Alternatives

@cite{fox-katzir-2011}

Fox, D. & Katzir, R. (2011). On the characterization of alternatives. Natural Language Semantics, 19(1), 87–107.

Core Argument

The formal alternatives for Scalar Implicatures (SI) and Association with Focus (AF) are determined the same way — via @cite{katzir-2007}'s structural complexity, not via Horn scales (for SI) or Rooth's focus semantics (for AF).

Key Formalized Results

1. Worked example: some/all symmetry verified computationally
2. Bridge to Fox 2007: exh vacuous with symmetric alts, correct without
3. Bridge to Katzir 2007: structural F breaks symmetry
4. Unified F(S,C) (37): structural alternatives with contextual extension

The core symmetry infrastructure (isSymmetric, symmetric_complement, both_excluded_inconsistent, context_cannot_break_symmetry) lives in Symmetry.lean — those concepts predate this paper and are used across the exhaustification literature.

Connection to Linglib

This file bridges @cite{katzir-2007} (StructuralAlternatives.lean) and @cite{fox-2007} (Fox2007.lean):

• Katzir defines F(S) structurally → symmetry is broken in F
• Fox defines exh via innocent exclusion → symmetric alts are not in I-E (they appear in different maximal consistent exclusions)
• Fox & Katzir prove that contextual restriction C cannot break symmetry — only F can

The Canonical Symmetric Example

S = "John did some of the homework" S₁ = "John did all of the homework" S₂ = "John did some but not all of the homework"

⟦S₁⟧ ∪ ⟦S₂⟧ = ⟦S⟧ and ⟦S₁⟧ ∩ ⟦S₂⟧ = ∅ — the classic partition.

inductive Alternatives.FoxKatzir2011.HWWorld : Type

Three homework worlds: did all, did some (but not all), did none.

• all_ : HWWorld
• someNotAll : HWWorld
• none_ : HWWorld

instance Alternatives.FoxKatzir2011.instReprHWWorld : Repr HWWorld

Equations

• Alternatives.FoxKatzir2011.instReprHWWorld = { reprPrec := Alternatives.FoxKatzir2011.instReprHWWorld.repr }

def Alternatives.FoxKatzir2011.instReprHWWorld.repr : HWWorld → ℕ → Std.Format

Equations

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

instance Alternatives.FoxKatzir2011.instDecidableEqHWWorld : DecidableEq HWWorld

Equations

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

def Alternatives.FoxKatzir2011.instBEqHWWorld.beq : HWWorld → HWWorld → Bool

Equations

• Alternatives.FoxKatzir2011.instBEqHWWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Alternatives.FoxKatzir2011.instBEqHWWorld : BEq HWWorld

Equations

• Alternatives.FoxKatzir2011.instBEqHWWorld = { beq := Alternatives.FoxKatzir2011.instBEqHWWorld.beq }

theorem Alternatives.FoxKatzir2011.some_all_symmetric : Symmetry.isSymmetric Alternatives.FoxKatzir2011.hwDomain✝ Alternatives.FoxKatzir2011.didSome✝ Alternatives.FoxKatzir2011.didAll✝ Alternatives.FoxKatzir2011.didSomeNotAll✝ = true

"All" and "some but not all" are symmetric alternatives of "some": they partition "some"'s denotation.

theorem Alternatives.FoxKatzir2011.some_all_complement : (Alternatives.FoxKatzir2011.hwDomain✝.all fun (w : HWWorld) => (Alternatives.FoxKatzir2011.didSome✝ w && !Alternatives.FoxKatzir2011.didAll✝ w) == Alternatives.FoxKatzir2011.didSomeNotAll✝ w) = true

Symmetric complement verified: some ∧ ¬all = sbna on this domain.

theorem Alternatives.FoxKatzir2011.some_symmetric_neither_ie : have ie := Exhaustification.Fox2007.ieIndices Alternatives.FoxKatzir2011.hwDomain✝ Alternatives.FoxKatzir2011.didSome✝ Alternatives.FoxKatzir2011.someAlts✝; ie.contains 1 = false ∧ ie.contains 2 = false

With both symmetric alternatives, neither is innocently excludable: MCE₁ excludes all (index 1), MCE₂ excludes sbna (index 2).

theorem Alternatives.FoxKatzir2011.some_hornscale_all_ie : have hornAlts := [Alternatives.FoxKatzir2011.didSome✝, Alternatives.FoxKatzir2011.didAll✝]; have ie := Exhaustification.Fox2007.ieIndices Alternatives.FoxKatzir2011.hwDomain✝ Alternatives.FoxKatzir2011.didSome✝¹ hornAlts; ie.contains 1 = true

Without the symmetric alternative sbna (i.e., with Horn-scale alternatives {some, all}), "all" IS innocently excludable.

theorem Alternatives.FoxKatzir2011.symmetry_problem : (∀ (w : HWWorld), Exhaustification.Fox2007.exhB Alternatives.FoxKatzir2011.hwDomain✝ Alternatives.FoxKatzir2011.someAlts✝ Alternatives.FoxKatzir2011.didSome✝ w = Alternatives.FoxKatzir2011.didSome✝¹ w) ∧ ∀ (w : HWWorld), Exhaustification.Fox2007.exhB Alternatives.FoxKatzir2011.hwDomain✝¹ [Alternatives.FoxKatzir2011.didSome✝², Alternatives.FoxKatzir2011.didAll✝] Alternatives.FoxKatzir2011.didSome✝³ w = (Alternatives.FoxKatzir2011.didSome✝⁴ w && !Alternatives.FoxKatzir2011.didAll✝¹ w)

The symmetry problem in a nutshell: with the full set {some, all, sbna}, exh is vacuous (no SIs). With the restricted set {some, all}, exh correctly derives ¬all.

F Breaks Symmetry

While C cannot break symmetry, the formal alternatives F(S) can. @cite{katzir-2007}'s structural definition excludes "some but not all" from F("some") because it requires ConjP/NegP structure not derivable from the substitution source.

• all_is_alternative_to_some: "all" ∈ F("some")
• symmetry_problem_solved: "some but not all" ∉ F("some")

These are re-exported from StructuralAlternatives.lean.

theorem Alternatives.FoxKatzir2011.f_breaks_symmetry : StructuralAlternatives.allSentence ∈ StructuralAlternatives.structuralAlternatives StructuralAlternatives.exLexicon StructuralAlternatives.someSentence ∧ ¬StructuralAlternatives.someButNotAllSentence ∈ StructuralAlternatives.structuralAlternatives StructuralAlternatives.exLexicon StructuralAlternatives.someSentence

F contains the non-symmetric alternative (all) but excludes the symmetric partner (sbna). This is exactly what's needed for exh to derive the correct SI ¬all.

Unified Definition: F_SI = F_AF (claim 27)

Fox & Katzir argue that the formal alternatives for SI and AF should be defined identically — both via structural complexity (extending @cite{katzir-2007} to focused constituents).

The standard view (26):

• For SI: F(S) = Horn scales (stipulated)
• For AF: F(S) = Rooth's focus semantics (type-based)

Their proposal (37): both use structural alternatives restricted to focused constituents: F(S, C) = {S' : S' derived from S by replacing focused constituents with items ≲_C-comparable}

This preserves focus sensitivity (from Rooth) while allowing symmetry breaking (from Katzir).

Simplification: our formalAlternatives does not enforce the focus restriction (replacements may target any constituent, not only focused ones). The full definition 37 would require focus-marking on parse tree nodes. This simplification is conservative: the actual F(S,C) is a subset of our formalAlternatives.

def Alternatives.FoxKatzir2011.substitutionSourceFC {W : Type} (lexicon : List (StructuralAlternatives.ParseTree W)) (φ : StructuralAlternatives.ParseTree W) (salient : List (StructuralAlternatives.ParseTree W)) : List (StructuralAlternatives.ParseTree W)

The substitution source for F(S, C) (conditions 34–35): Lexicon ∪ sub-constituents of S ∪ salient constituents in C.

This extends @cite{katzir-2007}'s substitution source (def 41) with contextually salient material, enabling examples like Matsumoto's "warm"/"a little bit more than warm" (ex. 36).

Equations

• Alternatives.FoxKatzir2011.substitutionSourceFC lexicon φ salient = lexicon ++ φ.subtrees ++ salient

def Alternatives.FoxKatzir2011.formalAlternatives {W : Type} (lex : List (StructuralAlternatives.ParseTree W)) (φ : StructuralAlternatives.ParseTree W) (salient : List (StructuralAlternatives.ParseTree W)) : Set (StructuralAlternatives.ParseTree W)

Structural alternatives with contextual extension (definition 37). F(S, C) = {S' : S' ≲_C S}, where the substitution source includes salient constituents from context C.

When salient = [], this reduces to @cite{katzir-2007}'s original structuralAlternatives (modulo the focus restriction; see above).

Equations

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