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

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?

• Gödel's theorem does not apply to "any" formal system, and it says nothing about us being "sure". It says that a consistent recursively axiomatizable first order system that contains Peano arithmetic cannot prove its own consistency statement. But even if drop one of the conditions and get a system that can prove its own consistency why should we trust the proof unless we have independent reasons to believe that the system is not just consistent but sound in the first place? It is easy to come up with consistent junk that "proves" its own consistency, and even soundness, see cult teachings Jul 20 '20 at 6:04
• Godel Theorems are about specific formal mathematical system: every "wild guess" about the "meaning" of the theorem in more general (and vague) contexts is quite useless. Jul 20 '20 at 6:34
• The word here is "consistent". What this theorem shows is that for an apparently "complete" system you can have a well-constructed statement, which is consistent with the system meaning: such that is analyzable by the rules of the system for truth or falsity, but nevertheless is undecidable if you go by using the algorithms prescribed by the system. This leads to incompleteness of the system to describe all possible combinations of tokens that are valid within the system, by virtue of a non-computable, human understanding of the "consistency" of the said statement. Jul 20 '20 at 16:16

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.

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.