# 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 – Conifold 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. – Mauro ALLEGRANZA 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. – Weezy 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.