🧵 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
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
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
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
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
@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
@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
text/geminiThis content has been proxied by September (3851b).