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

In any consistent formal system of logic, there are statements which are true, but unprovable.

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.

No formal system of logic, proving its own consistency, is consistent.

Tarski’s theorem on the undefinability of truth

Alfred Tarski proved that

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.

Löb’s theorem

Martin Hugo Löb proved that

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.

More

Kleene’s recursion theorems, the ${\displaystyle s_{n}^{m}}$ theorem, Rogers’ fixed-point theorem, and the diagonalization lemma also pertain to this category.