Search

Godel's incompleteness theorem states that there is no system of axioms and rules of inference such that the totality of all assertions deducible from the axioms is the same as the totality of all true assertions in arithmetic (indeed, for every consistent system one can construct effectively a true but unprovable assertion). The present article is devoted to a proof of this theorem, based on the concepts and methods of the theory of algorithms; the necessary information from the theory of algorithms is provided. The paper does not require specialized knowledge of any kind (in particular, none from mathematical logic), but assumes only a familiarity with elementary mathematical terminology and symbolism.

Publisher Summary This chapter illustrates Godel incompleteness theorem and proves the existence of free formulas not only for systems based on the usual rules of proof but also for systems based on the rule ω. The chapter discusses the systems based on the rule ω rests on the basis of the remark of J. R. Shoenfield that the decomposition of the ∏11 sets into constituents can on several occasions be exploited in the same way as the recursive enumerability of the Σ01sets.

Goedel's theorem states that in any consistent system which is strong enough to produce simple arithmetic there are formulae which cannot be proved-in-the-system, but which we can see to be true. Essentially, we consider the formula which says, in effect, "This formula is unprovable-in-the-system". If this formula were provable-in-the-system, we should have a contradiction: for if it were provablein-the-system, then it would not be unprovable-in-the-system, so that "This formula is unprovable-in-the-system" would be false: equally, if it were provable-in-the-system, then it would not be false, but would be true, since in any consistent system nothing false can be provedin-the-system, but only truths. So the formula "This formula is unprovable-in-the-system" is not provable-in-the-system, but unprovablein-the-system. Further, if the formula "This formula is unprovablein- the-system" is unprovable-in-the-system, then it is true that that formula is unprovable-in-the-system, that is, "This formula is unprovable-in-the-system" is true. Goedel's theorem must apply to cybernetical machines, because it is of the essence of being a machine, that it should be a concrete instantiation of a formal system. It follows that given any machine which is consistent and capable of doing simple arithmetic, there is a formula which it is incapable of producing as being true---i.e., the formula is unprovable-in-the-system-but which we can see to be true. It follows that no machine can be a complete or adequate model of the mind, that minds are essentially different from machines.

I WANT to start by considering certain fundamental differences between the major incompleteness theorems which have been discovered in researches in the foundations of mathematics during the past thirty years and the incomplete axiom systems which were found in the study of projective geometry during the last century. A confusion between these forms of incompleteness has led some mathematicians to underestimate the significance of the newer results and some philosophers to seek to understand the meaning of the new discoveries by reference to the technically simpler older work. When it was discovered, for instance, that a system of projective geometry in two dimensions which postulated the axioms of incidence and Pappus' Theorem was incomplete because Desargues' Theorem on perspective triangles was not derivable in the system, then this incompleteness could be interpreted as a proof of the independence of Desargues' Theorem, postulated as a new axiom, from the other axioms. The impossibility of proving Desargues' Theorem is surprising in view of the fact that the corresponding theorem in three dimensions is derivable from the three-dimensional axioms of incidence, but it is nevertheless, I think, without philosophical significance because it throws no light on the nature of formal systems as such and imposes no limitations upon the axiomatic method. The great modern incompleteness theorems which I shall consider are those due to Skolem and Gddel. Skolem's incompleteness theorem was discovered in an attempt to explain a paradox which Skolem himself found in the theory of sets. The paradox out of which Skolem's incompleteness theorem arises, is produced by applying a result of Ldwenheim's to a formalised set theory. L Swenheim showed that every consistent set of statements has a denumerable model, and so any formal system which admits some model (of the power of the continuum perhaps) has also a denumerable model. That is to say, for a consistent theory, we can find an interpretation in which all the objects, of which the theory * Received 25.vii.62 208

Descartes believed that (nonhuman) animals were essentially machines, but that humans were obviously not; for a machine could never use speech or other signs as we do when placing our thoughts on record for the benefit of others. ... it never happens that (a beast) arranges its speech in various ways, in order to reply appropriately to everything that may be said in its presence, as even the lowest type of man can do. (1) Descartes argued that Beasts were machines, because, like machines, they lacked certain capabilities of humans. La Mettrie accepted Descartes’ reasoning. (2) But he disagreed about what machines could do. He felt that a machine could be constructed to do anything that a man could do and thus agreed that a man too was a machine. Descartes’s argument took an obvious, well-proven fact about men (their speaking ability) and argued that machines did not have this ability. It’s not obvious that he established his point about machines for it’s not obvious that machines must fail where it is indeed obvious that men succeed. And, as we saw, La Mettrie, for one, was unconvinced to the extent that he turned Descartes’ arguments back upon him and, accepting Descartes’ test, argued that man was a machine, for he believed that machines could be constructed to pass the test. So things were once more at a standstill. In this paper, I concern myself with a similar claim but one placed in a different philosophical climate. Like Descartes, John Lucas (3) (and others) has argued that man couldn’t be a machine for (he argues) man can do something which has been shown by Godel to be beyond the reach of machines. The case is slightly different from Descartes’since Descartes had, of course, nothing resembling a proof that machines were incapable of man’s linguistic behaviour. Remember La Mettrie. Perhaps our latter-day Cartesian has finally struck the mark for now it has been shown that certain machines are logically precluded from succeeding at certain tasks. If it can be shown that man can perform these tasks, then the issue is settled once and for all.

In Minds, machines, and Godel, (1) J. R. Lucas claims that Goedel’s incompleteness theorem constitutes a proof “that Mechanism is false, that is, that minds cannot be explained as machines”. (2) He claims further that “if the proof of the falsity of mechanism is valid, it is of the greatest consequence for the whole of philosophy”. (3) It seems to me that both of these claims are exaggerated. It is true that no mind can be explained as a machine. But it is not true that Goedel’s theorem proves this. At most, Goedel’s theorem proves that not all minds can be explained as machines. Since this is so, Goedel’s theorem cannot be expected to throw much light on why minds are different from machines. Lucas overestimates the importance of Goedel’s theorem for the topic of mechanism, I believe, because he presumes falsely that being unable to follow any but mechanical procedures in mathematics makes something a machine. Lucas explains Goedel’s theorem in this way: Goedel’s theorem states that in any consistent system which is strong enough to produce simple arithmetic there are formulae which cannot be proved-in- the system, but which we can see to be true. (4)

Our unexplained notation is that of Rogers [4]. Let P ⊆ 2N × 2N. We call a sequence of subsets of N a P-sequence iff ∀n(An+1 = the unique B such that P(An, B)).Theorem. Let P ⊆ 2N × 2N be arithmetical. Then there is no P-sequence n: n ∈ N> such that ∀n(A′n+1 ≤T An).This theorem improves a result of Friedman [2] who showed that for no arithmetical P is there a P-sequence such that An + 1 is a code for an ω-model of the relative arithmetic comprehension schema, and An + 1 is present in the model coded by An, for all n. Other related results are those of Harrison [3], who showed there is a sequence such that ∀nn + 1 ≤T An>, and of Enderton and Putnam [1], who showed there is no sequence with ∀n(A′n + 1 ≤T An) and A0 hyperarithmetic.Our theorem is closely connected to Gödel's second incompleteness theorem. Its proof is a recursion theoretic parallel to the proof of Gödel's theorem. In §2 we draw a version of Gödel's theorem as a corollary to ours.

While it is commonly held that the notions of extension and intension originate with the Port Royal logicians, a lively oral tradition has it that they are found explicitly in ARISTOTLE. In several passages of the Organon, ARISTOTLE does speak of the extension of the universals genus and species, often expounding, on the same occasion, the principle that the species is predicated of fewer things than the genus, and giving as example the genus “animal” and the species “man”. He also asserts that the genus is predicated of the species, but not conversely. It can be reasonably argued that these assertions constitute the original formulation of the familiar relation between extension and intension, known as the law of inverse ratio: the extension of the genus contains the extension of the species, while the species comprehends or grasps more of the essence of a thing than does the genus.

Publisher Summary The method of formalizing mathematical proofs gives rise to various formal systems in which certain methods of derivation are delimited in a natural way. Within some of these systems, the chapter is able to formalize all demonstrations of classical number theory, analysis, and set theory. From Godel's incompleteness theorems, it is know that there is no consistent formal system that allows to derive every true arithmetic formula. This can be expressed also by saying that the set of Godel numbers is not recursively enumerable. In a less technical formulation, the number-theoretic concept of truth cannot be operatively defined—that is, the true arithmetic propositions cannot be characterized as those obtained from some explicitly stated propositions and propositional schemata by some rules of procedure given in advance. A complete system (a system that cannot consistently be extended by adding an axiom, which is expressible as a formula of the system) can admit different nonisomorphic models.

In order to prove the completeness theorem (cf. § 2), we use as a technical aid a mapping of the set of all expressions into itself, which we can regard as a sort of isomorphism. In this section, we shall bring together the theorems which we need about such isomorphisms; we shall treat the notion of an isomorphism only insofar as we need it for the following.

Modern computers do not only perform much faster tasks which are already feasible for older calculating machines, but are also fit for more refined, more complicated and more differentiated operations. In particular operations such as self-correction and self-programming make one think almost irresistably of ‘intelligent’ and ‘human’ behavior. For that reason it is no wonder that one has begun to speak of ‘thinking machines’. There is no longer a large step needed to arrive at the notion of a ‘thought machine’, even if that is something completely different.

Publisher Summary This chapter provides the formalization of the theory of ordinal diagrams of infinite order. There is a discussion about a formal theory of some systems of ordinal diagrams, which have been used to prove the consistency of subsystems of classical analysis. By exhibiting a formal system in which the consistency proofs can be formalized, Godel's incompleteness theorem can be used (in the form that no system can prove its own consistency) to form an estimate of what the limits are of the power of such methods. The chapter presents a formal system that is constructive. The intuitionistic arithmetic, that is, Peano's axioms plus primitive recursive definitions plus the intuitionistic predicate calculus are described. The properties of primitive recursive functions can be used and predicates freely in terms of mathematical axioms.

Publisher Summary This chapter discusses three syntactic relations—models, translations, and interpretations— between formal systems from the following points of view: (1) their relation to the consistency problem, (2) their relation to each other, and (3) some of their uses in understanding informal mathematics. The chapter discusses axiomatizable systems—that is, those whose axioms form a (general) recursive set, along with certain non-axiomatizable systems because they are better formalizations of such branches of mathematics as arithmetic and set theory. The systems in which these syntactic relations are established are mentioned explicitly. Both the use of non-axiomatizable systems and explicit mention of metamathematical methods of proof may be regarded as a natural reaction to Godel's incompleteness theorems which shows (1) that axiomatizable systems are not satisfactory approximations to certain branches of mathematics, (2) that various formalizations of these branches of mathematics are of different strength, so that one may expect to learn essentially more from the particular proofs of a theorem than from its assertion.

Publisher Summary This chapter discusses the ultra-intuitionistic criticism and the antitraditional program for foundations of mathematics. The program aims to banish faith from the foundations of mathematics, faith being defined as any violation of the law of sufficient reason (for sentences). This law is defined as the identification (by definition) of truth with the result of a (present or feasible) proof, in spite of the traditional incompleteness theorem, which deals with very narrow kinds of proofs. The methods of traditional mathematical logic are not sufficient for this program: and the domains of means that are explicitly studied in logic have to be enlarged. The rejection of the axiomatic method does not mean the expulsion of the axioms and rules of inference.

Publisher Summary This chapter discusses the principles of proof and ordinals implicit in given concepts. The process of recognizing the validity of such principles (including principles for defining new concepts, that is, formally, of extending a given language) is conceived in the chapter. The informal notions of proof plausible are studied. A number of proof theoretic methods are available. Godel's incompleteness theorem, with an absolute minimum of assumptions on the details of the distinction, shows the existence of theorems stated in elementary terms that do not have an elementary proof. The process of building up the integers by a successor operation, with the property that is distinct from x and from all y built up before x . This process determines an ordering between the integers, and hence an abstract order type.

This paper presents three generalizations of the Second Incompleteness Theorem of Gödel (see [2]) which apply to a broader class of formal systems than previous generalizations (as, e.g., the generalization in [1]).The content of all three of our results is that it is versions of the third derivability condition of Hilbert and Bernays (see p. 286 of [3]) which are crucial to Gödel's theorem. The second derivability condition plays some role in certain logics, but even there, only in the far weaker form of a definability condition (see Theorem 2).The elimination of the first derivability condition allows the application of the Consistency Theorem to cut-free logics which cannot prove that they are closed under cut.It is Theorem 1 which will probably have primary interest for readers who are not concerned with technical proof theory or with foundations, for it treats logics with quantifiers, and in that case one can dispose entirely of the first and second derivability conditions. The derivation of this result requires a “new twist” on old arguments. Specifically, we use a new variation on the standard self-referential lemma (this is Lemma 5.1 of [l]) to obtain a somewhat different self-referential construction than has previously been employed (this is our lemma in §2 below). With this new construction, we consider the sentence φ which “expresses” the fact: “My negation is provable.” Then, using hypotheses associated with Gödel's First Incompleteness Theorem, one shows that ⊢¬φ is impossible in a consistent logic. Finally, using only a version of the third Hilbert-Bernays derivability condition, one shows that the provability of the consistency statement implies ⊢¬φ, and hence that consistency is unprovable.

Godel's Proof By Ernest Nagel and James R. Newman. Pp. ix + 118. (London: Routledge and Kegan Paul, Ltd., 1959.) 12s. 6d. net.

In Philosophy for April 1961 Mr J. R. Lucas argues that Gödel's theorem proves that Mechanism is false. I wish to dispute this view, not because I maintain that Mechanism is true, but because I do not believe that this issue is to be settled by what looks rather like a kind of logical conjuring-trick. In my discussion I take for granted Lucas's account of Gödel's procedure, which I am not competent to criticise.

I Would like to draw attention to the basic defect in the argument used by Mr J. R. Lucas (Minds, Machines and Gödel, Philosophy, July 1961, p. 112).Mr Lucas there states that Gödel's theorem shows that any consistent formal system strong enough to produce arithmetic fails to prove, within its own structure, theorems that we, as humans (‘minds’), can nevertheless see to be true. From this he argues that ‘minds’ can do more than machines, since machines are essentially formal systems of this same type, and subject to the limitation implied by Godel's theorem.

On Formally Undecidable Propositions of Principia Mathematica and Related Systems By Kurt Godel. Translated by Dr. B. Meltzer. Pp. viii + 72. (Edinburgh and London: Oliver and Boyd, Ltd., 1963.) 12s. 6d. net.