Re: How many different unit fractions are lessorequal than all unit fractions? (repleteness)

On 9/20/2024 5:15 PM, Ross Finlayson wrote:

On 09/20/2024 12:26 PM, Jim Burns wrote:

On 9/20/2024 2:10 PM, WM wrote:

On 20.09.2024 19:51, Jim Burns wrote:

Put pencil to paper and
 draw two curves which cross.
There is a point at which
 the curves intersect.

Theorems or axioms?

Here, a theorem.
⎛ (axiom)
⎜ The sets of ZFC exist.
⎜ (theorems)
⎜ ℕ exists
⎜ ℤ exists
⎜ ℚ exists
⎜ The set of Q.subsets
⎜ {S⊆ℚ:∅≠Sᵉᵃᶜʰ<ₑₓᵢₛₜₛSᵉᵃᶜʰ<ᵉᵃᶜʰℚ\S≠∅}
⎜ exists and is the complete ordered field.
⎜ The Intermediate Value Theorem is true of
⎝ {S⊆ℚ:∅≠Sᵉᵃᶜʰ<ₑₓᵢₛₜₛSᵉᵃᶜʰ<ᵉᵃᶜʰℚ\S≠∅}
Here, an axiom.
⎛ (axiom)
⎜ The IVT is true of ordered field 𝔽ᑉᐧⁱᵛᵗ
⎜ (theorem)
⎝ 𝔽ᑉᐧⁱᵛᵗ is Dedekind.complete, and thus is ℝ

"Drawing" a line, "tire en regle", or curve,
has that when you put pencil to paper,
and draw a line, or curve if you will,
and life the pencil and put it back down,
and draw another one, intersecting the first:
the _curves_ cross.
>
... At a point, of for example where
they're incident, they coincide.

Yes.
Because continuous curves must cross,
bounded nonempty set S must have a least.upper.bound.c
⎛ In particular, the function
⎜⎛ 0 above S
⎜⎝ 1 otherwise
⎜ doesn't intersect line y = 1/2  and
⎜ must be discontinuous somewhere  and
⎜ can only be discontinuous at lub.S  and
⎝ lub.S therefore exists.

Then these lines-reals these iota-values
are about the only "standard infinitesimals"
there are: with extent you observe, density
you observe, least-upper-bound as trivial,
and measure as assigned, length assignment.

Lines with the least.upper.bound property
(equivalent to "crossing must intersect")
do not have infinitesimals.
For example,
there are no infinitesimals
between 0 and all the _finite_ unit.fractions.
⎛ Each positive point has
⎜ a finite unit.fraction between it and 0
⎜
⎜⎛ Otherwise,
⎜⎜ greatest.lower.bound β of finite unit.fractions
⎜⎜ is positive, and
⎜⎜ not.bounding 2⋅β > finite ⅟k
⎜⎜ ½⋅β > ¼⋅⅟k
⎜⎜ β > ½⋅β > ¼⋅⅟k
⎜⎜ greatest.lower.bound β is not.bounding,
⎝⎝ which is gibberish.