Topic: Liar's paradox and Russell's paradox
Topic: limitations of formalism
Topic: mathematics as a formal system
Topic: Turing machine
 
Summary
Godel's 1931 paper was an important landmark in mathematical logic. It proved that Hilbert's program to formalize mathematics could not be completed. Godel's approach was to arithmetize a formal system, i.e., he assigned a number to every statement in the system. He then constructed a statement that said of itself 'I am not provable'. As Godel showed, this statement is clearly true, but it can not be proved true in the system. Like all other statements, it had an equivalent number (its Godel number). Now, if G was proved in a consistent system, it would deny its nonprovability. On the contrary, if G is not provable and the system is suitably consistent, then we can construct a proof of not G. Godel's second theorem shows that the consistency of a system implies that G is provable. Thus the consistency of the formal system can not be proved within the formal system. For more details, see van Heinenoort's article on Godel's Theorem in Encyclopedia of Philosophy.
Godel's theorems are related to the Liar's paradox, to Richard's antimony, and to the halting problem of Turing machines. (cbb 4/94)
Subtopic: incompleteness
Quote: can not prove the consistency of any consistent formal system that contains a certain amount of number theory
 Quote: although Principia mathematica and ZermeloFraenkel set theory formalize all of mathematics, they contain simple, undecidable problems [»godeK_1931]
 Quote: the consistency of a recursive consistent class of formulas is not provable in the system [»godeK_1931]
 Quote: a formal system is complete if every true statement that can be expressed in the system is a theorem of the system [»hofsDR_1979]
 Subtopic: effective calculable
Quote: Church proposed a definition for effectively calculable functions and demonstrated an unsolvable problem [»churA_1936]
 Quote: no complete set of effectively calculable invariants of conversion exist; for example, if Principia Mathematica is omegaconsistent, its Enthscheidungsproblem is unsolvable [»churA_1936]
 Subtopic: Godel's sentence
Quote: gives Godel's sentence; it is true because it is unprovable in the system PM [»godeK_1931]
 Quote: Godel's sentence is similar to the Liar's paradox and Richard's antimony
 Quote: there is no general process to determine whether a given formula is provable; contrast with Godel's proof that there exist propositions U such that neither U nor U is provable [»turiAM11_1936]
 Quote: let 'Jack' be a name of the sentence 'Jack is short'; could use to prove Godel's incompleteness theorem [»kripS_1975]
 Quote: informal description of Godel's string [»hofsDR_1979]
 Quote: the Godel sentence G, if it were a true theorem, would state "G is not a theorem" [»hofsDR_1979]
 Quote: Godel's string is equivalent to "I can not be proved in the formal system" [»hofsDR_1979, OK]
 Subtopic: randomness
Quote: to prove that a particular series of digits is random must prove that there is no small program for it; probably impossible [»chaiGJ5_1975]
 Subtopic: Godel numbering
Quote: easily identify hierarchical relations with symbolic numbers; e.g., if man is 6 and ape is 10 then neither concept contains the other [»leibGW4_1679]
 Quote: a Godel numbering defines a number isomorphism for any formal system; typographic rules are arithmetic [»hofsDR_1979]
 Quote: a Godel number is a name for a string [»hofsDR_1979, OK]
 Subtopic: truth not provable
Quote: need a theory of truth because truth can not be identified with mathematical provability; Godel [»tarsA_1944, OK]
 Quote: Godel proved that provability is a weaker notion than truth no matter what axiomatic system is involved [»hofsDR_1979]

Related Topics
Topic: Liar's paradox and Russell's paradox (25 items)
Topic: limitations of formalism (93 items)
Topic: mathematics as a formal system (30 items)
Topic: Turing machine (30 items)
