>>22-23
Computation is still basically equivalent to Peano Arithmetic, or expressible in it. We cannot prove PA is consistent, but it's a very likely bet that it is.
We cannot say anything about (the physical existence or their consistency of) infinitary non-computable objects such as real numbers, hypercomputation, various set theories and ordinals higher than Aleph Null. The only thing we know as absolute is computation (if Church-Turing thesis is correct, which we cannot know, no more than we can know of PA's consistency).
>>24
It's true, but a lot of mathematics can be encoded exactly and verified using a theorem prover. I also don't see what this ha to do with Lisp (I'm not
>>22), despite that I am a Lisper.