[danharaj]

I think the distinction here is that even though a theory like Presburger arithmetic is about the infinite set of natural numbers and similarly for Euclidean geometry that they are still finitary objects precisely because they are decidable: the entire theory can be reduced to a finite object, the decision procedure.

On the other hand Peano arithmetic is not only about infinite objects, and very many more than just the naturals because it is rich enough to allow you to encode other ostensibly more sophisticated infinite objects in it, it is itself an infinite object. It can't be reduced to a finitary decision procedure the way weaker arithmetics can.

Diagonalization is accounted for by my second example of conceptualizing infinity: you can't do a diagonalization argument unless you contract a variable. In particular, you can admit full unrestricted set comprehension if you can't contract to derive absurdity. Referencing section 2.3 here [1]. It was this analysis of Russell's paradox that led to the discovery of light linear logics, or so the story goes.

[1] http://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf