*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**

- 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 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,cis used to stand for the class which Gödel denotes byk." -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^{‡}:

- 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 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:

- Thus the statement: "Set

Version 0.9 – April 1998.

Design and HMTL Presentation © 1998 Siegfried. All rights reserved.