Gödel and Computer Science
For today, I have only one question where I'd like to get some feedback from all you out there in the infinite void of the Web universe. As you might know, there was an austrian mathematician Kurt Gödel who lived in the last century. He proved that for simple mathematical logic calculi everything that is true also can be computed (i.e., automatically derived from some basic axioms). For higher level quantification theories (i.e., where logic statements can reflect on predicates) this does not hold anymore. Thus, there must be truths which can not be computed by any processor. In the software world processors can be CPUs, Model Generators, Interpreters, Inference Engines. I am wondering whether there are any practical implications of this constraint? Or is this theoretically interesting but without any practical consequence whatsoever? So, what's your guess?
posted by Michael at
11:43 PM
3 Comments:
Good point. I guess that this means for instance that there might be domains that can not be covered by model-driven approaches. And also that automation has its clear limitations in software engineering. It also means that our brains are somehow limited. So are our software systems :-)
By
Anonymous, at 11:54 PM
It was Jimmy Nilsson, Karlskrona, Sweden, who draws my attention to your blogg and asked me, at least, to recommend a good book for those interested. I will recommend not just one but the following two books that are very clearly and pedagogically written.
Godel's Proof by Ernest Nagel, James R. Newman, Douglas R. Hofstadter (Editor)
The Emperor's New Mind : Concerning Computers, Minds, and the Laws of Physics (Popular Science) (Paperback) by Roger Penrose, Martin Gardner (Foreword)
The second book is interesting in that it argues that Gödel’s theorems show that the human mind is superior to any formal system (computer). It should be noted that Penrose’s argument is not without objections and has been criticized by practicing logicians. In any case, it is a very thought-provoking book.
Just a few comments on your text. Your write: He proved that for simple mathematical logic calculi everything that is true also can be computed (i.e., automatically derived from some basic axioms). As I understand it, this statement is a confusion of two different concepts. First, if you by simple mathematical logic mean propositional calculus, it was proved before Gödel that the provable sentences are the valid. However, as is pointed out below, this is also true for predicate calculus. The second statement in your sentence is true for propositional calculus only, not for predicate calculus, as is clear from Gödel’s theorems given below.
Gödel’s dissertation was the proof of the completeness theorem in which he proves that “in any predicate calculus, the theorems are precisely the logically valid” (cf. with your statement above).
Then he proved two so called incompleteness theorem. In fact he did not prove the second of them because it seemed obvious even if the proof is tedious. It was not formally proved until 1939 by Hilbert and Bernays. Now for the theorems:
1. Given any carefully defined notion of proof, there exists either a provable but false statement in the language of arithmetic or else a true but unprovable statement in the language of arithmetic.
2. If F is a formal system (containing arithmetic), then if F is consistent, then the consistency of F cannot be proved within F, that is, a consistency proof of F must use ideas and methods that go beyond those available in F.
More popularly expressed, (1) says that no formal system can catch all the true statements. It means that if we have a statement, we cannot be sure of proving it or its negation: there is no mechanical method for generating true statements (cf. the second part of your quoted statement above).
However, it is the second theorem that has mostly been of concern when discussing whether Gödel’s theorems show that the human mind is more than a computer. Jaakko Hintikka (On Gödel [2000]) writes: It may be true in some sense that the human mind operates in a way different from the modus operandi of a Turing machine (computer: my comment), and even that Gödel’s theorem (second: my comment) shows this difference. However, the arguments offered in the literature are for the most part highly unsatisfactory. For one thing, what is it that humans are supposed to know but machines not? Presumably the existence of a true but unprovable arithmetic proposition. But Gödel’s argument does not prove the existence of absolutely unprovable arithmetic truths. Its conclusion is relative to some given first-order axiom system of elementary arithmetic […].
I hope this will bring some clarity of the subject but also that it will inspire to more reading on the subject. Good luck!
By
Anonymous, at 3:29 PM
Hi both of you,
thanks a lot for your comments. I know these books, Bertil. I am sceptical about Roger Penrose. But may be, I am too much influenced by my background in science and mathematics. There are also some more books by Douglas Hofstadter which are really recommendable.
In the case of Gödel: I had to illustrate the Gödel proof as part of my exams at university.
Below is a citation from http://www-history.mcs.st-andrews.ac.uk/Biographies/Godel.html which tells exactly what I had said. You are right with your comments but I didn't say anything about propositional or predicate logic. It was only my intention to proof that there are some kind of loop holes in logic:
Gödel is best known for his proof of "Gödel's Incompleteness Theorems". In 1931 he published these results in Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. He proved fundamental results about axiomatic systems, showing in any axiomatic mathematical system there are propositions that cannot be proved or disproved within the axioms of the system. In particular the consistency of the axioms cannot be proved. This ended a hundred years of attempts to establish axioms which would put the whole of mathematics on an axiomatic basis. One major attempt had been by Bertrand Russell with Principia Mathematica (1910-13). Another was Hilbert's formalism which was dealt a severe blow by Gödel's results. The theorem did not destroy the fundamental idea of formalism, but it did demonstrate that any system would have to be more comprehensive than that envisaged by Hilbert. Gödel's results were a landmark in 20th-century mathematics, showing that mathematics is not a finished object, as had been believed. It also implies that a computer can never be programmed to answer all mathematical questions.
By
Michael, at 5:12 PM
Post a Comment
<< Home