Addendum on Precise Generality
In my recent post Precise Generality I promised that I would follow up with further exposition. This post is not that promised follow-up providing further exposition and investigation of the idea of precise generality, but truly an “addendum” simply to add some further detail to the ideas expressed in Precise Generality. In that post I wrote:
“In so far as a formal system is the only known embodiment of a precise idea of precision (according to Heyting), and in so far as a formal system is intrinsically finitistic (in both conception and execution), the only precise idea of precision we possess is intrinsically finitistic.”
It is interesting to explore the ideas that Gödel had regarding formal systems in relation to their finitary nature. On the one hand, Gödel seems to unambiguously embody the above idea of formal systems being intrinsically finitistic. In particular, Gödel cited the work of Turing with approval:
“In consequence of later advances, in particular of the fact that due to A. M. Turing’s work a precise and unquestionably adequate definition of the general notion of formal system can now be given . . .”
Gödel added a footnote to this:
“In my opinion the term ‘formal system’ or ‘formalism’ should never be used for anything but this notion.” (Collected Works, Vol. I, p. 195)
More generally regarding formal systems Gödel wrote:
“A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas.”
Gödel goes on to say that the syntactical characterization of formal systems which he gives at the beginning of his 1934 paper (“On undecidable propositions”) is equivalent to the formulation in terms of mechanical procedures if his use of ‘finite procedure’ is understood to mean ‘mechanical procedure.’ Gödel then reiterates his point by mentioning, “...the concept of formal system, whose essence it is that reasoning is completely replaced by mechanical operations on formulas.” He also notes that the possibility of finite non-mechanical procedures such as “the use of abstract terms on the basis of their meaning” does not detract from the adequacy of the suggested definition of “formal system.”
But is not the adequacy of mechanical procedures for finitary reasoning relative to a conception of proof, so that if a broader conception of proof which takes account of human motivations (such as, e.g., the desire to rigorously formalize as much of classical mathematics as possible) is at issue mechanical methods are no longer adequate? If one assumes a notion of proof reducible to mechanical procedures and goes on to prove it so, this is nothing but a petitio principii. Gödel cannot be accused on this account, as he did not anticipate Turing’s work, though he may have reinterpreted his earlier work in the light of Turing’s results, and so engaged in a kind of personal anachronism.
Despite Gödel’s apparent willingness to revise his own thought in the light of Turing’s work, Gödel was in no sense limited by the influence of Turing, and in fact in one of my favorite quotes from Gödel (which I have quoted in many posts), he explicitly takes on Turing’s finitism:
“Turing... gives an argument which is supposed to show that mental procedures cannot go beyond mechanical procedures. However, this argument is inconclusive. What Turing disregards completely is the fact that mind, in its use, is not static, but is constantly developing, i.e., that we understand abstract terms more and more precisely as we go on using them, and that more and more abstract terms enter the sphere of our understanding. There may exist systematic methods of actualizing this development, which could form part of the procedure. Therefore, although at each stage the number and precision of the abstract terms at our disposal may be finite, both (and, therefore, also Turing’s number of distinguishable states of mind) may converge toward infinity in the course of the application of the procedure.” (“Some remarks on the undecidability results” in Gödel, Kurt, Collected Works, Volume II, Publications 1938-1974, New York and Oxford: Oxford University Press, 1990, p. 306)
There is, of course, no contradiction, not even any paradox, in observing that formal systems are finite but that the mind (which thinks formal systems) converges upon infinity. But what Gödel formulates in the above could be formulated even more strongly. One could say that formal systems, in their use, are not static, but are constantly developing, and that the development of formal systems is precisely the procedure envisioned by Gödel that can actualize the development of greater precision and scope in the use of abstract concepts.
I see Gödel as one of the few thinkers (if not the only thinker) to bridge the gap between constructive and non-constructive modes of thought, and he brought that ability to think both constructively and non-constructively to his idea of formal systems, which is, as a consequence, highly subtle and nuanced.
Thus while Gödel might have agreed that the only precise idea of precision we possess is intrinsically finitistic, I think he would have also pointed out that any one precise idea of precision could be infinitely transcended by more precise ideas of precision -- that is to say, it would be possible to extrapolate a hierarchy of precision and rigor, with formal systems embodying a given level of precision and rigor at each stage of that hierarchy.