Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The emergence of the mathematical concept of computability in the 1930 s was marked by an interesting shift of perspective, from viewing the intuitive concept, “human calculability following a fixed routine” in terms of calculability in a logic, to viewing the concept as more adequately expressed by Turing’s model.Footnote 1 This happened in spite of, or in parallel with, confluence, as Gandy called it in his [1], namely the proven extensional equivalence of the models of computability which had been given prior to Turing’s model.

In this talk we consider this shift—one in which Gödel was a key figure—in relation to Gödel’s philosophical outlook subsequently. On the way we consider a question that Kripke has asked recently [2]: why did Gödel not see that the Entscheidingsproblem is an immediate consequence of the Completeness and Incompleteness Theorems? Kripke’s analysis depends upon viewing computability in terms of calculability in a logic. We thus suggest that Kripke’s own explanation for Gödel’s purported blindness to the fact of having solved what was arguably viewed as the single most important problem in logic remaining open at the time,Footnote 2 be complemented by the story of the difficulties logicians had with viewing computability in this sense.

In particular we will suggest that the inherent circularity which characterises such a conception, may have contributed to a sense of reluctance on the part of the Princeton group of logicians at the time to embrace it: for if computability is understood in terms of calculability in a logic, then it must be the case that not any logic will serve, rather the logic in question must be given effectively. But then, how to understand the concept “given effectively”, as applied to the logic in question?

What follows is an abbreviated history of the development of computability in the 1930 s, from the point of view of this shift in perspective.Footnote 3

2 Isolating the Concept of “Computable Function”

Gödel defined the class of primitive recursive functions in his 1931 [5], while Church at the same time had developed the \(\lambda \)-calculus together with Kleene.

Church’s first presentation of the \(\lambda \)-calculus in 1932 [6], which embeds that calculus in a deductive formalism, in the Hilbert/Bernays terminology, was found to be inconsistent in 1934. Two years later Church published a, in Gandy’s words, logic-free definition of the \(\lambda \)-calculus, based on the primitives “function” and “iteration”:Footnote 4

When it began to appear that the full system is inconsistent, Church spoke out on the significance of \(\lambda \)-definability, abstracted from any formal system of logic, as a notion of number theory.Footnote 5

In the period between these two versions of the \(\lambda \)-calculus Church suggested his thesis, namely the suggestion to identify the \(\lambda \)-definable functions with those which are effectively computable.Footnote 6 The plausibility of the thesis became especially clear when Church, Kleene and Rosser established confluence, proving the equivalence of \(\lambda \)-definability with computability in the sense of the Herbrand-Gödel equational calculus, in 1935.Footnote 7

Interestingly, Gödel was not persuaded of its adequacy, when he was told of Church’s suggestion to view intuitive or effective computability in terms of \(\lambda \)-definability in early 1934, finding the proposal “thoroughly unsatisfactory."Footnote 8 Church described Gödel’s then suggestion to instead take an axiomatic approach to the problem, in a letter to Kleene:

His [Gödel’s ] only idea at the time was that it might be possible, in terms of effective calculability as an undefined notion, to state a set of axioms which would embody the generally accepted properties of this notion, and to do something on that basis. ...At that time he did specifically raise the question of the connection between recursiveness in this new sense and effective calculability, but said he did not think that the two ideas could be satisfactorily identified “except heuristically.”Footnote 9

Church may have been influenced by Gödel’s negative view of the adequacy of \(\lambda \)-calculus, as in his lecture on his Thesis to the American Mathematical Society in 1935, Church used the Herbrand-Gödel equational calculus as a model of effective computation, i.e. recursiveness in the “new sense,” rather than the \(\lambda \)-calculus.

In fact Church presented two approaches to computability in the AMS lectures and in his subsequent 1936 [13], based on the lectures: Firstly algorithmic, based still on what is now known as the untyped \(\lambda \)-calculus, i.e. the evaluation of the value fm of a function by the step-by-step application of an algorithm—and secondly logical, based on the idea of calculability in a logic:

And let us call a function F of one positive integer calculable within the logic if there exists an expression f in the logic such that \(f(\mu )=\nu \) is a theorem when and only when \(F(m)=n\) is true, \(\mu \) and \(\nu \) being the expressions which stand for the positive integers m and n.Footnote 10

In order to view computability in terms of calculability in a logic, one must first restrict the class of formal systems representing those computable functions. As we noted, not just any formalism will serve! For Church this meant that the theorems of the formal system should be recursively enumerable.Footnote 11 A number-theoretic function is taken to be effective, then, if its values can be computed in such an effectively given formalism.

The argument appears to be circular.Footnote 12 In Hilbert and Bernays’ 1939 Grundlagen der Mathematik II, the computable functions are also presented in terms of a logical calculus, but here effectivity is now reduced to primitive recursion. In his [14], Sieg has this to say about Hilbert and Bernays’ improvement of Church’s system:

In this way they provided the mathematical underpinnings for ... Church’s argument, but only relative to the recursiveness conditions: the crucial one requires the proof predicate of deductive formalisms, and thus the steps informal calculations, to be primitive recursive!

We now come to one of the topics of this note, the shift in perspective in 1934 noted by Gandy, writing: “...in 1934 the interest of the group shifted from systems of logic to the \(\lambda \)-calculus and certain mild extensions of it: the \(\lambda -\kappa \) and the \(\lambda -\delta \) calculi."Footnote 13 Gandy does not speculate on the deeper reasons for this shift; and indeed it is interesting that there are so few direct references to the circularity problem in the writings of logicians working on computability at the time. However it seems plausible that the circularity problem was at least partly responsible for this shift away from logical systems, especially given the initial inconsistency of the \(\lambda \)-calculus.

2.1 The “Scope Problem”: How General Are the Incompleteness Theorems?

We turn now to Gödel’s role in these developments. Gödel was perhaps the first to suggest isolating the concept of effective computability.Footnote 14 His interest was driven, at least in part, by an important piece of unfinished business as far as the Incompleteness Theorems are concerned, in that it was not clear at the time to which formal systems the theorems apply, outside of the fragment of the type theory of Principia Mathematica he used.

In short, solving the scope problem depends on articulating a precise and adequate notion of effective computability, because the formal systems at issue in the Incompleteness Theorems, are to be given effectively.Footnote 15

To this end, that is, with a wish to “make the incompleteness results less dependent on particular formalisms,”Footnote 17 Gödel introduced in 1934 the general recursive, or Herbrand-Gödel recursive functions. It is striking from the point of view of this note that he begins the section introducing those functions thus: “Now we turn to some considerations which for the present have nothing to do with a formal system.”, and defines the notion of “formal system” in the next section as consisting of “symbols and mechanical rules relating to them.”Footnote 18 Gödel seems here to have all the elements behind the Turing conception of computability in place. What is missing of course, is the model itself.

The Herbrand-Gödel calculus allows for forms of recursions that go beyond primitive recursion, however it was not clear to Gödel at the time, that the schema captured all recursions.Footnote 19

Gödel gave, in the same presentation, a precise definition of the conditions a formal system must satisfy so that the incompleteness theorems apply to it. These included the restriction that:

Supposing the symbols and formulas to be numbered in a manner similar to that used for the particular system considered above, then the class of axioms and the relation of immediate consequence shall be [primitive JK] recursive.Footnote 20

By 1935, Gödel’s reflections on computability in the higher order context began to point towards the possibility of a definitive notion of formal system. Nevertheless, an, in Gödel’s terminology now, absolute definition of effective computability was still missing at that point.Footnote 21

3 Turing’s Analysis of Computability

In 1936, Turing gave a self-standing analysis of human effective computability and used it to solve the Entscheidungsproblem.

Rather than calculability in a logic, Turing analyzed effectivity informally but exactly, via the concept of a Turing Machine—a machine model of computability, consisting of a tape scanned by a reader, together with a set of simple instructions in the form of quadruples.Footnote 23

We alluded to circularity in connection with approaches to computability that are centered on the idea of calculability in a logic.Footnote 24 The crucial point here is that Turing’s analysis does not require the specification of a logic at all.

The reaction to Turing’s work among the Princeton logicians was immediately positive. As Kleene would write in 1981, “Turing’s computability is intrinsically persuasive but \(\lambda \)-definability is not intrinsically persuasive and general recursiveness scarcely so (its author Gödel being at the time not at all persuaded).”

For Gödel, as he would later explain to Hao Wang, Turing’s model of human effective calculability is, in some sense, perfect:

The resulting definition of the concept of mechanical by the sharp concept of “performable by a Turing machine” is both correct and unique ...Moreover it is absolutely impossible that anybody who understands the question and knows Turing’s definition should decide for a different concept.Footnote 25

And Turing’s analysis led to the complete solution of the scope problem:

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 concept of formal system can now be given, the existence of undecidable arithmetical propositions and the non-demonstrability of the consistency of a system in the same system can now be proved rigorously for every consistent formal system containing a certain amount of finitary number theory.

Turing’s analysis thus settled definitively the adequacy question for computability. For Gödel, and for the logicians of the time, the Turing Machine was not just another in the list of acceptable notions of computability—it is the grounding of all of them.

We suggested that the issue of circularity was in the background of the shift away from a logical orientation to the problem of isolating and precisifying the notion of intuitive computability. Once again this is the problem of how to spell out the concept of effectivity of a logical system that embeds one’s notion of computability, without invoking that very notion. How did the Turing model of computation solve this problem for Gödel? We explain it thus: Turing’s model of computation allows for an autonomous logical perspective, because it is itself logic free.

What was the role of confluence? Church’s Thesis identified effective calculability with \(\lambda \)-calculability, and then with Herbrand-Gödel calculability, after the equivalence between the two was established. Prior to Turing’s work, the available confluence was seen as justifying adequacy in a weak sense only. Once one has a grounding example in hand this changes—confluence now plays an epistemologically important evidentiary role.

It is striking that Emil Post, who called for the return to meaning and truth in the opening of his [19], and the downplaying of what he called “postulational thinking,” aligns him both ideologically and mathematically with these developments. As it turns out, Post’s recommendation to develop recursion theory mathematically, by stripping off the formalism with which the theory was encumbered, led to the formalism free development of recursion theory just along the lines he advocated. It also gave rise to the development of Post Systems, a model of computability very similar to Turing’s.

The project of developing an autonomous logical perspective permeated Gödel’s outlook from then on. Gödel alludes to it a number of times in his Princeton Bicentennial Lecture, in connection with finding absolute notions of decidability and provability. One can also read the perspective into Gödel’s overarching goal of attaining decidability in set theory—for how else to achieve decidability in set theory, except by remaining, as we have called it, formalism free?

4 Kripke and the Entscheidungsproblem

Kripke advocates a, as he calls it, logical orientation to the problem of isolating the notion of effective computability.

My main point is this: a computation is a special form of mathematical argument.Footnote 26

He then asks, given that such an approach would have been very easily within reach of Gödel and other logicians working in the period immediately after the 1931 Incompleteness Theorems, why wasn’t it noticed that a negative solution to the Entscheidungsproblem follows immediately?

Suppose we had taken derivability by a computation expressible in a first-order language as one’s basic definition of computability. Then given the Gödel Completeness Theorem, any conventional formalism for first-order logic will be sufficient to formalise such derivability. ...It will be a short and direct step to conclude the undecidability in this sense of the Entscheidungsproblem.Footnote 27

Kripke gives the argument, which necessarily includes the notion of validity. He concludes, very reasonably in our view, that Gödel would have been reluctant to invoke a notion of truth in the proof, had he arrived at that proof. Indeed it is well known that Gödel’s initial proof of the Incompleteness Theorem followed from the undefinability of truth together with the observation that first order provability is not only definable, but r.e.Footnote 28

We suggest in this talk that the evidence in the record regarding Gödel’s response to the Turing model, together with the developments leading up to it (as recounted here), might also be taken into account in explaining Gödel’s so-called blindness. It just might be that for Gödel, grounding the notion of computability required an altogether new mathematical idea, and not a logical one. We saw how close he came to Turing’s conception in 1934, just before he turned his attention to the continuum problem in set theory.