Ancestors

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

🧵 A little thread on constructive mathematics and (tight) apartness relations in particular

[#]logic #math #constructiveMathematics

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

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

An apartness relation on a set X is a binary relation ♯ on X that is symmetric, irreflexive and cotransitive. The latter means that x ♯ y implies x ♯ z or y ♯ z for any x,y,z ∈ X.

An apartness relation ♯ is said to be tight if any two elements are equal as soon as they are not apart: ¬ (x ♯ y) ⇒ (x = y) for all x,y ∈ X.

It's not hard to show that in classical mathematics any set has exactly one tight apartness, namely x ♯ y := x ≠ y.

What happens constructively?

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

Toot

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

Because constructive mathematics is a generalization of classical mathematics, we cannot exhibit a set with two distinct apartness relations as that would contradict the law of excluded middle which is undecided in (neutral) constructive mathematics.

However, we can give a (simple!) example of set with two apartness relations such that the two relations cannot be shown to be the same.

More precisely, if the two relations were the same, then a so-called constructive taboo must hold.

A constructive taboo is a statement that is not constructively provable and false in some models.

What is funny is that the taboo in this case is an implication between taboos!

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

Descendants

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

For α : ℕ → 𝟚, let's say that α has a root if there exists n ∈ ℕ such that α n = 0.

Bishop's Limited Principle of Omniscience (LPO) says:

For any α : ℕ → 𝟚, it is decidable whether α has a root, i.e.

(∃ n ∈ ℕ . α n = 0) ∨ ¬ (∃ n ∈ ℕ . α n = 0).

Bishop's Weak Limited Principle of Omniscience (WLPO) says:

For any α : ℕ → 𝟚, it is decidable whether α does not have a root, i.e.

¬ (∃ n ∈ ℕ . α n = 0) ∨ ¬¬ (∃ n ∈ ℕ . α n = 0).

Both LPO and WLPO are constructive taboos and both are simple instances of the law of excluded middle.

Clearly, LPO implies WLPO, but the converse (WLPO ⇒ LPO) is actually a constructive taboo.

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

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 | More toots from de_Jong_Tom@mathstodon.xyz

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

The above is all formalized in the #Agda TypeTopology development, see

https://martinescardo.github.io/TypeTopology/Apartness.Properties.html#At-Most-One-Tight-Apartness-on-Cantor-gives-WLPO-implies-LPO

A (topological) model of intuitionistic set theory validating WLPO but not LPO is given in the below paper (see its fifth page and Theorem 5.1 in particular).

Matt Hendtlass and Robert Lubarsky. 'Separating Fragments of WLEM, LPO, and MP'

The Journal of Symbolic Logic. Vol. 81, No. 4, 2016, pp. 1315-1343.

DOI: 10.1017/jsl.2016.38

URL: https://www.math.fau.edu/people/faculty/lubarsky/separating-llpo.pdf

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

Written by Martin Escardo on 2025-02-01 at 21:29

@de_Jong_Tom

Let me say that on Friday morning I conjectured that any type has at most one tight apartness relation, and that Tom is proving me wrong in this thread.

=> More informations about this toot | More toots from MartinEscardo@mathstodon.xyz

Written by soaproot on 2025-02-02 at 14:29

@MartinEscardo @de_Jong_Tom Good conjectures have interesting answers, but those answers don't have to be "yes".

It is particularly satisfying to see an answer formulated and in TypeTopology so quickly.

=> More informations about this toot | More toots from soaproot@sfba.social

Written by soaproot on 2025-02-02 at 15:18

@de_Jong_Tom @MartinEscardo I have stated this theorem and outlined its proof in metamath notation (hopefully correctly) at https://github.com/metamath/set.mm/issues/4620 .

=> More informations about this toot | More toots from soaproot@sfba.social