Proof is not the same as truth

In this chapter we ask whether the concepts of proof and truth can be expressed algorithmically: is there an automatic way to prove theorems and verify mathematical statements? As we explained in Chapter 1, this was one of the central themes of early 20th-century mathematics.

Mathematics consists of deducing theorems from a certain list of axioms. To define this concept precisely, we turn to formal systems (Section 4.1).

However, we are especially interested in knowing whether the statements (or formulas) of a system are true. For this, we will need to define logical systems (Section 4.2).

Once we have distinguished provable from true, we ask about the relationship between these two concepts in a given logical system: from this we will understand the notions of soundness and completeness in Section 4.3, and finally we will ask whether we can algorithmically check if a formula is true—whether a logical system is decidable or not (see Chapter 3). Throughout this section we introduce multiple examples of logical systems that reinforce the concepts already mentioned, all revolving around a simple arithmetic operation.

Next, we introduce a logical system of special importance: Peano arithmetic (Section 4.4). This system is capable of proving a large number of number-theoretic theorems, so it will be especially interesting to know whether all its true statements are provable (this is precisely the First Incompleteness Theorem, which we prove in Chapter 5). To do this, we will find a way to translate the halting problem (Section 3.6) into a formula of this system.

Finally, we introduce further properties of the systems introduced in Section 4.5.

4.1 #Formal systems

Throughout this work we have presented multiple proofs, but what exactly is a proof? When we talk about proving something, we mean doing so mathematically. Unlike scientific proofs, mathematical proofs are exact and verifiable. In this way, we can ask whether a computer can perform proofs automatically.

To answer all these questions, we need to create a mathematical structure that allows us to formalize the concept of proof.

Let us see an example of a formal system that will be extremely useful in this chapter.

It is important to emphasize the notation used to describe the inference rules of $\textbf{BinarySum}$, in particular the meaning of maximal match. A maximal match, in this case, is a substring that satisfies the regular expression for $N$ and cannot be extended in either direction. In the formula 100+11+1001=101, we have four maximal matches of this type: 100, 11, 1001, and 101, in that order.

It would be possible to describe these rules using regular expressions, but this would make the notation less simple and intuitive.

Once a formal system is defined, it is possible to prove (or demonstrate) some of its formulas, which we call theorems.

Let us see an example of a theorem in $\textbf{BinarySum}$.

Note that, although it is not in the definition, proofs of theorems are usually accompanied by notes that help verify the proof. The companion repository provides binary_addition.py with is_theorem to generate proofs. To test whether a formula is a theorem in any of the systems in this chapter, specify the system name followed by the formula.

Below are some examples of using this function:

>>> from binary_addition import is_theorem
>>> is_theorem('BinarySum', '1+1+1=11')
    (F1) 1=1            (Axioma)
 -> (F2) 1+1=1+1        (R1)
 -> (F3) 1+1+1=1+1+1   (R1)
 -> (F4) 1+1+1=1+10     (R2)
 -> (F5) 1+1+1=11       (R3)
'theorem'
>>> is_theorem('BinarySum', '11+1=10')
'not proved within the first 109322 generated formulas'
>>> is_theorem('BinarySum', 'ill-formed')
'ill-formed formula'
>>> is_theorem('NonexistentSystem', 'whatever')
'system does not exist'

The proof of 1+1+1=11 performed by is_theorem is different from that of Example 4.4. This is perfectly possible: a theorem can have several proofs. This fact is evident from Definition 4.3 itself: a formula is a theorem if "there exists a proof".

4.2 #Logical systems

As the name suggests, the $\textbf{BinarySum}$ system is intended to check formulas of binary addition. In this way, a word like 11 represents the number $3$, and a formula like 1+1+1=11 represents that $1+1+1=3$. Note that this allows us to recognize whether a formula of $\textbf{BinarySum}$ is true: we simply interpret it as an arithmetic formula and declare it true if it is a correct arithmetic formula. In this way, formulas like 10+1=11 are true, while others like 11+1=10 are not.

In the previous section, we intentionally did not mention the concept of truth: a formal system has no notion of certainty. This is because the definitions of theorem and true formula are completely different.

Theorems depend only on syntax: "Can we prove a theorem from certain axioms and inference rules?" Truth, however, depends on semantics: "Is this formula true when interpreted by giving certain meaning to its symbols?"

By definition, formal systems depend only on syntax. In this section, we introduce logical systems, which are nothing more than formal systems to which we add a semantics. When we add the arithmetic semantics we have discussed to the formal system $\textbf{BinarySum}$, we obtain the logical system $\textbf{BinarySumLogical}$.

Formally, we can define these systems as:

Once we incorporate a truth assignment into a formal system, we can say when a formula is true. We make this precise in the following definition:

Let us see examples of true and false formulas for $\textbf{BinarySumLogical}$.

The file binary_addition.py also provides a function to check the truth of formulas in logical systems, called is_true. An example:

>>> from binary_addition import is_true
>>> is_true('BinarySumLogical', '1+1+1=11')
True
>>> is_true('BinarySumLogical', '11+1=10')
False
>>> is_true('BinarySumLogical', 'ill-formed')
False
>>> is_true('BinarySum', '1+1+1=11')
'system does not exist or is not a logical system'

We will introduce more logical systems obtained by adding (Logical system 4.8) and removing (Logical system 4.9) rules from $\textbf{BinarySumLogical}$.

These systems are especially interesting, since in them we can find both provable formulas that are not true (Example 4.10) and true formulas that are not provable (Example 4.11).

from binary_addition import is_theorem, is_true
is_theorem('BinarySumLogicalBroken', '1+1=1')
(F1) 1=1    (Axioma)
-> (F2) 1+1=1  (R1b)
'theorem'
is_true('BinarySumLogicalBroken', '1+1=1')
False

from binary_addition import is_theorem, is_true
is_theorem('BinarySumLogicalRestricted', '1+10=11')
'not proved within the first 154639 generated formulas'
is_true('BinarySumLogicalRestricted', '1+10=11')
True

4.3 #Soundness, completeness, and decidability

We have found logical systems in which there are true formulas that are not provable, and vice versa. This leads us to the definition of two important properties of logical systems.

Let us see whether the logical systems we have presented so far are sound and complete. A summary of all results can be seen in Table 4.1.

Proving that $\textbf{BinarySumLogical}$ is sound and complete is a matter of checking the axiom and each inference rule against the intended meaning of binary addition. A sketch is enough to see the idea; the full arguments are Proposition 4.14 and Proposition 4.15 below.

Since the other logical systems are "obtained" from $\textbf{BinarySumLogical}$, the following propositions are much simpler to prove. As is evident, Example 4.10 and Example 4.11 prove that $\textbf{BinarySumLogicalBroken}$ is unsound and that $\textbf{BinarySumLogicalRestricted}$ is incomplete, respectively.

Let us see these propositions next.

The logical systems $\textbf{BinarySumLogicalBroken}$ and $\textbf{BinarySumLogicalRestricted}$ were obtained by modifying the syntax of $\textbf{BinarySumLogical}$. We now introduce the last system of this type, which arises from modifying the semantics of $\textbf{BinarySumLogicalBroken}$.

In this last logical system we could have modified the symbol = to >=. However, we do not do so intentionally, to remember that syntax and semantics are independent—we can assign whatever truth value we wish.

Let us see a simple illustrative example of a true formula and a false formula.

from binary_addition import is_true
is_true('BinarySumLogicalFixed', '1+1=1')
True
is_true('BinarySumLogicalFixed', '1=1+1')
False

By modifying the semantics, we have managed to "fix" the $\textbf{BinarySumLogicalBroken}$ system, as its name suggests. Indeed, $\textbf{BinarySumLogicalFixed}$ is complete and sound.

As a summary, we see in the following table the completeness and soundness of the systems presented (along with other information we will see later).

In addition to the properties of soundness and consistency, we can introduce a computational property: decidability. We already know what decidable means for a decision problem: that we can solve it with a program that always halts and has the correct output. For a logical system $\mathcal{G}$ we can define a decision problem, $\textsc{IsTrue}_\mathcal{G}$.

For each logical system $\mathcal{G}$ we obtain a different decision problem. Once this problem is defined, it is natural to define the decidability of a logical system through the decidability of the problem.

Thus, a logical system is decidable if there exists a program that decides whether a formula is true or not. It is important to note that some authors define a system as decidable when the problem $\textsc{IsTheorem}_\mathcal{S}$ (which we define next) is decidable. As we have seen, truth and proof are different concepts, and we will always refer to truth when asking whether a logical system is decidable.

Let us see whether the logical systems we have introduced in this chapter are decidable. In the case of $\textbf{BinarySumLogical}$, it is straightforward to create a program capable of checking whether the inserted formulas are well formed, and of checking whether the arithmetic operation is correct. In fact, this program is implemented: it is the function is_true from binary_addition.py:

>>> from binary_addition import is_true
>>> is_true('BinarySumLogical', '1+1+1=11')
True
>>> is_true('BinarySumLogical', '11+1=10')
False

In the case of the remaining logical systems, creating programs that decide them is equally straightforward. The implementations of these programs are likewise in is_true. Below are more examples of running this function on the remaining logical systems.

>>> from binary_addition import is_true
>>> is_true('BinarySumLogical', '11=1+1')
False
>>> is_true('BinarySumLogicalBroken', '11=1+1')
False
>>> is_true('BinarySumLogicalRestricted', '11=1+1')
False
>>> is_true('BinarySumLogicalFixed', '11=1+1')
True

4.4 #Peano arithmetic

The logical systems we have explored are of little use. What we want is to work with logical systems that allow us to prove interesting results in mathematics. Mathematicians, logicians, and philosophers have studied many logical systems since the late 19th century, but two stand out for their importance: the Zermelo–Fraenkel axioms, of set theory, and Peano arithmetic, of number theory. In this section we focus on the latter, since Peano arithmetic contains formulas about integers, addition, multiplication, etc.

We call $\textbf{Peano}$ the logical system of Peano arithmetic. You can find the complete description of this system in Peano arithmetic. In Figure 4.22 you can find some details of that description.

In this system we can produce very interesting formulas about arithmetic. We see some of them below.

To work with $\textbf{Peano}$ in Python programs, we need to find a way to encode the various symbols, which we specify in Table 4.2.

For example, consider the statement "there do not exist integers $x$ and $y$ such that $2x = y$ and $y = 3$", which can be represented in $\textbf{Peano}$ as $\neg\exists x, y : S(S(0)) \cdot x = y \wedge y = S(S(S(0)))$ and admits the following string encoding:

NO EXISTE x,y : S(S(0))*x = y Y y = S(S(S(0)))

The formulas of $\textbf{Peano}$, being from a logical system, can be true or false. In Example 4.23, the first six formulas (from (PF1) to (PF6)) are true,⁸⁹ while the last one (formula (PF7)) is false.

To be able to prove whether a formula of $\textbf{Peano}$ is true, we need it to be closed: this occurs when all its variables are quantified by a "for all" ($\forall$) or an "exists" ($\exists$).¹⁰ An example is $\forall x,y : x = y \wedge x + S(0) = y + S(0)$, which is a closed formula since $x$ and $y$ are quantified, while $x = y \wedge x + S(0) = y + S(0)$ is not a closed formula. This distinction is important because, if a formula is not closed, we cannot know whether it is true. We will only consider closed formulas in $\textbf{Peano}$ from here on.

Once we accept that Peano arithmetic can express mathematical statements like those in Example 4.23, we can continue to express the outputs of a program in $\textbf{Peano}$. The following proposition shows how to do this for a concrete set of formulas about the programs we will need later.¹¹

From the previous proof, it is evident that the construction of $\phi_H$ from $H$ is carried out in a completely algorithmic way, which could in principle be implemented by a Python program. Let such a program be halting_to_peano.py. The code for this work does not provide a program that implements this, since doing so is a complex task.¹³ However, in the rest of this chapter, we will import the main function halting_to_peano when necessary.

We will next define two important decision problems: IsPeanoTheorem and IsPeanoTrue.¹⁴

Given a statement $\phi$ in $\textbf{Peano}$, the above problems ask whether $\phi$ is provable and/or true. It turns out that both problems are undecidable. The undecidability of IsPeanoTrue tells us, via Definition 4.20, that $\textbf{Peano}$ is not decidable (as we already anticipated in Table 4.1).¹¹

from is_true_peano import is_true_peano  # oracle
from halting_to_peano import halting_to_peano          # NOT an oracle
 
def halting_on_empty_to_is_true_peano(program):
halts_in_peano = halting_to_peano(program)
return is_true_peano(halts_in_peano)

The case of IsPeanoTheorem is less severe, since the problem is in fact semi-decidable (see Definition 3.20). This means we can write a program that checks whether a formula is a theorem (if the formula is not a theorem, the program need not halt).¹¹

import utilities
from is_proof_peano import is_proof_peano  # NOT an oracle
 
def is_theorem_peano(formula):
proof = ''
 
while True:
if is_proof_peano(proof, formula) == 'yes':
return 'yes'
proof = utilities.next_string(proof)

The fact that IsPeanoTheorem is semi-decidable is extremely important, and is due to a syntactic property of $\textbf{Peano}$: it is recursively axiomatizable.

Saying that a logical system $\mathcal{G}$ is recursively axiomatizable is nothing more than saying that the problem $\textsc{IsTheorem}_\mathcal{G}$ is semi-decidable. This property is fundamental for the proof we will carry out of the First Incompleteness Theorem (Theorem 5.2), since if $\textbf{Peano}$ were not recursively axiomatizable, we could not use the function is_theorem_peano.

The problem IsTheorem bears a strong relation to the Entscheidungsproblem (see Chapter 1). This problem seeks to find a general algorithm that, given a mathematical statement, determines whether it is a theorem. By Proposition 4.28, IsPeanoTheorem is undecidable, which proves the Entscheidungsproblem in the particular case of Peano arithmetic. The argument we have carried out is similar to the one Turing made in ¹⁷.

Finally, since $\textbf{Peano}$ is a logical system, we can ask about its soundness and completeness. The question of whether $\textbf{Peano}$ is complete is the central object of this work, and will be treated in Chapter 5.

Asking about the soundness of $\textbf{Peano}$ is a complex question. In this work, we assume its soundness, since it is reasonable that the theorems of $\textbf{Peano}$ are true.¹⁸

4.5 #Syntactic completeness and consistency

Logic books are extremely inconsistent¹⁹ in defining properties of logical systems (even in defining what a formal system and a logical system are). So far, we have defined the properties of soundness, (semantic) completeness, and decidability. There is another definition of completeness that depends only on syntax, and is therefore applicable to formal systems.²⁰

For this definition, the formal language must include a well-defined notion of negation ($\neg$). This is the case in first-order theories such as Peano arithmetic and Zermelo–Fraenkel set theory, but negation is also available in other logical languages.

For this class of systems it is also possible to define a new property: consistency. Again, we can define two types of consistency, a syntactic one and a semantic one.

In other words, a system is consistent if it does not give rise to contradictory proofs or truths. In a sound and complete system, a formula is syntactically consistent if and only if it is semantically consistent.

It is important to make an observation regarding the definitions of syntactic completeness and consistency: although we defined them for formal systems, it is straightforward to extend this definition to logical systems, taking into account their syntax.

Thus, we say that a logical system $\mathcal{G}$ is syntactically complete if, given a formula $\phi$ of $\mathcal{G}$, $\phi$ or $\neg\phi$ are theorems. Analogously, $\mathcal{G}$ is syntactically consistent if it is not possible that both $\phi$ and $\neg\phi$ are theorems.

The definitions we have made so far (not including that of decidability) are summarized in Figure 4.34.