Godel proved that there are statements that are true but not provable. Unproven conjectures such "Twin Primes" might fall into such a class, as I understand. If so, does it mean that we will never know if it's true or false? If true would it only be in the sense that some infinitely large and infinitely fast computer determined so by brute force? Or might it be that the conjecture (or another conjecture) could be neither true nor false and instead forever indeterminate?

  • $\begingroup$ I hate people downvoting reasonable queries without comment. What a tragedy has this site come to? $\endgroup$ – 1.. Sep 21 '18 at 12:22
  • 2
    $\begingroup$ Well, I didn't downvote the question (I even answered it), but to be quite honest, the question has very little to do with theoretical computer science and is not research-level. It belongs to math.stackexchange.com. $\endgroup$ – Andrej Bauer Sep 21 '18 at 12:51
  • $\begingroup$ @AndrejBauer I agree that the question is not research-level, and belongs elsewhere. So why not vote to close? This seems to me to be a problem these days that questions below the level of this site are rarely closed and referred to a more appropriate place. Instead they are just downvoted into oblivion. While the downvotes are justified in many cases, overall this is not a very productive outcome for anybody. $\endgroup$ – Emil Jeřábek Sep 21 '18 at 13:34
  • $\begingroup$ That's true, downvotes are not for signalling that the subject is unfit. Perhaps we should have the ability to migrate questions a bit more aggresively. $\endgroup$ – Andrej Bauer Sep 21 '18 at 14:23
  • $\begingroup$ Hi Jim Lewis, I suppose that it is a little problematic to say that "the conjecture (or another conjecture) could be neither true nor false". The TWIN PRIMES conjecture is a logical statement, and can be either true or false by the definition of a logical statement, not neither true nor false... The ability to tell weather it is true or false is another question, and we may never know the answer or be able to prove either way. $\endgroup$ – Avi Tal Sep 21 '18 at 17:28

Yes, there is a difference.

Incompleteness is a property of a formal system logic. Given a formal system $L$, we say that it is incomplete if there is a sentence $S$ such that $L$ does not prove $S$ and $L$ does not prove $\lnot S$.

Knowing is an activity of an agent, such as a human, or a robot which holds beliefs about its environment. To say that an agent knows a statement $S$ means that the agent correctly believes $S$ is the case.

So the first thing to make clear is that incompleteness and knowing are two very different sorts of things. It makes no sense to say that a formal system of logic "knows" that $S$ holds. And knowledge may be obtained by many different means, some of which are not related to logic. (For instance, I know that it is sunny outside at the moment through direct observation.)

There is a relation though: if an agent uses a sound formal system $F$ to prove a sentence $S$, then it will know $S$. This is what mathematicians do: they prove things so that they can correctly believe them. In that sense, your question may be understood as follows:

Given the incompleteness of formal systems, are there some mathematical facts which we will never know? What if we give ourselves infinite time to exhaustively search through all proofs?

The answer is this: for a fixed formal system $F$, such as first-order logic with Zermelo-Fraenkel set theory (which is proclaimed by many to be the "official" formal system of mathematics), there is always a sentence $S$ such that $F$ neither disproves nor proves $S$. Even if we had infinite time so that we could check all proofs of $F$, we still would not be able to prove $S$, nor would we be able to disprove $S$ using $F$. There just isn't a proof, and it doesn't matter how much time we have. Consequently, we cannot acquire knowledge of $S$ by using the formal system $F$. This does not mean that $S$ is uknowlable. It just means that $F$ is not helping us determine whether $S$ is true, but there might be another formal system $F'$ which does.

Mathematicians are not forced to use a single formal system $F$ all the time. Mathematical activity and knowing by mathematicians is not the same as a fixed formal system. For instance, mathematicians might agree to add another axiom to set theory, and thus some previously undecidable sentences will become decidable (and therefore knowable). In fact, such changes do occur in the history of mathematics, although it is difficult to track them back in time because mathematicians did not know what a formal system of logic was before the work of the modern logicians (Peano, Frege, Russell, and others).

How, why, and whether mathematicians should change the underlying rules of mathematics is a question for a different day, and a different forum.

Supplemental: Let me address the question in the comments about the Twin Primes. I am going to take the formal system of Peano arithmetic $PA$, but any other formal system would do. Recall that:

  1. $PA$ is consistent if it does not prove a contradiction.
  2. $PA$ is sound if, for any sentence $\phi$, if $PA$ proves $\phi$ then $\phi$ is actually true.

Here we take truth with respect to the intended model, i.e., our mathematical reality (I am not going to get into a discussion of what that might be, the OP is presuming one.) A sound formal system is consistent, but a consistent formal system need not be sound.

Another point of importance is this: truth and provability are different! Do not confuse "we cannot prove something" with "it is neither true nor false". By definition truth is always determined, i.e., a statement must have a truth value, but it need not have a proof.

Let $TP$ be the statement of the Twin Primes conjecture. Here are the possibilities, assuming Peano arithmetic is sound:

  1. If Twin Primes conjecture is true, then there is a sound formal system which proves it, namely Peano arithmetic extended with the axiom stating $TP$.

  2. If Twin Primes conjecture is false, then there is a sound formal system which proves it, namely Peano arithmetic extended with the axiom stating $\lnot TP$.

We can also look at the other side:

  1. If Peano arithmetic proves $TP$ then the Twin Primes conjecture is true.

  2. If Peano arithmetic proves $\lnot TP$ then the Twin Primes conjecture is false.

  3. If Peano arithmetic does not prove $TP$ and does not prove $\lnot TP$, then we may extend it at will with either $TP$ or $\lnot TP$. We will obtain a consistent formal system in either case, but it might be unsound.

| cite | improve this answer | |
  • $\begingroup$ Is it possible that for a given statement (e.g. Twin Primes conjecture) there is no consistent formal math system that can prove the statement? If so is there really still a sense to continue to say that the statement is true or false? Is it possible that the Twin Primes conjecture, for example, could be neither true nor false? $\endgroup$ – Jim Lewis Sep 21 '18 at 22:32
  • $\begingroup$ Please see the definition of "statement": math.ucsd.edu/~benchow/Week1notes.pdf $\endgroup$ – Avi Tal Sep 22 '18 at 0:18
  • 1
    $\begingroup$ @AviTal: that definition of statement is really bad and I would advise you not to take it too seriously. It's an outdated and simplified notion which historically comes from the early attempts to distinguish syntax from semantics. It's a mix of both. $\endgroup$ – Andrej Bauer Sep 22 '18 at 7:29
  • $\begingroup$ @JimLewis: I addressed your question in the comments. $\endgroup$ – Andrej Bauer Sep 22 '18 at 7:48

Not the answer you're looking for? Browse other questions tagged or ask your own question.