Toot

Written by Tom de Jong on 2025-02-01 at 21:02

Theorem: If the Cantor set (ℕ → 𝟚) has at most one tight apartness then WLPO implies LPO.

Proof:

The canonical apartness on the Cantor set is given by

α ♯ β := ∃ n ∈ ℕ . α n ≠ β n,

and it is well known (in constructive mathematics) that it is tight.

Another apartness is given by

α ♯₂ β := ∃ p : (ℕ → 𝟚) → 𝟚 . p α ≠ p β.

That this one is tight is due to @MartinEscardo and may be phrased as "the Cantor set is totally separated", see https://martinescardo.github.io/TypeTopology/TypeTopology.TotallySeparated.html.

Assuming WLPO, we can define

P : (ℕ → 𝟚) → 𝟚

P α := ¬ (α has a root).

Now, writing 𝟏 for the binary sequence that is always 1, we have, for any α : ℕ → 𝟚:

P α ≠ P 𝟏 if and only if ¬¬ (α has a root).

Hence, α ♯₂ 𝟏 if and only ¬¬ (α has a root), while α ♯ 𝟏 if and only if α has a root.

Thus, if the Cantor set has at most one tight apartness then

¬¬ (α has a root) ⇒ α has a root.

Together with WLPO which implies that ¬ (α has a root) is decidable, we get that it is decidable whether α has a root, i.e. LPO. ∎

=> More informations about this toot | View the thread | More toots from de_Jong_Tom@mathstodon.xyz

Mentions

=> View MartinEscardo@mathstodon.xyz profile

Tags