Philip Trettner@julesh There is still a gap as far as I understand it: there exist functions that are computable and total but where the totatily cannot be proven inside the same system. This should be a consequence of Gödel's incompleteness.
However, the CIC can represent almost all of math, so I don't know if such functions can exist in practice. How do you "know" that it is total while being unable to prove it?
Like, I think you can prove their existence but never provide an example. (I'm fuzzy on this)
All GNU social JP content and data are available under the