Kurt Gödel (1906-1978)
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 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
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 Introduction and implicit in the context of 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.
As you may have read in Gödel, Escher, Bach by Douglas Hofstadter, 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 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:
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 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 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:
Version 0.9 April 1998.
Design and HMTL Presentation © 1998 Siegfried. All rights reserved.