[Mih19]: Decomposing Modified Numerals

[Mih19] [Hac00] [Ken15] [Hor72] [GN07] [Nou10] [FH06b] [Spe14] [Chi13] [SS11] [Kri07a]

[Mih19] (Ch. 2) decomposes bare (BN), comparative-modified (CMN), and superlative-modified (SMN) numerals into extent indicators — much/little denote positive/negative extents on the cardinality scale, transposing Kennedy's earlier extent algebra (her §2.5) — and two operators: [comp] places the maximum of the degree predicate in the complement of the extent, [at-sup] inside it. The four modified forms are cross-pairings (more than = [comp]+much, less than = [comp]+little, at least = [at-sup]+little, at most = [at-sup]+much), and the truth conditions provably reduce to the Hackl/Kennedy meanings — here the named meanings of Semantics.Numerals, so the reduction theorems double as bridges to the [Ken15] spine. Alternatives fall out of the truth conditions: σA replaces the numeral with a scalemate; DA replaces the set the maximum is asserted to fall in — the complement of the extent for [comp] forms (her Ch. 2 (38c)), the extent for [at-sup] forms (her Ch. 2 (39c)) — with its proper subsets. Bare numerals generate no DA, since their (Hornian, lower-bounded) truth conditions reference no degree-set domain (her Ch. 2 (37c)).

Ch. 3 defends classical scalar implicatures for all three classes and locates the failures: σA-exhaustification at scale granularity 1 produces an 'exactly' meaning for every form — welcome for bare numerals ([Hor72], her Ch. 3 (2)), unwelcome for CMNs/SMNs (her Ch. 3 (24)–(27)) — while coarser granularities avoid it (her §3.7; [Spe14]'s grade context, her §3.6 (33), is the granularity-4 instance). The scale and its granularity are contextual ([SS11]'s granularity functions; rounder numerals select coarser scales, [Kri07a] and her pp. 110–111), not universally dense — contra [FH06b] (her fn. 8). On discrete scales the two accounts agree (FoxHackl2006Numerals.moreThan_has_maxInf_nat is the g = 1 'exactly n+1' rescue); they part on whether density ever obliterates the next-stronger alternative.

Main definitions

• much, little: the extent indicators, as Core.Order.Comparison.intervals
• compTC, atSupTC: the [comp]/[at-sup] truth conditions on the maximum
• Form: BN/CMN/SMN assertion forms; Form.toComparison factors them through the Comparison spine; Form.tc, Form.domainAlts, Form.strongerAlt, Form.exhSigma

Main results

• compTC_much_iff … atSupTC_much_iff: the reductions to the Semantics.Numerals named meanings (her Ch. 2 (32)–(33))
• Form.tc_iff_rel: the Op × Extent factorization lands on Comparison.rel
• comp_excludes_boundary / atSup_includes_boundary: the Class A/B strict/non-strict split ([GN07], [Nou10]) as corollaries of Comparison.boundary_mem
• exhSigma_bare_eq_exhNumeral: at granularity 1 her O_σA is the spine's exhNumeral (hence, via Spector2013.exhNumeral_eq_innocent_exh, Fox-2007 innocent exclusion); exhSigma is its granularity/direction generalization
• exhSigma_*_g1: 'exactly' meanings for all five forms at granularity 1 (her Ch. 3 (2), (24)–(27)); exhSigma_moreThan_proper: the strengthening is non-vacuous — deriving an implicature exactly where [Ken15]'s neo-Gricean account derives none (Kennedy2015.classA_moreThan3_no_primary)
• exhSigma_moreThan_coarse_not_exactly, spector_grade_context: coarser granularity avoids the 'exactly' overgeneration (her §3.6–3.7)
• exhSigma_moreThan_eq_exhChain / exhSigma_atMost_eq_exhChain: the one-scalemate operator equals whole-scale chain-exhaustification (Exhaustification.exhChain_iff_succ)
• Ignorance.parse_sg_total: unpruned parses force total ignorance — the structural core of her Tables 4.1/4.3, via Exhaustification.forall_not_preExh_iff; winner0_blocked, sg_accommodates_loser, db_blocks_loser: the residual table cells
• AntiNegativity.negation_fails_PS: O_ExhDA is vacuous under negation (her Ch. 5 (9)), so the SMN's Proper Strengthening requirement fails; NumeralClass: her [±prune DA, ±PS] parameter pair

Extent indicators (her §2.5, Ch. 2 (27)–(28))

def Mihoc2019.much (n : ℕ) : Set ℕ

⟦much⟧(n) = {d | d ≤ n}: the positive extent of n on the cardinality scale — Comparison.le.interval n.

Equations

• Mihoc2019.much n = Core.Order.Comparison.le.interval n

def Mihoc2019.little (n : ℕ) : Set ℕ

⟦little⟧(n) = {d | d ≥ n}: the negative extent — Comparison.ge.interval n.

Equations

• Mihoc2019.little n = Core.Order.Comparison.ge.interval n

@[simp]

theorem Mihoc2019.mem_much {d n : ℕ} : d ∈ much n ↔ d ≤ n

@[simp]

theorem Mihoc2019.mem_little {d n : ℕ} : d ∈ little n ↔ n ≤ d

The modifiers [comp] and [at-sup] (her Ch. 2 (30)–(31))

Both take an extent indicator f and the numeral n, and locate the maximum of the degree predicate — abstracted here as its value maxD — relative to the extent f n: [comp] in its complement, [at-sup] inside it.

def Mihoc2019.compTC (f : ℕ → Set ℕ) (n maxD : ℕ) : Prop

[comp] (her Ch. 2 (30)): max(D) ∈ complement of f(n).

Equations

• Mihoc2019.compTC f n maxD = (maxD ∈ (f n)ᶜ)

def Mihoc2019.atSupTC (f : ℕ → Set ℕ) (n maxD : ℕ) : Prop

[at-sup] (her Ch. 2 (31)): max(D) ∈ f(n).

Equations

• Mihoc2019.atSupTC f n maxD = (maxD ∈ f n)

Reduction to the Kennedy spine (her Ch. 2 (32)–(33))

The four cross-pairings recover exactly the named meanings of Semantics.Numerals. That at least pairs with little and at most with much — inverting the pairing of the comparatives — is what captures the shared much/little morphology across CMNs and SMNs.

theorem Mihoc2019.compTC_much_iff (n maxD : ℕ) : compTC much n maxD ↔ Semantics.Numerals.moreThanMeaning n maxD

theorem Mihoc2019.compTC_little_iff (n maxD : ℕ) : compTC little n maxD ↔ Semantics.Numerals.fewerThanMeaning n maxD

theorem Mihoc2019.atSupTC_little_iff (n maxD : ℕ) : atSupTC little n maxD ↔ Semantics.Numerals.atLeastMeaning n maxD

theorem Mihoc2019.atSupTC_much_iff (n maxD : ℕ) : atSupTC much n maxD ↔ Semantics.Numerals.atMostMeaning n maxD

Assertion forms (her §2.6)

Truth conditions of all three classes expose a scalar element (the numeral); those of CMNs/SMNs additionally expose a degree-set domain.

inductive Mihoc2019.Extent : Type

The two extent indicators as data.

• much : Extent

  Positive extent: ⟦much⟧(n) = {d | d ≤ n}.

• little : Extent

  Negative extent: ⟦little⟧(n) = {d | n ≤ d}.

@[implicit_reducible]

instance Mihoc2019.instDecidableEqExtent : DecidableEq Extent

Equations

• Mihoc2019.instDecidableEqExtent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mihoc2019.instReprExtent.repr : Extent → ℕ → Std.Format

Equations

• Mihoc2019.instReprExtent.repr Mihoc2019.Extent.much prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mihoc2019.Extent.much")).group prec✝
• Mihoc2019.instReprExtent.repr Mihoc2019.Extent.little prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mihoc2019.Extent.little")).group prec✝

@[implicit_reducible]

instance Mihoc2019.instReprExtent : Repr Extent

Equations

• Mihoc2019.instReprExtent = { reprPrec := Mihoc2019.instReprExtent.repr }

def Mihoc2019.Extent.set : Extent → ℕ → Set ℕ

The extent an Extent denotes.

Equations

• Mihoc2019.Extent.much.set = Mihoc2019.much
• Mihoc2019.Extent.little.set = Mihoc2019.little

inductive Mihoc2019.Op : Type

The [comp]/[at-sup] operators as data.

• comp : Op

  [comp]: maximum in the complement of the extent (strict, Class A).

• atSup : Op

  [at-sup]: maximum inside the extent (non-strict, Class B).

@[implicit_reducible]

instance Mihoc2019.instDecidableEqOp : DecidableEq Op

Equations

• Mihoc2019.instDecidableEqOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mihoc2019.instReprOp : Repr Op

Equations

• Mihoc2019.instReprOp = { reprPrec := Mihoc2019.instReprOp.repr }

def Mihoc2019.instReprOp.repr : Op → ℕ → Std.Format

Equations

• Mihoc2019.instReprOp.repr Mihoc2019.Op.comp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mihoc2019.Op.comp")).group prec✝
• Mihoc2019.instReprOp.repr Mihoc2019.Op.atSup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mihoc2019.Op.atSup")).group prec✝

inductive Mihoc2019.Form : Type

BN/CMN/SMN assertion forms.

• bare (n : ℕ) : Form

  A bare numeral (Hornian lower-bounded basic meaning, her §2.3).

• modified (op : Op) (f : Extent) (n : ℕ) : Form

  An extent indicator under [comp] or [at-sup].

def Mihoc2019.instDecidableEqForm.decEq (x✝ x✝¹ : Form) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Mihoc2019.instDecidableEqForm.decEq (Mihoc2019.Form.bare a) (Mihoc2019.Form.bare b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Mihoc2019.instDecidableEqForm.decEq (Mihoc2019.Form.bare n) (Mihoc2019.Form.modified op f n_1) = isFalse ⋯
• Mihoc2019.instDecidableEqForm.decEq (Mihoc2019.Form.modified op f n) (Mihoc2019.Form.bare n_1) = isFalse ⋯

@[implicit_reducible]

instance Mihoc2019.instDecidableEqForm : DecidableEq Form

Equations

• Mihoc2019.instDecidableEqForm = Mihoc2019.instDecidableEqForm.decEq

def Mihoc2019.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mihoc2019.instReprForm : Repr Form

Equations

• Mihoc2019.instReprForm = { reprPrec := Mihoc2019.instReprForm.repr }

@[reducible, inline]

abbrev Mihoc2019.Form.moreThan (n : ℕ) : Form

more than n = [comp]+much.

Equations

• Mihoc2019.Form.moreThan n = Mihoc2019.Form.modified Mihoc2019.Op.comp Mihoc2019.Extent.much n

@[reducible, inline]

abbrev Mihoc2019.Form.lessThan (n : ℕ) : Form

less than n = [comp]+little.

Equations

• Mihoc2019.Form.lessThan n = Mihoc2019.Form.modified Mihoc2019.Op.comp Mihoc2019.Extent.little n

@[reducible, inline]

abbrev Mihoc2019.Form.atLeast (n : ℕ) : Form

at least n = [at-sup]+little.

Equations

• Mihoc2019.Form.atLeast n = Mihoc2019.Form.modified Mihoc2019.Op.atSup Mihoc2019.Extent.little n

@[reducible, inline]

abbrev Mihoc2019.Form.atMost (n : ℕ) : Form

at most n = [at-sup]+much.

Equations

• Mihoc2019.Form.atMost n = Mihoc2019.Form.modified Mihoc2019.Op.atSup Mihoc2019.Extent.much n

def Mihoc2019.Form.tc : Form → ℕ → Prop

Truth conditions of a form, as a predicate on the maximum of the degree predicate. Bare numerals get the lower-bounded Horn meaning (Semantics.Numerals.atLeastMeaning; her §2.3, following [Hor72]).

Equations

• (Mihoc2019.Form.bare n).tc x✝ = Semantics.Numerals.atLeastMeaning n x✝
• (Mihoc2019.Form.modified Mihoc2019.Op.comp f n).tc x✝ = Mihoc2019.compTC f.set n x✝
• (Mihoc2019.Form.modified Mihoc2019.Op.atSup f n).tc x✝ = Mihoc2019.atSupTC f.set n x✝

@[implicit_reducible]

instance Mihoc2019.instDecidableTc (φ : Form) (maxD : ℕ) : Decidable (φ.tc maxD)

Equations

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

The Op × Extent factorization of the Comparison spine

The four modified forms are a coordinate system on the four non-eq Core.Order.Comparisons: the operator carries strictness (Class A/B, Comparison.isStrict), the extent and operator jointly fix the bound direction. Form.tc_iff_rel makes the factorization first-class; the Class A/B boundary facts then follow from Comparison.boundary_mem rather than being re-proved.

def Mihoc2019.Form.toComparison : Form → Core.Order.Comparison

The comparison a form's truth conditions instantiate.

Equations

• (Mihoc2019.Form.bare n).toComparison = Core.Order.Comparison.ge
• (Mihoc2019.Form.modified Mihoc2019.Op.comp Mihoc2019.Extent.much n).toComparison = Core.Order.Comparison.gt
• (Mihoc2019.Form.modified Mihoc2019.Op.comp Mihoc2019.Extent.little n).toComparison = Core.Order.Comparison.lt
• (Mihoc2019.Form.modified Mihoc2019.Op.atSup Mihoc2019.Extent.little n).toComparison = Core.Order.Comparison.ge
• (Mihoc2019.Form.modified Mihoc2019.Op.atSup Mihoc2019.Extent.much n).toComparison = Core.Order.Comparison.le

def Mihoc2019.Form.arg : Form → ℕ

The numeral argument of a form.

Equations

• (Mihoc2019.Form.bare a).arg = a
• (Mihoc2019.Form.modified a a_1 a_2).arg = a_2

theorem Mihoc2019.Form.tc_iff_rel (φ : Form) (maxD : ℕ) : φ.tc maxD ↔ φ.toComparison.rel maxD φ.arg

The factorization theorem: every form's truth conditions are its comparison's relation at its numeral argument.

@[simp]

theorem Mihoc2019.tc_bare (n maxD : ℕ) : (Form.bare n).tc maxD ↔ n ≤ maxD

@[simp]

theorem Mihoc2019.tc_moreThan (n maxD : ℕ) : (Form.moreThan n).tc maxD ↔ n < maxD

@[simp]

theorem Mihoc2019.tc_lessThan (n maxD : ℕ) : (Form.lessThan n).tc maxD ↔ maxD < n

@[simp]

theorem Mihoc2019.tc_atLeast (n maxD : ℕ) : (Form.atLeast n).tc maxD ↔ n ≤ maxD

@[simp]

theorem Mihoc2019.tc_atMost (n maxD : ℕ) : (Form.atMost n).tc maxD ↔ maxD ≤ n

Class A/B strictness from the decomposition

The Class A (strict) / Class B (non-strict) split of [GN07] and [Nou10] — Semantics.Numerals.ModifierClass — derived from complement-vs-extent through Comparison.boundary_mem, rather than stipulated per modifier.

theorem Mihoc2019.comp_excludes_boundary (f : Extent) (n : ℕ) : ¬(Form.modified Op.comp f n).tc n

theorem Mihoc2019.atSup_includes_boundary (f : Extent) (n : ℕ) : (Form.modified Op.atSup f n).tc n

Domain alternatives (her Ch. 2 (37)–(39))

σA replaces the numeral with a scalemate. DA replaces the set the maximum is asserted to fall in — the complement of the extent for [comp] forms (her (38c)), the extent itself for [at-sup] forms (her (39c)) — with its proper subsets; uniformly, the proper subsets of the form's truth-condition set. Bare numerals reference no degree-set domain and generate no DA (her (37c)): the structural asymmetry that drives the ignorance and polarity results of her Chs. 4–5.

def Mihoc2019.Form.domainAlts : Form → Set (Set ℕ)

The degree-set domains a form makes available for subdomain alternatives.

Equations

• (Mihoc2019.Form.bare n).domainAlts = ∅
• (Mihoc2019.Form.modified op f n).domainAlts = {D' : Set ℕ | D' ⊂ {d : ℕ | (Mihoc2019.Form.modified op f n).tc d}}

theorem Mihoc2019.Form.tc_of_mem_domainAlt {φ : Form} {D' : Set ℕ} (h : D' ∈ φ.domainAlts) {maxD : ℕ} (hm : maxD ∈ D') : φ.tc maxD

Every domain alternative strengthens the assertion: membership of the maximum in a DA entails the form's truth conditions — the premise of her Ch. 4 pre-exhaustification.

σA-exhaustification and 'exactly' overgeneration (her Ch. 3)

O_σA asserts the prejacent and negates its next-stronger scalar alternative on a scale of granularity g (stronger = larger numeral for lower-bounding forms, smaller for upper-bounding). Negating the next-stronger scalemate is her own computation shape (Ch. 3 (2), (24)–(27)) and coincides with full innocent-exclusion exhaustification for these monotone forms, whose stronger alternatives form an entailment chain.

At g = 1 the result is an 'exactly' meaning for every form: welcome for bare numerals (her Ch. 3 (2)), the unwelcome overgeneration of her Ch. 3 (24)–(27) for CMNs/SMNs. Coarser granularity yields a non-singleton interval instead (her §3.6–3.7). The scale and its granularity are contextual ([SS11]'s granularity functions; rounder numerals select coarser scales, [Kri07a], her pp. 110–111) rather than universally dense (her fn. 8, contra [FH06b] — though on discrete ℕ the accounts agree: cf. FoxHackl2006Numerals.moreThan_has_maxInf_nat).

def Mihoc2019.Form.strongerAlt (g : ℕ) : Form → Form

The next-stronger σA scalemate of a form at granularity g.

Equations

• Mihoc2019.Form.strongerAlt g (Mihoc2019.Form.bare n) = Mihoc2019.Form.bare (n + g)
• Mihoc2019.Form.strongerAlt g (Mihoc2019.Form.modified Mihoc2019.Op.comp Mihoc2019.Extent.much n) = Mihoc2019.Form.moreThan (n + g)
• Mihoc2019.Form.strongerAlt g (Mihoc2019.Form.modified Mihoc2019.Op.comp Mihoc2019.Extent.little n) = Mihoc2019.Form.lessThan (n - g)
• Mihoc2019.Form.strongerAlt g (Mihoc2019.Form.modified Mihoc2019.Op.atSup Mihoc2019.Extent.little n) = Mihoc2019.Form.atLeast (n + g)
• Mihoc2019.Form.strongerAlt g (Mihoc2019.Form.modified Mihoc2019.Op.atSup Mihoc2019.Extent.much n) = Mihoc2019.Form.atMost (n - g)

def Mihoc2019.Form.exhSigma (g : ℕ) (φ : Form) (maxD : ℕ) : Prop

O_σA at granularity g: assert the prejacent, negate the next-stronger scalemate.

Equations

• Mihoc2019.Form.exhSigma g φ maxD = (φ.tc maxD ∧ ¬(Mihoc2019.Form.strongerAlt g φ).tc maxD)

@[implicit_reducible]

instance Mihoc2019.instDecidableExhSigma (g : ℕ) (φ : Form) (maxD : ℕ) : Decidable (Form.exhSigma g φ maxD)

Equations

• Mihoc2019.instDecidableExhSigma g φ maxD = Mihoc2019.instDecidableExhSigma._aux_1 g φ maxD

theorem Mihoc2019.exhSigma_bare_eq_exhNumeral (n maxD : ℕ) : Form.exhSigma 1 (Form.bare n) maxD ↔ Semantics.Numerals.exhNumeral n maxD

At granularity 1 on a bare numeral, her O_σA is the spine's Semantics.Numerals.exhNumeral — and hence, via Spector2013.exhNumeral_eq_innocent_exh, Fox-2007 innocent exclusion. exhSigma is its generalization to arbitrary granularity and to the upper-bounding scalemate direction.

theorem Mihoc2019.exhSigma_atLeast_eq_exhNumeral (n maxD : ℕ) : Form.exhSigma 1 (Form.atLeast n) maxD ↔ Semantics.Numerals.exhNumeral n maxD

The at least form agrees with the bare form under O_σA at granularity 1 — both are exhNumeral.

theorem Mihoc2019.exhSigma_bare_g1 (n maxD : ℕ) : Form.exhSigma 1 (Form.bare n) maxD ↔ maxD = n

Her Ch. 3 (2): O_σA(bare n) = 'exactly n' — the classical Horn derivation.

theorem Mihoc2019.exhSigma_moreThan_g1 (n maxD : ℕ) : Form.exhSigma 1 (Form.moreThan n) maxD ↔ maxD = n + 1

Her Ch. 3 (24): O_σA(more than n) = 'exactly n+1' — unwelcome.

theorem Mihoc2019.exhSigma_lessThan_g1 (n maxD : ℕ) (hn : 1 ≤ n) : Form.exhSigma 1 (Form.lessThan n) maxD ↔ maxD = n - 1

Her Ch. 3 (25): O_σA(less than n) = 'exactly n−1' — unwelcome.

theorem Mihoc2019.exhSigma_atLeast_g1 (n maxD : ℕ) : Form.exhSigma 1 (Form.atLeast n) maxD ↔ maxD = n

Her Ch. 3 (26): O_σA(at least n) = 'exactly n' — unwelcome.

theorem Mihoc2019.exhSigma_atMost_g1 (n maxD : ℕ) (hn : 1 ≤ n) : Form.exhSigma 1 (Form.atMost n) maxD ↔ maxD = n

Her Ch. 3 (27): O_σA(at most n) = 'exactly n' — unwelcome.

theorem Mihoc2019.exhSigma_moreThan_proper (n : ℕ) : ∃ (maxD : ℕ), (Form.moreThan n).tc maxD ∧ ¬Form.exhSigma 1 (Form.moreThan n) maxD

The granularity-1 strengthening is non-vacuous: some worlds verify the CMN's truth conditions but not its exhaustification. Mihoc thus derives a scalar implicature for Class A forms exactly where [Ken15]'s neo-Gricean account derives none (Kennedy2015.classA_moreThan3_no_primary) — same truth conditions, opposite pragmatic verdict, reconciled only by the granularity parameter (coarse scales recover the weaker effect, exhSigma_moreThan_coarse_not_exactly).

theorem Mihoc2019.exhSigma_moreThan_coarse_not_exactly (n g : ℕ) (hg : 2 ≤ g) : ∃ (d₁ : ℕ) (d₂ : ℕ), d₁ ≠ d₂ ∧ Form.exhSigma g (Form.moreThan n) d₁ ∧ Form.exhSigma g (Form.moreThan n) d₂

Her §3.7: at granularity ≥ 2 the exhaustified CMN is no longer an 'exactly' meaning — two distinct values survive.

theorem Mihoc2019.spector_grade_context (maxD : ℕ) : Form.exhSigma 4 (Form.moreThan 5) maxD ↔ 5 < maxD ∧ maxD ≤ 9

[Spe14]'s grade context (her §3.6 (33)): with the contextually salient scale ⟨…, more than 5, more than 9, …⟩ (granularity 4), John solved more than five problems implicates not more than nine — the surviving meaning is the interval {6, …, 9} she glosses as "a B", not an 'exactly'.

σA scales as entailment chains

exhSigma negates one next-stronger scalemate; the substrate keystone Exhaustification.exhChain_iff_succ shows this equals exhaustification against the whole granularity-g scale, since the scale is an entailment chain. (Dually, Exhaustification.exhChain_not_of_dense is the [FH06b] crash that this file's contextual-granularity scales avoid: cf. FoxHackl2006Numerals.moreThan_exhChain_crash.)

theorem Mihoc2019.exhSigma_moreThan_eq_exhChain (n g maxD : ℕ) : Form.exhSigma g (Form.moreThan n) maxD ↔ Exhaustification.exhChain (fun (k : ℕ) => (Form.moreThan (n + k * g)).tc) 0 maxD

theorem Mihoc2019.exhSigma_atMost_eq_exhChain (n g maxD : ℕ) : Form.exhSigma g (Form.atMost n) maxD ↔ Exhaustification.exhChain (fun (k : ℕ) => (Form.atMost (n - k * g)).tc) 0 maxD

Ignorance (her Ch. 4)

Assertions carry a null epistemic necessity modal □_S; O applies above it, negating pre-exhaustified domain alternatives (Exhaustification.preExh) and the stronger σA. Her running model: the CMN less than three / SMN at most two, worlds = candidate maxima 0–3, □_S = ContextSet.entails over a nonempty epistemic state (boxS_iff_entails). The DA are the value-regions inside the prejacent set {0, 1, 2}: singletons and doubletons.

The load-bearing structure: negating the pre-exhaustified singleton DA says no region is settled uniquely (Exhaustification.forall_not_preExh_iff), and a nonempty state settles at most one of the disjoint regions (sgDA_subsingleton) — so none is settled: total ignorance, her Tables 4.1/4.3, derived structurally. The residual table cells (loser/winner accommodation and blocking) are checked exhaustively over all epistemic states.

@[reducible, inline]

abbrev Mihoc2019.Ignorance.EWorld : Type

Worlds: the candidate maximum, values 0–3.

Equations

• Mihoc2019.Ignorance.EWorld = Fin 4

def Mihoc2019.Ignorance.boxS (E : Finset EWorld) (p : EWorld → Prop) : Prop

□_S over a finite epistemic state — ContextSet.entails in computable clothing (boxS_iff_entails).

Equations

• Mihoc2019.Ignorance.boxS E p = ∀ w ∈ E, p w

@[implicit_reducible]

instance Mihoc2019.Ignorance.instDecidableBoxSOfDecidablePredEWorld (E : Finset EWorld) (p : EWorld → Prop) [DecidablePred p] : Decidable (boxS E p)

Equations

• Mihoc2019.Ignorance.instDecidableBoxSOfDecidablePredEWorld E p = Mihoc2019.Ignorance.instDecidableBoxSOfDecidablePredEWorld._aux_1 E p

theorem Mihoc2019.Ignorance.boxS_iff_entails (E : Finset EWorld) (p : EWorld → Prop) : boxS E p ↔ CommonGround.ContextSet.entails ↑E {w : EWorld | p w}

def Mihoc2019.Ignorance.prejacent (E : Finset EWorld) : Prop

The asserted prejacent: □_S(less than three).

Equations

• Mihoc2019.Ignorance.prejacent E = Mihoc2019.Ignorance.boxS E fun (w : Mihoc2019.Ignorance.EWorld) => (Mihoc2019.Form.lessThan 3).tc ↑w

@[implicit_reducible]

instance Mihoc2019.Ignorance.instDecidablePrejacent (E : Finset EWorld) : Decidable (prejacent E)

Equations

• Mihoc2019.Ignorance.instDecidablePrejacent E = Mihoc2019.Ignorance.instDecidablePrejacent._aux_1 E

def Mihoc2019.Ignorance.sgDA (E : Finset EWorld) (i : Fin 3) : Prop

Singleton domain alternatives: □_S(max = i) for i < 3.

Equations

• Mihoc2019.Ignorance.sgDA E i = Mihoc2019.Ignorance.boxS E fun (w : Mihoc2019.Ignorance.EWorld) => ↑w = ↑i

def Mihoc2019.Ignorance.dbDA (E : Finset EWorld) (i : Fin 3) : Prop

Doubleton domain alternatives: □_S of the prejacent region minus value i.

Equations

• Mihoc2019.Ignorance.dbDA E i = Mihoc2019.Ignorance.boxS E fun (w : Mihoc2019.Ignorance.EWorld) => ↑w < 3 ∧ ↑w ≠ ↑i

@[implicit_reducible]

instance Mihoc2019.Ignorance.instDecidableSgDA (E : Finset EWorld) (i : Fin 3) : Decidable (sgDA E i)

Equations

• Mihoc2019.Ignorance.instDecidableSgDA E i = Mihoc2019.Ignorance.instDecidableSgDA._aux_1 E i

@[implicit_reducible]

instance Mihoc2019.Ignorance.instDecidableDbDA (E : Finset EWorld) (i : Fin 3) : Decidable (dbDA E i)

Equations

• Mihoc2019.Ignorance.instDecidableDbDA E i = Mihoc2019.Ignorance.instDecidableDbDA._aux_1 E i

theorem Mihoc2019.Ignorance.sgDA_subsingleton {E : Finset EWorld} (hE : E.Nonempty) {i j : Fin 3} (hi : sgDA E i) (hj : sgDA E j) : i = j

A nonempty state settles at most one singleton region.

theorem Mihoc2019.Ignorance.total_ignorance_of_not_preExh {E : Finset EWorld} (hE : E.Nonempty) (h : ∀ (i : Fin 3), ¬Exhaustification.preExh (sgDA E) i) (i : Fin 3) : ¬sgDA E i

Total ignorance from unique-truth failure: negating every pre-exhaustified singleton DA leaves no settled region at all — the 'total' verdicts of her Tables 4.1/4.3, structurally.

def Mihoc2019.Ignorance.parse (sg db : Bool) (E : Finset EWorld) : Prop

The O_ExhDA+σA parse of □_S(less than three) (her (12)/(14)/(16)), with her DA-pruning parameter: sg/db select which DA sizes survive pruning.

Equations

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

@[implicit_reducible]

instance Mihoc2019.Ignorance.instDecidableParse (sg db : Bool) (E : Finset EWorld) : Decidable (parse sg db E)

Equations

• Mihoc2019.Ignorance.instDecidableParse sg db E = Mihoc2019.Ignorance.instDecidableParse._aux_1 sg db E

def Mihoc2019.Ignorance.TotalIgnorance (E : Finset EWorld) : Prop

Total ignorance (her total row): no value-region is settled.

Equations

• Mihoc2019.Ignorance.TotalIgnorance E = ∀ (i : Fin 3), ¬Mihoc2019.Ignorance.sgDA E i

def Mihoc2019.Ignorance.winner0 (E : Finset EWorld) : Prop

Her canonical 'winner' scenario: □_S 0.

Equations

• Mihoc2019.Ignorance.winner0 E = Mihoc2019.Ignorance.sgDA E 0

def Mihoc2019.Ignorance.loser0 (E : Finset EWorld) : Prop

Her canonical 'loser' scenario: □_S ¬0 ∧ ¬□_S 1 ∧ ¬□_S 2 — one region excluded, the rest unsettled.

Equations

• Mihoc2019.Ignorance.loser0 E = ((Mihoc2019.Ignorance.boxS E fun (w : Mihoc2019.Ignorance.EWorld) => ↑w ≠ 0) ∧ ¬Mihoc2019.Ignorance.sgDA E 1 ∧ ¬Mihoc2019.Ignorance.sgDA E 2)

@[implicit_reducible]

instance Mihoc2019.Ignorance.instDecidableLoser0 (E : Finset EWorld) : Decidable (loser0 E)

Equations

• Mihoc2019.Ignorance.instDecidableLoser0 E = Mihoc2019.Ignorance.instDecidableLoser0._aux_1 E

theorem Mihoc2019.Ignorance.parse_sg_total {db : Bool} {E : Finset EWorld} (hE : E.Nonempty) (h : parse true db E) : TotalIgnorance E

Any parse that keeps the singleton DA forces total ignorance — her Table 4.1 and 4.3 sum-ups, including the SMN (no-pruning) verdict.

theorem Mihoc2019.Ignorance.winner0_blocked {sg db : Bool} {E : Finset EWorld} (h : parse sg db E) : ¬winner0 E

The 'winner' scenario clashes with the σA-implicature — the ✗ cells of her Tables 4.1/4.2: □_S 0 entails □_S(less than one).

theorem Mihoc2019.Ignorance.sg_accommodates_loser : ∃ (E : Finset EWorld), E.Nonempty ∧ parse true false E ∧ loser0 E

The singleton-DA regime accommodates the 'loser' scenario — Table 4.1's ✓ cell (CMNs, which may prune, admit partial ignorance).

theorem Mihoc2019.Ignorance.db_blocks_loser (E : Finset EWorld) : E.Nonempty → parse false true E → ¬loser0 E

The doubleton-DA regime blocks the 'loser' scenario — Table 4.2's ✗ cell — checked over every epistemic state.

Anti-negativity (her Ch. 5)

Under clausemate negation each pre-exhaustified DA is individually inconsistent with the prejacent, so O_ExhDA is vacuous (her (9)) — and the Proper Strengthening requirement (Exhaustification.ProperlyStrengthens) fails. Her parameter pair: SMNs keep all DA (hence episodic total ignorance, Ignorance.parse_sg_total) and require PS (hence deviance under negation, negation_fails_PS); CMNs may prune and impose no PS requirement, escaping both.

@[reducible, inline]

abbrev Mihoc2019.AntiNegativity.NWorld : Type

Worlds for the negated case: candidate maxima 0–2.

Equations

• Mihoc2019.AntiNegativity.NWorld = Fin 3

def Mihoc2019.AntiNegativity.negPrejacent (w : NWorld) : Prop

John didn't call less than two people: the negated prejacent.

Equations

• Mihoc2019.AntiNegativity.negPrejacent w = ¬(Mihoc2019.Form.lessThan 2).tc ↑w

def Mihoc2019.AntiNegativity.negDA (w : NWorld) (i : Fin 2) : Prop

The embedded numeral's DA as propositions at w: max = i, i < 2.

Equations

• Mihoc2019.AntiNegativity.negDA w i = (↑w = ↑i)

def Mihoc2019.AntiNegativity.oParse (w : NWorld) : Prop

The O_ExhDA parse of the negated sentence (her (8)–(9)).

Equations

• Mihoc2019.AntiNegativity.oParse w = (Mihoc2019.AntiNegativity.negPrejacent w ∧ ∀ (i : Fin 2), ¬Exhaustification.preExh (Mihoc2019.AntiNegativity.negDA w) i)

theorem Mihoc2019.AntiNegativity.oParse_iff_negPrejacent (w : NWorld) : oParse w ↔ negPrejacent w

Her (9): every pre-exhaustified DA contradicts the negated prejacent, so negating them adds nothing — O_ExhDA is vacuous.

theorem Mihoc2019.AntiNegativity.negation_fails_PS : ¬Exhaustification.ProperlyStrengthens oParse negPrejacent

Vacuous exhaustification fails Proper Strengthening — the SMN anti-negativity verdict (her §5.1); CMNs, lacking the requirement, are fine under negation.

inductive Mihoc2019.AntiNegativity.NumeralClass : Type

Her Ch. 4–5 lexical parameter pair for modified numerals.

• cmn : NumeralClass

  Comparative-modified: may prune DA; no PS requirement.

• smn : NumeralClass

  Superlative-modified: full DA; PS required.

@[implicit_reducible]

instance Mihoc2019.AntiNegativity.instDecidableEqNumeralClass : DecidableEq NumeralClass

Equations

• Mihoc2019.AntiNegativity.instDecidableEqNumeralClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mihoc2019.AntiNegativity.instReprNumeralClass.repr : NumeralClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mihoc2019.AntiNegativity.instReprNumeralClass : Repr NumeralClass

Equations

• Mihoc2019.AntiNegativity.instReprNumeralClass = { reprPrec := Mihoc2019.AntiNegativity.instReprNumeralClass.repr }

def Mihoc2019.AntiNegativity.NumeralClass.canPruneDA : NumeralClass → Prop

Whether the class licenses DA pruning (her Ch. 4).

Equations

• Mihoc2019.AntiNegativity.NumeralClass.cmn.canPruneDA = True
• Mihoc2019.AntiNegativity.NumeralClass.smn.canPruneDA = False

def Mihoc2019.AntiNegativity.NumeralClass.requiresPS : NumeralClass → Prop

Whether the class requires Proper Strengthening (her Ch. 5).

Equations

• Mihoc2019.AntiNegativity.NumeralClass.cmn.requiresPS = False
• Mihoc2019.AntiNegativity.NumeralClass.smn.requiresPS = True