Symmetric Alternatives

The symmetry problem is the central challenge for any theory of scalar implicatures based on alternatives. The problem: for any stronger alternative A of an assertion S, the sentence S ∧ ¬A is also stronger than S and yields the opposite implicature. A theory of alternatives must explain why A enters the alternative set but S ∧ ¬A does not.

The problem emerged in the early 1970s: @cite{horn-1972} established the Gricean derivation of scalar implicatures, and @cite{kroch-1972} discussed the same reasoning for quantifiers, creating the conditions for recognizing that symmetric alternatives pose a fundamental obstacle. Every subsequent theory of alternatives is shaped by this problem:

• @cite{katzir-2007} addresses it via structural complexity: S ∧ ¬A is structurally more complex than S, so it is excluded from F(S)
• @cite{fox-2007}'s innocent exclusion correctly handles symmetric alternatives (they land in different MCEs, so neither is in I-E), but the problem of which alternatives enter the set remains
• @cite{fox-katzir-2011} show that contextual restriction cannot break symmetry — only the formal alternative set F can
• @cite{breheny-et-al-2018} show that none of these fully solve the problem (indirect SIs, gradable adjectives, too many/few lexical alternatives remain problematic)
• @cite{fox-spector-2018}'s economy condition constrains where exh can be inserted (not vacuous, not weakening), which interacts with symmetry: symmetric alternatives make exh vacuous (see symmetric_exhB_vacuous), so economy would block uninformative exhaustification rather than producing wrong results
• RSA (@cite{frank-goodman-2012}, @cite{franke-2011}) dissolves rather than solves the symmetry problem: the utterance space is specified directly (typically simple lexical items), and utterance cost penalizes complex expressions like "some but not all." Even without cost, Bayesian inference at finite rationality α handles symmetric alternatives gracefully — the symmetry problem only re-emerges in the categorical limit α → ∞ where RSA collapses to exh (see Comparisons.RSANeoGricean)

This file defines the core concepts — isSymmetric, complement equivalence, and inconsistency of joint exclusion — as theory-neutral infrastructure that any approach can import. The definition follows @cite{fox-katzir-2011} definition 12, but the concept is not specific to that paper.

Key Definitions and Theorems

• isSymmetric: S₁, S₂ partition S's denotation (def 12)
• symmetric_complement: S ∧ ¬S₁ = S₂ when symmetric
• both_excluded_inconsistent: excluding both contradicts S
• symmetric_not_ie: symmetric alternatives are never in I-E
• exhB_vacuous_of_ie_empty: exhB = identity when I-E is empty
• symmetric_exhB_vacuous: exhB is vacuous when only symmetric alts
• RelevanceClosure: closure under ¬ and ∧ (condition 50)
• context_cannot_break_symmetry: C preserves symmetry (constraint 28)

def Alternatives.Symmetry.isSymmetric {W : Type} (domain : List W) (s s₁ s₂ : W → Bool) : Bool

Two propositions are symmetric alternatives of S if they partition S's denotation: their union equals S and they are mutually exclusive.

Formalized from @cite{fox-katzir-2011} definition 12. The underlying problem was recognized in the early 1970s (@cite{horn-1972}, @cite{kroch-1972}).

Note: this is stricter than mere non-innocent-excludability. Disjuncts p, q of p∨q are often mutually compatible (p ∩ q ≠ ∅) and hence NOT symmetric, though they still resist innocent exclusion for related reasons (@cite{fox-katzir-2011} fn. 18).

Equations

• Alternatives.Symmetry.isSymmetric domain s s₁ s₂ = ((domain.all fun (w : W) => (s₁ w || s₂ w) == s w) && domain.all fun (w : W) => !(s₁ w && s₂ w))

theorem Alternatives.Symmetry.symmetric_complement {W : Type} (domain : List W) (s s₁ s₂ : W → Bool) (hsym : isSymmetric domain s s₁ s₂ = true) : (domain.all fun (w : W) => (s w && !s₁ w) == s₂ w) = true

When S₁, S₂ are symmetric alternatives of S, S ∧ ¬S₁ is extensionally equal to S₂. This is the key fact underlying the relevance argument: showing S ∧ ¬S₁ is relevant suffices to show S₂ is relevant.

theorem Alternatives.Symmetry.both_excluded_inconsistent {W : Type} (domain : List W) (s s₁ s₂ : W → Bool) (alts : List (W → Bool)) (i₁ i₂ : Nat) (excl : List Nat) (hsym : isSymmetric domain s s₁ s₂ = true) (hi₁ : alts[i₁]? = some s₁) (hi₂ : alts[i₂]? = some s₂) (hm₁ : i₁ ∈ excl) (hm₂ : i₂ ∈ excl) : Exhaustification.Fox2007.exclusionConsistent domain s alts excl = false

Excluding both symmetric alternatives is inconsistent with S. If S₁, S₂ partition S, then S ∧ ¬S₁ ∧ ¬S₂ is unsatisfiable: every S-world is an S₁-world or S₂-world (by the union condition) but the exclusion requires it to be neither.

theorem Alternatives.Symmetry.symmetric_not_ie {W : Type} (domain : List W) (s s₁ s₂ : W → Bool) (alts : List (W → Bool)) (i₁ i₂ : Nat) (_h_ne : i₁ ≠ i₂) (hsym : isSymmetric domain s s₁ s₂ = true) (hi₁ : alts[i₁]? = some s₁) (hi₂ : alts[i₂]? = some s₂) (h_sat₁ : domain.any s₁ = true) (h_sat₂ : domain.any s₂ = true) : have ie := Exhaustification.Fox2007.ieIndices domain s alts; ie.contains i₁ = false ∧ ie.contains i₂ = false

General principle: symmetric alternatives are never innocently excludable. If S₁, S₂ partition S's denotation and both appear in the alternative set, then neither is in I-E.

The argument: since ⟦S₁⟧ ∩ ⟦S₂⟧ = ∅ and ⟦S₁⟧ ∪ ⟦S₂⟧ = ⟦S⟧, excluding both is unsatisfiable (proved by both_excluded_inconsistent). So each MCE contains at most one of {S₁, S₂}. Since each can be consistently excluded individually (witnessed by an S₂-world or S₁-world respectively), each appears in some MCE but not all. Hence neither is in I-E = ⋂MCEs.

The proof establishes that {i₂} is a consistent exclusion set (using sym_witness), extends it to a maximal consistent exclusion (via exists_maximal_extension), and observes that this MCE cannot contain i₁ (by both_excluded_inconsistent). The symmetric argument shows an MCE containing i₁ but not i₂.

theorem Alternatives.Symmetry.exhB_vacuous_of_ie_empty {W : Type} (domain : List W) (alts : List (W → Bool)) (p : W → Bool) (h : Exhaustification.Fox2007.ieIndices domain p alts = []) (w : W) : Exhaustification.Fox2007.exhB domain alts p w = p w

When ieIndices returns the empty list, exhB reduces to the prejacent — no alternatives are excluded.

theorem Alternatives.Symmetry.symmetric_exhB_vacuous {W : Type} (domain : List W) (s s₁ s₂ : W → Bool) (alts : List (W → Bool)) (i₁ i₂ : Nat) (h_ne : i₁ ≠ i₂) (hsym : isSymmetric domain s s₁ s₂ = true) (hi₁ : alts[i₁]? = some s₁) (hi₂ : alts[i₂]? = some s₂) (h_sat₁ : domain.any s₁ = true) (h_sat₂ : domain.any s₂ = true) (h_only : ∀ (j : Nat), j ∈ Exhaustification.Fox2007.nonWeakerIndices domain s alts → j = i₁ ∨ j = i₂) (w : W) : Exhaustification.Fox2007.exhB domain alts s w = s w

Vacuity corollary: when the symmetric pair are the only non-weaker alternatives, exhB is the identity — exhaustification is vacuous.

This is the general principle underlying the concrete FoxKatzir2011.symmetry_problem: with both symmetric alternatives present and no other non-weaker alternatives, I-E is empty, so exh does nothing.

Context Cannot Break Symmetry

The set of contextually relevant sentences C must satisfy closure conditions (@cite{fox-katzir-2011} condition 50):

(50a) If S is relevant, so is ¬S. (50b) If S₁, S₂ are relevant, so is S₁ ∧ S₂.

From these conditions, constraint (28) follows: symmetry cannot be broken in C. If S₁ is relevant and S is relevant, then S ∧ ¬S₁ is relevant (by 50a + 50b). But when S₁, S₂ are symmetric, S ∧ ¬S₁ ≡ S₂ (by symmetric_complement). So S₂ is also relevant, and contextual restriction cannot selectively eliminate one symmetric alternative while keeping the other.

structure Alternatives.Symmetry.RelevanceClosure (W : Type) : Type

Closure conditions on relevance (condition 50).

• relevant : (W → Bool) → Bool
• negClosed (p : W → Bool) : self.relevant p = true → (self.relevant fun (w : W) => !p w) = true
• conjClosed (p q : W → Bool) : self.relevant p = true → self.relevant q = true → (self.relevant fun (w : W) => p w && q w) = true

theorem Alternatives.Symmetry.context_cannot_break_symmetry {W : Type} (rc : RelevanceClosure W) (s s₁ : W → Bool) (hs : rc.relevant s = true) (h₁ : rc.relevant s₁ = true) : (rc.relevant fun (w : W) => s w && !s₁ w) = true

C cannot break symmetry (constraint 28): if S₁ is relevant and S is relevant, then the symmetric partner S ∧ ¬S₁ (which equals S₂ when S₁, S₂ are symmetric by symmetric_complement) is also relevant.

Therefore any contextual restriction that keeps S₁ must also keep S₂. Symmetry breaking must happen in F, not in C.