[Sharlin]

We lose the ability to reason about sets of unbounded size. As long as we only restrict ourselves to some bounded subset of integers, Gödel can't do the trick with his numerals. Equivalently, on the CS side, we must restrict ourselves to total functions, that is, all valid programs must provably halt after some bounded number of steps.