Katzir (2007): Structurally-Defined Alternatives

This file formalizes the worked examples of Katzir's paper, which replaces the Horn scales of neo-Gricean pragmatics by alternatives defined on parse trees: the alternatives of a sentence are the trees obtainable from it by deletion, contraction, and substitution of constituents by same-category items of the substitution source, the lexicon together with the sentence's own subtrees (its definitions (19) to (21) and (41), the substrate Alternatives). The conversational principle (21) then forbids asserting a sentence when a structural alternative is strictly stronger and weakly assertable, the substrate's Competition.Blocked over the weakly assertable structural alternatives.

The examples are the paper's Section 4 and 5 sentences over a small lexicon. For (25), all of the cake is an alternative of the same complexity as some of the cake (all_mem_alternatives), so a speaker obeying (21) implicates that it is not weakly assertable (primary_implicature_some), while the symmetric some but not all is no alternative, since no operation introduces the conjunction it needs (someButNotAll_not_mem_alternatives). For the disjunction (26), the conjunction and each disjunct are alternatives (and_mem_alternatives, leftDisjunct_mem_alternatives, rightDisjunct_mem_alternatives), which yields the primary inferences (28) without Sauerland's L and R connectives (primary_inferences_or). Deleting a modifier gives a strictly simpler alternative, (29) (justMan_mem_alternatives), and the subtree clause of the substitution source (41) makes a little bit more than warm substitutable for warm in (40), so that the more complex sentence is an alternative of the simpler (moreThanWarmYesterday_mem_alternatives).

Implementation notes

The truth conditions the paper takes for granted enter as meaning functions on three-way and four-way world types; trees the paper does not interpret denote the contradiction, which never witnesses the principle. Determiners inside the noun phrases are omitted from the trees, and the symmetric alternative places the conjunction of quantifiers at the determiner.

References

• [Kat07]
• [Sau04], [Kro72]

inductive Katzir2007.Word : Type

The vocabulary of the paper's examples.

• john : Word
• ate : Word
• some_ : Word
• all_ : Word
• cake : Word
• apple : Word
• pear : Word
• or_ : Word
• and_ : Word
• but_ : Word
• not_ : Word
• tall : Word
• man : Word
• it : Word
• was : Word
• is : Word
• warm : Word
• yesterday : Word
• today : Word
• aLittleBitMoreThan : Word

@[instance_reducible]

instance Katzir2007.instDecidableEqWord : DecidableEq Word

Equations

• Katzir2007.instDecidableEqWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Katzir2007.instReprWord.repr : Word → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Katzir2007.instReprWord.repr Katzir2007.Word.john prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.john")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.ate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.ate")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.some_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.some_")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.all_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.all_")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.cake prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.cake")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.apple prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.apple")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.pear prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.pear")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.or_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.or_")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.and_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.and_")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.but_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.but_")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.not_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.not_")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.tall prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.tall")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.man prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.man")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.it prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.it")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.was prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.was")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.is prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.is")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.warm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.warm")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.yesterday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.yesterday")).group prec✝
• Katzir2007.instReprWord.repr Katzir2007.Word.today prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Word.today")).group prec✝

@[instance_reducible]

instance Katzir2007.instReprWord : Repr Word

Equations

• Katzir2007.instReprWord = { reprPrec := Katzir2007.instReprWord.repr }

def Katzir2007.lexicon : Finset (PhraseStructure.Tree PhraseStructure.Cat Word)

The lexicon lists the terminal items available for substitution.

Equations

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

Some, all, some but not all (Section 4.1)

def Katzir2007.someSentence : PhraseStructure.Tree PhraseStructure.Cat Word

(25a) John ate some of the cake.

Equations

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

def Katzir2007.allSentence : PhraseStructure.Tree PhraseStructure.Cat Word

(25b) John ate all of the cake.

Equations

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

def Katzir2007.someButNotAllSentence : PhraseStructure.Tree PhraseStructure.Cat Word

(25c) John ate some but not all of the cake, the symmetric alternative.

Equations

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

theorem Katzir2007.leafSubst_some_all : PhraseStructure.Tree.leafSubst Word.some_ Word.all_ PhraseStructure.Cat.Det someSentence = allSentence

(25b) is (25a) with all substituted for some.

theorem Katzir2007.all_mem_alternatives : allSentence ∈ PhraseStructure.Tree.structuralAlternatives lexicon someSentence

(25b) is a structural alternative of (25a), since the determiners are same-category items of the lexicon.

theorem Katzir2007.some_all_equalComplexity : PhraseStructure.Tree.equalComplexity (PhraseStructure.Tree.substitutionSource lexicon someSentence) someSentence allSentence

The two are of equal complexity, each one substitution from the other.

theorem Katzir2007.source_lacks_conjP (t : PhraseStructure.Tree PhraseStructure.Cat Word) : t ∈ PhraseStructure.Tree.substitutionSource lexicon someSentence → ∀ s ∈ RoseTree.subtrees t, ¬(s.value.IsPhrase ∧ PhraseStructure.Tree.cat s = PhraseStructure.Cat.Conj)

No item of the substitution source of (25a) contains a conjunction phrase.

theorem Katzir2007.someButNotAll_not_mem_alternatives : someButNotAllSentence ∉ PhraseStructure.Tree.structuralAlternatives lexicon someSentence

The symmetric alternative is no structural alternative, since the operations never introduce the conjunction phrase it needs, so the symmetry problem does not arise.

inductive Katzir2007.Cake : Type

How much of the cake John ate.

• none : Cake
• part : Cake
• whole : Cake

@[instance_reducible]

instance Katzir2007.instDecidableEqCake : DecidableEq Cake

Equations

• Katzir2007.instDecidableEqCake x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Katzir2007.instReprCake.repr : Cake → ℕ → Std.Format

Equations

• Katzir2007.instReprCake.repr Katzir2007.Cake.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Cake.none")).group prec✝
• Katzir2007.instReprCake.repr Katzir2007.Cake.part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Cake.part")).group prec✝
• Katzir2007.instReprCake.repr Katzir2007.Cake.whole prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Katzir2007.Cake.whole")).group prec✝

@[instance_reducible]

instance Katzir2007.instReprCake : Repr Cake

Equations

• Katzir2007.instReprCake = { reprPrec := Katzir2007.instReprCake.repr }

def Katzir2007.cakeMeaning (t : PhraseStructure.Tree PhraseStructure.Cat Word) : Set Cake

Under the truth conditions the paper assumes for (25), some holds of any eating, all of the whole, and some but not all of a part; the other trees are not interpreted.

Equations

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

def Katzir2007.assertableAlts (wa : PhraseStructure.Tree PhraseStructure.Cat Word → Prop) (t : PhraseStructure.Tree PhraseStructure.Cat Word) : Set (PhraseStructure.Tree PhraseStructure.Cat Word)

The alternatives of (21) are the structural alternatives that are weakly assertable.

Equations

• Katzir2007.assertableAlts wa t = {t' : PhraseStructure.Tree PhraseStructure.Cat Katzir2007.Word | t' ∈ PhraseStructure.Tree.structuralAlternatives Katzir2007.lexicon t ∧ wa t'}

theorem Katzir2007.blocked_of_weaklyAssertable_all {wa : PhraseStructure.Tree PhraseStructure.Cat Word → Prop} (h : wa allSentence) : Competition.Blocked (assertableAlts wa) cakeMeaning someSentence

If all is weakly assertable, asserting some violates the conversational principle.

theorem Katzir2007.primary_implicature_some {wa : PhraseStructure.Tree PhraseStructure.Cat Word → Prop} (h : ¬Competition.Blocked (assertableAlts wa) cakeMeaning someSentence) : ¬wa allSentence

In the primary implicature of (25a), a speaker who obeys the principle has all not weakly assertable; the symmetric alternative, being no alternative, licenses nothing.

Disjunction (Section 4.2)

def Katzir2007.orSentence : PhraseStructure.Tree PhraseStructure.Cat Word

(26a) John ate the apple or the pear.

Equations

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

def Katzir2007.andSentence : PhraseStructure.Tree PhraseStructure.Cat Word

(26b) John ate the apple and the pear.

Equations

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

def Katzir2007.leftDisjunct : PhraseStructure.Tree PhraseStructure.Cat Word

(27a) John ate the apple, the left disjunct.

Equations

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

def Katzir2007.rightDisjunct : PhraseStructure.Tree PhraseStructure.Cat Word

(27b) John ate the pear, the right disjunct.

Equations

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

theorem Katzir2007.leafSubst_or_and : PhraseStructure.Tree.leafSubst Word.or_ Word.and_ PhraseStructure.Cat.Conj orSentence = andSentence

theorem Katzir2007.and_mem_alternatives : andSentence ∈ PhraseStructure.Tree.structuralAlternatives lexicon orSentence

The conjunction is an alternative of the disjunction by substitution.

theorem Katzir2007.leftDisjunct_mem_alternatives : leftDisjunct ∈ PhraseStructure.Tree.structuralAlternatives lexicon orSentence

The left disjunct is an alternative of the disjunction, by deleting the right disjunct and the connective and then contracting, the effect of the L connective of [Sau04].

theorem Katzir2007.rightDisjunct_mem_alternatives : rightDisjunct ∈ PhraseStructure.Tree.structuralAlternatives lexicon orSentence

The right disjunct likewise, the effect of R.

@[reducible, inline]

abbrev Katzir2007.Fruits : Type

Which of the two fruits John ate.

Equations

• Katzir2007.Fruits = (Bool × Bool)

def Katzir2007.fruitMeaning (t : PhraseStructure.Tree PhraseStructure.Cat Word) : Set Fruits

These are the truth conditions of (26) and (27), for the disjunction, the conjunction, and each disjunct.

Equations

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

theorem Katzir2007.primary_inferences_or {wa : PhraseStructure.Tree PhraseStructure.Cat Word → Prop} (h : ¬Competition.Blocked (assertableAlts wa) fruitMeaning orSentence) : ¬wa andSentence ∧ ¬wa leftDisjunct ∧ ¬wa rightDisjunct

In the primary inferences (28), a speaker of the disjunction who obeys the principle has the conjunction and each disjunct not weakly assertable.

Strictly simpler alternatives (Section 4.3)

def Katzir2007.tallMan : PhraseStructure.Tree PhraseStructure.Cat Word

(29a) a tall man, without its determiner.

Equations

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

def Katzir2007.justMan : PhraseStructure.Tree PhraseStructure.Cat Word

(29b) a man.

Equations

• Katzir2007.justMan = PhraseStructure.Tree.node PhraseStructure.Cat.N [PhraseStructure.Tree.terminal PhraseStructure.Cat.N Katzir2007.Word.man]

theorem Katzir2007.justMan_mem_alternatives : justMan ∈ PhraseStructure.Tree.structuralAlternatives lexicon tallMan

Deleting the modifier gives an alternative, strictly simpler; in an upward-entailing context it is entailed and yields no inference, under a downward-entailing operator it does, (30) to (32).

The subtrees of the sentence as substitution source (Section 5)

def Katzir2007.moreThanWarm : PhraseStructure.Tree PhraseStructure.Cat Word

a little bit more than warm, an adjective phrase.

Equations

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

def Katzir2007.moreThanWarmToday : PhraseStructure.Tree PhraseStructure.Cat Word

it is a little bit more than warm today.

Equations

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

def Katzir2007.warmYesterday : PhraseStructure.Tree PhraseStructure.Cat Word

(40a) It was warm yesterday, and it is a little bit more than warm today.

Equations

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

def Katzir2007.moreThanWarmYesterday : PhraseStructure.Tree PhraseStructure.Cat Word

(40b) It was a little bit more than warm yesterday, and it is a little bit more than warm today.

Equations

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

theorem Katzir2007.moreThanWarmYesterday_mem_alternatives : moreThanWarmYesterday ∈ PhraseStructure.Tree.structuralAlternatives lexicon warmYesterday

Matsumoto's (40b) is an alternative of (40a) although more complex, since the adjective phrase it needs is a subtree of (40a), hence in the substitution source (41).