Gödel and Metamathematics

David Baños Abril

12 de July de 2026 15 min read

This article is dedicated to what is undoubtedly one of the most extraordinary mathematical discoveries of all time—and the culmination of attempts to formalize mathematics dating back to the era of Frege, which has been the subject of this series: the Incompleteness Theorems. Their implications for our understanding of mathematics and our own cognition still resonate today and have elevated Gödel to the ranks of the century's great minds.

Kurt Gödel and Metamathematics

A still-unknown Kurt Gödel astonished the mathematical community when, at only twenty-three years of age, he provided a proof of the completeness of the first-order predicate calculus. Gödel presented this result in his 1929 doctoral thesis and published it the following year. As we noted in the previous article, completeness was one of the fundamental questions that remained open in Mathematical Logic.

Hilbert’s lecture at the 1928 International Congress of Mathematicians in Bologna helped awaken Gödel’s interest in problems concerning the completeness, consistency, and decidability of formal systems. This early interest would enable him to produce the important result we have just mentioned.

But he still had much more to offer. Barely two years later, in 1930, Gödel announced the results that would bring him lasting fame. His complete proof would be published in 1931 under the title Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme —“On Formally Undecidable Propositions of Principia Mathematica and Related Systems.”

The Incompleteness Theorems will be the subject of the next article. Before approaching their proof, we need to introduce two tools developed by Gödel: recursive functions and the arithmetization of syntax through the so-called Gödel numbers.

The Formalist Program

As we have seen throughout this series, by the late 1920s the objectives of the so-called Formalist Program had been fully formulated, with Hilbert as its leading advocate. This program sought to formalize mathematical theories—that is, to transform Arithmetic, Geometry, and Analysis into systems of symbols governed by explicit axioms and rules of inference.

Within a formal system, proofs had to be checkable solely by attending to the form of the symbols, without relying on an intuitive interpretation of their meaning. Starting from a set of initial axioms, the rules would make it possible to obtain, in a finite number of steps, new formulas expressing the theorems characteristic of each mathematical field.

This mechanical character of formal deduction can be compared with the operation of a computer program: to check whether each step of a proof is correct, it is not necessary to understand the content of the formulas, but only to verify that the permitted rules have been applied.

Finitism, however, did not consist merely in formal proofs having finite length. It required metamathematical consistency proofs to rely exclusively on elementary procedures applied to finite signs and configurations. Whether this project could be carried out still remained an open question.

Metamathematics

Hilbert did not believe that every intuitive approach had to be excluded from Mathematics. Intuitive understanding was to operate primarily at the metamathematical level. The axioms, formulas, and proofs of a formal theory could be studied from the outside as finite sequences of signs.

The mathematician then assumes the role of a metamathematician: an external observer who studies the formal system and its properties as a mathematical object. The metamathematician can determine, for example, whether a string of formulas constitutes a legitimate proof, whether the axioms are independent, or whether a contradiction can be derived within the system.

Two of the principal properties are consistency and completeness. A system is consistent if it does not allow both a formula and its negation to be proved. A system is syntactically complete if, for every sentence \(A\) expressible within it, either \(A\) or \(\neg A\) can be proved.

This form of completeness should not be confused with the Completeness Theorem for First-Order Logic previously proved by Gödel. The latter states that every formula valid under all interpretations is provable in the logical calculus. The Incompleteness Theorems, by contrast, concern particular formal theories powerful enough to express Arithmetic.

Gödel’s results would impose a profound limitation on Hilbert’s Program: certain consistent formal systems cannot prove every arithmetical sentence expressible in their language and, under certain conditions, cannot prove their own consistency either.

Gödel’s Recursive Functions

Before entering into the proof of the Incompleteness Theorems, we must introduce the notion of recursion. This notion was already known, but Gödel incorporated it into his 1931 paper as a tool for rigorously describing certain effective arithmetical operations.

The class that Gödel then called “recursive functions” is close to what we now call primitive recursive functions, although the two definitions do not coincide exactly in every detail. In this account, we will use the modern presentation of primitive recursion.

We say that a numerical function \(f\), whose arguments and values are natural numbers, is defined by primitive recursion from the functions \(h\) and \(q\) if:

$$f(0,x_{2},\ldots,x_{n})=h(x_{2},\ldots,x_{n})$$

$$f(k+1,x_{2},\ldots,x_{n})=q\left(k,f(k,x_{2},\ldots,x_{n}),x_{2},\ldots,x_{n}\right)$$

for every natural number \(k\) and all values \(x_{2},\ldots,x_{n}\).

The first equation establishes the initial case. The second shows how to calculate the value corresponding to \(k+1\) from the value already obtained for \(k\). The function is not defined through an indeterminate circular reference: after a finite number of steps, every calculation reduces to the initial case.

We can see this in the simplest case, when \(f\) has a single argument. Suppose:

$$f(0)=h$$

$$f(k+1)=q(k,f(k))$$

To calculate \(f(4)\), we apply the second rule repeatedly until we reach the initial case:

$$f(1)=q(0,h)$$

$$f(2)=q(1,q(0,h))$$

$$f(3)=q(2,q(1,q(0,h)))$$

$$f(4)=q(3,q(2,q(1,q(0,h))))$$

Recursion is therefore, as we can see, a scheme of definition.

Primitive Recursive Functions

A function is primitive recursive if it can be constructed from a set of elementary initial functions through a finite number of applications of composition and primitive recursion.

The initial functions are:

  • the constant zero function;
  • the successor function \(s(x)=x+1\);
  • the projection functions, which select one of the arguments supplied.

Primitive recursive functions are total functions: they return a value for every admissible combination of arguments. Their value can be effectively calculated in a finite number of steps.

In modern programming languages, they can be compared, approximately, with procedures built from compositions and loops whose number of iterations is determined in advance by the input data. This comparison is only intuitive, but it helps explain why the computation always terminates.

Gödel’s Recursive Arithmetic

Gödel emphasizes that the fundamental operations of Arithmetic, such as addition and multiplication, can be expressed through primitive recursive functions. Their values can therefore be calculated in a finite number of steps by reducing the problem to the initial case in which one of the variables equals \(0\).

Consider, for example, the addition function \(a\), recursively defined from the successor function \(s\):

$$a(0,y)=y$$

$$a(x+1,y)=s(a(x,y))$$

The first equation states that adding \(0\) to \(y\) returns \(y\). The second indicates that adding the successor of \(x\) is equivalent to applying the successor function to the result of adding \(x\).

From addition we can define multiplication \(m\):

$$m(0,y)=0$$

$$m(x+1,y)=a(m(x,y),y)$$

Multiplying \(x+1\) by \(y\) consists in adding \(y\) to the result of multiplying \(x\) by \(y\).

Throughout this article, we will use lowercase letters such as \(x\), \(y\), \(z\), and \(k\) to represent natural numbers. The letters \(f\), \(g\), \(h\), \(a\), and \(m\) will designate numerical functions when applied to arguments.

Recursive Relations

Gödel also uses what are known as recursive relations, which play a fundamental role in the proof of the Incompleteness Theorems. These are properties or relations defined over natural numbers whose truth can be decided by an effective calculation.

A relation \(R\) of \(n\) arguments is primitive recursive if there is a primitive recursive function \(r\) that acts as its characteristic function. Following Gödel’s convention, we can represent truth by \(0\):

$$R(x_{1},x_{2},\ldots,x_{n})\leftrightarrow r(x_{1},x_{2},\ldots,x_{n})=0$$

When the relation does not hold, the function returns a value other than \(0\). This choice is a convention and does not imply that the number \(0\) is true in any general logical sense.

Consider an example of logical disjunction encoded by a numerical function \(D\). If \(0\) represents true and \(1\) represents false, we define:

$$D(0,x)=D(x,0)=0$$

and:

$$D(x,y)=1\quad\text{si }x\neq0\text{ e }y\neq0$$

The disjunction is true when at least one of its arguments represents a true proposition.

Conjunction can be represented by a function \(C\):

$$C(0,0)=0$$

and:

$$C(x,y)=1\quad\text{si }x\neq0\text{ o }y\neq0$$

By definition, every primitive recursive relation \(R(x_{1},x_{2},\ldots,x_{n})\) is decidable for any particular combination of values: there is a procedure that determines in a finite number of steps whether or not it holds.

Bounded Minimization

One consequence of the decidability of primitive recursive relations is that we can search for the least number satisfying a property whenever the search is limited by a finite bound.

Given a relation \(R(z)\) and a number \(j\), we can successively check:

$$R(0),R(1),R(2),\ldots,R(j)$$

The bounded minimization operation returns the least \(z\leq j\) for which \(R(z)\) holds. If no number less than or equal to \(j\) satisfies the property, we can conventionally assign \(j+1\) as the result.

The bound is essential. An unbounded search could continue indefinitely if no number satisfied the relation. Unbounded minimization does not, in general, preserve primitive recursiveness or guarantee that the computation terminates.

Bounded minimization allows us to express assertions such as “there exists a number \(z\) less than \(j\) that satisfies the property \(S\).” One example is the definition of a prime number:

$$\operatorname{Primo}(x)\leftrightarrow x>1\land\neg\exists z\left[1<z<x\land z\mid x\right]$$

The expression \(z\mid x\) means that \(z\) divides \(x\). Since only the possible divisors smaller than \(x\) need to be checked, we can decide in a finite number of steps whether a particular number is prime. The relation \(\operatorname{Primo}(x)\) is therefore primitive recursive.

Gödelization

We now turn to another pillar of the proof of the Incompleteness Theorems: the arithmetization of syntax. Throughout this series, we have seen that a common technique for solving metamathematical problems is to construct a numerical representation of the objects of a formal system.

A truth table provides an elementary analogy: we transform truth values into \(0\) and \(1\), and represent the connectives by operations defined over those numbers. Gödel takes this idea much further and devises a procedure by which every symbol, formula, and proof of a formal system is associated with a natural number.

This procedure is known as Gödelization or Gödel numbering. Its importance lies not merely in replacing formulas with numbers, but in the fact that the syntactic properties of formulas can be translated into arithmetical properties of their corresponding numbers.

Prime Factors

We will now explain the mechanism of Gödelization—the assignment of a natural number to each expression—known as a Gödel number. The entire process rests on the Fundamental Theorem of Arithmetic.

This theorem states that every natural number greater than \(1\) is either prime or can be expressed uniquely as a product of prime numbers, apart from the order of its factors.

Thus, for example:

$$17576=2^{3}\times13^{3}$$

There is no other decomposition of \(17576\) into prime factors. Likewise:

$$2023=7\times17\times17=7^{1}\times17^{2}$$

The uniqueness of factorization makes it possible to encode a finite sequence of numbers within a single natural number and later recover each of its components.

Gödel Number

Let us begin by assigning a different natural number to each basic symbol. In the system presented by Gödel, based on a version of the type theory of the Principia Mathematica enriched with arithmetical resources, some of the signs receive the following numbers:

$$0\Rightarrow1$$

$$s\Rightarrow3$$

$$\neg\Rightarrow5$$

$$\lor\Rightarrow7$$

$$\forall\Rightarrow9$$

$$(\Rightarrow11$$

$$)\Rightarrow13$$

These codes are not necessarily prime numbers. They are simply different numbers assigned to the elementary symbols.

Numbers must also be assigned to variables. Gödel reserves powers of prime numbers greater than \(13\) for them. A variable of type \(n\) is assigned a number of the form:

$$p^{n}$$

where \(p\) is a prime number greater than \(13\). Thus, an individual variable \(x\) could receive the number \(17\), while a predicate variable \(X\), belonging to the next type, could receive the number:

$$19^{2}=361$$

We can thus associate every formula with a finite sequence of natural numbers. For example, the formula:

$$\forall x\left(X(x)\right)$$

corresponds to the sequence:

$$9-17-11-361-11-17-13-13$$

Once we have obtained the sequence of codes \(t_{1},t_{2},\ldots,t_{n}\), we construct its Gödel Number as follows:

$$2^{t_{1}}\times3^{t_{2}}\times5^{t_{3}}\times\cdots\times p_{n}^{t_{n}}$$

where \(p_{n}\) is the \(n\)-th prime number. The position of each symbol is represented by the corresponding prime base, while its code appears as the exponent.

The Gödel Number of the preceding formula would be:

$$2^{9}\times3^{17}\times5^{11}\times7^{361}\times11^{11}\times13^{17}\times17^{13}\times19^{13}$$

This is an immense number, but it is perfectly determined and unique to that sequence of symbols. Thanks to the uniqueness of prime factorization, two different sequences do not receive the same number.

We can also construct the Gödel Number corresponding to an entire proof. Since every proof is a finite sequence of formulas, if \(r_{1},r_{2},\ldots,r_{n}\) are the Gödel numbers of its formulas, we can encode it by:

$$2^{r_{1}}\times3^{r_{2}}\times5^{r_{3}}\times\cdots\times p_{n}^{r_{n}}$$

Given the Gödel Number of a proof, it is possible, at least in principle, to factor it, recover the numbers of each of its formulas, and reconstruct the complete sequence.

Arithmetization of Metamathematics

So far, we have presented two apparently independent resources: primitive recursive functions and Gödelization. The proof of the Incompleteness Theorems arises precisely from their combination.

Gödelization transforms symbols, formulas, and proofs into natural numbers. Primitive recursive relations make it possible to define decidable properties of those numbers. In this way, certain metamathematical statements about a formal system can be translated into purely arithmetical statements.

For example, we can define a relation:

$$\operatorname{Prf}_{P}(x,y)$$

interpreted as “\(x\) is the Gödel Number of a valid proof in the system \(P\), whose final formula has Gödel Number \(y\).”

The relation \(\operatorname{Prf}_{P}(x,y)\) is primitive recursive when the axioms and rules of the system can be effectively recognized. Given a particular number \(x\), we can decompose it, check whether it encodes a sequence of formulas, and verify, step by step, whether each formula is an axiom or is legitimately obtained from the preceding formulas.

The assertion that the formula with Gödel Number \(y\) is provable is then expressed by:

$$\operatorname{Prov}_{P}(y)\equiv\exists x\,\operatorname{Prf}_{P}(x,y)$$

We must distinguish these two notions. Checking whether a particular number \(x\) encodes a particular proof of \(y\) is a decidable operation. Determining whether there exists some number \(x\) that encodes a proof of \(y\) requires searching through an unlimited number of possible proofs and is not, in general, a decidable problem.

Gödel also proves that the relevant primitive recursive relations can be represented by formulas within the arithmetical system itself. The system can therefore formulate, in its own language, properties that we interpret from the outside as statements about its own expressions and proofs.

Outline of Gödel’s Incompleteness Theorems

We have presented a simplified version of the numbering used by Gödel in the paper in which he introduces the Incompleteness Theorems. Many other procedures can be used to encode symbols and formulas. Some use a different repertoire of signs or simpler coding systems. The particular choice is not essential, provided that the encoding is effective and unambiguous.

So far, we have presented two distinct schemes: primitive recursive functions and Gödelization. In the next article, we will see how Gödel connects them.

Primitive recursive functions allow us to work with decidable arithmetical relations between natural numbers. Gödelization allows us to interpret some of those numbers as symbols, formulas, or proofs. Thus, an arithmetical relation such as \(\operatorname{Prf}_{P}(x,y)\) can be interpreted metamathematically as “\(x\) is a proof of the formula \(y\).”

The decisive step will be to construct, through a procedure of substitution and self-reference, a sentence that expresses within the system itself that it is not provable. Under the appropriate consistency conditions, the system will be unable to prove that sentence or, in Gödel’s original formulation, its negation.

In this way, Arithmetic ceases to speak only about numbers and begins to reflect properties of its own formulas and proofs. This ability to represent metamathematics within Arithmetic will be the key to the Incompleteness Theorems.

Recommended Reading

– Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.

– Gödel, K. (2006). Complete Works. Edited by Jesús Mosterín.