Itzhaki (2021): Qualitative versus Quantitative Representation: A Non-Standard Analysis of the Sorites Paradox

Itzhaki traces the Sorites paradox to the conflation of two maps from individuals to degrees. A quantitative map sends a pile to its number of grains and a person to their height, in an Archimedean scale; a qualitative map sends piles and changes into the hyperreals. A heap gets an infinite qualitative size, so that adding or removing a grain never crosses between heaps and non-heaps, and a change of one millimetre gets an infinitesimal qualitative magnitude, so that the standard part of a height ignores it. The premises of each Sorites are then jointly satisfiable under the qualitative map and inconsistent under the quantitative one, and the conclusion of the argument follows from its premises only when the inverse of the size map is total.

A soritical argument is one schema, Sorites: a base case, tolerance along a step relation, and a counterexample. The classic and the reverse paradox of the heap are its instances along steps of one grain, read through either size map.

Main statements

• Itzhaki2021.Sorites.conclusion, Itzhaki2021.Sorites.false_of_total: the conclusion of a Sorites follows from its premises when the inverse of the size map is total, and the premises are then inconsistent.
• Itzhaki2021.sorites_not_heap, Itzhaki2021.sorites_heap: under the qualitative size, the classic and the reverse paradox of the heap hold for any heap predicate with a heap and a non-heap, while under the quantitative size of the model they are inconsistent (Itzhaki2021.Model55.not_sorites_size).
• Itzhaki2021.induction_premise, Itzhaki2021.conclusion_tall, Itzhaki2021.not_forall_sub_natCast_ge: with an infinitesimal unit of change the premises of the tall paradox hold, and with the quantitative unit its conclusion fails.
• Itzhaki2021.instIsTransInfinitelyLess, Itzhaki2021.merged_iff, Itzhaki2021.not_merged_qualSize: being infinitely less is transitive, and the merged paradox of the small heap is satisfiable exactly when the qualitative sizes of its two heaps are infinitely apart, which the qualitative size of the heap paradox never makes them.

Implementation notes

• The finite and the infinitesimal hyperreals are mathlib's subgroups of archimedean classes at least and above that of 1, and the standard part is mathlib's stdPart.
• Whether the size of a heap is known is a parameter of the qualitative size; no result depends on it.
• The pluralities of the heap model are their sizes, as the paper reduces them (fn. 23), and the individuals of the tall model their heights in millimetres.
• As printed, (9d) claims that an infinite number times a nonzero finite one is infinite, which ω * ε = 1 refutes (not_forall_mk_mul_neg), and (80) is unsatisfiable under the qualitative size (36) (not_merged_qualSize).

References

• [Itz21]
• [Ken07b]
• [Lin83]
• [Wil94]

Finite, infinitesimal and infinite hyperreals

@[reducible, inline]

noncomputable abbrev Itzhaki2021.infinitesimals : AddSubgroup ℝ*

The infinitesimal hyperreals, those of archimedean class above that of 1 (7b).

Equations

• Itzhaki2021.infinitesimals = ArchimedeanClass.ballAddSubgroup 0

@[reducible, inline]

noncomputable abbrev Itzhaki2021.finites : AddSubgroup ℝ*

The finite hyperreals, those of archimedean class at least that of 1 (7a).

Equations

• Itzhaki2021.finites = ArchimedeanClass.closedBallAddSubgroup 0

theorem Itzhaki2021.mem_infinitesimals {a : ℝ*} : a ∈ infinitesimals ↔ 0 < ArchimedeanClass.mk a

theorem Itzhaki2021.mem_finites {a : ℝ*} : a ∈ finites ↔ 0 ≤ ArchimedeanClass.mk a

def Itzhaki2021.InfinitesimallyClose (a b : ℝ*) : Prop

a is indistinguishable from b when their difference is infinitesimal (10).

Equations

• Itzhaki2021.InfinitesimallyClose a b = (a - b ∈ Itzhaki2021.infinitesimals)

def Itzhaki2021.FinitelyClose (a b : ℝ*) : Prop

a and b are finitely close when their difference is finite (74).

Equations

• Itzhaki2021.FinitelyClose a b = (a - b ∈ Itzhaki2021.finites)

def Itzhaki2021.InfinitelyLess (a b : ℝ*) : Prop

a is infinitely less than b when it is less and not finitely close (78).

Equations

• Itzhaki2021.InfinitelyLess a b = (a < b ∧ ¬Itzhaki2021.FinitelyClose a b)

instance Itzhaki2021.instIsEquivHyperrealInfinitesimallyClose : IsEquiv ℝ* InfinitesimallyClose

Being indistinguishable is an equivalence relation (11).

theorem Itzhaki2021.FinitelyClose.refl (a : ℝ*) : FinitelyClose a a

theorem Itzhaki2021.FinitelyClose.symm {a b : ℝ*} (h : FinitelyClose a b) : FinitelyClose b a

theorem Itzhaki2021.FinitelyClose.trans {a b c : ℝ*} (h₁ : FinitelyClose a b) (h₂ : FinitelyClose b c) : FinitelyClose a c

instance Itzhaki2021.instIsEquivHyperrealFinitelyClose : IsEquiv ℝ* FinitelyClose

Being finitely close is an equivalence relation (fn. 31).

theorem Itzhaki2021.not_infinitesimallyClose_coe {r s : ℝ} (h : r ≠ s) : ¬InfinitesimallyClose ↑r ↑s

Distinct reals are distinguishable (14), so a taller person's height is never indistinguishable from a shorter one's (67).

theorem Itzhaki2021.stdPart_sub_infinitesimal (r : ℝ) {e : ℝ*} (he : e ∈ infinitesimals) : ArchimedeanClass.stdPart (↑r - e) = r

The standard part of a real minus an infinitesimal is the real (22).

theorem Itzhaki2021.not_forall_mk_mul_neg : ¬∀ (H a : ℝ*), ArchimedeanClass.mk H < 0 → a ≠ 0 → 0 ≤ ArchimedeanClass.mk a → ArchimedeanClass.mk (H * a) < 0

An infinite number times a nonzero finite one need not be infinite, against (9d) as printed.

theorem Itzhaki2021.exists_sub_of_mk_nonneg {a : ℝ*} (ha : 0 ≤ ArchimedeanClass.mk a) : ∃ (G : ℝ*) (H : ℝ*), ArchimedeanClass.mk G < 0 ∧ ArchimedeanClass.mk H < 0 ∧ a = G - H

Every finite number is a difference of two infinite ones (§2.2.2).

theorem Itzhaki2021.mk_add_natCast_nonneg {a : ℝ*} (ha : 0 ≤ ArchimedeanClass.mk a) (n : ℕ) : 0 ≤ ArchimedeanClass.mk (a + ↑n)

Adding a natural number keeps a number finite (38a).

theorem Itzhaki2021.mk_sub_natCast_neg {a : ℝ*} (ha : ArchimedeanClass.mk a < 0) (n : ℕ) : ArchimedeanClass.mk (a - ↑n) < 0

Subtracting a natural number keeps a number infinite (38b).

The soritical argument

structure Itzhaki2021.Sorites {α : Type u_1} (P : α → Prop) (R : α → α → Prop) (a b : α) : Prop

A soritical argument has a base case a with P, tolerance of P along R, and a counterexample b without P, premises I, II and IV of (1) and (2).

• base : P a
• tolerance ⦃x y : α⦄ : P x → R x y → P y
• counter : ¬P b

theorem Itzhaki2021.Sorites.not_reflTransGen {α : Type u_1} {P : α → Prop} {R : α → α → Prop} {a b : α} (h : Sorites P R a b) : ¬Relation.ReflTransGen R a b

No chain of steps leads from a to b, since it would cross from P out of P in a single step.

theorem Itzhaki2021.Sorites.of_reflTransGen {α : Type u_1} {P : α → Prop} {R : α → α → Prop} {a b : α} (h : Sorites P R a b) {y : α} (hy : Relation.ReflTransGen R a y) : P y

Whatever a chain of steps leads to from a has P.

def Itzhaki2021.Step {α : Type u_1} (s : α → ℝ*) (d : ℝ*) (x y : α) : Prop

y is one step d above x along the size map s.

Equations

• Itzhaki2021.Step s d x y = (s y = s x + d)

theorem Itzhaki2021.Sorites.conclusion {α : Type u_1} {P : α → Prop} {a b : α} {s : α → ℝ*} {d : ℝ*} (h : Sorites P (Step s d) a b) (hs : Function.Injective s) (n : ℕ) : (∀ m < n, ∃ (x : α), s x = s a + ↑m * d) → ∀ (y : α), s y = s a + ↑n * d → P y

The conclusion of a Sorites (52.III) follows from its premises when every intermediate value is the size of some individual, the totality of the inverse of the size map (44)–(46).

theorem Itzhaki2021.Sorites.false_of_total {α : Type u_1} {P : α → Prop} {a b : α} {s : α → ℝ*} {d : ℝ*} (h : Sorites P (Step s d) a b) (hs : Function.Injective s) (n : ℕ) (htot : ∀ m < n, ∃ (x : α), s x = s a + ↑m * d) (hb : s b = s a + ↑n * d) : False

When the inverse of the size map is total and b is reached arithmetically from a, the premises of a Sorites are inconsistent.

Collective nouns

noncomputable def Itzhaki2021.qualSize {De : Type u_2} (heap known : De → Prop) [DecidablePred heap] [DecidablePred known] (size : De → ℕ) (H : ℝ*) (x : De) : ℝ*

The qualitative size (36) maps a heap of known size to H plus its size, a heap of unknown size to H, and anything else to its size.

Equations

• Itzhaki2021.qualSize heap known size H x = if heap x then if known x then H + ↑(size x) else H else ↑(size x)

theorem Itzhaki2021.qualSize_of_not_heap {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {x : De} (hx : ¬heap x) : qualSize heap known size H x = ↑(size x)

theorem Itzhaki2021.mk_qualSize_nonneg {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {x : De} (hx : ¬heap x) : 0 ≤ ArchimedeanClass.mk (qualSize heap known size H x)

What is not a heap has finite qualitative size (37a).

theorem Itzhaki2021.mk_qualSize_neg {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {x : De} (hH : ArchimedeanClass.mk H < 0) (hx : heap x) : ArchimedeanClass.mk (qualSize heap known size H x) < 0

A heap has infinite qualitative size when H is infinite (37b).

theorem Itzhaki2021.natCast_lt_qualSize {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {x : De} (hH : ArchimedeanClass.mk H < 0) (hpos : 0 < H) (hx : heap x) (n : ℕ) : ↑n < qualSize heap known size H x

A heap's qualitative size exceeds every natural number when H is positive and infinite (37b).

theorem Itzhaki2021.finitelyClose_qualSize {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {x y : De} (hx : heap x) (hy : heap y) : FinitelyClose (qualSize heap known size H x) (qualSize heap known size H y)

The qualitative sizes of two heaps are finitely close.

theorem Itzhaki2021.sorites_not_heap {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} (hH : ArchimedeanClass.mk H < 0) {g₁ g : De} (h₁ : ¬heap g₁) (hg : heap g) : Sorites (fun (x : De) => ¬heap x) (Step (qualSize heap known size H) 1) g₁ g

Under the qualitative size, a non-heap and a heap make the classic paradox of the heap consistent (52), since adding a grain to a non-heap never yields a heap (38a).

theorem Itzhaki2021.sorites_heap {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} (hH : ArchimedeanClass.mk H < 0) {g₁ g : De} (h₁ : ¬heap g₁) (hg : heap g) : Sorites heap (Step (qualSize heap known size H) (-1)) g g₁

Under the qualitative size, the reverse paradox of the heap is consistent too (54), since removing a grain from a heap never yields a non-heap (38b).

theorem Itzhaki2021.natCast_size_notMem_range {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {x : De} (hH : ArchimedeanClass.mk H < 0) (hs : Function.Injective size) (hx : heap x) : ↑(size x) ∉ Set.range (qualSize heap known size H)

The size of a heap is nobody's qualitative size (47a).

theorem Itzhaki2021.add_natCast_size_notMem_range {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {x : De} (hH : ArchimedeanClass.mk H < 0) (hs : Function.Injective size) (hx : ¬heap x) (hpos : 0 < size x) : H + ↑(size x) ∉ Set.range (qualSize heap known size H)

H plus the size of a non-heap is nobody's qualitative size (47b).

The model of the heap

@[reducible, inline]

abbrev Itzhaki2021.Model55.De : Set ℕ

The pluralities of 1 to 10,000 grains, one of each size.

Equations

• Itzhaki2021.Model55.De = Set.Icc 1 10000

def Itzhaki2021.Model55.heap (x : ↑De) : Prop

Only the plurality of 10,000 grains is a heap.

Equations

• Itzhaki2021.Model55.heap x = (↑x = 10000)

@[instance_reducible]

instance Itzhaki2021.Model55.instDecidablePredElemNatDeHeap : DecidablePred heap

Equations

• Itzhaki2021.Model55.instDecidablePredElemNatDeHeap x = { decide := (↑x).beq 10000, reflects_decide := ⋯ }

def Itzhaki2021.Model55.g₁ : ↑De

One grain.

Equations

• Itzhaki2021.Model55.g₁ = ⟨1, Itzhaki2021.Model55.g₁._proof_1⟩

def Itzhaki2021.Model55.g₁₀₀₀₀ : ↑De

10,000 grains.

Equations

• Itzhaki2021.Model55.g₁₀₀₀₀ = ⟨10000, Itzhaki2021.Model55.g₁₀₀₀₀._proof_1⟩

@[reducible, inline]

noncomputable abbrev Itzhaki2021.Model55.qs : ↑De → ℝ*

The qualitative size of the model, every size known and H = ω.

Equations

• Itzhaki2021.Model55.qs = Itzhaki2021.qualSize Itzhaki2021.Model55.heap (fun (x : ↑Itzhaki2021.Model55.De) => True) Subtype.val Hyperreal.omega

theorem Itzhaki2021.Model55.sorites_qs : Sorites (fun (x : ↑De) => ¬heap x) (Step qs 1) g₁ g₁₀₀₀₀

The classic paradox of the heap holds of the qualitative size (52).

theorem Itzhaki2021.Model55.sorites_qs_reverse : Sorites heap (Step qs (-1)) g₁₀₀₀₀ g₁

The reverse paradox holds of the qualitative size (54).

theorem Itzhaki2021.Model55.not_sorites_size : ¬Sorites (fun (x : ↑De) => ¬heap x) (Step (fun (x : ↑De) => ↑↑x) 1) g₁ g₁₀₀₀₀

Under the quantitative size, the premises of the classic paradox are inconsistent.

Gradable adjectives

noncomputable def Itzhaki2021.qualUnit (U : ℝ) (e : ℝ*) (r : ℝ) : ℝ*

The qualitative magnitude (62) of a change r is an infinitesimal e when r is below the smallest contextually relevant unit U, and r otherwise.

Equations

• Itzhaki2021.qualUnit U e r = if r < U then e else ↑r

theorem Itzhaki2021.mem_infinitesimals_of_forall_mul_le {u : ℝ*} {c : ℝ} (hu : 0 < u) (h : ∀ (n : ℕ), ↑n * u ≤ ↑c) : u ∈ infinitesimals

A positive unit of change whose every multiple stays below a real bound is infinitesimal (61).

theorem Itzhaki2021.induction_premise {E : Type u_2} {tall : E → ℝ} {S U : ℝ} {e : ℝ*} (he : e ∈ infinitesimals) (hU : 1 < U) {x : E} (hx : x ∈ tall ⁻¹' Set.Ici S) : S ≤ ArchimedeanClass.stdPart (↑(tall x) - qualUnit U e 1)

With a millimetre below the relevant unit, the induction premise (63) holds, since the standard part of the height of anyone tall, less the qualitative millimetre, still meets the standard.

theorem Itzhaki2021.conclusion_tall {S U : ℝ} {e : ℝ*} (he : e ∈ infinitesimals) (hU : 1 < U) (hS : S ≤ 2000) (n : ℕ) : S ≤ ArchimedeanClass.stdPart (2000 - ↑n * qualUnit U e 1)

With a millimetre below the relevant unit, the conclusion (70.III) holds, since any number of qualitative millimetres below two metres is still tall.

theorem Itzhaki2021.not_forall_sub_natCast_ge {S U : ℝ} {e : ℝ*} (hU : U ≤ 1) (hS : 1000 < S) : ¬∀ (n : ℕ), S ≤ ArchimedeanClass.stdPart (2000 - ↑n * qualUnit U e 1)

With the quantitative unit, the conclusion of the tall paradox fails for any standard above one metre (66).

The merged paradox

def Itzhaki2021.LeUpToFinite (a b : ℝ*) : Prop

a is at most b up to a finite difference when they are finitely close or a is infinitely less (79).

Equations

• Itzhaki2021.LeUpToFinite a b = (Itzhaki2021.FinitelyClose a b ∨ Itzhaki2021.InfinitelyLess a b)

instance Itzhaki2021.instIsTransInfinitelyLess : IsTrans ℝ* InfinitelyLess

Being infinitely less is transitive (78).

theorem Itzhaki2021.InfinitelyLess.of_finitelyClose {a b c : ℝ*} (hab : FinitelyClose a b) (hbc : InfinitelyLess b c) : InfinitelyLess a c

What is finitely close to something infinitely less than c is infinitely less than c.

theorem Itzhaki2021.leUpToFinite_iff_not_infinitelyLess {a b : ℝ*} : LeUpToFinite a b ↔ ¬InfinitelyLess b a

theorem Itzhaki2021.LeUpToFinite.add_one {a S : ℝ*} (h : LeUpToFinite a S) : LeUpToFinite (a + 1) S

One grain is negligible for a standard of size (80.II). What is at most the standard up to a finite difference stays so after adding a grain.

theorem Itzhaki2021.finitelyClose_or_infinitelyLess {a b : ℝ*} (h : a < b) : FinitelyClose a b ∨ InfinitelyLess a b

Of two heaps whose qualitative sizes are ordered, the larger is either finitely close or infinitely larger, never both (81).

theorem Itzhaki2021.merged_iff {De : Type u_3} {s : De → ℝ*} {g₅₀ g : De} : (∃ (S : ℝ*), Sorites (fun (x : De) => LeUpToFinite (s x) S) (Step s 1) g₅₀ g) ↔ InfinitelyLess (s g₅₀) (s g)

The merged paradox (80) has a standard of size making it consistent exactly when the qualitative sizes of its small heap and its large heap are infinitely apart.

theorem Itzhaki2021.not_merged_qualSize {De : Type u_3} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} {g₅₀ g : De} (h₅₀ : heap g₅₀) (hg : heap g) : ¬∃ (S : ℝ*), Sorites (fun (x : De) => LeUpToFinite (qualSize heap known size H x) S) (Step (qualSize heap known size H) 1) g₅₀ g

Under the qualitative size (36), the merged paradox (80) is unsatisfiable, since two heaps are never infinitely apart.