3 ms·

Right, but the system we're interested in is normal computers, which is more powerful than arithmetic.

• JadeNB 10y ago
  > Right, but the system we're interested in is normal computers, which is more powerful than arithmetic. On the other hand, a theorem prover does not have to be able to prove everything about a system to be able to prove some useful things. One might also say "the system mathematicians are interested in is all of mathematics, which is more powerful than arithmetic", or, for that matter, "the system programmers are interested in is all of theoretical computation, which is (at least) Turing complete"—but sometimes it's useful intentionally to restrict our power. (I think of https://news.ycombinator.com/item?id=10567408 https://news.ycombinator.com/item?id=10567408 , for example.) (If we're being very picky, then, as pfortuny points out (https://news.ycombinator.com/item?id=12762192 https://news.ycombinator.com/item?id=12762192), a computer, having only a finite address space, isn't even as powerful as ordinary arithmetic; but it's fair to guess that this isn't a useful kind of pickiness.)