A truth that cannot be proved

From Leibniz and Boole to Hilbert, mathematicians imagined that it would be possible to determine the truth of mathematical formulas automatically. We now ask the same question: we have worked with simple logical systems that are decidable, i.e., for which a program can determine whether a formula is true or false. In the case of more complex logical systems, such as Peano arithmetic, this is not possible. This is because the existence of undecidable computational problems leads directly to the existence of undecidable mathematical statements.

5.1 #A first approach

Before proceeding with the proof of a first version of the First Incompleteness Theorem, we will discuss in detail Program 5.1. In Line 3 we import the function is_theorem_peano, whose existence we proved in Proposition 4.29. Recall that, since the axioms of $\textbf{Peano}$ are recursively enumerable (i.e., $\textbf{Peano}$ is recursively axiomatizable), we can write the program is_theorem_peano(formula) that returns yes if formula is a theorem in $\textbf{Peano}$, and does not halt otherwise (see Proposition 4.29).

import utilities
 
from is_theorem_peano import is_theorem_peano  # NOT an oracle
from halting_to_peano import halting_to_peano      # NOT an oracle
 
def godel_peano(input):
godel_program = utilities.read('godel_peano.py')
halts_in_peano = halting_to_peano(godel_program)
does_not_halt_in_peano = 'NO (' + halts_in_peano + ')'
 
if is_theorem_peano(does_not_halt_in_peano) == 'yes':
return 'halts'
else:
utilities.loop_forever()

Line 4 imports the function halting_to_peano, whose existence we already discussed after Proposition 4.24. This function translates, given a program $P$, the statement “$P$ halts on empty input” into a $\textbf{Peano}$ formula.

In Line 7 we store the program godel_peano.py itself in the variable godel_program. In Line 8 we use the function halting_to_peano just discussed, and in Line 9 we negate the formula halts_in_peano. In this way:

Now is when things get interesting. If does_not_halt_in_peano is a theorem, the function is_theorem_peano will return yes, and in this way the program will verify the condition in Line 11 and return halts, making the program halt. If does_not_halt_in_peano is not a theorem, it will enter an infinite loop (is_theorem_peano will not halt, and therefore neither will godel_peano.py). It is clear that Line 14 will never execute, but we include it to emphasize this fact.

Now we ask: what is the behavior of godel_peano.py on empty input?

We are now in a position to prove the main result of this work.

We have just shown that $\textbf{Peano}$ is incomplete, as we already anticipated in Table 4.1. We explore the consequences of this fact in detail in Section 5.4. However, let us pause for a moment to analyze what we have just proved.

5.2 #Semantic version

To find a true and unprovable formula, we have needed a logical system that is, first of all, recursively axiomatizable. Otherwise, we would not have been able to create a program capable of knowing when a formula of the system is a theorem. On the other hand, we have assumed that the system is sound, which is to be expected. We also need effective translations of statements about programs and a formal account of finite-computation verification (see Proposition 4.24). We collect these conditions in the following definition of a “Turing-type” system.

Merely being able to write these statements in the language is insufficient: we need a computable translation and the stated provability properties for finite runs. A classical theory extending Robinson arithmetic $Q$ admits an encoding with these properties.⁴

To understand the last condition, we can encode $A_P$ as “there is an accepting computation before any rejection”. If $P$ accepts, a finite trace supplies a witness. If it rejects after $r$ steps, we can verify that it did not accept before $r$ and that any later acceptance would already have an earlier rejection; that same trace lets the theory prove $\neg A_P$. The ability to formalize this reasoning is part of the hypothesis, rather than a consequence of consistency alone.

Observe that, however, at no point have we used the system $\textbf{Peano}$ itself. This indicates that we could carry out this proof with another system that is not $\textbf{Peano}$, as long as it satisfies such conditions. We state this result below.

To reinforce this important result, we include a summary of the process we have followed for $\textbf{Peano}$, in general form, in the proof of this theorem.

import utilities
 
from is_theorem_G import is_theorem_G  # NOT an oracle
from halting_to_G import halting_to_G      # NOT an oracle
 
def semantic_incomplete(input):
program = utilities.read('semantic_incomplete.py')
halts_in_G = halting_to_G(program)
does_not_halt_in_G = 'NOT (' + halts_in_G + ')'
 
if is_theorem_G(does_not_halt_in_G) == 'yes':
return 'halts'
else:
utilities.loop_forever()

Our result tells us that, if we have a logical system that is recursively axiomatizable and of Turing type, we cannot expect it to be both sound and complete at the same time. That is, if all theorems of the system are true, we will always be able to find formulas of the system that are true but are not theorems.

We can apply the Theorem 5.4 to other logical systems, as long as they satisfy the hypotheses. One of them is, for example, the Zermelo–Fraenkel axiom system.

5.3 #Syntactic version

The previous result uses soundness. We now want syntactic incompleteness under the weaker assumption of consistency. The distinction matters: a consistent system can prove false statements without proving a contradiction.

First we need a procedure to decide theoremhood if we additionally assume that the system is complete.

from enumerate_theorems_S import enumerate_theorems_S  # NOT an oracle
from syntax_S import negate
 
def is_theorem_S(formula):
negated_formula = negate(formula)
for theorem in enumerate_theorems_S():
if theorem == formula:
return 'yes'
if theorem == negated_formula:
return 'no'

We now use the impossibility of solving GuessConsistent with a total computable predictor (Proposition 3.28).⁵

from acceptance_to_S import acceptance_to_S  # effective translation
from is_theorem_S import is_theorem_S  # under the completeness assumption
 
def guess_consistent(program):
accepts_formula = acceptance_to_S(program)
return is_theorem_S(accepts_formula)

The case of looping programs is essential. We have not assumed that a proof of halting implies actual halting, or that the system can recognize every infinite run. Querying a proof of halting and then running the program could leave the predictor stuck: consistency alone does not guarantee the truth of that proof. Here the answer depends only on a proof search that terminates by the assumed completeness.

We have proved two versions of the First Incompleteness Theorem. We summarize the differences between them below.

The corresponding classical formulation is the Gödel–Rosser theorem. We state it next with an explicit arithmetic hypothesis.

As in our syntactic version, we require that the system be syntactically consistent and recursively axiomatizable. Gödel's original theorem required as a hypothesis a stronger form of syntactic consistency called $\omega$-consistency. This more general form of the theorem is due to the work of John B. Rosser, author of what is today known as the Rosser trick.⁶⁷

The third hypothesis requires that the system be able to prove certain statements of elementary arithmetic. This is because Gödel intended to prove that no sufficiently expressive, effective, consistent axiomatization of arithmetic could be complete (see Chapter 1), so he used in his proof a way of numbering theorems that is today known as Gödel numbering.

5.4 #Consequences

The First Incompleteness Theorem has profound mathematical and philosophical implications.

5.4.1 #Relationship to Hilbert's second problem

We already introduced Hilbert's celebrated problems in Chapter 1, and in particular the second of them, which we will refer to again below:

1. Is mathematics complete? That is, can every mathematical sentence be proved or disproved?
2. Is mathematics consistent? That is, is it impossible to prove simultaneously a statement and its negation?
3. Is mathematics decidable? That is, does there exist an automatic method that can be applied to any mathematical statement and determine whether it is true? This problem is known as the Entscheidungsproblem.

It is necessary to point out that Hilbert's formulation of this problem is relative to arithmetic. It is clear that, for this case, the Theorem 5.7 guarantees the existence of unprovable formulas, answering (1) negatively⁸. On the other hand, in Proposition 4.27 we prove that truth in $\textbf{Peano}$ is undecidable, proving that the answer to question (3) is negative. Question (2) falls outside the scope of this work.

However, it is interesting to see these questions without needing to limit ourselves to arithmetic. We introduced logical systems precisely to formalize the concepts of truth and proof, which are the soul of mathematics.

We can find analogous answers for recursively enumerable formal systems of Turing type. In such a case, the Theorem 5.6 answers question (1) negatively, while a generalization of Proposition 4.27 (similar to the one we made in the Theorem 5.4 from the Theorem 5.2) allows us to answer question (3) negatively.

5.4.2 #Relationship to the human mind and the Church–Turing thesis

Some authors draw much more epistemological conclusions, concerning the human mind. Roger Penrose and John Lucas⁹¹⁰ argue that the role of consciousness is non-algorithmic when we form mathematical judgments, which can be generalized to the role of human consciousness.

To this end, the authors comment that in any formal system there are unprovable propositions, i.e., ones for which its algorithm cannot provide an answer. If the functioning of the human mind were completely algorithmic, then the algorithm (or formal system) it uses to form its judgments could not handle such a proposition. However, the human mind can deduce that such a proposition is true. This contradiction may indicate that the human mind, as far as mathematical reasoning is concerned, was not using an algorithm in the first place.

Douglas Hofstadter¹¹¹² presents Gödel's theorems as an example of a “strange loop”, a hierarchical and self-referential structure that exists in a formal system. He argues that this is the same structure that gives rise to consciousness, the sense of “self”, in the human mind: self-reference comes from the way the brain abstracts and categorizes stimuli into “symbols”, or groups of neurons, that correspond to concepts, in what is de facto a formal system, which eventually forms symbols that correspond to the entity itself that performs the perception.

The difference between mathematics and consciousness resides, according to Hofstadter, in the direction in which reasoning is carried out: whether it is “bottom-up”, from axioms toward more complex propositions and theorems, or “top-down”, in the opposite sense.

Mathematics works bottom-up: to determine whether a formula is a theorem we must start from the axioms and reason until we reach it. The human mind, according to the physicist, works top-down, from a higher level—of desires, concepts, personalities, ideas, and thoughts—down to the lowest level of interactions between neurons and even fundamental particles. Human beings are made to perceive “big things” rather than “small things”, even though in the domain of the small seems to reside the engine of reality.

Both arguments are intimately connected to the Church–Turing thesis (see Section 2.4). If the human mind is a Turing machine, all the procedures of our brain would be nothing more than algorithms, and through Gödel's theorems, our way of reasoning would be limited—there exist statements we cannot prove! This may lead to more fantastical conclusions, with some authors speaking of Gödel's theorems, although they do not allow us to prove it, as strong evidence for the existence of God.^{13 14}

The syntactic-version programs are presented here as updated pseudocode; they are not assumed to match files in the companion intro-to-incompleteness repository.