[ziroshima]

I feel the same way. My take away was that every system of logic will have some sort of "This sentence is a lie." type of paradox. But it feels more like a technical quirk to me than anything of real significance. The fact that many people smarter than I am feel otherwise indicates to me that I'm missing something.

[rsj_hn]

It is not about paradoxes like this, but missing proofs. Paradoxes are features of inconsistent systems, and we do not care about inconsistent systems. The types of paradoxes discovered in the early 20th century led people to refine set theory so that the paradoxes were removed and the systems were believed to be paradox free and thus useful for proving theorems. Once you've gotten rid of the paradoxes, you have a consistent system. This is the system of interest. Here, Godel is saying that consistent systems are incomplete.

E.g. any consistent system will have some theorems that cannot be proved within that system. Note that I am not saying there are theorems for which we don't know the proof. E.g. the proof is too difficult or unknown, waiting for a more brilliant mind to discover it. I mean that the theorem cannot possibly have a proof of its truth or falsehood.

The most famous example is the Continuum Hypothesis, which cannot be proved or disproved using standard set theory. The question of whether the continuum hypothesis is true is unanswerable. Thus the formal system is incomplete.

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

The reductio ad absurdum, i.e. assume the system is complete and prove that it is inconsistent is not used to seriously consider inconsistent systems but rather to demonstrate that the systems we care about -- e.g. the consistent systems -- are incomplete.

[ProfHewitt]

It is only for 1st-order logic that it has been shown that the

Continuum Hypothesis can neither be proved non disproved.

The issue of the Continuum Hypothesis is still open for more

powerful theories. See the following:

https://papers.ssrn.com/abstract=3457802

[ProfHewitt]

It's not about "missing proofs". Instead its about

propositions not being provable.

See the following for contradictions in foundations:

https://papers.ssrn.com/abstract=3603021

[ProfHewitt]

Ziroshima:

Your intuition is correct in that Gödel's proposition

I'mUnprovable does indeed lead to an inconsistency in foundations.

However, there are foundational theories that can be proved

to be free of contradiction. For example, see the following:

https://papers.ssrn.com/abstract=3418003