Ata Keskin (Dec 24 2022 at 22:38): Ata Keskin (Dec 24 2022 at 22:38):Hi everyone, I am looking for a proof showing that any two Cauchy-complete and ordered fields are isomorphic to one another. Basically the formalized version of this. I will use this in formalizing the Eudoxus reals, which is an alternative construction of the real numbers which only uses integers as building blocks (skipping the rationals). Thanks in advance!
Sławomir Kołodyńaski (Dec 25 2022 at 11:45):Just a note that IsarMathLib has a formalization of this construction in Isabelle/ZF which may be useful as a reference, see https://isarmathlib.org/Real_ZF.html and https://isarmathlib.org/Real_ZF_1.html. I would be happy to find a good source with the proof of the fact you are asking about as well especially to see the role of the Axiom of Choice in it. Please post here if you find one.
Ata Keskin (Dec 25 2022 at 19:44):Yes! I also saw this referenced on the wikipedia entry on the construction of reals, but I also wanted to formalize this in Isabelle/HOL. For now, I am following this entry on AFP on the construction of reals from Dedekind cuts to figure out the best way to show that my construction is a complete and ordered field. If I can't find what I'm looking for (and if I have the energy left for it) I will also try to formalize it by following this tweet which was also mentioned in the blog post linked above .
All complete ordered fields are isomorphic. So let the real numbers be whichever complete ordered field you prefer... https://twitter.com/JDHamkins/status/1169935061480804352/photo/1
- Joel David Hamkins (@JDHamkins) Jelena Markovic (Dec 29 2022 at 10:41):Can we connect quotient_type and locale somehow? Can we use quotient_type inside locale on some way? Currently we use axiomatization but we don't want that.
Last updated: Apr 26 2024 at 16:20 UTC