 In the proof above we reduced Gödel’s incompleteness theorem to an application of Tarski’s theorem in order to show the close link between the two (this version of the proof is due to Bolander, 2002). Gödel was well aware of this link, and indeed it seems that Gödel even proved Tarski’s theorem before Tarski himself did (Feferman, 1984). Gödel’s theorem can be interpreted as demonstrating a limitation in what can be achieved by purely formal procedures. It says that if first-order arithmetic is \(\omega\)-consistent (which it is believed to be), then there must be arithmetical sentences that can neither be proved nor disproved by the formal procedures of first-order arithmetic. One might at first expect this limitation to be resolvable by the inclusion of additional axioms, but Gödel showed that the incompleteness result still holds when first-order arithmetic is extended with an arbitrary finite set of axiom schemas (or, more generally, an arbitrary recursive set of axioms). Thus we obtain a general limitation result saying that there cannot exist a formal proof procedure by which any given arithmetical sentence can be proved to hold or not to hold. For more details on Gödel’s incompleteness theorem, see the entry on  Kurt Gödel.