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 | View the thread
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
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 | View the thread
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 | View the thread
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 | View the thread
𧡠A little thread on constructive mathematics and (tight) apartness relations in particular
[#]logic #math #constructiveMathematics
=> More informations about this toot | View the thread
βAbstractβ
While ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus far been missing. We present two seemingly different definitions of constructive ordinal exponentiation in the setting of homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by SierpiΕski based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. All our results are formalized in the proof assistant Agda.
=> More informations about this toot | View the thread
I'm pleased to advertise our latest paper titled "Ordinal Exponentiation in Homotopy Type Theory".
https://arxiv.org/abs/2501.14542
This is joint work with @fnf @Nicolai_Kraus and Chuangjie Xu.
All our results are formalized in Agda, building on @MartinEscardo's TypeTopology development, see the HTML version at https://ordinal-exponentiation-HoTT.github.io/
In particular, the Paper file links every numbered environment in the paper to its implementation in Agda.
[#]logic #TypeTheory #HoTT #Agda
=> More informations about this toot | View the thread
The slides for my speed talk on our JSL paper about epimorphisms and acyclic #types in #HoTT at the Yorkshire and Midlands #Category Theory Seminar (https://conferences.leeds.ac.uk/yamcats/meeting-36/) are up at https://tdejong.com/talks/YaMCATS-2025-01-24.pdf
=> More informations about this toot | View the thread
I'm pleased to announce that the Heyting Day will be held in Amsterdam on Friday 14 March 2025.
Its theme will be models of #intuitionism and #computability and mark the retirement of Jaap van Oosten.
The invited speakers are:
Attendance is free. Sign up and more details here: https://www.knaw.nl/en/heyting-day-2025
The attached poster is thanks to the amazing @jacobneu.
=> More informations about this toot | View the thread
The annual Workshop on Homotopy Type Theory and Univalent Foundations will take place on 15β16 April 2025 in Genoa, Italy and is co-located with the WG6 meeting of the EuroProofNet COST action on 17-18 April.
Please consider submitting a talk abstract! For details, see https://hott-uf.github.io/2025/
=> More informations about this toot | View the thread
@MartinEscardo and I have been working on injective #types in #constructive #univalent mathematics.
Last week I gave an informal talk in our group's seminar and I wrote a brief blog post with several pointers in case you'd like to know more: https://fplunchnott.wordpress.com/2024/10/25/injective-types/
=> More informations about this toot | View the thread
@jacobneu had some mugs made π
=> More informations about this toot | View the thread
I'm pleased that my paper with @egbertrijke and @buchholtz on epimorphisms and acyclic types in #HoTT got accepted to The Journal of Symbolic #Logic!
I'm quite proud of this paper as I feel that many of its arguments are rather slick and nicely illustrate the methods of synthetic homotopy theory.
arXiv link: https://arxiv.org/abs/2401.14106
=> More informations about this toot | View the thread
It's some time away, but I'm looking forward to lecturing on Categorical Realizability at the European Summer School in #Logic, Language and Computation in 2025!
https://2025.esslli.eu/courses-workshops-accepted.html
=> More informations about this toot | View the thread
On the train to another edition of the wonderful Proof and Computation autumn school π
https://www.mathematik.uni-muenchen.de/~schwicht/pc24.php
=> More informations about this toot | View the thread
=> This profile with reblog | Go to de_Jong_Tom@mathstodon.xyz account This content has been proxied by September (3851b).Proxy Information
text/gemini