[Overview] [Previous] [Next]
Gödel proved that a sufficiently powerful formal system cannot be both consistent and complete. (Simple arithmetic on integers is an example of a system that is "sufficiently powerful.") We prefer to give up completeness rather than consistency, because in a consistent system any proposition can be proven.
Gödel left open the possibility that we could somehow distinguish between the provable propositions and the unprovable ones. Ideally, we would like to have a mechanical (algorithmic) theorem-proving procedure. Alan Turing invented Turing machines in an attempt to solve this problem. With the Halting Problem, he showed that we cannot, in all cases, distinguish between soluable and insoluable problems.
Other mathematicians, working with very different models of computation, ended up with very similar results. One of these was Alonzo Church, who invented recursive function theory.
I have sometimes referred to this course, Formal Languages and Automata Theory, as "compiler construction made difficult." A fairer statement is that this course presents a mathematician's view of the subject, while a course in Compiler Construction presents a programmer's view.
In the same way, recursive function theory is "Lisp made difficult." If, like me, you understand programming more readily than mathematics, learn Lisp before you take a course in recursive function theory. You would not believe the difference it will make.
Copyright © 1996 by David Matuszek
Last modified Apr 17, 1996