Post #1782141
2026-04-28 03:42 UTC
Out of curiosity, what does ACL2 say about the square root of -1?
Conceivably, it may have Gaussian numbers, even though it doesn't have real numbers.
Again repeating the well-known, while both √2 and √-1 don't exist in the set of rational numbers, the circumstances are rather different.
@screwlisp @simon_brooke
Replies (1)
-
@screwlisp@gamerplus.org 2026-04-28 06:05
@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