2
$\begingroup$

The main current implementations of hyperreal numbers are model-theoretic and set-theoretic approaches. Most of these implementations are strongly non-constructive, and many require a very deep encoding of set theory.

Similar to the success of real and surreal numbers, I wondered if HoTT could provide an axiom-free, inductive type-based implementation of hyperreal numbers.

$\endgroup$
1
  • $\begingroup$ "User friendly" is a very subjective term. You call the HoTT Cauchy reals "user friendly", and even I as one of the authors would claim that the construction is anything but user friendly. Please reformulate the question to ask something specific that we can answer, rather than it being just an expression of your opinions about what is simple and user friendly. $\endgroup$ Dec 28, 2023 at 18:39

2 Answers 2

3
$\begingroup$

For a survey of formalizations of real numbers you can look at Formalization of real analysis: a survey of proof assistants and libraries by Sylvie Boldo, Catherine Lelay and Guillaume Melquiond. Section 3.3 discusses existing (in 2015) implementations of non-standard analysis in ACL2 and Isabelle.

The question seems to assume that there is a correlation between an implementation being "axiom-free" and (somewhat subjective) "user friendly". There is sufficient evidence from the practice of formalization to indicate that such a correlation is not there.

Supplemental: The question has been made more specific, namely can homotopy type theory construct the non-standard reals without positing any further axioms? The usual ultraproduct construction cannot be achieved this way, because the existence of a non-principal ultrafilters cannot be established in ZF, so you can even thrown in excluded middle without success. However, all is not lost. One could pursue the work of Erik Palmgren's on constructive non-standard analysis, see his Developments in Constructive Nonstandard Analysis. This would very likely make for a worthy formalization project, in case anyone has a free year on their hands.

$\endgroup$
3
  • $\begingroup$ I sorry that I didn't use the exact wording to ask the question, which has been corrected, but the reference you provided is still very valuable and much appreciated. $\endgroup$ Dec 29, 2023 at 3:27
  • $\begingroup$ I supplemented my answer to address the modified question. $\endgroup$ Dec 29, 2023 at 8:30
  • $\begingroup$ I checked the paper you mentioned, and the papers that cite it. The paper you mention requires the introduction of LLPO and WKL, and is not fully constructivist. But the Constructivism Hyperreal does correspond to sheaves, maybe. $\endgroup$ Feb 13 at 11:17
0
$\begingroup$

There is more recently axiom systems like SPOT by Mikhail Katz and Karel Hrbacek which are conservative extensions of ZF and allow for infinitesimals. Maybe implementing one of them would help. I think ZFC has already been formalized. This is an area I’m interested in too. Are you on the Lean Zulip?

$\endgroup$
1
  • $\begingroup$ As it’s currently written, your answer is unclear. Please edit to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers in the help center. $\endgroup$
    – Community Bot
    Jan 9 at 21:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.