Mihoc (2019): Decomposing logic: Modified numerals, polarity, and exhaustification

Mihoc builds more than n and less than n from a comparative operator and at least n and at most n from a superlative one, each applied to the extent indicator much or little; the comparative places the maximum of the counted degrees outside the extent and the superlative inside it. The truth conditions mention a domain, the set the maximum falls in, so the modified numerals have subdomain alternatives besides their scalar ones. Exhaustifying against the pre-exhaustified subdomain alternatives across the speaker's epistemic modal yields ignorance as epistemic free choice, total for the superlative numerals, which keep every alternative, and possibly partial for the comparative ones, which may prune. Under negation that exhaustification is vacuous, so the superlative numerals, which require their exhaustification to strengthen the prejacent, are deviant there.

Main statements

• Mihoc2019.Form.tc_iff_rel: each form's truth conditions compare the maximum with the numeral, strictly for the comparative operator and non-strictly for the superlative one.
• Mihoc2019.Ignorance.domainImplicatures_iff: the implicatures from the subdomain alternatives of one size hold exactly when the number of values the speaker considers possible is not that size.
• Mihoc2019.Ignorance.forall_domainImplicatures_iff: keeping every subdomain alternative yields total ignorance.
• Mihoc2019.AntiNegativity.not_negExh_lt: under negation the subdomain exhaustification does not strengthen the prejacent.

Implementation notes

• The maximum of the counted degrees is abstracted to its value, so a truth condition is a predicate on ℕ and an epistemic state is seen through the values it leaves possible.
• Scalar alternatives range over a contextual scale of numerals, which is all her granularity is; the full scale of naturals is her scale of granularity one.
• Ignorance is stated for a finite truth set, which her running examples less than three and at most two have; the infinite truth sets of more than n and at least n need a contextual bound for the same argument.
• Each subdomain alternative is pre-exhaustified against the others of its size, her choice for the parse that keeps alternatives of several sizes.

References

• [Mih19]
• [Hac00]
• [Ken15]
• [Hor72]
• [GN07]
• [Nou10]
• [FH06b]
• [Spe14]
• [Chi13]

Extent indicators and the two operators

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

The positive extent ⟦much⟧(n) = {d | d ≤ n} (her (28a)).

Equations

• Mihoc2019.much n = Degree.Comparison.le.interval n

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

The negative extent ⟦little⟧(n) = {d | d ≥ n} (her (28b)).

Equations

• Mihoc2019.little n = Degree.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

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

The comparative operator puts the maximum of the degree predicate in the complement of the extent f n (her (30)).

Equations

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

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

The superlative operator puts the maximum of the degree predicate in the extent f n (her (31)).

Equations

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

Assertion forms

inductive Mihoc2019.Extent : Type

The two extent indicators.

• much : Extent

  The positive extent indicator much.

• little : Extent

  The negative extent indicator little.

@[instance_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✝

@[instance_reducible]

instance Mihoc2019.instReprExtent : Repr Extent

Equations

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

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

The extent an extent indicator denotes.

Equations

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

inductive Mihoc2019.Op : Type

The two modifier operators.

• comp : Op

  The comparative operator of more than and less than.

• atSup : Op

  The superlative operator of at least and at most.

@[instance_reducible]

instance Mihoc2019.instDecidableEqOp : DecidableEq Op

Equations

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

@[instance_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

Bare and modified numerals.

• bare (n : ℕ) : Form

  A bare numeral, with the lower-bounded meaning of [Hor72].

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

  An extent indicator and a numeral under one of the two operators.

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 ⋯

@[instance_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.

@[instance_reducible]

instance Mihoc2019.instReprForm : Repr Form

Equations

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

@[reducible, inline]

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

more than n is the comparative operator with 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 is the comparative operator with 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 is the superlative operator with 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 is the superlative operator with much.

Equations

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

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

The truth conditions of a form, as a predicate on the maximum of the degree predicate.

Equations

• (Mihoc2019.Form.bare n).tc x✝ = (x✝ ∈ Degree.Comparison.ge.interval n)
• (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✝

def Mihoc2019.Form.toComparison : Form → Degree.Comparison

The comparison a form's truth conditions instantiate.

Equations

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

def Mihoc2019.Form.arg : Form → ℕ

The numeral of a form.

Equations

• (Mihoc2019.Form.bare n).arg = n
• (Mihoc2019.Form.modified op f n).arg = n

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

Every form's truth conditions compare the maximum with its numeral, which recovers the truth conditions of [Hac00] and [Ken15] (her (32)–(33)).

@[instance_reducible]

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

Equations

• Mihoc2019.instDecidableTc φ maxD = decidable_of_iff (φ.toComparison.Rel maxD φ.arg) ⋯

@[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

Strictness

The comparative forms exclude the numeral and the superlative ones include it, the split of [GN07] and [Nou10] into Class A and Class B modifiers, here derived from the operator through Comparison.boundary_mem.

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

Subdomain alternatives

A modified form's subdomain alternatives replace the set its maximum is asserted to fall in, the complement of the extent or the extent itself, by its proper subsets (her (38c), (39c)). A bare numeral mentions no such set and has none (her (37c)).

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

The subdomain alternatives of a form.

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_domainAlts {φ : Form} {D' : Set ℕ} (h : D' ∈ φ.domainAlts) {maxD : ℕ} (hm : maxD ∈ D') : φ.tc maxD

Every subdomain alternative entails the form it is an alternative to.

theorem Mihoc2019.coe_mem_domainAlts {op : Op} {f : Extent} {n k : ℕ} {T S : Finset ℕ} (hT : ∀ (d : ℕ), (Form.modified op f n).tc d ↔ d ∈ T) (hS : S ∈ Finset.powersetCard k T) (hk : k < T.card) : ↑S ∈ (Form.modified op f n).domainAlts

The subsets of a modified form's finite truth set smaller than it are its subdomain alternatives.

Scalar implicatures

A form's scalar alternatives replace its numeral by the other points of a contextual scale S (her (37b)–(39b)), and exhaustifying denies those the form does not entail, the stronger ones. On the full scale of naturals every form comes out 'exactly n', the bare numeral's reading after [Hor72] and an unattested one for the modified forms. A scale with gaps instead leaves an interval up to the next point (mem_exh_moreThan_iff), and the scale is contextual rather than universally dense (her fn. 8, against [FH06b]).

def Mihoc2019.Form.withArg : Form → ℕ → Form

The form with its numeral replaced by m.

Equations

• (Mihoc2019.Form.bare n).withArg x✝ = Mihoc2019.Form.bare x✝
• (Mihoc2019.Form.modified op f n).withArg x✝ = Mihoc2019.Form.modified op f x✝

def Mihoc2019.Form.scalarAlts (S : Set ℕ) (φ : Form) : Set (Set ℕ)

The scalar alternatives of a form on the scale S.

Equations

• Mihoc2019.Form.scalarAlts S φ = (fun (m : ℕ) => {d : ℕ | (φ.withArg m).tc d}) '' S

theorem Mihoc2019.mem_exh_moreThan_iff {S : Set ℕ} {n s : ℕ} (hs : s ∈ S) (hns : n < s) (hnext : ∀ m ∈ S, n < m → s ≤ m) (maxD : ℕ) : maxD ∈ Exhaustification.exh (Form.scalarAlts S (Form.moreThan n)) {d : ℕ | (Form.moreThan n).tc d} ↔ n < maxD ∧ maxD ≤ s

On a scale whose next point above n is s, more than n is exhaustified to the values up to s.

theorem Mihoc2019.mem_exh_moreThan_univ (n maxD : ℕ) : maxD ∈ Exhaustification.exh (Form.scalarAlts Set.univ (Form.moreThan n)) {d : ℕ | (Form.moreThan n).tc d} ↔ maxD = n + 1

On the full scale more than n comes out 'exactly n + 1' (her Ch. 3 (24)).

theorem Mihoc2019.mem_exh_moreThan_five {S : Set ℕ} (h9 : 9 ∈ S) (hgap : ∀ m ∈ S, 5 < m → 9 ≤ m) (maxD : ℕ) : maxD ∈ Exhaustification.exh (Form.scalarAlts S (Form.moreThan 5)) {d : ℕ | (Form.moreThan 5).tc d} ↔ 5 < maxD ∧ maxD ≤ 9

In the grading context of [Spe14] (her Ch. 3 (33)), with more than nine the next point above more than five, John solved more than five problems is exhaustified to between six and nine.

theorem Mihoc2019.mem_exh_bare_univ (n maxD : ℕ) : maxD ∈ Exhaustification.exh (Form.scalarAlts Set.univ (Form.bare n)) {d : ℕ | (Form.bare n).tc d} ↔ maxD ∈ Numerals.exhNumeral n

On the full scale the bare numeral is the exhaustified numeral Numerals.exhNumeral, 'exactly n' (her Ch. 3 (2)).

theorem Mihoc2019.mem_exh_lessThan_univ {n : ℕ} (hn : 1 ≤ n) (maxD : ℕ) : maxD ∈ Exhaustification.exh (Form.scalarAlts Set.univ (Form.lessThan n)) {d : ℕ | (Form.lessThan n).tc d} ↔ maxD = n - 1

On the full scale less than n comes out 'exactly n − 1' (her Ch. 3 (25)).

theorem Mihoc2019.mem_exh_atLeast_univ (n maxD : ℕ) : maxD ∈ Exhaustification.exh (Form.scalarAlts Set.univ (Form.atLeast n)) {d : ℕ | (Form.atLeast n).tc d} ↔ maxD = n

On the full scale at least n comes out 'exactly n' (her Ch. 3 (26)).

theorem Mihoc2019.mem_exh_atMost_univ (n maxD : ℕ) : maxD ∈ Exhaustification.exh (Form.scalarAlts Set.univ (Form.atMost n)) {d : ℕ | (Form.atMost n).tc d} ↔ maxD = n

On the full scale at most n comes out 'exactly n' (her Ch. 3 (27)).

Ignorance

An assertion carries a null epistemic necessity modal □_S, and exhaustification applies above it, negating each pre-exhaustified subdomain alternative □_S (max ∈ S) and the stronger scalar alternatives. A state settles □_S (max ∈ S) just when every value it leaves possible lies in S (box_mem_iff), so of the subdomains of one size exactly one is settled iff the possible values number exactly that size, and the implicatures from the subdomain alternatives of a size hold iff they do not (domainImplicatures_iff). Her three parses of less than three follow: keeping the singletons rules out settling a value, a 'winner' state (her Table 4.1); keeping the larger alternatives rules out excluding a value without settling one, a 'loser' state (her Table 4.2); keeping all leaves only total ignorance (her Table 4.3), the only parse open to the superlative forms, which cannot prune their subdomain alternatives.

def Mihoc2019.Ignorance.possibleValues {W : Type u_1} (R : SetRel W W) (μ : W → ℕ) (w : W) : Set ℕ

The values of the maximum that the speaker considers possible at w.

Equations

• Mihoc2019.Ignorance.possibleValues R μ w = {x : ℕ | ModalLogic.Diamond R (fun (x_1 : W) => μ x_1 = x) w}

def Mihoc2019.Ignorance.Winner {W : Type u_1} (R : SetRel W W) (μ : W → ℕ) (w : W) : Prop

The speaker knows the value of the maximum, a 'winner' state.

Equations

• Mihoc2019.Ignorance.Winner R μ w = ∃ (x : ℕ), ModalLogic.Box R (fun (x_1 : W) => μ x_1 = x) w

def Mihoc2019.Ignorance.DomainImplicatures {W : Type u_1} (R : SetRel W W) (μ : W → ℕ) (w : W) (T : Finset ℕ) (k : ℕ) : Prop

The implicatures from the size-k subdomain alternatives of T deny each □_S (max ∈ S) pre-exhaustified against the others of its size.

Equations

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

theorem Mihoc2019.Ignorance.box_mem_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {s : Set ℕ} : ModalLogic.Box R (fun (x : W) => μ x ∈ s) w ↔ possibleValues R μ w ⊆ s

theorem Mihoc2019.Ignorance.nonempty_possibleValues {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} [ModalLogic.IsSerial R] : (possibleValues R μ w).Nonempty

theorem Mihoc2019.Ignorance.existsUnique_subset_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {T : Finset ℕ} {k : ℕ} (hT : possibleValues R μ w ⊆ ↑T) (hk : k < T.card) : (∃! S : ↥(Finset.powersetCard k T), possibleValues R μ w ⊆ ↑↑S) ↔ (possibleValues R μ w).ncard = k

Exactly one subdomain of size k contains the possible values iff there are k of them.

theorem Mihoc2019.Ignorance.domainImplicatures_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {T : Finset ℕ} {k : ℕ} (hT : ModalLogic.Box R (fun (x : W) => μ x ∈ ↑T) w) (hk : k < T.card) : DomainImplicatures R μ w T k ↔ (possibleValues R μ w).ncard ≠ k

The implicatures from the subdomain alternatives of size k hold iff the speaker does not consider exactly k values possible.

theorem Mihoc2019.Ignorance.winner_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} [ModalLogic.IsSerial R] : Winner R μ w ↔ (possibleValues R μ w).ncard = 1

theorem Mihoc2019.Ignorance.freeChoice_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {T : Finset ℕ} (hT : ModalLogic.Box R (fun (x : W) => μ x ∈ ↑T) w) : (Exhaustification.FreeChoice R w T fun (x1 : W) (x2 : ℕ) => μ x1 = x2) ↔ (possibleValues R μ w).ncard = T.card

Total ignorance, free choice over the values of T, holds iff as many values are possible as T has.

theorem Mihoc2019.Ignorance.domainImplicatures_one_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {T : Finset ℕ} [ModalLogic.IsSerial R] (hT : ModalLogic.Box R (fun (x : W) => μ x ∈ ↑T) w) (h : 1 < T.card) : DomainImplicatures R μ w T 1 ↔ ¬Winner R μ w

Keeping only the singleton subdomain alternatives rules out a 'winner' state and admits the rest, total ignorance and a 'loser' state that excludes some value without settling one (her Table 4.1).

theorem Mihoc2019.Ignorance.forall_two_le_domainImplicatures_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {T : Finset ℕ} [ModalLogic.IsSerial R] (hT : ModalLogic.Box R (fun (x : W) => μ x ∈ ↑T) w) : (∀ (k : ℕ), 2 ≤ k → k < T.card → DomainImplicatures R μ w T k) ↔ Winner R μ w ∨ Exhaustification.FreeChoice R w T fun (x1 : W) (x2 : ℕ) => μ x1 = x2

Keeping only the subdomain alternatives of size at least two admits exactly a 'winner' state and total ignorance, ruling out a 'loser' state (her Table 4.2).

theorem Mihoc2019.Ignorance.forall_domainImplicatures_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {T : Finset ℕ} [ModalLogic.IsSerial R] (hT : ModalLogic.Box R (fun (x : W) => μ x ∈ ↑T) w) : (∀ (k : ℕ), 0 < k → k < T.card → DomainImplicatures R μ w T k) ↔ Exhaustification.FreeChoice R w T fun (x1 : W) (x2 : ℕ) => μ x1 = x2

Keeping every subdomain alternative, as the superlative forms must, leaves only total ignorance (her Table 4.3).

theorem Mihoc2019.Ignorance.not_box_lessThan_pred_iff {W : Type u_1} {R : SetRel W W} {μ : W → ℕ} {w : W} {n : ℕ} (hT : possibleValues R μ w ⊆ ↑(Finset.range n)) : ¬ModalLogic.Box R (fun (v : W) => (Form.lessThan (n - 1)).tc (μ v)) w ↔ n - 1 ∈ possibleValues R μ w

The scalar implicature of □_S less than n on the full scale, against less than n − 1, holds iff the largest value is possible, so it clashes with a 'loser' state excluding that value and with a 'winner' state settling another (the mixed cells of her Tables 4.1 and 4.2).

def Mihoc2019.Ignorance.zeroRuledOut : SetRel ℕ ℕ

Her 'loser' state for less than three rules out zero, with each world the value of the maximum and the speaker's accessible worlds one and two.

Equations

• Mihoc2019.Ignorance.zeroRuledOut = {p : ℕ × ℕ | p.2 = 1 ∨ p.2 = 2}

instance Mihoc2019.Ignorance.instIsSerialNatZeroRuledOut : ModalLogic.IsSerial zeroRuledOut

theorem Mihoc2019.Ignorance.zeroRuledOut_domainImplicatures : DomainImplicatures zeroRuledOut id 0 (Finset.range 3) 1 ∧ ¬DomainImplicatures zeroRuledOut id 0 (Finset.range 3) 2

The 'loser' state survives the singleton parse open to less than three but not the full parse forced on at most two.

Anti-negativity

Under clausemate negation the subdomain alternatives are negated too, and each pre-exhaustified negated alternative ¬ (max ∈ D i) ∧ max ∈ D j contradicts the negated prejacent, so negating them adds nothing (her Ch. 5 (9)) and exhaustification fails to strengthen the prejacent (not_negExh_lt). The superlative forms require their exhaustification to strengthen the prejacent, so they are deviant under negation, while the comparative forms, without the requirement, are not.

def Mihoc2019.AntiNegativity.negExh {ι : Type u_1} (φ : Form) (D : ι → Set ℕ) (maxD : ℕ) : Prop

Exhaustifying a negated form against its negated subdomain alternatives D, each pre-exhaustified against the others (her Ch. 5 (8)–(9)).

Equations

• Mihoc2019.AntiNegativity.negExh φ D maxD = (¬φ.tc maxD ∧ ∀ (i : ι), ¬Exhaustification.exhAgainst (fun (x1 x2 : ι) => x1 ≠ x2) (fun (j : ι) => maxD ∉ D j) i)

theorem Mihoc2019.AntiNegativity.negExh_iff {ι : Type u_1} {φ : Form} {D : ι → Set ℕ} [Nontrivial ι] (hD : ∀ (i : ι), D i ∈ φ.domainAlts) (maxD : ℕ) : negExh φ D maxD ↔ ¬φ.tc maxD

With two or more subdomain alternatives, exhaustifying the negated form says no more than the negated form.

theorem Mihoc2019.AntiNegativity.not_negExh_lt {ι : Type u_1} {φ : Form} {D : ι → Set ℕ} [Nontrivial ι] (hD : ∀ (i : ι), D i ∈ φ.domainAlts) : ¬negExh φ D < fun (maxD : ℕ) => ¬φ.tc maxD

Exhaustifying the negated form is not strictly stronger than the negated form.