<p>Yes, there is a difference.</p>

<p><em>Incompleteness</em> is a property of a formal system logic. Given a formal system <span class="math-container">$L$</span>, we say that it is incomplete if there is a sentence <span class="math-container">$S$</span> such that <span class="math-container">$L$</span> does not prove <span class="math-container">$S$</span> and <span class="math-container">$L$</span> does not prove <span class="math-container">$\lnot S$</span>.</p>

<p><em>Knowing</em> 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 <span class="math-container">$S$</span> means that the agent <em>correctly</em> believes <span class="math-container">$S$</span> is the case.</p>

<p>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 <span class="math-container">$S$</span> 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.)</p>

<p>There is a relation though: if an agent uses a <em>sound</em> formal system <span class="math-container">$F$</span> to prove a sentence <span class="math-container">$S$</span>, then it will <em>know</em> <span class="math-container">$S$</span>. 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:</p>

<blockquote>
  <p>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?</p>
</blockquote>

<p>The answer is this: for a <em>fixed</em> formal system <span class="math-container">$F$</span>, 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 <span class="math-container">$S$</span> such that <span class="math-container">$F$</span> neither disproves nor proves <span class="math-container">$S$</span>. Even if we had infinite time so that we could check all proofs of <span class="math-container">$F$</span>, we still would not be able to prove <span class="math-container">$S$</span>, nor would we be able to disprove <span class="math-container">$S$</span> <em>using <span class="math-container">$F$</span></em>. There just isn't a proof, and it doesn't matter how much time we have. Consequently, we cannot acquire knowledge of <span class="math-container">$S$</span> by using the formal system <span class="math-container">$F$</span>. This does <em>not</em> mean that <span class="math-container">$S$</span> is uknowlable. It just means that <span class="math-container">$F$</span> is not helping us determine whether <span class="math-container">$S$</span> is true, but there might be another formal system <span class="math-container">$F'$</span> which does.</p>

<p>Mathematicians are not forced to use a single formal system <span class="math-container">$F$</span> all the time. Mathematical activity and <em>knowing</em> by mathematicians is <em>not</em> 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 <em>do</em> 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).</p>

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

<p><strong>Supplemental:</strong> Let me address the question in the comments about the Twin Primes. I am going to take the formal system of Peano arithmetic <span class="math-container">$PA$</span>, but any other formal system would do. Recall that:</p>

<ol>
<li><span class="math-container">$PA$</span> is <strong>consistent</strong> if it does not prove a contradiction.</li>
<li><span class="math-container">$PA$</span> is <strong>sound</strong> if, for any sentence <span class="math-container">$\phi$</span>, if <span class="math-container">$PA$</span> proves <span class="math-container">$\phi$</span> then <span class="math-container">$\phi$</span> is actually true.</li>
</ol>

<p>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.</p>

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

<p>Let <span class="math-container">$TP$</span> be the statement of the Twin Primes conjecture. Here are the possibilities, assuming Peano arithmetic is sound:</p>

<ol>
<li><p>If Twin Primes conjecture is true, then there is a sound formal system which proves it, namely Peano arithmetic extended with the axiom stating <span class="math-container">$TP$</span>.</p></li>
<li><p>If Twin Primes conjecture is false, then there is a sound formal system which proves it, namely Peano arithmetic extended with the axiom stating <span class="math-container">$\lnot TP$</span>.</p></li>
</ol>

<p>We can also look at the other side:</p>

<ol>
<li><p>If Peano arithmetic proves <span class="math-container">$TP$</span> then the Twin Primes conjecture is true.</p></li>
<li><p>If Peano arithmetic proves <span class="math-container">$\lnot TP$</span> then the Twin Primes conjecture is false.</p></li>
<li><p>If Peano arithmetic does not prove <span class="math-container">$TP$</span> and does not prove <span class="math-container">$\lnot TP$</span>, then we may extend it at will with either <span class="math-container">$TP$</span> or <span class="math-container">$\lnot TP$</span>. We will obtain a consistent formal system in either case, but it might be unsound.</p></li>
</ol>

CC BY-SA 4.0
2018-09-21T22:32:52.280Z
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?
Jim Lewis
CC BY-SA 4.0
2018-09-22T00:18:37.290Z
Please see the definition of "statement": http://www.math.ucsd.edu/~benchow/Week1notes.pdf
Avi Tal
CC BY-SA 4.0
2018-09-22T07:29:31.600Z
@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.
Andrej Bauer
CC BY-SA 4.0
2018-09-22T07:48:37.750Z
@JimLewis: I addressed your question in the comments.
Andrej Bauer
CC BY-SA 4.0
2018-09-21T11:50:53.420Z
2018-09-22T07:48:23.897Z
2018-09-22T07:48:23.897Z
Andrej Bauer
<p>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?</p>

CC BY-SA 4.0
2018-09-21T12:22:26.580Z
I hate people downvoting reasonable queries without comment. What a tragedy has this site come to?
Turbo
CC BY-SA 4.0
2018-09-21T12:51:14.903Z
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.
Andrej Bauer
CC BY-SA 4.0
2018-09-21T13:34:49.697Z
@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.
Emil Jeřábek
CC BY-SA 4.0
2018-09-21T14:23:16.017Z
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.
Andrej Bauer
CC BY-SA 4.0
2018-09-21T17:28:04.237Z
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.
Avi Tal
<computability>
Is there a difference between incompleteness and unknowable?
Jim Lewis
# Is there a difference between incompleteness and unknowable?

(Asked by: username_0 on 2018-09-21)

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?

**Tags:** computability
> **Comments:**
> **username_1**: I hate people downvoting reasonable queries without comment. What a tragedy has this site come to?  
> **username_2**: 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.  
> **username_3**: @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.  
> **username_2**: 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.  
> **username_4**: 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.  

---

## 1 answers

### Answer by username_2 on 2018-09-21. Score: 9

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.

> **Comments:**
> **username_0**: 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?  
> **username_4**: Please see the definition of "statement": http://www.math.ucsd.edu/~benchow/Week1notes.pdf  
> **username_2**: @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.  
> **username_2**: @JimLewis: I addressed your question in the comments.  

---

