Chow & Erlewine 2022: Restrictions on the Position of exh

@cite{chow-erlewine-2022}

Keng Ji Chow & Michael Yoshitaka Erlewine. Restrictions on the position of exh. Proceedings of SALT 32: 522--542.

Core Contributions

1. Additive particles (also, again) diagnose the structural position of exh: the presupposition of also is sensitive to whether exh is in its scope.

2. "As low as possible" generalization (9): for certain SI triggers (disjunction, bare numerals, unstressed some, conjunction, all), exh must adjoin to the lowest position where it is not vacuous.

3. Three-way lexical classification of SI triggers by [uexh] feature (§3.3, (30)), following @cite{chierchia-2013}'s feature-checking approach:

   • [uexh*] (strong): or, bare numerals, sm, and, all
   • [uexh] (weak): stressed SOME
   • [—] (none): scalar adjectives

4. Ignorance implicatures in embedded positions (§4): the covert □ that derives ignorance can occur below the clause edge, contra Meyer's "Matrix K" theory.

Formalization Strategy

Adjunction sites are derived from tree structure via OpTree.inScopeOf, not stipulated as an enum. The tree determines whether exh must be below a presupposition trigger (like also), and @cite{fox-2007}'s computable exhB verifies the resulting semantic predictions on finite models.

Related Files

• Exhaustification/InnocentExclusion.lean: exhB, innocent exclusion algorithm
• Exhaustification/FreeChoice.lean: feature-checking, scale reversal, FC
• Exhaustification/InnocentExclusion.lean: exhB, ieIndices (computable exhaustification)
• ScalarImplicatures/CompareRSAExh.lean: grammatical vs pragmatic SI

inductive Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree : Type

A tree for reasoning about operator scope and adjunction.

Operators (exh, also, not, □) are unary nodes; propositional content is at the leaves. Labels are theory-neutral strings — no syntactic framework is assumed. The tree structure alone determines scope relations.

• content (label : String) : OpTree
• op (label : String) (scope : OpTree) : OpTree
• merge (left right : OpTree) : OpTree

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprOpTree : Repr OpTree

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprOpTree = { reprPrec := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprOpTree.repr }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprOpTree.repr : OpTree → Nat → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree : DecidableEq OpTree

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree = Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree.decEq

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree.decEq (x✝ x✝¹ : OpTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree.decEq (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.content label) (left.merge right) = isFalse ⋯
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree.decEq (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.op label scope) (left.merge right) = isFalse ⋯
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree.decEq (left.merge right) (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.content label) = isFalse ⋯
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqOpTree.decEq (left.merge right) (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.op label scope) = isFalse ⋯

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqOpTree : BEq OpTree

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqOpTree = { beq := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqOpTree.beq }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqOpTree.beq : OpTree → OpTree → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqOpTree.beq x✝¹ x✝ = false

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.hasLabel : OpTree → String → Bool

Does the tree contain a node (content or operator) with the given label?

Equations

• (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.content l).hasLabel x✝ = (l == x✝)
• (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.op l child).hasLabel x✝ = (l == x✝ || child.hasLabel x✝)
• (left.merge right).hasLabel x✝ = (left.hasLabel x✝ || right.hasLabel x✝)

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.inScopeOf : OpTree → (opLabel target : String) → Bool

Is the target label in the scope of the given operator? The scope of an operator is its child subtree.

Equations

• (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.content label).inScopeOf x✝¹ x✝ = false
• (Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.OpTree.op l child).inScopeOf x✝¹ x✝ = (l == x✝¹ && child.hasLabel x✝ || child.inScopeOf x✝¹ x✝)
• (left.merge right).inScopeOf x✝¹ x✝ = (left.inScopeOf x✝¹ x✝ || right.inScopeOf x✝¹ x✝)

inductive Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature : Type

Syntactic feature governing exh placement (@cite{chow-erlewine-2022} §3.3).

SI triggers bear one of three features constraining where their associated exh may adjoin. This is orthogonal to SITrigger (which governs when SIs fire); ExhFeature governs where exh adjoins.

• strong [uexh*]: exh as low as possible (non-vacuously)
• weak [uexh]: exh within local finite clause or just above embedding verb
• none [—]: no constraint on exh position

• strong : ExhFeature
• weak : ExhFeature
• none : ExhFeature

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqExhFeature : DecidableEq ExhFeature

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqExhFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqExhFeature : BEq ExhFeature

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqExhFeature = { beq := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqExhFeature.beq }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqExhFeature.beq : ExhFeature → ExhFeature → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqExhFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprExhFeature : Repr ExhFeature

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprExhFeature = { reprPrec := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprExhFeature.repr }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprExhFeature.repr : ExhFeature → Nat → Std.Format

Equations

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

structure Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.SITriggerSpec : Type

An SI trigger paired with its exh-placement feature.

• trigger : String
• feature : ExhFeature

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprSITriggerSpec.repr : SITriggerSpec → Nat → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprSITriggerSpec : Repr SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprSITriggerSpec = { reprPrec := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprSITriggerSpec.repr }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.orTrigger : SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.orTrigger = { trigger := "or", feature := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature.strong }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.andTrigger : SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.andTrigger = { trigger := "and", feature := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature.strong }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.allTrigger : SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.allTrigger = { trigger := "all", feature := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature.strong }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.smTrigger : SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.smTrigger = { trigger := "sm", feature := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature.strong }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.bareNumeral : SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.bareNumeral = { trigger := "three", feature := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature.strong }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.stressedSOME : SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.stressedSOME = { trigger := "SOME", feature := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature.weak }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.scalarAdj : SITriggerSpec

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.scalarAdj = { trigger := "cold", feature := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ExhFeature.none }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.satisfiesUExhStar (tree : OpTree) (presupOp exhLabel triggerLabel : String) : Bool

Does a parse tree satisfy the [uexh*] constraint relative to a presupposition trigger (also/again)?

If the SI trigger is in the presupposition trigger's scope, then the exh checking [uexh*] must ALSO be in that scope — i.e., exh is below the presupposition trigger. If the SI trigger is outside the presupposition trigger's scope (e.g., after passivization), any exh position is fine.

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex3_tree : OpTree

Example (3): [Nina]_F also teaches Arabic or Basque. The SI trigger "or" is inside the scope of "also".

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex7_tree : OpTree

Example (7): Arabic or Basque is also taught by [Nina]_F. (passive) The SI trigger "or" has moved to subject position, outside "also"'s scope.

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex3_trigger_below_also : ex3_tree.inScopeOf "also" "or" = true

In (3), "or" IS in "also"'s scope: exh must go below also.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex7_trigger_above_also : ex7_tree.inScopeOf "also" "or" = false

In (7), "or" is NOT in "also"'s scope: exh goes above also.

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.exhDisj : Exhaustification.InnocentExclusion.PQWorld → Bool

Exhaustified disjunction: exh(A ∨ B) = exclusive or. Directly reuses @cite{fox-2007}'s disj_exh_eq_exor.

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.exhDisj_eq_exor (w : Exhaustification.InnocentExclusion.PQWorld) : exhDisj w = (Exhaustification.InnocentExclusion.pOrQ w && !Exhaustification.InnocentExclusion.pAndQ w)

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.alsoScopeContent (exhBelow : Bool) : Exhaustification.InnocentExclusion.PQWorld → Bool

Content of also's scope, determined by tree structure.

• exh below also: also's scope contains the exhaustified content
• exh above also: also's scope contains the bare (unexhaustified) content

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex3a_felicitous : alsoScopeContent true Exhaustification.InnocentExclusion.PQWorld.pOnly = true

(3a) Disjunctive antecedent (Mira teaches Arabic only) is felicitous: antecedent satisfies exclusive or.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex3b_infelicitous : alsoScopeContent true Exhaustification.InnocentExclusion.PQWorld.both = false

(3b) Conjunctive antecedent (Mira teaches both) is infelicitous: antecedent does NOT satisfy exclusive or.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex3a_qOnly : alsoScopeContent true Exhaustification.InnocentExclusion.PQWorld.qOnly = true

Symmetric: Basque-only antecedent is also felicitous.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex3b_wrongly_ok_if_exh_above : alsoScopeContent false Exhaustification.InnocentExclusion.PQWorld.both = true

If exh were above also in (3), (3b) would be wrongly predicted felicitous: the conjunctive antecedent satisfies bare A ∨ B.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex7_conjunctive_ok : alsoScopeContent false Exhaustification.InnocentExclusion.PQWorld.both = true

(7) Conjunctive antecedent is felicitous in the passive: exh is above also (the only non-vacuous position), so also's scope is unexhaustified A ∨ B. Conjunctive antecedent satisfies this.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex3_end_to_end : have exhBelow := ex3_tree.inScopeOf "also" "or"; alsoScopeContent exhBelow Exhaustification.InnocentExclusion.PQWorld.pOnly = true ∧ alsoScopeContent exhBelow Exhaustification.InnocentExclusion.PQWorld.both = false

The tree for (3) determines exh below also, which correctly predicts (3a) felicitous and (3b) infelicitous — both in one theorem.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex7_end_to_end : have exhBelow := ex7_tree.inScopeOf "also" "or"; alsoScopeContent exhBelow Exhaustification.InnocentExclusion.PQWorld.both = true

The tree for (7) determines exh above also, which correctly predicts conjunctive antecedent felicitous.

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notPandQ : Exhaustification.InnocentExclusion.PQWorld → Bool

Negated propositions for indirect SI computation (§2.3).

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notPandQ w = !Exhaustification.InnocentExclusion.pAndQ w

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notPorQ : Exhaustification.InnocentExclusion.PQWorld → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notPorQ w = !Exhaustification.InnocentExclusion.pOrQ w

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notP : Exhaustification.InnocentExclusion.PQWorld → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notP w = !Exhaustification.InnocentExclusion.pProp w

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notQ : Exhaustification.InnocentExclusion.PQWorld → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.notQ w = !Exhaustification.InnocentExclusion.qProp w

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.negConjAlts : List (Exhaustification.InnocentExclusion.PQWorld → Bool)

Alternatives for ¬(A ∧ B) under scale reversal: {¬(A∧B), ¬A, ¬B, ¬(A∨B)}. The scale ⟨∨, ∧⟩ reverses under negation to ⟨¬∧, ¬∨⟩, where ¬(A∨B) is strongest.

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.indirect_si_eq_exclusive_or (w : Exhaustification.InnocentExclusion.PQWorld) : Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain negConjAlts notPandQ w = (Exhaustification.InnocentExclusion.pOrQ w && !Exhaustification.InnocentExclusion.pAndQ w)

The indirect SI of negated conjunction equals exclusive or: exh(¬(A ∧ B)) = ¬(A ∧ B) ∧ (A ∨ B) = A ⊕ B.

The same result as the direct SI of disjunction — as expected from duality under negation.

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.conjAlts : List (Exhaustification.InnocentExclusion.PQWorld → Bool)

Sauerland alternatives for conjunction: {A∧B, A, B, A∨B}.

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.exh_conj_vacuous (w : Exhaustification.InnocentExclusion.PQWorld) : Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain conjAlts Exhaustification.InnocentExclusion.pAndQ w = Exhaustification.InnocentExclusion.pAndQ w

exh applied directly to conjunction is vacuous: A∧B entails every Sauerland alternative, so NW = {} and I-E = {}. This is why position ③ in (19) is ruled out — exh there makes no contribution.

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse18a_tree : OpTree

Parse (18a): exh [also [not [A∧B]]] exh above also — [uexh*] violated. The paper shows this parse wrongly predicts (16b) felicitous.

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse18b_tree : OpTree

Parse (18b): also [exh [not [A∧B]]] exh below also, above not — [uexh*] satisfied. This is the correct parse: exh exhaustifies ¬(A∧B) to get the indirect SI A⊕B, and also presupposes a salient individual satisfying A⊕B.

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse18c_tree : OpTree

Parse (18c): also [not [exh [A∧B]]] exh below not, directly on conjunction — vacuous by exh_conj_vacuous. satisfiesUExhStar passes but exh contributes nothing, so this parse is equivalent to having no SI.

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse18a_violates : satisfiesUExhStar parse18a_tree "also" "exh" "and" = false

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse18b_satisfies : satisfiesUExhStar parse18b_tree "also" "exh" "and" = true

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse18c_structural_ok_but_vacuous : satisfiesUExhStar parse18c_tree "also" "exh" "and" = true

Parse (18c) passes the structural check but is vacuous — the "as low as possible" generalization (9) requires the non-vacuity qualification to correctly rule out this position.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex16a_felicitous : Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain negConjAlts notPandQ Exhaustification.InnocentExclusion.PQWorld.pOnly = true

(16a) not>and antecedent (teaches exactly one) is felicitous: satisfies exh(¬(A ∧ B)) = exclusive or.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex16b_infelicitous : Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain negConjAlts notPandQ Exhaustification.InnocentExclusion.PQWorld.neither = false

(16b) not>or antecedent (teaches neither) is infelicitous: neither does NOT satisfy exclusive or.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.ex16_end_to_end : satisfiesUExhStar parse18b_tree "also" "exh" "and" = true ∧ Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain negConjAlts notPandQ Exhaustification.InnocentExclusion.PQWorld.pOnly = true ∧ Exhaustification.InnocentExclusion.exhB Exhaustification.InnocentExclusion.pqDomain negConjAlts notPandQ Exhaustification.InnocentExclusion.PQWorld.neither = false

End-to-end for indirect SI: parse (18b) places exh below also, yielding exh(¬(A∧B)) = A⊕B as also's scope content. Combined with the structural constraint and semantic predictions, this closes the argument chain: tree → [uexh*] satisfied → indirect SI → correct judgments.

inductive Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.TempWorld : Type

Temperature scale: freezing > cold > warm. Scalar adjectives bear no [uexh] feature (§3.1).

• freezing : TempWorld
• cold : TempWorld
• warm : TempWorld

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqTempWorld : DecidableEq TempWorld

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instDecidableEqTempWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqTempWorld.beq : TempWorld → TempWorld → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqTempWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqTempWorld : BEq TempWorld

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqTempWorld = { beq := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instBEqTempWorld.beq }

instance Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprTempWorld : Repr TempWorld

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprTempWorld = { reprPrec := Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprTempWorld.repr }

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.instReprTempWorld.repr : TempWorld → Nat → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isCold : TempWorld → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isCold Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.TempWorld.freezing = true
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isCold Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.TempWorld.cold = true
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isCold Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.TempWorld.warm = false

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isFreezing : TempWorld → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isFreezing Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.TempWorld.freezing = true
• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isFreezing x✝ = false

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.tempDomain : List TempWorld

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.coldAlts : List (TempWorld → Bool)

Equations

• Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.coldAlts = [Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isCold, Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.isFreezing]

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.exhCold : TempWorld → Bool

exh(cold) = cold ∧ ¬freezing: exactly cold, not freezing.

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.freezing_fails_exh_cold : exhCold TempWorld.freezing = false

If [uexh*] forced exh low (below also), a "freezing" antecedent would need to satisfy exh(cold) = cold ∧ ¬freezing. It doesn't.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.freezing_satisfies_cold : isCold TempWorld.freezing = true

But (24) IS felicitous with a "freezing" antecedent, showing scalar adjectives allow exh above also. The antecedent satisfies unexhaustified "cold" (since freezing entails cold).

Multiple exh instances + the covert necessity modal □ derive both the scalar implicature (A ∨ B → ¬(A ∧ B)) and the ignorance implicature (the speaker doesn't know which disjunct is true).

Three candidate parses for (32) [Nina]_F also teaches A or B with ignorance inferences. The inner exh (exh1) must check [uexh*]. The outer exh (exh2) applies above □ to derive ignorance.

Once [uexh*] is checked by exh₁, it imposes no conditions on the placement of additional exh instances — this explains why both (37a) and (37b) are grammatical despite differing in exh₂'s position.

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse37a : OpTree

Parse (37a): also [exh₂ [□ [exh₁ [A ∨ B]]]] exh₁ is below also — [uexh*] satisfied.

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse37b : OpTree

Parse (37b): exh₂ [□ [also [exh₁ [A ∨ B]]]] exh₁ is below also — [uexh*] satisfied. □ is in an embedded position (contra Meyer's Matrix K).

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse37c : OpTree

Parse (37c): exh₂ [□ [exh₁ [also [A ∨ B]]]] exh₁ is ABOVE also — [uexh*] violated.

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse37a_ok : satisfiesUExhStar parse37a "also" "exh1" "or" = true

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse37b_ok : satisfiesUExhStar parse37b "also" "exh1" "or" = true

Parse (37b) is grammatical AND places □ in an embedded position. This is the empirical argument against Meyer's Matrix K theory, which requires the ignorance-generating operator to adjoin only at the clause root. Parse (37b) is necessary to account for "split" antecedents (33c) — the grammar must generate it.

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.parse37c_bad : satisfiesUExhStar parse37c "also" "exh1" "or" = false

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.box_embedded_in_37b : parse37b.inScopeOf "exh2" "box" = true

In (37b), □ is dominated by exh₂ — an embedded, non-root position. This demonstrates that ignorance implicatures can be generated in embedded positions, contra the Matrix K theory.

ExhFeature determines which tree positions are available for exh.

The standard M/O/I positions correspond to specific nodes in a doubly-quantified sentence tree. The tree-based inScopeOf predicate subsumes an enumeration of positions by computing them from tree structure rather than stipulating them.

ExhFeature answers: "where MUST exh go, given the trigger's feature?"

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.treeExhI : OpTree

Doubly-quantified tree with exh at position I (below also): [Q₁ [also [exh [V Q₂]]]]

Equations

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

def Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.treeExhM : OpTree

Doubly-quantified tree with exh at position M (above everything): [exh [Q₁ [also [V Q₂]]]]

Equations

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

theorem Phenomena.ScalarImplicatures.Studies.ChowErlewine2022.strong_forces_inner : satisfiesUExhStar treeExhI "also" "exh" "Q2" = true ∧ satisfiesUExhStar treeExhM "also" "exh" "Q2" = false

For a [uexh*] trigger (e.g., "Q2") inside also's scope, the tree-based constraint forces exh below also — i.e., position I. Position M (above also) is ruled out. This recovers the M/O/I distinction as a special case of tree structure.