Link

Okay, so the result shown is somewhat weaker than the title implies, but the blog post contains some interesting stuff about the place of infinity in mathematics, its history, and finitism versus Platonism.

Deeply cool stuff, thanks for posting.

The articles says that a theorem is finitely reducible if it's provable without "invoking infinity" - does that just mean without making use of any infinite sets or is there more to it?

It is seriously restrictive. The purely informal idea is due to Hilbert much like the purely informal idea of intuitionism is due to Brouwer, but I don't believe either settled for a definite formalism. But even informally, Hilbert was insistent that it is literally meaningless to quantify over the naturals!

But there are formalisms, the standard being primitive recursive arithmetic. This is the quantifier free fragment of first order arithmetic, together with rules allowing you to introduce primitive recursive functions (these are the total functions you get doing recursion just like induction: you define the case for 0, then you define the n+1 case in terms of the n case). You also have induction as an inference rule.

The closest you get to quantification is with variables. You can prove that m + n = n + m, but this is really thought of as a schema or pattern. It doesn't say anything until you plug numerals in, after which you could run back over the proof with the numbers inserted and get back to reflexivity of equality.

This really is finite, because once you hve collected all your mathematical proofs, you can just pick a suitably big number and then unfold a finite number of all possible concrete results. You cannot do the same for first order PA, even though PA has no infinite objects in its domain.

Rest assured, no one actually wants to work in this theory. They want to work in a powerful metatheory that can be finitistically provably reduced to finitism. Hilbert thought the metatheory would be ZFC, and if he had been right, we would have laid the foundational crisis to bed. Goedel shot down that dream, and I'll state the why more strongly than the blogger: set theory proves PRA consistent, so if PRA proves set theory is one of its conservative extensions, then set theory also proves itself consistent, whilst being subject to Goedel's second.

I cannot resist the opportunity to moan again about William Lane Craig, who likes to bring up Hilbert's rejection of the infinite in the Kalam. Hilbert only felt able to do so because he was betting on a doomed project. As the blog post says though, finitism isn't dead yet (by my standards anyhow), only the initial aims of the Hilbert programme.