Does Godel's second incompleteness theorem mean it's impossible to know whether a proven statement cannot also be disproven?

Question

I am trying to understand Godel's Second Incompleteness Theorem which says that any formal system cannot prove itself consistent.

In math, we have axiomatic systems like ZFC, which could ultimately lead to a proof for, say, the infinitude of primes. Call this "InfPrimes=True". In that case, does Godel's Second Incompleteness Theorem mean that we cannot be sure whether there exists a proof for NOT("InfPrimes=True"), or "InfPrimes=False"?

Since Godel's Second Incompleteness Theorem says we cannot be sure the system is consistent, is there a way to know for sure whether any given statement is true AND there does not exist any proof in that system showing the statement is false?

Answer 1

Since Godel's Second Incompleteness Theorem says we cannot be sure the system is consistent, is there a way to know for sure whether any given statement is true AND there does not exist any proof in that system showing the statement is false?

As talked about in the comments, I will assume we're talking about the appropriate formal mathematical systems.

Well, it depends on what you mean by 'know for sure'. If you mean being provable from within the system, the answer is no we can't be sure. Leave off the first part about being true... we cannot even prove that "there does not exist any proof that within a system that a statement is false".

The thing to note is that if one contradiction is true within the system, then every contradiction is true, by the principle of explosion:

https://en.wikipedia.org/wiki/Principle_of_explosion

So "a contradiction exists in the system" implies "all statements are provable in the system".

The contrapositive is, "not all statements are provable in the system" implies "there does not exist a contradiction in the system"

So if we were able to prove that any given statement is not provable within a system, we prove that there does not exist a contradiction within the system. But that would prove the consistency of the system. Which violates godel's 2nd incompleteness theorem.

So a proof from within a system that a given statement is not provable within the system would violate godel's 2nd incompleteness theorem.

Answer 2

Assume you have a mathematical system, powerful enough to express the sentence S: “In this mathematical system, there is no proof for the sentence S” in a strict mathematical way.

Now either there is a proof for S, or there isn’t. If there is a proof for S, then S is false because it says there is no proof, so we have a proof for a false statement and this mathematical system is contradictory. If there is no proof for S, then S is true because that’s exactly what S claims, so we have a true sentence that has no proof, and the mathematical system is incomplete.

What Gödel did was to express S in strict mathematical terms in our standard mathematical system, which shows it is either contradictory or incomplete. Which one it is we don’t know, but no contradictions have been found yet, and there are many statements for which no proof is known.

Now your question: It is entirely possible that our mathematical system is inconsistent, and if it is, then someone can prove it, and that someone would have proved that every mathematical statement X has both a proof for X and a proof for not X.

It is always possible to find a contradiction if it exists, because it actually exists. Proof for incompleteness may be impossible, because just because we haven’t found a proof doesn’t proof it doesn’t exist, only that we didn’t search hard enough.