Chow and Erlewine (2022): Restrictions on the position of exh

Chow and Erlewine argue that the covert exhaustification operator exh of Fox's grammatical theory of scalar implicature is syntactically constrained: for most SI triggers exh must adjoin at the lowest position where it is not vacuous (their generalization (9)), a requirement they encode as a feature [uexh*] on the trigger in the style of Chierchia. The diagnostic is the additive presupposition of also: whether exh sits below or above also determines whether the additive presupposition is exhaustified, which antecedent contexts then satisfy or fail.

Parses are operator spines interpreted compositionally into trivalent propositions. exh is Spector and Sudo's strong-negation EXH² (Exhaustification.Trivalent.exh2, the operator the paper adopts in its footnote 4), so the presupposition of a negated alternative projects: the parse exh > also presupposes a salient conjunctive antecedent, which is what blocks a disjunctive one. Adjunction sites are computed from a base clause, and generalization (9) is BaseClause.lowestNonVacuousSite: the deepest trigger-commanding site where inserting exh changes the interpretation. Section 4's ignorance implicatures are derived over belief states with exh above the covert doxastic necessity operator; the four antecedent types of Marty and Romoli separate the two grammatical parses, and the parse needed for the plain disjunctive antecedent places the necessity operator below surface-scope also, embedded, contra Meyer's Matrix K theory.

Implementation notes

The trigger moved to subject position, (7), reconstructs semantically, with movement reflected only in the site calculus; the embedding verb of (28) is opaque to interpretation and matters only to the site calculus; and the presupposition of parse (35) is taken from the paper's display, since they defer its derivation to Marty and Romoli. The again data of their section 2.4 replicate the also pattern and are not modeled separately.

References

• [CE22]
• [SS17]
• [MR21a]
• [Fox07]
• [Chi13]
• [Mey13]

Individuals and worlds

The running examples predicate teaching Arabic and teaching Basque of a focused individual (Nina) and a salient alternative (Mira). A world fixes both teaching profiles.

structure ChowErlewine2022.Taught : Type

Which of the two languages an individual teaches.

• arabic : Bool
• basque : Bool

def ChowErlewine2022.instDecidableEqTaught.decEq (x✝ x✝¹ : Taught) : Decidable (x✝ = x✝¹)

Equations

• ChowErlewine2022.instDecidableEqTaught.decEq { arabic := a, basque := a_1 } { arabic := b, basque := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqTaught : DecidableEq Taught

Equations

• ChowErlewine2022.instDecidableEqTaught = ChowErlewine2022.instDecidableEqTaught.decEq

@[instance_reducible]

instance ChowErlewine2022.instFintypeTaught : Fintype Taught

Equations

• ChowErlewine2022.instFintypeTaught = Fintype.ofEquiv ((_ : Bool) × Bool) ChowErlewine2022.Taught.proxyTypeEquiv

@[instance_reducible]

instance ChowErlewine2022.instReprTaught : Repr Taught

Equations

• ChowErlewine2022.instReprTaught = { reprPrec := ChowErlewine2022.instReprTaught.repr }

def ChowErlewine2022.instReprTaught.repr : Taught → ℕ → Std.Format

Equations

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

def ChowErlewine2022.Taught.either (t : Taught) : Bool

Teaches Arabic or Basque.

Equations

• t.either = (t.arabic || t.basque)

def ChowErlewine2022.Taught.both (t : Taught) : Bool

Teaches Arabic and Basque.

Equations

• t.both = (t.arabic && t.basque)

def ChowErlewine2022.Taught.exactlyOne (t : Taught) : Bool

Teaches exactly one of the two languages.

Equations

• t.exactlyOne = (t.either && !t.both)

def ChowErlewine2022.Taught.neither (t : Taught) : Bool

Teaches neither language.

Equations

• t.neither = !t.either

def ChowErlewine2022.Taught.onlyArabic (t : Taught) : Bool

Teaches Arabic and not Basque.

Equations

• t.onlyArabic = (t.arabic && !t.basque)

def ChowErlewine2022.Taught.onlyBasque (t : Taught) : Bool

Teaches Basque and not Arabic.

Equations

• t.onlyBasque = (!t.arabic && t.basque)

inductive ChowErlewine2022.Individual : Type

The focused individual of the prejacent and the salient antecedent individual.

• nina : Individual
• mira : Individual

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqIndividual : DecidableEq Individual

Equations

• ChowErlewine2022.instDecidableEqIndividual x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChowErlewine2022.instFintypeIndividual : Fintype Individual

Equations

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

def ChowErlewine2022.instReprIndividual.repr : Individual → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChowErlewine2022.instReprIndividual : Repr Individual

Equations

• ChowErlewine2022.instReprIndividual = { reprPrec := ChowErlewine2022.instReprIndividual.repr }

def ChowErlewine2022.Individual.other : Individual → Individual

The salient focus alternative.

Equations

• ChowErlewine2022.Individual.nina.other = ChowErlewine2022.Individual.mira
• ChowErlewine2022.Individual.mira.other = ChowErlewine2022.Individual.nina

structure ChowErlewine2022.TeachWorld : Type

A world records both individuals' teaching profiles.

• nina : Taught
• mira : Taught

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqTeachWorld : DecidableEq TeachWorld

Equations

• ChowErlewine2022.instDecidableEqTeachWorld = ChowErlewine2022.instDecidableEqTeachWorld.decEq

def ChowErlewine2022.instDecidableEqTeachWorld.decEq (x✝ x✝¹ : TeachWorld) : Decidable (x✝ = x✝¹)

Equations

• ChowErlewine2022.instDecidableEqTeachWorld.decEq { nina := a, mira := a_1 } { nina := b, mira := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance ChowErlewine2022.instFintypeTeachWorld : Fintype TeachWorld

Equations

• ChowErlewine2022.instFintypeTeachWorld = Fintype.ofEquiv ((_ : ChowErlewine2022.Taught) × ChowErlewine2022.Taught) ChowErlewine2022.TeachWorld.proxyTypeEquiv

@[instance_reducible]

instance ChowErlewine2022.instReprTeachWorld : Repr TeachWorld

Equations

• ChowErlewine2022.instReprTeachWorld = { reprPrec := ChowErlewine2022.instReprTeachWorld.repr }

def ChowErlewine2022.instReprTeachWorld.repr : TeachWorld → ℕ → Std.Format

Equations

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

def ChowErlewine2022.TeachWorld.taught (w : TeachWorld) : Individual → Taught

The profile of an individual at a world.

Equations

• w.taught ChowErlewine2022.Individual.nina = w.nina
• w.taught ChowErlewine2022.Individual.mira = w.mira

Parses and their trivalent interpretation

inductive ChowErlewine2022.Parse (F W : Type) : Type

An LF parse is an operator spine over a scalar leaf. The leaf carries the denotation of the scalar item and of its Horn-scale mate, both predicated of a focus individual F.

• lex {F W : Type} (den alt : F → W → SignType) : Parse F W
• exh {F W : Type} (t : Parse F W) : Parse F W
• not {F W : Type} (t : Parse F W) : Parse F W
• also {F W : Type} (t : Parse F W) : Parse F W

def ChowErlewine2022.Parse.interpWithMate {F W : Type} [Fintype W] [DecidableEq W] (sal : F → F) : Parse F W → F → (W → SignType) × (W → SignType)

A parse and its scale-mate are interpreted in one recursion. exh is EXH² ([SS17], the paper's footnote 4) with the scale-mate as its alternative, negation is strong Kleene (a presupposition hole), and also presupposes that its scope holds of the salient focus alternative sal x ([CE22] section 2, following Kripke and Heim).

Equations

• One or more equations did not get rendered due to their size.
• ChowErlewine2022.Parse.interpWithMate sal (ChowErlewine2022.Parse.lex den alt) x✝ = (den x✝, alt x✝)
• ChowErlewine2022.Parse.interpWithMate sal t.not x✝ = match ChowErlewine2022.Parse.interpWithMate sal t x✝ with | (p, q) => (fun (w : W) => -p w, fun (w : W) => -q w)

def ChowErlewine2022.Parse.interp {F W : Type} [Fintype W] [DecidableEq W] (sal : F → F) (t : Parse F W) (x : F) : W → SignType

The trivalent interpretation of a parse, about the focus individual x.

Equations

• ChowErlewine2022.Parse.interp sal t x = (ChowErlewine2022.Parse.interpWithMate sal t x).1

def ChowErlewine2022.Parse.FelicitousIn {F W : Type} [Fintype W] [DecidableEq W] (sal : F → F) (t : Parse F W) (x : F) (ctx : Finset W) : Prop

The parse's presuppositions are met throughout a context when no context world leaves it undefined. Antecedent contexts are the worlds compatible with the antecedent sentence, including that sentence's own implicatures.

Equations

• ChowErlewine2022.Parse.FelicitousIn sal t x ctx = ∀ w ∈ ctx, ChowErlewine2022.Parse.interp sal t x w ≠ 0

@[instance_reducible]

instance ChowErlewine2022.instDecidableFelicitousIn {F W : Type} [Fintype W] [DecidableEq W] (sal : F → F) (t : Parse F W) (x : F) (ctx : Finset W) : Decidable (Parse.FelicitousIn sal t x ctx)

Equations

• ChowErlewine2022.instDecidableFelicitousIn sal t x ctx = { decide := decide (∀ a ∈ Finset.univ, (fun (w : W) => w ∈ ctx → ChowErlewine2022.Parse.interp sal t x w ≠ 0) a), reflects_decide := ⋯ }

Adjunction sites and generalization (9)

inductive ChowErlewine2022.ClauseOp : Type

An overt operator of the base clause. The embedding verb is opaque to interpretation (attitude semantics is out of scope) and matters only to the site calculus.

• alsoOp : ClauseOp
• notOp : ClauseOp
• embedOp : ClauseOp

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqClauseOp : DecidableEq ClauseOp

Equations

• ChowErlewine2022.instDecidableEqClauseOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChowErlewine2022.instReprClauseOp.repr : ClauseOp → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChowErlewine2022.instReprClauseOp : Repr ClauseOp

Equations

• ChowErlewine2022.instReprClauseOp = { reprPrec := ChowErlewine2022.instReprClauseOp.repr }

def ChowErlewine2022.wrapOps {F W : Type} : List ClauseOp → Parse F W → Parse F W

Wrap a spine of overt operators around a parse, top-down.

Equations

• ChowErlewine2022.wrapOps [] x✝ = x✝
• ChowErlewine2022.wrapOps (ChowErlewine2022.ClauseOp.alsoOp :: rest) x✝ = (ChowErlewine2022.wrapOps rest x✝).also
• ChowErlewine2022.wrapOps (ChowErlewine2022.ClauseOp.notOp :: rest) x✝ = (ChowErlewine2022.wrapOps rest x✝).not
• ChowErlewine2022.wrapOps (ChowErlewine2022.ClauseOp.embedOp :: rest) x✝ = ChowErlewine2022.wrapOps rest x✝

structure ChowErlewine2022.BaseClause (F W : Type) : Type

A base clause carries the scalar item, the overt operators above the verb phrase (top-down), and the number of them taking scope over the trigger's surface position. Site i is the adjunction position with i operators above it; a site commands the trigger iff i ≤ triggerDepth. The trigger interprets in its base position throughout, so movement (the paper's (7)) shows up only in triggerDepth.

• den : F → W → SignType
• alt : F → W → SignType
• ops : List ClauseOp
• triggerDepth : ℕ

def ChowErlewine2022.BaseClause.leaf {F W : Type} (b : BaseClause F W) : Parse F W

The scalar leaf of the clause.

Equations

• b.leaf = ChowErlewine2022.Parse.lex b.den b.alt

def ChowErlewine2022.BaseClause.plain {F W : Type} (b : BaseClause F W) : Parse F W

The clause with no exh.

Equations

• b.plain = ChowErlewine2022.wrapOps b.ops b.leaf

def ChowErlewine2022.BaseClause.withExhAt {F W : Type} (b : BaseClause F W) (i : ℕ) : Parse F W

The clause with exh adjoined at site i.

Equations

• b.withExhAt i = ChowErlewine2022.wrapOps (List.take i b.ops) (ChowErlewine2022.wrapOps (List.drop i b.ops) b.leaf).exh

def ChowErlewine2022.BaseClause.Vacuous {F W : Type} [Fintype W] [DecidableEq W] (sal : F → F) (b : BaseClause F W) (i : ℕ) : Prop

exh at site i is vacuous when inserting it does not change the interpretation.

Equations

• ChowErlewine2022.BaseClause.Vacuous sal b i = (ChowErlewine2022.Parse.interp sal (b.withExhAt i) = ChowErlewine2022.Parse.interp sal b.plain)

@[instance_reducible]

instance ChowErlewine2022.instDecidableVacuousOfFintypeOfDecidableEq {F W : Type} [Fintype W] [DecidableEq W] [Fintype F] [DecidableEq F] (sal : F → F) (b : BaseClause F W) (i : ℕ) : Decidable (BaseClause.Vacuous sal b i)

Equations

• ChowErlewine2022.instDecidableVacuousOfFintypeOfDecidableEq sal b i = decidable_of_iff (ChowErlewine2022.Parse.interp sal (b.withExhAt i) = ChowErlewine2022.Parse.interp sal b.plain) ⋯

def ChowErlewine2022.BaseClause.lowestNonVacuousSite {F W : Type} [Fintype W] [DecidableEq W] [Fintype F] [DecidableEq F] (sal : F → F) (b : BaseClause F W) : Option ℕ

Generalization (9) of [CE22] names the lowest trigger-commanding site where exh is not vacuous. A [uexh*] trigger's exh must adjoin exactly here.

Equations

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

def ChowErlewine2022.BaseClause.clauseEdge {F W : Type} (b : BaseClause F W) : ℕ

The site just above the verb embedding the trigger's finite clause (0 when mono-clausal) is the highest site [uexh]-checking may reach ([CE22] section 3.3).

Equations

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

The feature table (30)

inductive ChowErlewine2022.ExhFeature : Type

The exhaustification feature an SI trigger bears ([CE22] (30), after [Chi13]). strong is [uexh*], weak is [uexh], and none is unmarked.

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

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqExhFeature : DecidableEq ExhFeature

Equations

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

@[instance_reducible]

instance ChowErlewine2022.instReprExhFeature : Repr ExhFeature

Equations

• ChowErlewine2022.instReprExhFeature = { reprPrec := ChowErlewine2022.instReprExhFeature.repr }

def ChowErlewine2022.instReprExhFeature.repr : ExhFeature → ℕ → Std.Format

Equations

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

def ChowErlewine2022.ExhFeature.allowedSites {F W : Type} [Fintype W] [DecidableEq W] [Fintype F] [DecidableEq F] (f : ExhFeature) (sal : F → F) (b : BaseClause F W) : Finset ℕ

The adjunction sites a feature makes available for the trigger's exh are the forced site of generalization (9) for [uexh*], any trigger-commanding site from the clause edge down for [uexh], and any trigger-commanding site for unmarked triggers.

Equations

• ChowErlewine2022.ExhFeature.strong.allowedSites sal b = match ChowErlewine2022.BaseClause.lowestNonVacuousSite sal b with | some i => {i} | none => ∅
• ChowErlewine2022.ExhFeature.weak.allowedSites sal b = (List.filter (fun (i : ℕ) => decide (b.clauseEdge ≤ i) && decide (i ≤ b.triggerDepth)) (List.range (b.ops.length + 1))).toFinset
• ChowErlewine2022.ExhFeature.none.allowedSites sal b = (List.filter (fun (i : ℕ) => decide (i ≤ b.triggerDepth)) (List.range (b.ops.length + 1))).toFinset

inductive ChowErlewine2022.SITrigger : Type

The SI triggers the paper classifies.

• disj : SITrigger
• conj : SITrigger
• univAll : SITrigger
• unstressedSome : SITrigger
• bareNumeral : SITrigger
• stressedSome : SITrigger
• scalarAdj : SITrigger

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqSITrigger : DecidableEq SITrigger

Equations

• ChowErlewine2022.instDecidableEqSITrigger x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChowErlewine2022.instReprSITrigger.repr : SITrigger → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChowErlewine2022.instReprSITrigger : Repr SITrigger

Equations

• ChowErlewine2022.instReprSITrigger = { reprPrec := ChowErlewine2022.instReprSITrigger.repr }

def ChowErlewine2022.SITrigger.feature : SITrigger → ExhFeature

In the feature specification (30), disjunction, conjunction, all, unstressed sm and bare numerals are [uexh*], stressed SOME is [uexh], and scalar adjectives are unmarked.

Equations

• ChowErlewine2022.SITrigger.stressedSome.feature = ChowErlewine2022.ExhFeature.weak
• ChowErlewine2022.SITrigger.scalarAdj.feature = ChowErlewine2022.ExhFeature.none
• x✝.feature = ChowErlewine2022.ExhFeature.strong

Section 2: the also diagnostic with disjunction

def ChowErlewine2022.orLex : Individual → TeachWorld → SignType

"teaches Arabic or Basque", of the focus individual.

Equations

• ChowErlewine2022.orLex x w = SignType.ofProp ((w.taught x).either = true)

def ChowErlewine2022.andLex : Individual → TeachWorld → SignType

"teaches Arabic and Basque", of the focus individual.

Equations

• ChowErlewine2022.andLex x w = SignType.ofProp ((w.taught x).both = true)

def ChowErlewine2022.teachOr : BaseClause Individual TeachWorld

The base clause of (3) is [Nina]F also teaches Arabic or Basque, with also above the in-situ trigger.

Equations

• ChowErlewine2022.teachOr = { den := ChowErlewine2022.orLex, alt := ChowErlewine2022.andLex, ops := [ChowErlewine2022.ClauseOp.alsoOp], triggerDepth := 1 }

def ChowErlewine2022.passiveOr : BaseClause Individual TeachWorld

The base clause of the passive (7) is Arabic or Basque is also taught by [Nina]F, with the trigger moved above also.

Equations

• ChowErlewine2022.passiveOr = { den := ChowErlewine2022.teachOr.den, alt := ChowErlewine2022.teachOr.alt, ops := ChowErlewine2022.teachOr.ops, triggerDepth := 0 }

def ChowErlewine2022.antecedent (p : Taught → Bool) : Finset TeachWorld

The worlds an antecedent sentence about Mira leaves open.

Equations

• ChowErlewine2022.antecedent p = {w : ChowErlewine2022.TeachWorld | p w.mira = true}

theorem ChowErlewine2022.exh_or_direct (w : TeachWorld) : Parse.interp Individual.other teachOr.leaf.exh Individual.nina w = 1 ↔ w.nina.exactlyOne = true

The direct SI of disjunction, (1), makes exh (A ∨ B) exclusive disjunction.

theorem ChowErlewine2022.also_exh_presup (w : TeachWorld) : Parse.interp Individual.other (teachOr.withExhAt 1) Individual.nina w ≠ 0 ↔ w.mira.exactlyOne = true

The presupposition of parse (4), also > exh, is that a salient individual teaches exactly one of the two languages.

theorem ChowErlewine2022.exh_over_also_presup (w : TeachWorld) : Parse.interp Individual.other (teachOr.withExhAt 0) Individual.nina w ≠ 0 ↔ w.mira.both = true

Under parse (5), exh > also, EXH²'s strong negation projects the presupposition of the negated alternative also (A ∧ B), so a salient individual must teach both languages.

theorem ChowErlewine2022.exh_over_also_true_iff (w : TeachWorld) : Parse.interp Individual.other (teachOr.withExhAt 0) Individual.nina w = 1 ↔ w.mira.both = true ∧ w.nina.either = true ∧ ¬w.nina.both = true

The truth conditions of parse (5) conjoin the salient conjunctive presupposition with the exhaustified assertion about Nina.

theorem ChowErlewine2022.also_exh_verdicts : Parse.FelicitousIn Individual.other (teachOr.withExhAt 1) Individual.nina (antecedent Taught.exactlyOne) ∧ ¬Parse.FelicitousIn Individual.other (teachOr.withExhAt 1) Individual.nina (antecedent Taught.both)

By the judgments (3), under the also > exh parse the disjunctive antecedent (with its SI) satisfies the additive presupposition and the conjunctive antecedent does not.

theorem ChowErlewine2022.exh_over_also_verdicts : Parse.FelicitousIn Individual.other (teachOr.withExhAt 0) Individual.nina (antecedent Taught.both) ∧ ¬Parse.FelicitousIn Individual.other (teachOr.withExhAt 0) Individual.nina (antecedent Taught.exactlyOne)

Parse (5) predicts the reverse pattern, licensing exactly the conjunctive antecedent, which is felicitous in (3b)'s context and infelicitous in (3a)'s. The facts are the reverse, so the grammar must block this parse in (3), as or_exh_sites shows it does.

theorem ChowErlewine2022.or_exh_sites : SITrigger.disj.feature.allowedSites Individual.other teachOr = {1} ∧ SITrigger.disj.feature.allowedSites Individual.other passiveOr = {0}

For the attested positions (8), generalization (9) forces exh below also in (3), while in the passive (7) the only trigger-commanding site is above also, so exh adjoins to TP, whose parse licenses the conjunctive antecedent (exh_over_also_verdicts). Passivization reverses the (3b) judgment, and there is no blanket ban on TP adjunction.

Section 2.3: indirect scalar implicatures under negation

def ChowErlewine2022.negConj : BaseClause Individual TeachWorld

The base clause of (16) is [Nina]F also does not teach Arabic and Basque, with also over negation over the conjunctive trigger.

Equations

• ChowErlewine2022.negConj = { den := ChowErlewine2022.andLex, alt := ChowErlewine2022.orLex, ops := [ChowErlewine2022.ClauseOp.alsoOp, ChowErlewine2022.ClauseOp.notOp], triggerDepth := 2 }

theorem ChowErlewine2022.exh_vacuous_below_negation : BaseClause.Vacuous Individual.other negConj 2

exh directly on conjunction, position 3 of (19) and parse (18c), is vacuous, since the disjunctive alternative is entailed and nothing is excludable.

theorem ChowErlewine2022.negConj_site : SITrigger.conj.feature.allowedSites Individual.other negConj = {1}

At position 2 of (19), the [uexh*] of the conjunctive trigger forces exh to the lowest non-vacuous site, just above negation, where it computes the indirect SI.

theorem ChowErlewine2022.si_under_also_true_iff (w : TeachWorld) : Parse.interp Individual.other (negConj.withExhAt 1) Individual.nina w = 1 ↔ w.mira.exactlyOne = true ∧ w.nina.exactlyOne = true

In the truth conditions of parse (18b), the indirect SI exh ¬(A ∧ B) is exclusive disjunction, of the salient individual (the presupposition) and of Nina (the assertion).

theorem ChowErlewine2022.indirect_si_contrast : Parse.FelicitousIn Individual.other (negConj.withExhAt 1) Individual.nina (antecedent Taught.exactlyOne) ∧ ¬Parse.FelicitousIn Individual.other (negConj.withExhAt 1) Individual.nina (antecedent Taught.neither)

By the judgments (16) under the forced parse (18b), the not-and antecedent (with its indirect SI) is licensed and the not-or antecedent is not.

theorem ChowErlewine2022.exh_over_also_negConj_verdicts : Parse.FelicitousIn Individual.other (negConj.withExhAt 0) Individual.nina (antecedent Taught.neither) ∧ ¬Parse.FelicitousIn Individual.other (negConj.withExhAt 0) Individual.nina (antecedent Taught.exactlyOne)

Under parse (18a), exh above also, EXH² projects the presupposition of the negated alternative also ¬(A ∨ B), so it licenses exactly the not-or antecedent, the reverse of the facts.

theorem ChowErlewine2022.vacuous_parse_licenses_both : Parse.FelicitousIn Individual.other (negConj.withExhAt 2) Individual.nina (antecedent Taught.exactlyOne) ∧ Parse.FelicitousIn Individual.other (negConj.withExhAt 2) Individual.nina (antecedent Taught.neither)

Under parse (18c), vacuous exh on the conjunction, the unstrengthened presupposition is satisfied by both antecedents of (16), so this parse cannot explain the contrast; the non-vacuity clause of (9) is what rules it out.

Section 3: variation by SI trigger

The scale of sm and all over a two-membered domain is the disjunction-conjunction scale, so the (14) and (26) clauses reuse the teaching model, with Taught read as which of the two students the focus individual met.

theorem ChowErlewine2022.sm_below_also_SOME_free : SITrigger.unstressedSome.feature.allowedSites Individual.other teachOr = {1} ∧ 0 ∈ SITrigger.stressedSome.feature.allowedSites Individual.other teachOr

In the rows (14) and (26a) of the sm and SOME minimal pair, on the same base clause, the [uexh*] of unstressed sm forces exh below also (whence (14a)'s infelicity with an all antecedent), while the [uexh] of stressed SOME also allows the site above also (whence (26a)'s felicity). Bare numerals pattern with sm on the same base, (13).

def ChowErlewine2022.embeddedSome : BaseClause Individual TeachWorld

The base clause of (28) puts matrix also above the verb embedding the SOME clause.

Equations

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

theorem ChowErlewine2022.embedded_SOME_trapped : SITrigger.stressedSome.feature.allowedSites Individual.other embeddedSome = {1, 2}

In (28), every site [uexh] allows, within the embedded clause or just above the embedding verb, lies below the matrix also, so the additive presupposition is necessarily strengthened and (28) is infelicitous.

Section 3.1: scalar adjectives

inductive ChowErlewine2022.City : Type

The two cities of (24a).

• paris : City
• newYork : City

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqCity : DecidableEq City

Equations

• ChowErlewine2022.instDecidableEqCity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChowErlewine2022.instFintypeCity : Fintype City

Equations

• ChowErlewine2022.instFintypeCity = { elems := { val := ↑ChowErlewine2022.City.enumList, nodup := ChowErlewine2022.City.enumList_nodup }, complete := ChowErlewine2022.instFintypeCity._proof_1 }

def ChowErlewine2022.instReprCity.repr : City → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChowErlewine2022.instReprCity : Repr City

Equations

• ChowErlewine2022.instReprCity = { reprPrec := ChowErlewine2022.instReprCity.repr }

def ChowErlewine2022.City.other : City → City

The salient focus alternative among the cities.

Equations

• ChowErlewine2022.City.paris.other = ChowErlewine2022.City.newYork
• ChowErlewine2022.City.newYork.other = ChowErlewine2022.City.paris

inductive ChowErlewine2022.Temp : Type

On the temperature scale of (24a), freezing entails cold.

• mild : Temp
• cold : Temp
• freezing : Temp

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqTemp : DecidableEq Temp

Equations

• ChowErlewine2022.instDecidableEqTemp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChowErlewine2022.instFintypeTemp : Fintype Temp

Equations

• ChowErlewine2022.instFintypeTemp = { elems := { val := ↑ChowErlewine2022.Temp.enumList, nodup := ChowErlewine2022.Temp.enumList_nodup }, complete := ChowErlewine2022.instFintypeTemp._proof_1 }

@[instance_reducible]

instance ChowErlewine2022.instReprTemp : Repr Temp

Equations

• ChowErlewine2022.instReprTemp = { reprPrec := ChowErlewine2022.instReprTemp.repr }

def ChowErlewine2022.instReprTemp.repr : Temp → ℕ → Std.Format

Equations

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

def ChowErlewine2022.Temp.atLeastCold : Temp → Bool

At least cold.

Equations

• ChowErlewine2022.Temp.mild.atLeastCold = false
• x✝.atLeastCold = true

def ChowErlewine2022.Temp.isFreezing : Temp → Bool

Freezing.

Equations

• ChowErlewine2022.Temp.freezing.isFreezing = true
• x✝.isFreezing = false

def ChowErlewine2022.coldClause : BaseClause City (City → Temp)

The base clause of (24a) is it's also cold in [Paris]F.

Equations

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

def ChowErlewine2022.freezingNY : Finset (City → Temp)

Contexts where it is freezing in New York.

Equations

• ChowErlewine2022.freezingNY = {w : ChowErlewine2022.City → ChowErlewine2022.Temp | w ChowErlewine2022.City.newYork = ChowErlewine2022.Temp.freezing}

theorem ChowErlewine2022.scalarAdj_high_exh_ok : 0 ∈ SITrigger.scalarAdj.feature.allowedSites City.other coldClause ∧ Parse.FelicitousIn City.other (coldClause.withExhAt 0) City.paris freezingNY

In (24a), scalar adjectives bear no exh feature, so the site above also is available, and that parse's presupposition (that it is cold in New York, and freezing there via EXH²'s projection from the negated also freezing alternative) is satisfied by the freezing antecedent.

theorem ChowErlewine2022.low_exh_would_block : ¬Parse.FelicitousIn City.other (coldClause.withExhAt 1) City.paris freezingNY

Had cold carried [uexh*], exh would sit below also and presuppose that New York is cold but not freezing, wrongly blocking (24a).

Section 4: ignorance implicatures

Ignorance implicatures arise from a second exh above a covert doxastic necessity operator ([Chi13]; K in [Mey13]). The state level works with the speaker's belief state about one individual's teaching profile; the alternatives of the higher exh are the pre-exhaustified disjunct alternatives, so its prejacent □ exh (A ∨ B) uses the inner SI derived in exh_or_direct.

@[reducible, inline]

abbrev ChowErlewine2022.Doxa : Type

A belief state about one individual's teaching profile.

Equations

• ChowErlewine2022.Doxa = Finset ChowErlewine2022.Taught

def ChowErlewine2022.Doxa.must (s : Doxa) (p : Taught → Bool) : Bool

The covert necessity operator holds when the state supports p throughout.

Equations

• s.must p = decide (∀ t ∈ s, p t = true)

def ChowErlewine2022.Doxa.may (s : Doxa) (p : Taught → Bool) : Bool

The state leaves p open.

Equations

• s.may p = decide (∃ t ∈ s, p t = true)

def ChowErlewine2022.ignoranceScope : Finset Doxa

The meaning of exh > □ > exh over disjunction is computed by innocent exclusion over belief states, with prejacent □ exh (A ∨ B) and the pre-exhaustified disjuncts □ (A ∧ ¬B) and □ (B ∧ ¬A) as alternatives.

Equations

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

theorem ChowErlewine2022.ignorance_scope_eq : ignoranceScope = Exhaustification.predToFinset fun (s : Doxa) => (s.must Taught.exactlyOne && s.may fun (x : Taught) => !x.arabic) && s.may fun (x : Taught) => !x.basque

In (31), the derived meaning is the scalar implicature plus speaker ignorance about each disjunct, so the state supports exactly-one while leaving each disjunct's falsity open.

def ChowErlewine2022.presup34 (salient : List Doxa) : Prop

The additive presupposition of parse (34) = (37a), also over the full ignorance meaning, is that some salient individual's belief-state content is the whole of (31).

Equations

• ChowErlewine2022.presup34 salient = ∃ s ∈ salient, s ∈ ChowErlewine2022.ignoranceScope

@[instance_reducible]

instance ChowErlewine2022.instDecidablePresup34 (salient : List Doxa) : Decidable (presup34 salient)

Equations

• ChowErlewine2022.instDecidablePresup34 salient = ChowErlewine2022.instDecidablePresup34._aux_1 salient

def ChowErlewine2022.presup35 (salient : List Doxa) : Prop

The additive presupposition of parse (35) = (37b), from the paper's display, demands a salient individual believed to teach exactly one, one believed to teach Arabic only, and one believed to teach Basque only. The paper defers the derivation to [MR21a]'s (85).

Equations

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

@[instance_reducible]

instance ChowErlewine2022.instDecidablePresup35 (salient : List Doxa) : Decidable (presup35 salient)

Equations

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

def ChowErlewine2022.disjCtx : List Doxa

In the disjunctive antecedent context of (33a), the speaker believes Mira teaches exactly one of the two languages, without knowing which. Each context lists the speaker's belief state about each salient individual.

Equations

• ChowErlewine2022.disjCtx = [{{ arabic := true, basque := false }, { arabic := false, basque := true }}]

def ChowErlewine2022.conjCtx : List Doxa

The conjunctive antecedent context of (33b).

Equations

• ChowErlewine2022.conjCtx = [{{ arabic := true, basque := true }}]

def ChowErlewine2022.splitCtx : List Doxa

In the split antecedent context of (33c), Mira teaches Arabic only and Ora Basque only.

Equations

• ChowErlewine2022.splitCtx = [{{ arabic := true, basque := false }}, {{ arabic := false, basque := true }}]

def ChowErlewine2022.simpleCtx : List Doxa

In the simple antecedent context of (33d), Mira teaches Arabic only.

Equations

• ChowErlewine2022.simpleCtx = [{{ arabic := true, basque := false }}]

theorem ChowErlewine2022.antecedent_pattern : (presup34 disjCtx ∧ ¬presup35 disjCtx) ∧ (¬presup34 conjCtx ∧ ¬presup35 conjCtx) ∧ (¬presup34 splitCtx ∧ presup35 splitCtx) ∧ ¬presup34 simpleCtx ∧ ¬presup35 simpleCtx

By the judgment pattern (33), the disjunctive antecedent is licensed only by parse (34), the split antecedent only by parse (35), and the conjunctive and simple antecedents by neither, so the grammar must generate both (37a) and (37b), and only those.

inductive ChowErlewine2022.IgnOp : Type

The covert and overt operators of the (37) parses, top-down over the disjunctive leaf, are also, the ignorance exh, the doxastic necessity operator, and the SI exh that checks [uexh*].

• also : IgnOp
• ignExh : IgnOp
• nec : IgnOp
• siExh : IgnOp

@[instance_reducible]

instance ChowErlewine2022.instDecidableEqIgnOp : DecidableEq IgnOp

Equations

• ChowErlewine2022.instDecidableEqIgnOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChowErlewine2022.instReprIgnOp.repr : IgnOp → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChowErlewine2022.instReprIgnOp : Repr IgnOp

Equations

• ChowErlewine2022.instReprIgnOp = { reprPrec := ChowErlewine2022.instReprIgnOp.repr }

def ChowErlewine2022.parse37a : List IgnOp

Parse (37a) is also > exh > □ > exh. The necessity operator sits below also, which occupies its surface vP-adjoined position, so once this parse is needed the ignorance-deriving □ is available clause-medially, (38) against [Mey13]'s Matrix K theory.

Equations

• ChowErlewine2022.parse37a = [ChowErlewine2022.IgnOp.also, ChowErlewine2022.IgnOp.ignExh, ChowErlewine2022.IgnOp.nec, ChowErlewine2022.IgnOp.siExh]

def ChowErlewine2022.parse37b : List IgnOp

Parse (37b) is exh > □ > also > exh.

Equations

• ChowErlewine2022.parse37b = [ChowErlewine2022.IgnOp.ignExh, ChowErlewine2022.IgnOp.nec, ChowErlewine2022.IgnOp.also, ChowErlewine2022.IgnOp.siExh]

def ChowErlewine2022.parse37c : List IgnOp

Parse (37c) is exh > □ > exh > also.

Equations

• ChowErlewine2022.parse37c = [ChowErlewine2022.IgnOp.ignExh, ChowErlewine2022.IgnOp.nec, ChowErlewine2022.IgnOp.siExh, ChowErlewine2022.IgnOp.also]

def ChowErlewine2022.siExhSite (p : List IgnOp) : ℕ

The site the SI exh occupies is given by the number of overt operators above it.

Equations

• ChowErlewine2022.siExhSite p = List.count ChowErlewine2022.IgnOp.also (List.takeWhile (fun (x : ChowErlewine2022.IgnOp) => x != ChowErlewine2022.IgnOp.siExh) p)

def ChowErlewine2022.ChecksUExhStar (p : List IgnOp) : Prop

[uexh*] is checked iff the SI exh occupies the site generalization (9) forces on the base clause of (3) = (32). Once checked, the feature imposes nothing on the higher exh and □ ([CE22] section 3.3).

Equations

• ChowErlewine2022.ChecksUExhStar p = (some (ChowErlewine2022.siExhSite p) = ChowErlewine2022.BaseClause.lowestNonVacuousSite ChowErlewine2022.Individual.other ChowErlewine2022.teachOr)

@[instance_reducible]

instance ChowErlewine2022.instDecidableChecksUExhStar (p : List IgnOp) : Decidable (ChecksUExhStar p)

Equations

• ChowErlewine2022.instDecidableChecksUExhStar p = ChowErlewine2022.instDecidableChecksUExhStar._aux_1 p

theorem ChowErlewine2022.parse37_grammaticality : ChecksUExhStar parse37a ∧ ChecksUExhStar parse37b ∧ ¬ChecksUExhStar parse37c

In the grammaticality pattern (37), (37a) and (37b), which differ only in where the freely placed higher exh and □ sit, check [uexh*], while (37c), whose SI exh is above also, does not. This is the pattern [MR21a] and [SS17] would overgenerate without the feature.