View source for Category:Incompleteness theorems

Kurt Gödel dealt a death blow to David Hilbert’s program of formalizing all of mathematics. That was the equivalent then, a century earlier, of Clay Mathematics Institute’s Millennium Problems today.

== Gödel’s first incompleteness theorem ==
Gödel first proved that<blockquote>In any consistent formal system of logic, there are statements which are true, but unprovable.</blockquote>When we say “consistent,” we mean simply that the system is not self-contradictory. However Gödel used a slightly different notion of ω-consistency for technical reasons.

== Gödel’s second incompleteness theorem ==
The second incompleteness theorem is a considerable sharpening of the first.<blockquote>No formal system of logic, proving its own consistency, is consistent.</blockquote>

== Tarski’s theorem on the undefinability of truth ==
Alfred Tarski proved that<blockquote>No well-formed formula exists within any consistent formal system of logic, that assigns a truth value to all well-formed formulæ with no free variables.</blockquote>

== Löb’s theorem ==
Martin Hugo Löb proved that<blockquote>If any mathematical statement is provable assuming ''a priori'' that a valid proof for it exists already, then this assumption may be formally discharged, and the statement is provable ''prima facie'' without any assumption of a pre-existing proof.</blockquote>

== More ==
Kleene’s recursion theorems, the <big><math>s^m_n</math></big> theorem, Rogers’ fixed-point theorem, and the diagonalization lemma also pertain to this category.