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