In principle a statement that involves only finite sets of natural numbers can be proved by exhaustive calculation. A statement involving infinity in an essential way cannot. This means there is a gap in certitude between finite and infinite mathematics. There's many ways to describe this divide. For example, an arithmetic statement involving unbounded quantifiers. You can measure how much such a statement fails to be finite by counting the alternation of universal and existential unbounded quantifiers. This is a measurement of the naive logical complexity of a statement.
Godels incompleteness theorems can be seen as a statement about the gap between finite and infinite mathematics. Decidability, semidecidability and undecidability can be seen as the relationship between boundedly quantified arithmetic statements, statements with one unbounded existential quantifier, and statements with one unbounded universal quantifier.
Another avenue of exploring the gap between finite and infinite mathematics is via linear logic. There the thesis is that contraction, the logical reuse of variables, is where infinity creeps into logical reasoning. Indeed logic without contraction is quite tame. Logic with unlimited contraction is wild. Surprisingly there are logics with an intermediate strength of contraction: so-called light linear logics. These can classify reasoning that embodies polynomial time computation or elementary time computation. So in another sense infinity can be measured by algorithmic complexity.
First-order arithmetic with bounded quantification is decidable, but so is arithmetic with unbounded quantification but no multiplication (just addition). So is the elementary theory of real numbers, and elementary geometry. Meanwhile, there are plenty of small, finitary theories that are undecidable.
The key to decidability or undecidability is whether diagonalization is possible, not whether or not there are disguised references to infinity somewhere.
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.
You just gave me a new frame for thinking about a few things I'd already learned, as well as some interesting leads on questions I didn't even know to ask. Thank you!
[the divide] separates two kinds of mathematical statements: “finitistic” ones, which can be proved without invoking the concept of infinity, and “infinitistic” ones, which rest on the assumption — not evident in nature — that infinite objects exist.
The article stated this in a very silly way. Infinite objects existing in nature has nothing to do with whether reasoning about certain infinite objects (e.g. The real numbers) is sound, any more than thinking about counterfactuals is impossible because they differ from the real world.
