(Notations, non-standard concepts, and definitions used commonly in these investigations are detailed in this post.)

A new proof?

An interesting review by Natalie Wolchover on May 24, 2016, in the on-line magazine Quanta, reports that:

“With a surprising new proof, two young mathematicians have found a bridge across the finite-infinite divide, helping at the same time to map this strange boundary.

The boundary does not pass between some huge finite number and the next, infinitely large one. Rather, it 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.”

More concretely:

“In the new proof, Keita Yokoyama, 34, a mathematician at the Japan Advanced Institute of Science and Technology, and Ludovic Patey, 27, a computer scientist from Paris Diderot University, pin down the logical strength of $RT_{2}^{2}$ — but not at a level most people expected. The theorem is ostensibly a statement about infinite objects. And yet, Yokoyama and Patey found that it is ‘finitistically reducible’: It’s equivalent in strength to a system of logic that does not invoke infinity. This result means that the infinite apparatus in $RT_{2}^{2}$ can be wielded to prove new facts in finitistic mathematics, forming a surprising bridge between the finite and the infinite.”

The proof appeals to properties of transfinite ordinals

My immediate reservation—after a brief glance at the formal definitions in $\S$1.6 on p.6 of the Yokoyama-Patey paper—was that the domain of the structure in which the formal result is proved necessarily contains at least Cantor’s smallest transfinite ordinal $\omega$, whereas the result is apparently sought to be ‘finitistically reducible’ (as considered by Stephen G. Simpson in an absorbing survey of Partial Realizations of Hilbert’s Program), in the sense of being not only finitarily provable, but interpretable in, and applicable to, finite structures (such as that of the natural numbers) whose domains may not contain (nor, in some cases, even admit—see Theorem 1 in $\S$4.1 of this post) an infinite ‘number’.

Prima facie, the implicit assumption here (see also this post) seems to reflect, for instance, the conventional wisdom that every proposition which is formally provable about the finite, set-theoretically defined ordinals (necessarily assumed consistent with an axiom of infinity), must necessarily interpret as a true proposition about the natural numbers.

Why we cannot ignore Skolem’s cautionary remarks

In this conventional wisdom—by terming it as Skolem’s Paradox—both accepts and implicitly justifies ignoring Thoraf Skolem’s cautionary remarks about unrestrictedly corresponding putative mathematical relations and entities across domains of different axiom systems.

(Thoralf Skolem. 1922. Some remarks on axiomatized set theory. Text of an address delivered in Helsinki before the Fifth Congress of Scandinavian Mathematicians, 4-7 August 1922. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.)

However, that the assumption is fragile is seen since, without such an assumption, we can only conclude from, say, Goodstein’s argument that a Goodstein sequence defined over the finite ZF ordinals must terminate finitely even if the corresponding Goodstein sequence over the natural numbers does not terminate (see Theorem 2 of this unpublished investigation)!

(R. L. Goodstein. 1944. On the Restricted Ordinal Theorem. In the Journal of Symbolic Logic 9, 33-41.)

A remarkable exposition of Ramsey’s Theorem

The Yokoyama-Patey proof invites other reservations too.

In a comment—remarkable for its clarity of exposition—academically minded ‘Peter’ illustrates Ramsey’s Theorem as follows:

Something that might help to understand what’s going on here is to start one level lower: Ramsey’s theorem for singletons ($RT^1_2$) says that however you colour the integers with two colours (say red and blue), you are guaranteed to find an infinite monochromatic subset. To see this is true, simply go along the integers starting from $1$ and put them into the red or the blue bag according to their colour. Since in each step you increase the size of one or the other bag, without removing anything, you end up with an infinite set. This is a finitistic proof: it never really uses infinity, but it tells you how to construct the first part of the ‘infinite set’.

Now let’s try the standard proof for $RT^2_2$, pairs. This time we will go along the integers twice, and we will throw away a lot as we go.

The first time, we start at $1$. Because there are infinitely many numbers bigger than $1$, each of which makes a pair with $1$ and each of which pairs is coloured either red or blue, there are either infinitely many red pairs with $1$ or infinitely many blue pairs (note: this is really using $RT_2^1$). I write down under $1$ ‘red’ or ‘blue’ depending on which it turned out to be (in case both sets of pairs are infinite, I’ll write red just to break a tie), then I cross out all the numbers bigger than $1$ which make the ‘wrong colour’ pair with $1$.

Now I move on to the next number, say $s$, I didn’t cross out, and I look at all the pairs it makes with the un-crossed-out numbers bigger than it. There are still infinitely many, so either the red pairs or the blue pairs form an infinite set (or both). I write down red or blue below $s$ as before, and again cross out all the number bigger than $s$ which make a wrong colour pair with $s$. And I keep going like this; because everything stays infinite I never get stuck.

After an infinitely long time, I can go back and look at all the numbers which I did not cross out – there is an infinite list of them. Under each is written either ‘red’ or ‘blue’, and if under (say) number $t$ the word ‘red’ is written, then $t$ forms red pairs with all the un-crossed-out numbers bigger than $t$. Now (using $RT^1_2$ again) either the word ‘red’ or the word ‘blue’ was written infinitely often, so I can pick an infinite set of numbers under which I wrote either always ‘red’ or always ‘blue’. Suppose it was always ‘red’; then if $s$ and $t$ are any two numbers in the collection I picked, the pair $st$ will be red – this is because one of $s$ and $t$, say $s$, is smaller, and by construction all the pairs from $s$ to bigger un-crossed-out numbers, including $t$, are red. If it were always blue, by the same argument I get an infinite set where all pairs are blue.

What is different here to the first case? The difference is that in order to say whether I should write ‘red’ or ‘blue’ under $1$ (or any other number) in the first step, I have to ‘see’ the whole infinite set. I could look at a lot of these numbers and make a guess – but if the guess turns out to be wrong then it means I made a mistake at all the later steps of the process too; everything falls apart. This is not a finitistic proof – according to some logicians, you should be worried that it might somehow be wrong. Most mathematicians will say it is perfectly fine though.

Moving up to $RT^3_2$, the usual proof is an argument that looks quite a lot like the $RT^2_2$ argument, except that instead of using $RT^1_2$ in the ‘first pass’ it uses $RT^2_2$. All fine; we believe $RT^2_2$, so no problem. But now, when you want to write down ‘red’ or ‘blue under $1$ in this ‘first pass’ you have to know something more complicated about all the triples using $1$; you want to know if you can find an infinite set $S$ such that any pair $s,t$ in $S$ forms a red triple with $1$. If not, $RT^2_2$ tells you that you can find an infinite set $S$ such that any pair $s,t$ in $S$ forms a _blue_ triple with $1$. Then you would cross off everything not in $S$, and keep going as with $RT^2_2$. The proof doesn’t really get any harder for the general case $RT^k_2$ (or indeed changing the number of colours to something bigger than $2$). If you’re happy with infinity, there’s nothing new to see here. If not – well, these proofs have you recursively using more and infinitely more appeals to something infinite as you increase k, which is not a happy place to be in if you don’t like infinity.

Implicit assumptions in Yokoyama-Patey’s argument

Peter’s clarity of exposition makes it easier to see that, in order to support the conclusion that their proof of Ramsey’s Theorem for pairs is ‘finitistically reducible’, Yokoyama-Patey must assume:

(i) that ZFC is consistent, and therefore has a Tarskian interpretation in which the ‘truth’ of a ZFC formula can be evidenced;

(ii) that their result must be capable of an evidence-based Tarskian interpretation over the ‘finitist’ structure of the natural numbers.

As to (i), Peter has already pointed out in his final sentence that there are (serious?) reservations to accepting that the ZF axiom of infinity can have any evidence-based interpretation.

As to (ii), Ramsey’s Theorem is an existensial ZFC formula of the form $(\exists x)F(x)$ (whose proof must appeal to an axiom of choice).

Now in ZF (as in any first-order theory that appeals to the standard first-order logic FOL) the formula $(\exists x)F(x)$ is merely an abbreviation for the formula $\neg(\forall x)\neg(F(x)$.

So, under any consistent ‘finitistically reducible’ interpretation of such a formula, there must be a unique, unequivocal, evidence-based Tarskian interpretation of $(\forall x)F(x)$ over the domain of the natural numbers.

Now, if we are to avoid intuitionistic objections to the admitting of ‘unspecified’ natural numbers in the definition of quantification under any evidence-based Tarskian interpretation of a formal system of arithmetic, we are faced with the ambiguity where the questions arise:

(a) Is the $(\forall x)F(x)]$ to be interpreted constructively as:

For any natural number $n$, there is an algorithm $T_n$ (say, a deterministic Turing machine) which evidences that $\{F(1), F(2), \ldots, F(n)\}$ are all true; or,

(b) is the formula $(\forall x)F(x)$ to be interpreted finitarily as:

There is a single algorithm $T$ (say, a deterministic Turing machine) which evidences that, for any natural number $n, F(n)$ is true, i.e., each of $\{F(1), F(2), \ldots\}$ is true?

As Peter has pointed out in his analysis of Ramsey’s Theorem $RT_2^2$ for pairs, the proof of the Theorem necessitates that:

“I have to ‘see’ the whole infinite set. I could look at a lot of these numbers and make a guess – but if the guess turns out to be wrong then it means I made a mistake at all the later steps of the process too; everything falls apart. This is not a finitistic proof – according to some logicians, you should be worried that it might somehow be wrong.”

In other words, Yokoyama-Patey’s conclusion (that their new proof is ‘finitistically reducible’) would only hold if they have established (b) somewhere in their proof; but a cursory reading of their paper does not suggest this to be the case.

Author’s working archives & abstracts of investigations