Re: The set of necessary FISONs

On 2/21/2025 4:19 AM, WM wrote:

On 20.02.2025 20:46, Jim Burns wrote:

On 2/20/2025 12:50 PM, WM wrote:

On 20.02.2025 15:30, Jim Burns wrote:

AXIOM I 'extensionality' means
proving each FISON is omissible  is no
proving {F} is omissible.

>
∀n ∈ ℕ: n+1 ∈ ℕ.
Together with 1 ∈ ℕ this defines the set ℕ.
 (*)

>
You (WM) have left out that
ℕ is the only.inductive.subset of ℕ

>
ℕ_def to be precise.

To be precise,
the set which is
its own only.inductive.subset
is
the set for which
proofs.by.induction are reliable.
⎛ ... for each version of induction, there is
⎜ a version of the set ℕ which
⎜ is its own only.inductive.subset
⎜
⎜ For inductive′ S meaning
⎜  1 ∈ S ∧ ∀n∈S: S ∋ n+1
⎜ ℕ′ = {1,2,3,...}
⎜
⎜ For inductive″ S meaning
⎜  {} ∈ S ∧ ∀a∈S: S ∋ {a}
⎜ ℕ″ = {{},{{}},{{{}}},...}
⎜
⎜ For inductive‴ S meaning
⎜  F₁ = {1} ∈ S ∧ ∀F∈S: S ∋ F∪{1+max.F}
⎜ ℕ‴ = {F₁,F₂,F₃,...}
⎜
⎝ ...
If
you (WM) give the set which is
its own only.inductive′.subset
the name ℕ_def,
and ℕ′ ⊃≠ ℕ_def
then
proofs.by.induction′ are unreliable for ℕ′

S⊆ℕ ∧ 1∈S ∧ ∀n∈S:n+1∈S ⇒ S=ℕ
  (**)
>

Addition of all numbers defined by (*)
to the empty set
is tantamount to addition of ℕ to the empty set.

>
{**} prevents the addition of extra elements.

>
No extra elements are available and
no extra elements shall be added.

⎛ ℕ′ is its own only.inductive′.subset
⎜ S⊆ℕ ∧ 1∈S ∧ ∀n∈S:n+1∈S ⇒ S=ℕ
⎝  (**)
is
how to say ℕ′ has no extra elements.

Subtraction of all numbers defined by (*)
from ℕ
is tantamount to subtraction of ℕ from ℕ.
>
Homework:
Prove the same for FISONs or v. Neumann ordinals.

>
(!) Have you (WM) started reading my proofs?

>
Why should I? I discuss my proof.

Why are you asking me for proofs you won't read?

For the sets of all (finite) FISONs and
of all finite von Neumann ordinals,
(**) is satisfied as a consequence of
the finitude of their elements.

>
S = ℕ_def

ℕ_def = ℕ′
S = {i:A(i)}
⎛ A(1)  ∧  ∀n∈ℕ′:A(n)⇒A(n+1)   ⇒
⎜ {i:A(i)} ∈ {S″⊆ℕ′:inductive.S″}
⎜
⎜ {S″⊆ℕ′:inductive.S″} = {ℕ′}
⎜ ⇐ all and only finites are in ℕ′
⎜
⎜ ( {ℕ′} ≠ ℕ′ )
⎜
⎜ {i:A(i)} ∈ {S″⊆ℕ′:inductive.S″}  ∧
⎜ {S″⊆ℕ′:inductive.S″} = {ℕ′}  ⇒
⎜ {i:A(i)} = ℕ′
⎜
⎜ {i:A(i)} = ℕ′  ∧
⎜ ∀k ∈ {i:A(i)}: A(k)  ⇒
⎝ ∀k ∈ ℕ′: A(k)
Proof by induction for ℕ′
  ⇐ all and only finites are in ℕ′