Can a computer determine whether a mathematical statement is true or not?

Question

I was reading Introduction to the Theory of Computation by Michael Sipser and I found the following paragraph quite interesting:

During the first half of the twentieth century, mathematicians such as Kurt Godel, Alan Turing, and Alonzo Church discovered that certain basic problems ¨ cannot be solved by computers. One example of this phenomenon is the problem of determining whether a mathematical statement is true or false. This task is the bread and butter of mathematicians. It seems like a natural for solution by computer because it lies strictly within the realm of mathematics. But no computer algorithm can perform this task. Among the consequences of this profound result was the development of ideas concerning theoretical models of computers that eventually would help lead to the construction of actual computers

As a CS student, completely new to the theory of computation, this is hard to believe for me. It said that a computer can't solve a basic task such as determining whether a mathematical statement is true or false. Can't it really!? I have programmed lots of codes that determine if a mathematical statement is true or not. For example, a simple code such as return 6 == 2*3 will return true if this statement is true, so why does the text says that a computer can't perform this task?

I'm sure I'm missing something here. Perhaps I'm mistaken by the definition of "Mathematical statement". But I'm quite sure "Is 6 equal to 2 * 3?" is a mathematical statement and can be validated by a computer. So what did the text mean by that? I'm confused!

PS: Sorry if the Complexity theory tag is misplaced here. As I said I'm new to the field and on the same page the author of the book stated that the theories of computability and complexity are closely related.

Answer 1

The claim is not that a computer cannot determine the validity of some mathematical statements. Rather, the claim is that there is a class $\mathcal{C}$ of mathematical statements such that no algorithm can decide, given a statement from class $\mathcal{C}$, whether it is valid or not.

The standard choice for the class $\mathcal{C}$ is statements about natural numbers, for example:

Every even integer greater than two is a sum of two primes.

The class $\mathcal{C}$ contains all statements of the form:

For all natural $n_1$ there exists natural $n_2$ such that for all natural $n_3$ there exists natural $n_4$ such that ... there exists natural $n_{2m}$ such that $P(n_1,\ldots,n_{2m})$,

where $P$ is an expression using logical operators, comparison operators, addition, subtraction, multiplication, division, and integer constants.

Another popular choice for the class $\mathcal{C}$ is:

The following algorithm halts: ...

In both cases, there is no algorithm that takes an arbitrary statement from class $\mathcal{C}$ and correctly outputs whether the statement is valid or not.

---

It is crucial that the algorithm be required to answer correctly for all statements in $\mathcal{C}$. We can easily write an algorithm that answers correctly on a single statement from $\mathcal{C}$. Indeed, one of the following algorithms will work:

The statement is valid.

The statement is not valid.

Similarly, we can design an algorithm that answers correctly on two different statements $A,B$. One of the following will work:

The statement is valid.

The statement is not valid.

If the statement is $A$, then it is valid, otherwise it is not valid.

If the statement is $B$, then it is valid, otherwise it is not valid.

We cannot implement this strategy in the case of infinitely many statements, since an algorithm, by definition, has a finite description. This is the hard part – being able to decide, for infinitely many statements, whether they are valid or not.

Answer 2

On top of what everyone else has said, it may be worth talking about where some of the boundaries of decidability and undecidability are.

For natural numbers:

• The first-order theory of natural numbers with only addition (Presburger arithmetic) is decidable.
• The first-order theory of natural numbers with only multiplication (Skolem arithmetic) is decidable.
• The first-order theory of natural numbers with addition and multiplication (Robinson arithmetic; this is very close to Peano arithmetic without induction) is undecidable.

For real numbers:

• The first-order theory of real numbers with addition, subtraction, multiplication, and division (real closed fields) is decidable.
• The first-order theory of real numbers with addition, subtraction, multiplication, division, and the sine function is undecidable. This is one of the extensions of Richardson's theorem.
• Decidabiility of the first-order theory of real numbers with addition, subtraction, multiplication, division, and the exponential function is unknown. This is Tarski's exponential function problem, and it is one of the great unsolved problems in computability theory.

Answer 3

The key is quantifiers, both in the theorem, and in the "mathematical statements."

First, the theorem says that "there is no algorithm that can take in an arbitrary mathematical statement and prove if it is true or false." This does not mean that, for every mathematical statement, a computer can't determine if it's true or false. It just means that there's no computer program that will work on all mathematical statements.

The second relevant detail is that the mathematical statements they're talking about include quantifiers, For example, questions of the form "does there exist a number such that" or "does this hold for all numbers." Essentially, the intuition is that there's no way to know when you're done searching. If you're looking for a number with a given property, when do you stop? You can look at each number in sequence, but if none satisfy the property, you'll keep checking numbers forever.

As a concrete example of this, nobody currently knows whether the Collatz conjecture is true. Either there is some number that makes the Collatz sequence continue without a 1, or there is no such number. But there's no way to ask a computer whether such a number exists, since we wouldn't know when to stop looking. So, we have no idea.

In the absence of quantifiers, most mathematical statements about (computable) operations on numbers are easy: just evaluate the left hand side, evaluate the right hand side, and see if they're the same. But this is a very restricted subset of the questions that are interesting in math.

Answer 4

The statement is overly broad, as well as being overly complimentary to people. Computers can’t solve all problems but neither can people. Not sure why the extra drama was added.

What that is referring to is basically an aspect of the Halting Problem. A Turing machine can determine the answer to some questions but is unable to do so for others. They even mention Turing/Church.

Answer 5

A simple example of undecidable mathematical statements are whether multivariate integer polynomials have natural roots.

This means that we an expression $E(n_0,\ldots,n_k)$ built from natural number constants, natural number variables $n_0,\ldots,n_k$, addition, substraction and multiplication. We then want to know whether a solution for $E(n_0,\ldots,n_k) = 0$ exists.

A computer can in principle find a solution if there is one, just by exhaustively searching through all candidates, plugging them in and evaluating the expression. However, there is no general procedure to rule out the existence of a solution.

Further reading: https://en.wikipedia.org/wiki/Diophantine_set

Answer 6

What you're misunderstanding is how "problem" is used in computer science. "Problem" does not refer to finding the correct output for a particular input, but writing an algorithm that returns the correct output for all inputs. For instance, is there an algorithm that sorts a list in linear time? You could write a program that simply goes through the inputs and checks whether it's already sorted, and if so, returns that input, and that would constitute "an algorithm that can sort a list in linear time" for some interpretation of the phrase, but it's not a solution to the problem of linear sort, because a linear sorting algorithm has to be capable of sorting any list. So when they say "One example of this phenomenon is the problem of determining whether a mathematical statement is true or false", they mean "One example of this phenomenon is the problem of writing a program that determines, for all mathematical statement, whether that statement is true or false."

The reason we can't do this is because computer science is a subset of mathematics. Any computer science question can be put in terms of mathematics. Given a mathematical statement and a program, "the program will say that the statement is true" can itself be expressed as a mathematical statement. What the work of Godel, Turing, and Church shows is that given any program, it's possible to construct a mathematical statement such that the statement claims that the program will say that it's false. That is, given a program P, it's possible to define a statement S such that S = "Program P will say that Statement S is false". So if P does in fact say that S is false, then S is true, so P was wrong. But if P says S is true, then S is false, so P was wrong. P can't possibly return a correct response. It's like asking someone "Are you going to answer 'no' to this question?" Whether they say 'yes' or 'no', they're wrong.

This argument only applies once we create statements that are complicated enough to talk about themselves. It doesn't say that programs can't evaluate simpler statements, such as 6 == 2*3.

Answer 7

Other people have covered explaining the actual meaning of the theory this paragraph referenced. I will instead address how the quoted paragraph was intended to be interpreted, such that it does in fact correctly describe the theory.

During the first half of the twentieth century, mathematicians such as Kurt Godel, Alan Turing, and Alonzo Church discovered that certain basic problems ¨ cannot be solved by computers. One example of this phenomenon is the problem of determining whether a mathematical statement is true or false.

The crucial point for this segment is that "a mathematical statement" is not referring to any particular specific statement, nor even to a not-yet-specified statement. "A mathematical statement" is describing an input to the problem, that may be given any arbitrary value that matches the description, and truly solving the problem requires specifying a solution that will work for every conceivable possible value of that input.

This task is the bread and butter of mathematicians. It seems like a natural for solution by computer because it lies strictly within the realm of mathematics. But no computer algorithm can perform this task.

This segment confusingly uses the phrase "this task" to mean different things in different places, only one of which actually matches the problem described immediately before it.

The task of determining whether an individual specific mathematical statement is true or false is indeed the bread and butter of mathematicians, and that application of the problem to individual input values is what the first use of "this task" refers to.

The other use of "this task" refers to the general case I described above, of solving the problem for every conceivable input value, so that your solution is guaranteed to produce a correct answer no matter what input value you apply it to.

The general case task is impossible for computers, and it is also impossible for mathematicians. In fact, it's simply impossible, period. That result, the fact that the general case cannot be completely solved by any means, is the really remarkable thing about this.

Among the consequences of this profound result was the development of ideas concerning theoretical models of computers that eventually would help lead to the construction of actual computers

This section is going off on another topic, irrelevant to understanding the issue asked about here.

Answer 8

The computability-based generalized incompleteness theorem with its proof would shed more light on your question. In particular, Yuval's answer states but does not prove that the set of true arithmetical sentences (true according to the standard model $(ℕ,0,1,+,·)$ of PA) is undecidable. The linked post shows via reduction to the halting problem that the set of sentences about whether a specified program halts on a specified input is undecidable, and every such sentence can be expressed as an arithmetical sentence.

Note that the linked post also explains why the crux for undecidability is in fact not really about having the ability to reason about both addition and multiplication, contrary to what some people might think after seeing that both Presburger arithmetic and Skolem arithmetic are decidable. That actually is an artifact of arithmetic, not undecidability! To see why, note that TC (a simple finite axiomatization of finite binary strings with just concatenation, as mentioned in the linked post) is essentially incomplete; there is no program that decides whether a sentence over TC is a theorem of TC or not.

The crux of incompleteness is actually nothing more than the ability to reason about finite program execution, and Godel's crucial contribution was to show that PA can do this. Turing noticed that if we ignore the encoding issue, the crux is that the halting problem is undecidable by a program. The encoding issue (which is the actually hard part of Godel's work) is in fact a distraction from the core of incompleteness, which you can see from the case of TC.

In fact, Dan Willard designed a theory that can reason about enough arithmetic and yet can prove its own consistency, and the trick was simply to axiomatize subtraction and division instead of addition and multiplication, to evade the unbounded generation property that is one key ingredient of the ability to reason about finite program execution. See this post for more philosophical stuff related to this unboundedness issue.

Answer 9

I find postings above saying a computer can decide the truth or falsity of some statements but not of some others.

I find that a somewhat misleading way of putting it. For statements in first-order logic, a computer can search for a proof and if one exists it will find it. But if the program has been running for a trillion years and hasn't yet found a proof, there is no way to know whether that's because no proof exists or the search hasn't gone on long enough. This was proved in the 1930s.

Answer 10

So, Captain Kirk tells the android that Harry Mudd is a liar. Everything he says is a lie. The android accepts this premise, whereupon Harry Mudd says, "I am lying." The android expresses confusion that Mudd cannot be lying b/c that would be true and that cannot be true b/c he is a liar. Smoke comes out of his ears and Kirk saves the day! This is Star Trek.

You ask a question famous enough to have a name, "The Halting Problem."

Kurt Goedel shook the foundations of mathematics by formulated a theorem equivalent to "This theorem cannot be proven." He thus demonstrated any interesting axiomatic system could not be complete (including Mudd-like theorems) and consistent (including provably false theorems).

Apply this thinking to the Halting Problem. Suppose you had a program that proves theorems in an axiomatic system. Now construct a Muddy theorem therein and hand it to the program. If it halts, it's verified a falsehood. If it doesn't, the program hasn't done its job.

This is an old enough result that the people who thought of it performed computations using rooms full of people with a job title of "computer." The bosses would like to know when they could send folks home and how much overtime they'd have to pay... This paradox is even older than that b/c the Apostle Paul writes in Titus 1:12 'One of Crete's own prophets has said it: "Cretans are always liars, evil brutes, lazy gluttons."'

Douglas Hofstadter has written this much better than I in his book Gödel, Escher, Bach: an Eternal Golden Braid,

Answer 11

Interesting question.

The sentence is: determining whether a mathematical statement is true or false

1 - There are plenty of mathematical statements which could easily be decided right or wrong as you have depicted using 2*3=6 example. Hence making a general rule using the phrase -a mathematical statement- is startling, since it simply implies "any problem". Even though it is said in the previous sentence that "...certain basic problems cannot be solved...", but it is still ambiguous and mind boggling. So I should give it to you. In my humble opinion, the sentence is wrong as a general rule which makes you right. (don't panic, keep reading)

2 - When one reads through the introduction, the assumption is, one is not properly familiar with the true meaning behind terms like "problem classes" and "degree of complexity" and omitting those terms makes it very uneasy to demonstrate the very correct notion behind such an advanced scientific fact. (look at what you get in the accepted answer: ...there is a class C of mathematical statements such that...).

Answer 12

You can write a computer program that will prove / disprove some mathematical theorems. There are some problems that can be solved very easily but need an enormous number of steps to solve; computers can handle them easier than humans. For example the statement “1526753673279839 is a prime” is no big deal for a computer.

But there are two problems. One is there are many statements that are in principle impossible to prove true or false. Humans can’t solve them, and computers can’t. Can’t solve them now, and won’t be able to solve them ever.

The other more interesting (in my opinion) problem is that writing a program that can prove difficult theorems is very, very difficult. Proving Fermat's Last Theorem was really, really hard. I’d bet that writing a computer program that could do this would be ten times harder. Not impossible, but really hard.

Wiles needed an awful lot of intuition for his proof, and intuition is just “anything that we have no idea how to turn into an algorithm”. Not impossible, but we have no idea.

PS. I’m not talking about hypotheticals. When I say “a program that can solve FLT” I mean that in the sense that every sensible person would mean it, that is a program that can run on a reasonable computer in a human’s lifetime and produce a result.

PPS. Why do I find it a lot more interesting to look at how to write software that can prove provable theorems? Because unsolvable problems have been examined years ago, and mostly we only look at them because a new generation of new students arrives. All you need to know about them can be found on this single webpage, and read in an hour.

But actually proving theorems, that is both possible and very, very hard. Just try writing a program that can solve the Intermediate Value Theorem. Make it understand what a continuous function is. What a compact set is. What real numbers are. And then let it come up with the idea that the supremum axiom can be used. And of course you can't prove a theorem by producing ten to the gazillionth power of logical conclusions, because you don't have enough time to do it, you can't represent the proof if you found it, and it can't be verified.

(One class of proofs that hasn't been mentioned: Proofs that can be quite short but are practically impossible to find. There's a nice theorem: For every prime p, there is a proof that p is prime which can be checked in polynomial time. But that proof can be very hard to find!)