Yggdrasil's WN Library

Gödel's Theorem

An HMTL Presentation by Siegfried

Kurt Gödel (1906-1978)

Kurt Gödel

Table of Contents

  1.  Meltzer's Preface
  2.  Braithwaite's Introduction
  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 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:

Also given is an a common rule of inference (termed by Gödel the 'immediate consequence of'):

Note on Typography

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:

Afrom 'Anzahl' = number
Aeqfrom 'Aequivalenz' = equivalence
Axfrom 'Axiom' = axiom
Bfrom 'Beweis' = proof
Bewfrom 'Beweisbar' = provable
Bwfrom 'Beweisfigur' = proof-schema
Confrom 'Conjunktion' = conjunction
Disfrom 'Disjunktion' = disjunction
Efrom 'Einklammern' = include in brackets
Elffrom 'Elementarformel' = elementary formula
Exfrom 'Existenz' = existence
Flfrom 'unmittelbare Folge' = immediate consequence
Flgfrom 'Folgerungsmenge' = set of consequences
Formfrom 'Formel' = formula
Frfrom 'frei' = free
FRfrom 'Reihe von Formeln' = series of formulae
Gebfrom 'gebunden' = bound
Genfrom 'Generalisation' = generalization
Glfrom 'Glied' = term
Impfrom 'Implikation' = implication
Ifrom 'Lange' = length
Negfrom 'Negation' = negation
Opfrom 'Operation' = operation
Prfrom 'Primzahl' = prime number
Primfrom 'Primzahl' = prime number
Rfrom 'Zahlenreihe' = number series
Sbfrom 'Substitution' = substitution
Stfrom 'Stelle' = place
Sufrom 'Substitution' = substitution
Thfrom 'Typenerhohung' = type-lift
Typfrom 'Typ' = type
Varfrom 'Variable' = variable
Widfrom 'Widerspruchsfreiheit' = consistency
Zfrom '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.