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?
closed as off-topic by Emil Jeřábek, Andrej Bauer, Gamow, D.W., Aryeh Sep 22 '18 at 19:44
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Emil Jeřábek, Andrej Bauer, Gamow, D.W., Aryeh
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:
- $PA$ is consistent if it does not prove a contradiction.
- $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:
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$.
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:
If Peano arithmetic proves $TP$ then the Twin Primes conjecture is true.
If Peano arithmetic proves $\lnot TP$ then the Twin Primes conjecture is false.
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.