Return to the home page for Patrick Kellogg
Throughout history, there has been a desire to use machines to replace human beings. Kurt Vonnegut uses this as the basis of his novel “Player Piano”, by noting the ways machines have been integrated into the workplace. “First the musclework, then the routine work, then, maybe, the real brainwork”. If computers are better than us at calculating complex equations and analyzing large sets of data, why couldn't they be used to create the proofs and theorems that make up math itself?
For example, I could create a propositional calculus that has the definition “A rectangle has four right angles” and the definition that “A right angle has 90 degrees”. Then, I could create a computer program that can modify the given rules, and test to see if certain new theorems were true. Perhaps my program could use the first two rules to “discover” the idea that the interior angles of a rectangle sum up to 360 degrees! Left running for a few weeks, could my computer figure out all of geometry, and then move on to discover topology and statistics by itself?
For the first thirty years of this century, many top scientists studied the metamathematics of trying to derive all of mathematics from a few basic proofs and a solid propositional calculus. In 1910, Alfred North Whitehead and Bertrand Russell thought they had the problem solved by publishing “Principia Mathematica”, a giant exploration of the foundations of mathematical logic. Hundreds of lines of their proof are spent discussing the cardinality of the number “1”, or the idea of assertions or true/ false statements. For years afterward, mathematicians debated whether this new grand system of Russell and Whitehead's was consistent (contradiction-free) and complete (i.e. every true statement of number theory could be derived from the Principia Mathematica).
Then, in 1931, a mathematician named Kurt Gödel shattered the foundation of P.M. by publishing a paper called “On Formally Undecidable Propositions in Principia Mathematica and Related Systems 1”. He analyzed the following sentence:
In can be shown that the above sentence could be true and valid, but still be unprovable within Whitehead and Russell's calculus. The idea is similar to the paradox, “This sentence is false”, which is neither true nor false, but exists in a separate world from simple true or false statements.
So, how is this applicable to the Verification Logic we have learned in CSCI 3155? In class, we talked about how we could determine if a loop is infinite or if it terminates. Gödel's Theorem was used in 1937 by another mathematician, Alan Turing, to prove the unsolvability of the “halting problem”. In the same way that a formal logic cannot discover the rules that govern itself, a program cannot decide if it itself will ever terminate. It is important for students to realize that the tools of Verification Logic are powerful, but not complete.
I personally dislike the idea that a complete solution can be achieved by the sum of smaller bits. This idea is at the heart of science and math, but doesn't take into consideration the “holistic” nature of human knowledge. The field of artificial intelligence has suffered due to the idea that adding “enough” knowledge to a system will suddenly make it self-aware or intelligent. Kurt Vonnegut agreed with the futility of adding up rules upon rules of facts in another book, “Cat's Cradle”:
“(Dr. Breed said that) New knowledge is the most valuable commodity on earth. The more truth we have to work with, the richer we become. Had I been a Bokononist then, that statement would have made me howl.”
Hájek, Petr (Editor) “Gödel '96” Bruno, Czech Republic, August 1996Proceedings
Hofstadter, Douglas R. “Gödel, Escher, Bach: and Eternal Golden Braid” Basic Books, Inc. New York, 1979
Vonnegut Jr., Kurt “Cat's Cradle” Dell Publishing Co, Inc. New York 1963
Vonnegut Jr., Kurt “Player Piano” Dell Publishing Co, Inc. New York 1952
Whitehead, Alfred North and Russell, Bertrand “Principia Mathematica”