Post #1782142
2026-04-28 06:05 UTC
@vnikolov
ACL2 has an extended version, acl2(r) that uses nonstandard analysis to provide the reals. (Er, I think this means that you provide a function that rationally converges toward the real number from below, and then you plus a nonstandard number onto the series if the real number is irrational).
I was speaking informally about (Sqrt 2) not existing: Actually, not having sqrt at all is this whole big thing: https://www.cs.uwyo.edu/~ruben/static/pdf/sqrt.pdf (I do not remember reading this paper yet).
@simon_brooke
Replies (2)
-
@screwlisp@gamerplus.org 2026-04-28 06:14
@vnikolov They show, (implies (rationalp x) (not (equal (* x x) 2))) @simon_brooke
-
@vnikolov@ieji.de 2026-04-28 06:31
@screwlisp wrote: «ACL2 has an extended version, acl2(r) that uses nonstandard analysis to provide the reals. (Er, I think this means that you provide a function that rationally converges toward the real number from below, and then you plus a nonstandard number onto the series if the real number is irrational).» Thank you. Non-standard, as in Robinson's? A close encounter with ACL2 is the next thing I have to leave for another time, alas. @simon_brooke