Kurt Gödel and the origins of computer science

Kurt Gödel and the origins of computer science

• John W. Dawson, Jr.

• Pennsylvania State University

• York, PA U.S.A.

Kurt Gödel (1906–1978)

• Considered the greatest mathematical logician of the twentieth century, he was one of the founders of recursion theory.

• A Princeton colleague of Alonzo Church and John von Neumann, his impact on computer science was seminal, but largely indirect.

Works by Gödel of special relevance to computer science

• Completeness of first-order logic (1930)

• Incompleteness of formal number theory (1931)

• Papers on decision problems (1932–33)

• Definition of the notion of general recur-sive function (IAS lectures, 1934; first published 1965)

• “On the lengths of proofs” (1936)

• “Some basic theorems on the founda-tions of mathematics, and their philo-sophical implications” (Gibbs Lecture, *1951)

• Letter to von Neumann (*1956)

• “A philosophical error in Turing’s work” (1972; first published 1974)

• *First published posthumously in Gödel’s Collected Works

The 1930 Completeness Paper

• In his first published paper (a revision of his doctoral dissertation), Gödel stated the com-pleteness of first-order logic in the form: “Every valid formula of first-order logic [one true under every interpretation] is provable from the logical axioms.”

• But as in the dissertation, he proved it in the form “Every formula is either refutable or satis-fiable.” He then extended the result to countable sets of formulas, to yield “A countable consistent set of formulas has a model”.

The Strong Completeness Theorem

• The main focus of Gödel’s 1930 paper is that a formula of first-order logic is valid if and only if it is derivable using the rules of inference given earlier by Hilbert and Ackermann. But he actually proved more:

• (Strong completeness) For any set Σ of first-order axioms, φ holds in every model of Σ if and only if φ is provable from Σ ( a result first stated explicitly by Abraham Robinson in 1951).

Significance for computer science

• The strong completeness theorem shows

• that the rules of inference developed prior

• to Gödel’s work are adequate for the pur-

• pose of deriving all logical consequences of

• a set of axioms. A computer incorporating

• just those rules will thus be able to carry out

• all such derivations.

Completeness vs. incompleteness

• The completeness theorem entails that the

• statements provable in any first-order

• axiomatization of number theory are those

• that are true in all models of the axioms.

• But for no recursive axiomatization will

• those statements coincide with the state-

• ments that are true of the natural numbers:

The Gödel-Rosser Theorem

• Any recursive axiomatization A of arithmetic

• must either be inconsistent (and so prove

• every statement φ ) or else fail to prove both

• some variable-free statement φ and its

• negation. Hence if A is consistent, it must

• fail to prove some statement that is true of

• the natural numbers.

• The Gödel-Rosser Theorem is a limitative

• result. In the context of computer science,

• as is well known, Alan Turing used the

• correspondence between computer pro-

• grams and formal systems to recast it as

• The Halting Problem: No recursive pro-cedure can correctly determine, for an arbitrarily given computer running any specified program, whether or not the computer will eventually come to a halt.

The larger significance of Gödel’s incompleteness paper

• For the development of computer science,

• the proof Gödel gave of his incompleteness

• results was more important than the

• theorems themselves. Three aspects of

• the proof were of particular significance:

• His precise definition of the class of (what are now called) primitive recursive functions

• His distinction between object language and metalanguage.

• His idea of representing one data type (sequences of strings) by another type (numbers), thereby coding metatheo-retical notions as number-theoretic predicates.

• In addition, as Martin Davis has remarked, the

• overall structure of Gödel’s proof “looks very much

• like a computer program” to anyone acquainted

• with modern programming languages — unsur-

• prisingly, since though “an actual … general-

• purpose … programmable computer was still

• decades in the future,” Gödel faced “many of the

• same issues that those designing programming

• languages and …writing programs in those

• languages” face today.

The second incompleteness theorem

• As a further example of a numerical state-

• ment that must be formally undecidable

• within any consistent, recursive axioma-

• tization of arithmetic, Gödel adduced a

• numerical encoding of a statement asserting

• the theory’s consistency.

Philosophical significance of the incompleteness theorems

• Much later, in his Gibbs Lecture to the American

• Mathematical Society (1951),Gödel would suggest

• that the incompleteness theorems are relevant to

• the questions

• whether the powers of the human mind exceed those of any machine, and

• whether there are mathematical problems that are undecidable for the human mind.

Special cases of the decision problem

• During the years 1932–33 Gödel turned his

• attention to the decision problem — the

• question whether there is an algorithm for

• determining whether an arbitrary formula

• of first-order logic is valid or not. He estab-

• lished two results, concerning particular

• prefix classes of quantificational formulas:

• He exhibited an algorithm for deciding the validity or invalidity of formulas in one quantifier-prefix class.

• He showed that the (full) decision problem is reducible to that for formulas in another quantifier-prefix class.

• Subsequently, on the basis of Church’s Thesis,

• Church and Turing each demonstrated that the full

• decision problem is algorithmically unsolvable.

Extending the scope of the incompleteness theorems

• Gödel spent the academic year 1933–34 in

• Princeton at the Institute for Advanced Study.

• That spring, in a course of lectures on exten-

• sions of his incompleteness results, he defined

• the notion of general recursive function, based on

• an idea suggested to him by Jacques Herbrand.

Gödel’s definition and Church’s Thesis

• Gödel’s was one of several definitions later shown

• to characterize the same class of functions.

• On 19 April 1935, in a talk before a meeting of the

• American Mathematical Society, Church pro-

• pounded his Thesis:

• The class so characterized consists of exactly

• those functions informally thought of as being

• effectively computable.

Two points of note

• In enunciating his Thesis, Church used the Gödel-Herbrand definition, rather than his own characterization of that class of functions (as those that are λ-definable).

• Gödel himself was skeptical of Church’s Thesis, and only came to accept it in the wake of Turing’s analysis of the opera-tions performed by human computors.

Gödel’s prescience (I)

• On 19 June 1935 Gödel made his last pre-

• sentation to Karl Menger’s mathematical

• colloquium. Titled “On the length of proofs”,

• it appeared the following year as a two-page

• article in the colloquium proceedings. It is

• now regarded as the first announcement of

• a “speed-up” theorem.

Remarks:

• Gödel stated his result without proof. The first published proof was given by Sam Buss in 1994.

• The measure of length Gödel used is the number of lines (inferences) in the proof, not the number of symbols.

• It is unclear whether Gödel intended + and ∙ to be represented by function symbols or predicate symbols.

Gödel’s Prescience (II)

• Gödel did not pursue the ideas in his length-

• of-proof paper, which seems to have been

• an afterthought to his incompleteness

• theorems.

• Much later, in a letter to his terminally ill

• friend von Neumann, Gödel made another

• observation he did not follow up: The first

• known formulation of the P = NP problem.

Gödel’s 1956 letter to von Neumann

The Gibbs Lecture (1951)

• In his Gibbs Lecture, Gödel attempted

• to draw implications from the incom-

• pleteness theorems concerning three

• problems in the philosophy of mind:

• Whether there are mathematical ques-tions that are “absolutely unsolvable” by any proof the human mind can conceive

• Whether the powers of the human mind exceed those of any machine

• Whether mathematics is our own creation or exists independently of the human mind

Gödel’s conclusions

• With regard to the first two questions, Gödel

• argued that “Either … the human mind (even

• within the realm of pure mathematics)

• infinitely surpasses the powers of any finite

• machine, or else there exist absolutely

• unsolvable diophantine problems”. He

• believed the first alternative was more likely.

What Gödel didn’t claim

• Unlike commentators such as John Lucas

• and Roger Penrose, Gödel did not assert

• that the incompleteness theorems defini-

• tively refute mechanism, nor (as Judson

• Webb has asserted) that “the Church-Turing

• thesis … is the principal bastion protecting

• mechanism”.

• As to the ontological status of mathematics,

• Gödel claimed that the existence of abso-

• lutely unsolvable problems would seem

• “to disprove the view that mathematics is …

• our own creation; for [a] creator necessarily

• knows all properties of his creatures”. He

• admitted that “we build machines and still

• cannot predict their behavior in every detail”.

• But that objection, he said, is “very poor”:

• “For we don’t create … machines out of

• nothing, but build them out of some

• given material.”

• It seems he recognized that hardware

• may behave unpredictably, but not

• software (!)

Turing’s contrary view (1948)

• “The view that intelligence in machinery is merely a reflection of that of its creator is … similar to the view that … credit for the discoveries of a pupil should be given to his teacher. In such a case the teacher [sh]ould be pleased with the success of his methods of education, but [sh]ould not claim the results themselves unless he ha[s] actually communicated them to his pupil” --- Alan Turing, “Intelligent machinery”

• To put Gödel’s belief in perspective, note

• that, unlike Turing or von Neumann, he was

• never involved with the design or operation

• of actual computers — even though it was at

• the IAS that von Neumann built one of the

• earliest computers.

• Consider also the statement that computer

• pioneer Howard Aiken made five years later:

“If it should turn out that the basic logics of a machine designed for the numerical solution of differential equations coincide with the logics of a machine intended to make bills for a department store, I would re-gard this as the most amazing coin-cidence I have ever encountered.”

Gödel’s criticism of Turing

• Despite his high regard for Turing’s work,

• late in his life Gödel claimed that Turing had

• erred in arguing that mental procedures

• cannot go beyond mechanical procedures.

• Specifically, he charged that Turing had

• completely disregarded “that mind, in its

• use, is not static but constantly developing.”

In defense of Turing

• Contrary to Gödel’s charge, in his 1950

• paper “Computing machinery and intelli-

• gence”, Turing explicitly discussed learning

• machines. There, too, he countered various

• objections to the idea that machines could

• simulate human thought, including the

• “mathematical objection” based on the

• incompleteness theorems.

Some imponderables

• Gödel and Turing never met, nor did they

• exchange any correspondence of sub-

• stance. Gödel delivered his Gibbs Lecture

• one year after the appearance of Turing’s

• paper quoted above, and his criticism of

• Turing came long after Turing’s death.

• One must therefore wonder:

• At the time of his Gibbs Lecture, was Gödel aware of Turing’s 1950 paper?

• Gödel’s Gibbs Lecture was delivered less that three years before Turing’s death, just months before his prosecution for homosexuality, and it was not pub-lished until 1995. Did Turing ever become aware of its contents?

Gödel and Emil Post

• Emil Post was an important contributor to

• recursion theory, and helped to initiate the

• field of automata theory. Twenty years

• before Gödel, he also conjectured (and

• nearly proved) the incompleteness of formal

• number theory. His outlook, however, was

• very different from Gödel’s.

• Post met Gödel in October of 1938.

• Shortly afterward he wrote to Gödel to

• expound further on his “near miss”. He

• explained that he had set out to demonstrate

• the existence of absolutely unsolvable prob-

• lems, and thought he “saw a way of analyz-

• ing ‘all finite processes of the human mind’ ”

• that would establish incompleteness “in

• general, … not just for Principia Mathema-

• tica.”

• Arguably, Post contributed more directly to

• the development of computer science than

• Gödel did. But as he himself conceded in

• that same letter, “Nothing that I had done

• could have replaced the splendid actuality of

• your proof.” Sidetracked by his quest to

• exhibit an absolutely unsolvable problem,

• Post failed to give an example of one that

• was undecidable in a particular formalism.

Questions to ponder

• If Gödel were alive today, what would he think of the role of computers in mathe-matics?

• Would he approve of their use in providing numerical evidence for conjectures?

• What would he think of computer-assisted proofs?

• Would he maintain his belief in the mind’s superiority?

Basic References

• Kurt Gödel, Collected Works (5 vols.), ed. Solomon Feferman et al. Oxford University Press, 1986–2003.

• The Essential Turing, ed. B. Jack Copeland, Oxford University Press, 2004.

• Solvability, Provability, Definability: The Collected Works of Emil L. Post, ed. Martin Davis. Birkhäuser, 1994.