Email Gateway (Aug 22 2022 at 19:58): Email Gateway (Aug 22 2022 at 19:58):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello,
One of the most attractive features of Isabelle/HOL, at least for me, is
the possibility to use nonstandard analysis, i.e., Leibniz' infinitesimals
(by the way, Leibniz is also a precursor of proof assistants in general).
References:
Fleuriot, Jacques D. "Nonstandard geometric proofs." *International
Workshop on Automated Deduction in Geometry*. Springer, Berlin, Heidelberg,
2000. https://link.springer.com/chapter/10.1007/3-540-45410-1_15
Fleuriot, Jacques D., and Lawrence C. Paulson. "Mechanizing nonstandard
real analysis." LMS Journal of Computation and Mathematics 3 (2000):
140-190.
https://www.cambridge.org/core/journals/lms-journal-of-computation-and-mathematics/article/mechanizing-nonstandard-real-analysis/A1A4325EE3C91A18EF68D55407D184FB
I am curious whether or not nonstandard analysis can be developed in
Isabelle/Naproche.
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 19:59):From: Makarius <makarius@sketis.net>
(You would have to ask Peter Koepke, but he is probably not on this
mailing list).
The underlying logical language of Isabelle/Naproche is Naproche-SAD (or
ForTheL), which is very open to almost anything: it starts out as
first-order logic with minimal notions of set-theory. Applications then
axiomatize a bit further context, before doing some proofs in the
quasi-natural mathematical language.
So in principle, the answer is: yes. In practice it is: not yet. Proper
library support is still missing in Naproche-SAD, and scalability is not
for free -- it is future work and requires some more efforts. (You can
get a glimpse of general scalability aspects for Isabelle/AFP in my
current paper https://arxiv.org/abs/1905.07244).
Makarius
Last updated: Apr 20 2024 at 08:16 UTC