Kurt Gödel and the origins of computer science



Yüklə 9,15 Mb.
tarix01.08.2018
ölçüsü9,15 Mb.
#60068


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.



Yüklə 9,15 Mb.

Dostları ilə paylaş:




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2023
rəhbərliyinə müraciət

    Ana səhifə