Yggdrasil's WN Library Gödel's Theorem^† An HMTL Presentation by Siegfried Kurt Gödel (1906-1978) Kurt Gödel Table of Contents I. [1]Meltzer's Preface II. [2]Braithwaite's Introduction III. [3]On Formally Undecidable Propositions Note on Logical Systems For those of you with an introduction to logic, formal mathematics or computer science, you will undoubtedly have heard of Kurt Gödel. The Austrian mathematician indelibly left his mark on 20th-century science and philosophy with his 1931 paper "On Formally Undecidable Propositions Of Principia Mathematica And Related Systems". His proof of the Undecidability Theorem, summarized and translated herein, is much spoken of but little read. My goal is to make this work available for personal and academic use to all who are interested. The author frequently refers to [4]Principia Mathematica by Alfred North Whitehead and Bertrand Russell. The major contribution of Principia Mathematica is its notation and rules of inference, which can be grasped with a little effort. Even if the reader has only had high-school Geometry or Algerbra II, if persistant he or she should be able to make sense of the logical formulas in the proof. Every statement in logic can be represented by a letter: A, B, C, etc. A single statement A may be attached to a phrase such as "Socrates is a man". A when used in a formula represents the truth-value of the statement behind A. A statement may be determined true or false by observation - or it may also by deduced from an initial set of axioms within a system. Theorems are simply statments deduced from the initial axioms, or any theorems already proven. The operators in logical notation are not very numerous: ~ is the NOT operator; is the OR operator (disjunction); or & is the AND operator (conjunction); means "equivalent to"; means "follows from" or "implies"; "x means "for all x"; $x means "there exists x such that". Some elements from set theory are also used by the author: means "subset of" (subsethood); means "element of" (memberhood). And finally, the author sometimes uses the operators and interchangeably. Given below are examples of laws (or tautologies) in a 'consistent' system: Double Negative: ~(~A) A Law of Noncontradiction: ~(A ~A) TRUE Law of Excluded Middle: A ~A TRUE Also given is an a common rule of inference (termed by Gödel the 'immediate consequence of'): Modus Ponens: (A (A B)) B Note on Typography * You must have the Symbol Truetype font properly installed; * And your internet connection must handle 8-bit transmissions properly -- * If you are using Navigator™ or Internet Explorer™, you should have no problems. The actual proof is quite 'typographically complex' and I have formatted this document to utilize the Symbol Truetype font for the logical symbols needed to convey its meaning adequately. If the above logical statements are readable in your browser, then the proof will be also. I have made a tremendous effort to preserve the original look of the text in HTML format. All 'strings' and 'numerals' are in bold type, as the distinction is explicit in the [5]Introduction and implicit in the context of [6]Gödel's paper. Every reference in the texts has been replaced with a hyperlink to the appropriate location in the proof, if possible. "The symbols Gödel uses for metamathematical concepts or their Gödel numbers are mainly abbreviations of German words. Although the concepts themselves are carefully defined in the text, the following alphabetical list of the more important of these symbols with their etymology may be helpful to the reader: A from 'Anzahl' = number Aeq from 'Aequivalenz' = equivalence Ax from 'Axiom' = axiom B from 'Beweis' = proof Bew from 'Beweisbar' = provable Bw from 'Beweisfigur' = proof-schema Con from 'Conjunktion' = conjunction Dis from 'Disjunktion' = disjunction E from 'Einklammern' = include in brackets Elf from 'Elementarformel' = elementary formula Ex from 'Existenz' = existence Fl from 'unmittelbare Folge' = immediate consequence Flg from 'Folgerungsmenge' = set of consequences Form from 'Formel' = formula Fr from 'frei' = free FR from 'Reihe von Formeln' = series of formulae Geb from 'gebunden' = bound Gen from 'Generalisation' = generalization Gl from 'Glied' = term Imp from 'Implikation' = implication I from 'Lange' = length Neg from 'Negation' = negation Op from 'Operation' = operation Pr from 'Primzahl' = prime number Prim from 'Primzahl' = prime number R from 'Zahlenreihe' = number series Sb from 'Substitution' = substitution St from 'Stelle' = place Su from 'Substitution' = substitution Th from 'Typenerhohung' = type-lift Typ from 'Typ' = type Var from 'Variable' = variable Wid from 'Widerspruchsfreiheit' = consistency Z from 'Zahlzeichen' = number-sign "The only way in which the translation deviates from Gödel's symbolism is that, from p. 57 onwards, c is used to stand for the class which Gödel denotes by k." - Trans. Conclusion As you may have read in [7]Gödel, Escher, Bach by Douglas Hofstadter, [8]The Emperor's New Mind by Roger Penrose, or any number of other contemporary works, the conclusion of 'unprovability' that Gödel proves for a general arithmetic has broader consequences for humanity. One cannot reasonably expect a legal system, a set of physical laws, or a set of religious commandments to have the same rigor that characterizes a recursively enumerable arithmetic. Nevertheless, one can expect examples of logical statements (ex.: 'Is seccession constitutional?') to arise that are neither provable, nor disprovable, within a complete logical framework. Even more interesting, the reality of Platonic 'forms' - ideals contemplated by the human intellect - is questioned by some simple corollaries to Gödel's Theorem. His [9]Propostion XI states that the consistency of any formal deductive system (if it is consistent) is neither provable nor disprovable within the system. A quick leap of logic interprets this corollary as such: 'Any sufficiently complex, consistent logical framework cannot be self-dependent' - i.e., it must rely on intuition, or some external confirmation of certain propositions (specifically, one that proves internal consistency). I now leave to the interested reader the following exercise, attributed to Bertrand Russell^‡: You are trainee at a very formal library in London. Every book must be indexed in one of two giant catalogs. Catalog A contains the citation of every book that makes no reference to itself. Catalog B contains the citation of every book that does contain a reference to itself. The elderly librarian, who is assigned to your group of trainees, now asks the group: "In which volume would you index catalog B?" A perceptive student suggests placing a reference for 'Catalog B' in volume A, since B does not make any reference to itself. The librarian asks again: "Then where would you index Catalog A?" SIEGFRIED __________________________________________________________________ ^† The copyright status of this work is indeterminate. Gödel's original German essay is in the public domain under U.S. Copyright laws. The copyright for the English translation and Braithwaite's Introduction may still be asserted, though there are no renewals on record at the [10]U.S. Copyright Office. Meltzer states in the Preface his desire to make this paper as widely read as possible, and I take this as license to distribute this electronic copy for personal and academic use (after all, this is an academic paper). A [11]paperbound volume is available from Dover Publications (though they do not assert a copyright) and I encourage all who value this work to purchase a copy. ^‡ His original paradox, or epistemologicol antinomy, is as follows: R is the set of all sets which are not members of themselves. Thus the statement: "Set R is a member of itself" is indeterminate. __________________________________________________________________ [12]Back Version 0.9 – April 1998. Design and HMTL Presentation © 1998 Siegfried. All rights reserved. References 1. file:///var/lib/mailman/archives/private/cypherpunks-legacy/attachments/20001104/d41abe11/godel1.htm 2. file:///var/lib/mailman/archives/private/cypherpunks-legacy/attachments/20001104/d41abe11/godel2.htm 3. file:///var/lib/mailman/archives/private/cypherpunks-legacy/attachments/20001104/d41abe11/godel3.htm 4. http://plato.stanford.edu/entries/principia-mathematica/ 5. file:///var/lib/mailman/archives/private/cypherpunks-legacy/attachments/20001104/d41abe11/godel2.htm 6. file:///var/lib/mailman/archives/private/cypherpunks-legacy/attachments/20001104/d41abe11/godel3.htm 7. http://www.amazon.com/exec/obidos/ISBN=0394756827/ 8. http://www.amazon.com/exec/obidos/ISBN=0140145346/ 9. file:///var/lib/mailman/archives/private/cypherpunks-legacy/attachments/20001104/d41abe11/godel3.htm#PROP-XI 10. http://lcweb.loc.gov/copyright/rb.html 11. http://www.amazon.com/exec/obidos/ISBN=0486669807/ 12. file:///var/lib/mailman/archives/private/cypherpunks-legacy/attachments/20001104/index.htm