Logic and Modern Philosophy of Mathematics - Gödel, Tarski, And The Individuation Of Metatheory

More bad news for Hilbert arrived in 1931, when the young Austrian Kurt Gödel proved that his metamathematical program could not be achieved for arithmetic with quantification over integers, and thus a fortiori for almost all acclimatized mathematical theories T; for Gödel showed that, in order to prove the consistency of T, its metamathematics had to be richer in assumptions than T itself rather than poorer, as Hilbert had hoped. This theorem was a corollary of another one, which torpedoed logicism by showing that there was a proposition M statable within T but neither provable nor disprovable; thus T, assumed to be consistent, was undecidable.

In addition, Gödel's proof-method soon led to a focus on recursion and to computability as conceived by the Englishman Alan Turing, thus launching a link between logic and computing. Finally, for Gödel's proofs to work the distinction between T and its metatheory had to be observed rigidly, as a central feature of both metamathematics and metalogic. The Polish logician Alfred Tarski also stressed this distinction around this time, for formal systems in general; his motive was treating as metatheoretic the (meta-)proposition that a proposition was true if it corresponded to the facts.