A curious inference (Q1091390)

The paper discusses the proof of a statement about a recursively defined rapidly increasing function. The hypotheses involve universal quantifiers and the statement is easily proved in second order logic. An estimate of the size of the set needed to replace the quantifiers by Gentzen cuts shows that the first order proof would need a number of symbols largely in excess of the number of atoms in the universe; such a proof cannot be written down. The author's conclusion is that this gives additional strength to the position ''that first order logic ought never to have been accorded canonical status as logic''. \{The argument is mathematically sound but the conclusion is questionable. In mathematics and computer science one presupposes a sufficiently large supply of labels that allow one to use abbreviations (from the purely logical point of view these would transform the language used to a new one) and which bring the proof down to manageable size.\}