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