Post #1782140
2026-04-27 21:49 UTC
@simon_brooke
acl2 and not coalton: Since ACL2 base does not have real numbers, we get the wonderful logical result "the square root of two does not exist". ( ACL2(r) exists for when it is important that there actually are irrational numbers).
@vnikolov
Replies (1)
-
@vnikolov@ieji.de 2026-04-28 03:42
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