Re: The set of necessary FISONs

On 2/6/2025 3:54 AM, WM wrote:

On 06.02.2025 01:46, Jim Burns wrote:

On 2/5/2025 2:18 PM, WM wrote:

On 05.02.2025 19:43, Jim Burns wrote:

On 2/5/2025 12:32 PM, WM wrote:

On 05.02.2025 18:19, Jim Burns wrote:

Either way, the axioms do not create,
but only describe.

>
The axioms of
non-standard analysis or string theory
create.

>
The axioms of
non-standard analysis or string theory
do not create, but only describe.

The axiom of induction:

[...]

A description, not a magic spell.
>
...which could also be written...

>
Why should we use two different writings?

Two are unnecessary.
The axiom of induction:
∀P:ℕ₁→{⊤,⊥}:
P(1) ∧ ∀k∈ℕ₁:P(k)⇒P(k+1) ⇒ ∀n∈ℕ₁:P(n)
P(1) :⇔ ⋃({F(j):j∈ℕ₁}\{F(1)})=ℕ₁
⎛ P(k) :⇔ ⋃({F(j):j∈ℕ₁}\{F(j):(j≤k)∧j∈ℕ₁})=ℕ₁
⎜ ⇒
⎝ P(k+1) :⇔ ⋃({F(j):j∈ℕ₁}\{F(j):(j≤k+1)∧j∈ℕ₁})=ℕ₁
----
F(j) = {i∈ℕ₁:i≤j}
P(k) ⇔ ⋃{{i∈ℕ₁:(i≤j)}:(k<j)∧j∈ℕ₁}=ℕ₁

I can remove all FISONs from U(F(n))
without changing the claimed union.

>
What you (WM) mean by 'remove all...without changing..."
is that, by induction,

∀n∈ℕ₁:P(n)
which is true because                  [!]
∀ᴺ¹n: ∀i′∈ℕ₁: ∃ᴺ¹j′: i′≤j′ ∧ n<j′ ∧
  i′ ∈ ⋃{{i∈ℕ₁:(i≤j)}:(n<j)∧j∈ℕ₁}
Proof: Let j′ = max{n+1,i′}. Done.
The key is that  ∀ᴺ¹n: ∃ᴺ¹j′: n<j′
----
∀ᴺ¹n: ∀i′∈ℕ₁:
  i′ ∈ ⋃{{i∈ℕ₁:(i≤j)}:(n<j)∧j∈ℕ₁}
∀ᴺ¹n: ℕ₁ ⊆ ⋃{{i∈ℕ₁:(i≤j)}:(n<j)∧j∈ℕ₁}
And also,
∀ᴺ¹n: ℕ₁ ⊇ ⋃{{i∈ℕ₁:(i≤j)}:(n<j)∧j∈ℕ₁}
∀ᴺ¹n: ℕ₁ = ⋃{{i∈ℕ₁:(i≤j)}:(n<j)∧j∈ℕ₁}
∀n∈ℕ₁:P(n)

it is proved that all F(n) can be subtracted
like
by induction
all natural numbers can be subtracted from ℕ:
>
{1} can be subtracted
because it is an element of in ℕ.
If {n} has been subtracted,
then {n+1} can be subtracted
because it is an element of in ℕ.
>
By the axiom of induction
the result is the empty set.

You (WM) agree that  ∀ᴺ¹n: ∃ᴺ¹j′: n<j′
⎛ Before all swaps n⇄n+1
⎜ Bob is in the first room, room 1.
⎜
⎜ After all swaps n⇄n+1
⎜ Bob is not in the first room, and
⎜ Bob is not in any room which he has swapped into
⎝ because it has a swap.out later than its swap.in.