Fox and Katzir (2011): On the Characterization of Alternatives

This file formalizes [FK11]'s argument that the alternatives of scalar implicature and of association with focus are one set, [Kat07]'s structural alternatives extended by the salient constituents of the context (formalAlternatives), and that symmetry among alternatives is broken only there: contextual restriction never keeps one of two alternatives that partition the assertion while pruning the other. The implicature and only operators SM and Exhaustification.exh negate the strictly stronger and the non-entailed alternatives; on symmetric alternatives both are contradictory (SM_eq_empty_of_isSymmetric), a universal operator above the assertion removes the symmetry and both inferences arise (mem_SM_nec), innocent exclusion negates neither symmetric alternative (exhIE_eq_self_of_isSymmetric), and a contextual set closed under negation and conjunction keeps both or neither (Alternatives.IsSymmetric.mem_of_mem). The paper's stronger condition, allowable restriction through exhaustive relevance, forbids pruning one of two compatible disjuncts as well (not_isAllowableRestriction_pair).

Implementation notes

Sentences are propositions Set W, alternative sets are Set (Set W), and the operators are intersections of complements, the paper's propositional rendering of only. The structural definition is stated without focus marking, so formalAlternatives contains the paper's set; its one new clause, salient constituents, is what brings a symmetric alternative into the set (mem_formalAlternatives_of_salient). Universal operators are ModalLogic.Box over an accessibility relation, covering the modal and the quantificational cases alike.

References

• [FK11]
• [Kat07]
• [Kro72]
• [Hor72]
• [Roo85]
• [Sau04]
• [Fox07]

Formal alternatives

def FoxKatzir2011.contextualSource {C V : Type} (lex : Finset (PhraseStructure.Tree C V)) (φ : PhraseStructure.Tree C V) (salient : Finset (PhraseStructure.Tree C V)) : Set (PhraseStructure.Tree C V)

The substitution source in a context consists of the lexicon, the sub-constituents of the sentence, and the salient constituents of the context.

Equations

• FoxKatzir2011.contextualSource lex φ salient = ↑lex ∪ {t : PhraseStructure.Tree C V | t ∈ RoseTree.subtrees φ} ∪ ↑salient

def FoxKatzir2011.formalAlternatives {C V : Type} (lex : Finset (PhraseStructure.Tree C V)) (φ : PhraseStructure.Tree C V) (salient : Finset (PhraseStructure.Tree C V)) : Set (PhraseStructure.Tree C V)

The formal alternatives in a context are whatever is at most as complex as the sentence over the contextual substitution source.

Equations

• FoxKatzir2011.formalAlternatives lex φ salient = {ψ : PhraseStructure.Tree C V | PhraseStructure.Tree.atMostAsComplex (FoxKatzir2011.contextualSource lex φ salient) ψ φ}

theorem FoxKatzir2011.formalAlternatives_empty {C V : Type} (lex : Finset (PhraseStructure.Tree C V)) (φ : PhraseStructure.Tree C V) : formalAlternatives lex φ ∅ = PhraseStructure.Tree.structuralAlternatives lex φ

Without salient constituents the alternatives are [Kat07]'s.

theorem FoxKatzir2011.mem_formalAlternatives_of_salient {C V : Type} (lex : Finset (PhraseStructure.Tree C V)) (φ : PhraseStructure.Tree C V) (salient : Finset (PhraseStructure.Tree C V)) {ψ : PhraseStructure.Tree C V} (hψ : ψ ∈ salient) (hcat : ψ.cat = φ.cat) : ψ ∈ formalAlternatives lex φ salient

A salient constituent of the sentence's category is a formal alternative.

theorem FoxKatzir2011.someButNotAll_mem_formalAlternatives : Katzir2007.someButNotAllSentence ∈ formalAlternatives Katzir2007.lexicon Katzir2007.someSentence {Katzir2007.someButNotAllSentence}

The symmetric some but not all is not a structural alternative of some, but it becomes a formal alternative once it is salient.

The operators

def FoxKatzir2011.nSI {W : Type u_1} (A : Set (Set W)) (S : Set W) : Set (Set W)

Scalar implicature negates the strictly stronger alternatives.

Equations

• FoxKatzir2011.nSI A S = {p : Set W | p ∈ A ∧ p ⊂ S}

def FoxKatzir2011.SI {W : Type u_1} (A : Set (Set W)) (S : Set W) : Set W

The scalar implicature is the conjunction of the negations of the strictly stronger alternatives.

Equations

• FoxKatzir2011.SI A S = ⋂ p ∈ FoxKatzir2011.nSI A S, pᶜ

def FoxKatzir2011.SM {W : Type u_1} (A : Set (Set W)) (S : Set W) : Set W

The strengthened meaning.

Equations

• FoxKatzir2011.SM A S = S ∩ FoxKatzir2011.SI A S

theorem FoxKatzir2011.mem_SM {W : Type u_1} {A : Set (Set W)} {S : Set W} {w : W} : w ∈ SM A S ↔ w ∈ S ∧ ∀ p ∈ A, p ⊂ S → w ∉ p

theorem FoxKatzir2011.exh_subset_SM {W : Type u_1} {A : Set (Set W)} {S : Set W} : Exhaustification.exh A S ⊆ SM A S

Only, the prejacent with the alternatives it does not entail denied (Exhaustification.exh), is at least as strong as the strengthened meaning.

Symmetry

theorem FoxKatzir2011.SM_eq_empty_of_isSymmetric {W : Type u_1} {A : Set (Set W)} {S S₁ S₂ : Set W} (h : Alternatives.IsSymmetric S S₁ S₂) (h₁ : S₁ ∈ A) (h₂ : S₂ ∈ A) (hne₁ : S₁.Nonempty) (hne₂ : S₂.Nonempty) : SM A S = ∅

With both symmetric alternatives in the set, the strengthened meaning is contradictory, since negating either asserts the other. This is the symmetry problem.

theorem FoxKatzir2011.exh_eq_empty_of_isSymmetric {W : Type u_1} {A : Set (Set W)} {S S₁ S₂ : Set W} (h : Alternatives.IsSymmetric S S₁ S₂) (h₁ : S₁ ∈ A) (h₂ : S₂ ∈ A) (hne₁ : S₁.Nonempty) (hne₂ : S₂.Nonempty) : Exhaustification.exh A S = ∅

Only on symmetric alternatives is contradictory as well.

theorem FoxKatzir2011.not_isInnocentlyExcludable_of_isSymmetric {W : Type u_1} {S S₁ S₂ : Set W} (h : Alternatives.IsSymmetric S S₁ S₂) (hne₁ : S₁.Nonempty) : ¬Exhaustification.IsInnocentlyExcludable {S, S₁, S₂} S S₁

Neither symmetric alternative is innocently excludable given the assertion.

theorem FoxKatzir2011.exhIE_eq_self_of_isSymmetric {W : Type u_1} {S S₁ S₂ : Set W} (h : Alternatives.IsSymmetric S S₁ S₂) (hne₁ : S₁.Nonempty) (hne₂ : S₂.Nonempty) : Exhaustification.exhIE {S, S₁, S₂} S = S

Innocent exclusion negates neither symmetric alternative, so exhaustification is vacuous.

theorem FoxKatzir2011.exhIE_pair_eq_sdiff {W : Type u_1} {S S₁ S₂ : Set W} (h : Alternatives.IsSymmetric S S₁ S₂) (hne₂ : S₂.Nonempty) : Exhaustification.exhIE {S, S₁} S = S₂

With the symmetric alternative absent, as under Horn scales, the other is innocently excludable and the implicature arises.

Universal operators

theorem FoxKatzir2011.not_isSymmetric_nec {W : Type u_1} {R : SetRel W W} {S S₁ S₂ : Set W} {x : W} (hx : x ∈ R.core S) (hx₁ : x ∉ R.core S₁) (hx₂ : x ∉ R.core S₂) : ¬Alternatives.IsSymmetric (R.core S) (R.core S₁) (R.core S₂)

Under a universal operator the alternatives are no longer symmetric whenever some world's accessible worlds fall on both sides.

theorem FoxKatzir2011.mem_SM_nec {W : Type u_1} {R : SetRel W W} {S S₁ S₂ : Set W} {x : W} (hx : x ∈ R.core S) (hx₁ : x ∉ R.core S₁) (hx₂ : x ∉ R.core S₂) : x ∈ SM {R.core S, R.core S₁, R.core S₂} (R.core S)

Both implicatures arise under the universal operator, since such a world lies in the strengthened meaning.

theorem FoxKatzir2011.mem_exh_nec {W : Type u_1} {R : SetRel W W} {S S₁ S₂ : Set W} {x : W} (hx : x ∈ R.core S) (hx₁ : x ∉ R.core S₁) (hx₂ : x ∉ R.core S₂) : x ∈ Exhaustification.exh {R.core S, R.core S₁, R.core S₂} (R.core S)

Both exclusions of only arise under the universal operator.

Contextual restriction

theorem FoxKatzir2011.mem_inter_of_isSymmetric {W : Type u_1} {S S₁ S₂ : Set W} {F : Set (Set W)} (h : Alternatives.IsSymmetric S S₁ S₂) (R : BooleanSubalgebra (Set W)) (hS : S ∈ R) (hF : S₂ ∈ F) (h₁ : S₁ ∈ ↑R ∩ F) : S₂ ∈ ↑R ∩ F

Context cannot break symmetry. With the context set the relevant propositions, closed under negation and conjunction, the actual alternatives keep both symmetric alternatives or neither.

def FoxKatzir2011.ExhaustivelyRelevant {W : Type u_1} (A : Set (Set W)) (p : Set W) : Prop

A sentence is exhaustively relevant given a restriction when its only-meaning lies in the Boolean closure of the restriction.

Equations

• FoxKatzir2011.ExhaustivelyRelevant A p = (Exhaustification.exh A p ∈ BooleanSubalgebra.closure A)

def FoxKatzir2011.IsAllowableRestriction {W : Type u_1} (F A : Set (Set W)) (S : Set W) : Prop

A restriction of the formal alternatives is allowable when it keeps the assertion and prunes nothing exhaustively relevant.

Equations

• FoxKatzir2011.IsAllowableRestriction F A S = (S ∈ A ∧ ∀ p ∈ F \ A, ¬FoxKatzir2011.ExhaustivelyRelevant A p)

theorem FoxKatzir2011.not_isAllowableRestriction_pair {W : Type u_1} {S S₁ S₂ : Set W} {F : Set (Set W)} (hS : S = S₁ ∪ S₂) (h₂₁ : ¬S₂ ⊆ S₁) (hF : S₂ ∈ F) (h₂ : S₂ ∉ {S, S₁}) : ¬IsAllowableRestriction F {S, S₁} S

Neither disjunct of a disjunction can be pruned in favour of the other, symmetric or not, since its only-meaning is the assertion without the kept disjunct.

The data

structure FoxKatzir2011.Row : Type

A sentence of the data records whether its formal alternatives contain a symmetric pair, whether a universal operator intervenes, whether the alternatives at issue are compatible, and whether the inference arises.

• symmetric : Bool
• universal : Bool
• compatible : Bool
• inference : Bool

def FoxKatzir2011.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FoxKatzir2011.instDecidableEqRow : DecidableEq Row

Equations

• FoxKatzir2011.instDecidableEqRow = FoxKatzir2011.instDecidableEqRow.decEq

def FoxKatzir2011.yesNoTable : List (String × Bool)

Equations

• FoxKatzir2011.yesNoTable = [("yes", true), ("no", false)]

def FoxKatzir2011.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def FoxKatzir2011.rows : List Row

Equations

• FoxKatzir2011.rows = List.filterMap FoxKatzir2011.Row.ofDatum FoxKatzir2011.Examples.all

theorem FoxKatzir2011.rows_predicted (r : Row) : r ∈ rows → (r.inference = true ↔ r.universal = true ∨ r.symmetric = false ∧ r.compatible = false)

The inference arises exactly when a universal operator removes the symmetry, or when the formal alternatives contain neither a symmetric pair nor compatible disjuncts.