Re: The set of necessary FISONs

On 2/16/2025 6:18 AM, WM wrote:

On 16.02.2025 00:52, Jim Burns wrote:

{F} has only one inductive subset: {F}

>
Correct.

1.
Prove that a proof by induction
is a proof
2.
Prove by induction.
1.
Prove ℕ has an only.inductive.subset ℕ
Prove {S⊆ℕ:inductive.S} = {ℕ}
⎛ For example:
⎜ For inductive Z
⎜ let ℕ = ⋂{S⊆Z:inductive.S}
⎜
⎜⎛ The intersection of inductive sets is
⎜⎝ is an inductive set.
⎜
⎜ ℕ is inductive
⎜ ℕ ⊆ᵉᵃᶜʰ {S⊆Z:inductive.S}
⎜
⎜ {S⊆ℕ:inductive.S} ⊆ {S⊆Z:inductive.S}
⎜ ℕ ⊆ᵉᵃᶜʰ {S⊆ℕ:inductive.S}
⎜
⎜ ∀S′ ∈ {S⊆ℕ:inductive.S}:
⎜ ℕ ⊆ S′  ∧
⎜ S′ ⊆ ℕ  ∧  S′ = ℕ
⎜
⎝ {S⊆ℕ:inductive.S} = {ℕ}
2.
Prove {i∈ℕ:A(i)} is any inductive subset.
⎛ For example
⎜ let Aᶠˡⁱᵍ(k) == "finitely.many < k < infinitely many"
⎜
⎜ finitely.many < 0 < infinitely many
⎜ 0 ∈ {i∈ℕ:Aᶠˡⁱᵍ(i)}
⎜
⎜ If finitely.many < k < infinitely many
⎜ then finitely.many < k+1 < infinitely many
⎜ k ∈ {i∈ℕ:Aᶠˡⁱᵍ(i)}  ⇒  k+1 ∈ {i∈ℕ:Aᶠˡⁱᵍ(i)}
⎜
⎝ inductive {i∈ℕ:Aᶠˡⁱᵍ(i)}
{i∈ℕ:Aᶠˡⁱᵍ(i)} ∈ {S⊆ℕ:inductive.S}
{i∈ℕ:Aᶠˡⁱᵍ(i)} ∈ (ℕ}   [from 1]
{i∈ℕ:Aᶠˡⁱᵍ(i)} is the only.inductive.subset.
{i∈ℕ:Aᶠˡⁱᵍ(i)} = ℕ
∀k ∈ {i∈ℕ:Aᶠˡⁱᵍ(i)}: Aᶠˡⁱᵍ(k)
∀k ∈ ℕ: Aᶠˡⁱᵍ(k)   [from 1]
∀k ∈ ℕ:  finitely.many < k < infinitely many

All elements can be omitted.

Proven:  ∀k ∈ ℕ: Omissible(k)

The set can be omitted.

Not proven:  Omissible(ℕ)