sequence of plausible claims is made, interspersed with phrases like “it can be
seen easily” and “it follows from this.” Such phrases are conventional, and what
one means by them is that, if challenged to do so, one could give more detailed
reasoning. Of course, this is very dangerous, since it is possible to overlook
things, use faulty hidden assumptions, or make wrong inferences. Whenever we
see arguments like this, we cannot help but wonder if the proof we are given is
indeed correct. Often there is no way of telling, and long and involved proofs
have been published and found erroneous only after a considerable amount of
time. Because of practical limitations, however, this type of reasoning is
accepted by most mathematicians. The arguments throw light on the subject and
at least increase our confidence that the result is true. But to those demanding
complete reliability, they are unacceptable.
One alternative to such “sloppy” mathematics is to formalize as far as
possible. We start with a set of assumed givens, called axioms, and precisely
defined rules for logical inference and deduction. The rules are used in a
sequence of steps, each of which takes us from one proven fact to another. The
rules must be such that the correctness of their application can be checked in a
routine and completely mechanical way. A proposition is considered proven true
if we can derive it from the axioms in a finite sequence of logical steps. If the
proposition conflicts with another proposition that can be proved to be true, then
it is considered false.
Finding such formal systems was a major goal of mathematics at the end of
the nineteenth century. Two concerns immediately arose. The first was that the
system should be consistent. By this we mean that there should not be any
proposition that can be proved to be true by one sequence of steps, then shown to
be false by another equally valid argument. Consistency is indispensable in
mathematics, and anything derived from an inconsistent system would be
contrary to all we agree on. A second concern was whether a system is
complete, by which we mean that any proposition expressible in the system can
be proved to be true or false. For some time it was hoped that consistent and
complete systems for all of mathematics could be devised thereby opening the
door to rigorous but completely mechanical theorem proving. But this hope was
dashed by the work of K.Gödel. In his famous incompleteness theorem, Gödel
showed that any interesting consistent system must be incomplete; that is, it
must contain some unprovable propositions. Gödel's revolutionary conclusion
was published in 1931.
Gödel's work left unanswered the question of whether the unprovable
statements could somehow be distinguished from the provable ones, so that there
seen easily” and “it follows from this.” Such phrases are conventional, and what
one means by them is that, if challenged to do so, one could give more detailed
reasoning. Of course, this is very dangerous, since it is possible to overlook
things, use faulty hidden assumptions, or make wrong inferences. Whenever we
see arguments like this, we cannot help but wonder if the proof we are given is
indeed correct. Often there is no way of telling, and long and involved proofs
have been published and found erroneous only after a considerable amount of
time. Because of practical limitations, however, this type of reasoning is
accepted by most mathematicians. The arguments throw light on the subject and
at least increase our confidence that the result is true. But to those demanding
complete reliability, they are unacceptable.
One alternative to such “sloppy” mathematics is to formalize as far as
possible. We start with a set of assumed givens, called axioms, and precisely
defined rules for logical inference and deduction. The rules are used in a
sequence of steps, each of which takes us from one proven fact to another. The
rules must be such that the correctness of their application can be checked in a
routine and completely mechanical way. A proposition is considered proven true
if we can derive it from the axioms in a finite sequence of logical steps. If the
proposition conflicts with another proposition that can be proved to be true, then
it is considered false.
Finding such formal systems was a major goal of mathematics at the end of
the nineteenth century. Two concerns immediately arose. The first was that the
system should be consistent. By this we mean that there should not be any
proposition that can be proved to be true by one sequence of steps, then shown to
be false by another equally valid argument. Consistency is indispensable in
mathematics, and anything derived from an inconsistent system would be
contrary to all we agree on. A second concern was whether a system is
complete, by which we mean that any proposition expressible in the system can
be proved to be true or false. For some time it was hoped that consistent and
complete systems for all of mathematics could be devised thereby opening the
door to rigorous but completely mechanical theorem proving. But this hope was
dashed by the work of K.Gödel. In his famous incompleteness theorem, Gödel
showed that any interesting consistent system must be incomplete; that is, it
must contain some unprovable propositions. Gödel's revolutionary conclusion
was published in 1931.
Gödel's work left unanswered the question of whether the unprovable
statements could somehow be distinguished from the provable ones, so that there