Gödel's incompleteness theorems

Kurt Gödel at the age of 19, five years before the demonstration of the theorems.

The Gödel incompleteness theorems are two famous theorems of mathematical logic proved by Kurt Gödel in 1931. Both are related to the existence of undecidable propositions in certain arithmetic theories.

Summary

The first incompleteness theorem asserts that, under certain conditions, no formal mathematical theory capable of describing the natural numbers and arithmetic with sufficient expressiveness is both consistent and complete. That is, if the axioms of said theory do not contradict each other, then there are statements that cannot be proved or disproved from them. In particular, the conclusion of the theorem applies whenever the arithmetic theory in question is recursive, that is, a theory in which the process of deduction can be carried out by an algorithm.

The proof of the theorem is totally explicit and in it a formula is built, usually denoted G in honor of Gödel, for which given a demonstration of it, a refutation can be constructed, and vice versa. However, the natural interpretation of said statement in terms of natural numbers is true.

Second Gödel incompleteness theorem

The second incompleteness theorem is a particular case of the first: it states that one of the undecidable sentences of said theory is the one that «affirms» its consistency. That is to say, that if the system of axioms in question is consistent, it is not possible to demonstrate it by means of said axioms.

Gödel's incompleteness theorems are one of the great advances in mathematical logic, and were—according to most of the mathematical community—a negative answer to Hilbert's second problem. The theorems imply that first-order axiomatic systems order have severe limitations for the foundation of mathematics, and dealt a severe blow to the so-called Hilbert program for the foundation of mathematics. On the other hand, for some time neither Hilbert nor other of his collaborators were aware of the importance of Gödel's work for his program.

Context

Gödel's incompleteness theorems place certain limitations on what can be proved by mathematical reasoning. To talk precisely about what "can be proved" or not, a mathematical model called formal theory is studied. A formal theory consists of a series of signs and a set of rules for manipulating and combining them. By means of these rules it is possible to distinguish certain collections of signs as formulas, and certain sequences of formulas as demonstrations. The theorems of a certain theory are then all the formulas that can be proved from a certain initial collection of formulas that are assumed as axioms.

A formal theory can be assigned certain properties based on what it is capable of demonstrating.

• A consistent theory does not contain contradictions, that is, it is not possible to demonstrate both a formula and its opposite. A theory that is not consistent has no use: due to the principle of explosion, from a contradiction all its formulas can be demonstrated, and it does not serve to model mathematical reasoning.
• A complete theory "responses any question", in the sense that for each of its formulas is either demonstrable, or there is a demonstration of its opposite (is refutable). A complete theory is optimal, and it corresponds to the intuition about logical truth: like any judgment must be true or false, in a complete theory all formula is demonstrable or refutable.

However, the first incompleteness theorem states that, under certain hypotheses, a formal theory cannot have both properties at the same time. The first of these is that it is an arithmetic theory, that is, that its symbols serve to describe the natural numbers and their operations and relationships; and that is capable of proving some basic properties about them. The second hypothesis is that it is a recursive theory, which means that the rules for manipulating its signs and formulas in the proofs must be executable by an algorithm: a precise unambiguous series of steps that can be carried out in finite time, and even be implemented through a computer program.

First Theorem

The statement of the first theorem reads:

The proof of this theorem involves constructing a certain formula, the «Gödel sentence» G, which cannot be proven or disproved in the recursive arithmetic theory T: neither G nor ¬G (the negation of G) are theorems of T. It is then said that G and ¬G are undecidable or independent in T.

To arrive at this, Gödel developed a method for encoding signs and formulas by numbers, called Gödel numbering. Using this numbering, it is possible to translate the properties of a formal T theory, such as «these signs constitute a formula» or «these formulas are not a proof in T”, to arithmetic properties of said numbers. In particular, the Gödel sentence G is an arithmetic formula whose meaning is «there is no proof of G in T theory", or in other words, "I am not provable in T».

Consequences

Gödel's sentence G is not provable but it is true, as it precisely asserts its own unprovability. This means that no arithmetic theory in the conditions of the theorem is capable of proving all the true statements of arithmetic.

Furthermore, even if ¬G is false (by asserting otherwise that G) is not refutable (since G is unprovable). This sentence can be taken as an axiom if desired and this does not produce a contradiction. The resulting theory contains many of the true statements about the natural numbers and some false ones, starting with ¬G. The objects described by such a theory form a non-standard model of arithmetic.

Taking G (or its opposite) as an axiom, a new theory T&#39 is obtained; in which G (or its opposite) is automatically provable. However this does not invalidate the theorem, since G asserts its unprovability relative to the T. The new theory T' is also incomplete: a new independent statement G&#39 can be found;, which states "I am not provable in T'".

In short, in a formal theory that is consistent and complete one of the hypotheses must fail: either it is not recursive and there is no algorithm to distinguish the axioms from the rest of the formulas; or they are not arithmetic, and do not include the necessary basic properties of the natural numbers. For example, consistent and complete theories that are not recursive are used in the proof of the semantic completeness theorem. On the other hand, Presburger arithmetic is a collection of axioms about the natural numbers that omits several of their properties, to such an extent that a theory based on them can be consistent and complete.

Second Theorem

The second incompleteness theorem shows another explicit example of a formula that no arithmetic theory can prove, besides G. Again, using Gödel's numbering, one can find a formula, denoted Consis T, whose meaning is "cannot find a contradiction in T”, or in other words, “T is consistent”.

The proof of the second theorem requires translating the first into a formula. The first theorem states, among other things, that if T is consistent, then G is not provable. The formula that asserts the consistency of T is Consis T, while the formula that affirms the unprovability of G is the G. The formula that translates the first theorem (a part of it) is Consis T ⇒ G, where “⇒” means implication. Gödel proved that this formula is a theorem, and that therefore Consis T is not a theorem: if it were, from the basic rules of T as a formal theory it would follow that G is provable, in contradiction with the statement of the first incompleteness theorem.

Consequences

The second incompleteness theorem limits the possibilities of proving the consistency of a formal T theory, since it cannot be done using only the T. Furthermore, if a stronger theory T' is found in which Consis T cannot be proved, the consistency of T' itself cannot be proved in T' nor in T. For this reason, the second theorem is considered a negative response to the so-called Hilbert program, which proposed to demonstrate the correctness of mathematical reasoning based on infinite objects using only reasoning based on finite objects, less powerful than the first ones.

Undecidable statements

Gödel's first incompleteness theorem proves the existence of undecidable or independent statements in Peano arithmetic, and both the first and second show concrete examples of undecidable statements. Other examples of independent statements of the Peano axioms have since been found, such as Ramsey's "strong" theorem. There are also numerous examples of independent statements in other formal theories stronger than arithmetic, such as the continuum hypothesis or the axiom of choice in set theory; or even in theories not directly related to arithmetic, as in the case of Euclidean geometry and the parallel postulate.

Discussion and implications

The incompleteness results affect the philosophy of mathematics, particularly views such as formalism, which uses formal logic to define its principles.

The first theorem can be paraphrased by saying that «an axiomatic system can never be found that is capable of demonstrating all mathematical truths and none falsehoods».

On the other hand, from a strictly formalist perspective this paraphrase would be considered meaningless because it presupposes that mathematical "truth" and "falsehood" are well-defined in an absolute sense, rather than relative to each formal system.

The following restatement of the second theorem is even more disturbing for the foundations of mathematics:

If you can prove that an axiomatic system is consistent from itself, then it is inconsistent.

Therefore, to establish the consistency of a system S{displaystyle S} need to use another system T{displaystyle T}but a test in T{displaystyle T} is not totally convincing unless the consistency of T{displaystyle T} it has already been proved without employing S{displaystyle S}. The consistency of Peano axioms for natural numbers for example can be demonstrated in the theory of assemblies, but not in the theory of natural numbers alone. This provides a negative response to problem number two of the famous list of important open issues in mathematics of David Hilbert (called problems of Hilbert).

In principle, Gödel's theorems still leave some hope: it might be possible to produce a general algorithm that for a given statement determines whether it is undecidable or not, allowing mathematicians to avoid undecidable problems altogether. However, the negative answer to the Entscheidungsproblem shows that there is no such algorithm.

Note that Gödel's theorems are only applicable to strong enough axiomatic systems. This term means that the theory contains enough arithmetic to carry out the coding instructions required by the proof of the first incompleteness theorem. Essentially, all that is required are some basic facts about addition and multiplication as formalized, for example, in Robinson's Q arithmetic.

There are even weaker axiomatic systems that are consistent and complete, for example Presburger arithmetic which proves all first-order statements true by applying only addition.

The axiomatic system can consist of an infinite number of axioms (as Peano's first-order arithmetic does), but for Gödel's theorem to apply there must be an effective algorithm that is capable of checking the correctness of the axioms. evidence. For example, the set of all first-order statements that are true in the standard model of the natural numbers is complete. Gödel's theorem cannot be applied because there is no effective procedure that decides whether a certain statement is an axiom. In fact, that this is so is a consequence of Gödel's first incompleteness theorem.

Another example of a specification of a theory in which Gödel's first theorem does not apply can be constructed as follows: arrange all possible statements about the natural numbers first by their length and then in lexicographical order; let's start with an axiomatic system initially equal to the Peano axioms, go through the list of statements one by one, and, if the current statement cannot be proved or disproved from the current system of axioms, then add it to the list. This creates a system that is complete, consistent, and powerful enough, but not recursively enumerable.

Gödel himself only proved a version of the above theorems that is technically a bit weaker; the first demonstration of the versions described above was given by J. Barkley Rosser in 1936.

In essence, the first theorem test consists of building a declaration p{displaystyle p} within an axiomatic formal system that can be given the following mathematical goal interpretation:

p={displaystyle p=} "This statement cannot be proved. »

As such, it can be seen as a modern version of the paradox of the liar. Contrary to the statement of the liar, p{displaystyle p} it does not refer directly to itself; the above interpretation can only be "see" from outside the formal system.

In a paper published in 1957 in the Journal of Symbolic Logic, Raymond Smullyan showed that Gödel incompleteness results can be obtained for much more elementary systems than those considered by Gödel. Smullyan has also claimed simpler proofs with the same scope, based on Alfred Tarski's work on the concept of truth in formal systems. Simpler, but no less philosophically disturbing. Smullyan has not captured his reflections on incompleteness only in technical works; They have also inspired famous popular books such as What is the name of this book?

If the axiomatic system is consistent, the Gödel test shows that p{displaystyle p} (and their denial) cannot be demonstrated in the system. So... p{displaystyle p} That's it. Right. (p{displaystyle p} claims not to be demonstrable and is not) and yet it cannot be formally tested in the system. Note that add p{displaystyle p} a the axioms of the system would not solve the problem: there would be another Gödel ruling for the extended theory.

Roger Penrose claims that this (alleged) difference between what can be proven mechanically and what humans can see as true shows that human intelligence is not mechanical in its nature. John R. Lucas has also dealt with this question in Minds, Machines and Gödel.

This perspective is not widely accepted, because as Marvin Minsky puts it, human intelligence is capable of making mistakes and understanding statements that are actually inconsistent or false. However, Minsky has reported that Kurt Gödel told him in person that he believed that human beings have an intuitive, not just computational, way of arriving at the truth and therefore his theorem does not limit what can be. known to be true by humans.

See Rebuttals to Penrose's interpretation in the Links in English in the External links and references section.

The position that theorem shows that humans have an ability to transcend formal logic can also be criticized as follows: We do not know if the sentence p{displaystyle p} is true or not, because we do not know (or we can know) if the system is consistent. So we don't really know any truth that's out of the system. All we know is the following:

O p{displaystyle p} is indemonstrable within the system, or the system is inconsistent.

This statement is easily provable within the system.

Another implication is that Gödel's work motivated Alan Turing (1912-1954) to study which functions were calculable and which were not. For this he used his Turing Machine, a general purpose machine through which he formalized the functions and calculation procedures, demonstrating that there were functions that cannot be calculated using the Turing Machine. The paradigm of this set of functions is represented by the function that establishes: «if given a Turing Machine, it produces a result or, on the contrary, it remains calculating indefinitely». This function, known as Halting Problem, will be a fundamental piece to demonstrate the incomputability of certain functions.

Proof of theorems

The proof of the incompleteness theorems is based on three concepts:

1. The numbering of Gödel, which allows the translation of formal theories into pure arithmetic operations.
2. The expressive power of arithmetic formal theories, whose expressions collect such operations.
3. The diagonal motto, which allows the formulas to be self-referential.

The original statement due to Gödel, whose proof is outlined in this section, is weaker than the one presented above, since instead of the consistency of T theory a stronger property is required, the ω-consistency.

(The numerals [n] are the symbols used by the language of the theory to specify the natural numbers In the Peano arithmetic example in the next section, the numerals are the symbols given by: [0] ≡ 0, [ 1] ≡ S0, [2] ≡ SS0, etc.). ω-consistency implies consistency (but not the other way around). The "strong" statement, in which only the consistency of the theory is required, was proved by J. B. Rosser by a very similar method.

Gödel numbering

Gödel numbering is a tool that allows relating formal theories with arithmetic. The language of a first-order formal theory is composed of a countable quantity —at most— of signs, such as:

consuming ⇒ ¬ 日本語, =, x and z... 0 + × S

in the case of the language of Peano arithmetic, where in addition to logical symbols and variables, there are some additional symbols for arithmetic (where S is the symbol for denote "the number following"). Also the set of all chains (finite sequences of signs) is countable, as well as the set of finite sequences of chains.

A Gödel numbering is an assignment of a unique natural number to each element of each of these three sets: signs, strings of signs, and sequences of strings.

Since the manipulation of these signs, strings and sequences can be translated into the manipulation of certain numbers, both the syntax that distinguishes strings of "sense" signs —formulas— and the deductive calculus that distinguishes string sequences "that prove something"—the proofs—are translated into arithmetic operations. That is, there are a series of relations and arithmetic functions that correspond to the syntactic rules and deductive calculus, such as:

Sig x: x is (the number of Gödel of) a sign

Cad x: x is (the Gödel number of) a chain (signs)

(The Gödel number is omitted from below)

Suc x: x is a succession (of chains)

Form x: the chain x It's a formula.

Ax x: the formula x It's an axiom.

Cons(x, and, z): «x is an immediate consequence of formulas and and z»

Demx, and): «the succession x is a demonstration of the formula and»

The precise form of these functions and relations is laborious and depends on the criteria that have been chosen to carry out the Gödel numbering. In particular, the relation Ax x has to be constructed taking into account a certain set of concrete axioms, then the relation Dem refers to a particular theory that is not specified.

Expressibility and recursion

Using Gödel numbering, it is possible to “translate” the signs and rules of a formal T theory into numbers and arithmetic operations. It is possible to go further, since T is an arithmetic theory and the aforementioned operations can be “recoded” using the formal language of T, as can be done with other functions and arithmetic relations such as:

The function "multiplicate by 2" is represented by the formula: and = [2] x

The relation of order x ≤ andcan be expressed by: consumingz, z + x = and

The relationship «x e and are cousins among themselves” can be expressed as: Русскийz, z [1] ∧ consumingw, x = z × w ⇒ ¬consumingu, and = z × u.

Each of these relations is expressed by its corresponding formula, in the sense that if two numbers are related, the corresponding formal expression can be proved; and when they are not, it can be refuted. For example:

For each integer nYou have to. n it's even possible to prove the formal expression consumingx[n] = [2] × x; and if it is unstoppable, such a formula may be refuted.

For every couple of integers m and nIf you have m ≤ n the formula can be demonstrated consumingz, z +m] =n]when m ▪ nThat expression can be refuted.

That the relations presented in the previous section —such as Dem— are expressible implies that a formal arithmetic theory is powerful enough to «talk» about the characteristics of a arbitrary formal theory and, in particular, of itself.

Proving that all these relations and functions are expressible is easy if they are recursive, that is, if they can be calculated or verified by an algorithm, since it can be shown that every recursive relation is expressible in an arithmetic theory. The formal theories for which this is possible—assigning the Gödel numbers in such a way that distinguishing signs, strings, sequences, formulas, consequences, and axioms can be done with an algorithm—are the so-called recursive theories. b>, and for this reason this characteristic is assumed as a hypothesis in the incompleteness theorems.

Diagonalization

In order to construct the self-referring sentence G a way must be devised for a formula to speak of the properties of its corresponding Gödel number. This has to be done indirectly, since given a formula φ with Gödel number n, another formula that “speaks” of φ by the numeral [ n] will in general have a Gödel number greater than n, and thus cannot be φ. This is achieved by the so-called diagonal lemma.

In short, given any property φ(x) there exists a sentence ψ which states “my Gödel number satisfies the property φ”.

Proof of the first theorem

Let be a recursive arithmetic formal theory T ω-consistent. Let the formula be ¬∃z, DEM(z, x), where DEM is the formula expressing the numerical relation Dem —relating to the formal theory T—. By the diagonalization lemma there exists a sentence G with Gödel number g, for which we demonstrate G ⇔ ¬∃z, DEM(z, [g]), that is, stating "no number encodes a proof (in T) of the formula represented by g”, or of otherwise, "I am not provable (in T)”. The negation of this statement, ¬G, is equivalent to ∃z, DEM(z, [g]), or "my negation is provable (in T)”.

Suppose then that G can be proved. Then there exists a number n satisfying Dem(n, g), and in T can then be tested DEM([n], [g]), which formally implies ¬G; and this is impossible if T is consistent. Thus there is no proof of G, and ¬Dem(n) holds, g) for all numbers n, resulting in an infinite number of formal theorems ¬DEM([n], [g]) for each numeral [n]. Since T is ω-consistent, then it cannot happen that ∃x, DEM(x, [g]) is a theorem, so ¬G is unprovable, and T is undecidable.

Proof of the second theorem

The proof of the second incompleteness theorem requires a technical fact that Gödel did not originally prove. Let be a theory T in the above conditions and let be the formula Consis T ≡ ¬ ∃z, DEM(z, [k]), where k is the Gödel number of the statement 0 = 1. Consis T asserts that the theory T is consistent (since it leaves something unproven). The formal version (of the first part) of the first incompleteness theorem can be expressed as Consis T ⇒ ¬∃y, DEM(y, [g]) and this is equivalent precisely to Consis T ⇒ G. So, if this statement could be formally proved, Consis T would be unprovable since we would then have a proof of G, in contradiction with the first theorem.

The technical fact that is needed is precisely a proof that the proof of the first incompleteness theorem can be "translated" into a formal proof of the statement Consis T ⇒ ¬∃y, DEM(y, [g]). This is possible in all recursive arithmetic theory, since they verify certain provability conditions.