Re: The set of necessary FISONs

On 3/10/2025 1:20 PM, WM wrote:

On 10.03.2025 17:31, Jim Burns wrote:

For example, here:
⎛ A  FISON is linearly ordered,
⎜ begins at 0, ends at a FISON.end,

>
That is sufficient.

Insufficient.

And that is what I use, except 0.

Then don't use that. It's insufficient.

That description isn't the usual description.
I'd guess the Peano axioms are the usual.

>
It is irrelevant what you prefer.
Zermelo, Peano, v. Neumann.
All use the same induction.

For FISONs _as I describe them_
⎛ A  FISON is linearly ordered,
⎜ begins at 0, ends at a FISON.end, and,
⎜ for each split,
⎜ its foresplit ends at i or is empty  and
⎜ its hindsplit begins at j or is empty,
⎝ i and j such that i+1 = j
the proof.by.induction
⎛ This is an inductive property.
⎝ Therefore, this a property with no exceptions.
is
reliable.
⎛ Assume otherwise.
⎜ Assume
⎜ A(k) is inductive on FISON.numbers
⎜  A(0) ∧ ∀k:∃⁽ꟳ⁾F′∋k: A(k)⇒A(k+1)
⎜ and
⎜ FISON.number 𝔊 exists such that ¬A(𝔊)
⎜
⎜ {F} ∋ F(𝔊) = [0,𝔊] ∋ 𝔊
⎜
⎜ From property A(k)
⎜ define sweep A{≤k}
⎜ A{≤k}  ⇔  ∀j≤k: A(j)
⎜
⎜ A{≤k+1}  ⇔  A{≤k} ∧ A(k+1)
⎜
⎜ Sweep A{≤k} determines a split of [0,𝔊]
⎜ F′ = {i:A{≤i}} ∋ 0
⎜ H′ = {j:¬A{≤j}} ∋ 𝔊
⎜ F′ ᵉᵃᶜʰ<ᵉᵃᶜʰ H′
⎜
⎜ [0,𝔊] is a FISON.
⎜ F′ holds last i′
⎜ H′ holds first j′
⎜ i′+1 = j′
⎜
⎜ From the definition of F′ and H′
⎜ A{≤i′} ∧ ¬A{≤i′+1}
⎜
⎜ A{≤i′} ∧ ¬(A{≤i′} ∧ A(i'+1))
⎜
⎜ A{≤i′} ∧ ¬A(i'+1)
⎜
⎜ A(i′) ∧ ¬A(i'+1)
⎜
⎜ ¬(A(i′)⇒A(i′+1))
⎜
⎜ However,
⎜ ∀k:∃⁽ꟳ⁾F′∋k: A(k)⇒A(k+1)
⎜
⎜ A(i′)⇒A(i′+1)
⎝ Contradiction.
Therefore,
the proof.by.induction on FISON.numbers
⎛ This is an inductive property.
⎝ Therefore, this a property with no exceptions.
is
reliable.