> What Godel actually proved is that given a consistent formal system capable of representing arithmetic, there are statements in the language of that system such that neither the statement nor its negation can be proved in the system.

It goes what step further, there are statements that are true but can not be proved.

> Godel's theorems are notoriously liable to misinterpretation, and to be honest this sounds like one.

What do you think was Godel's philosophical motivation for investigating incompleteness?

"Many philosophers and logicians have explored the significance of these theorems. However, they would often find a reason to distance themselves from the interpretation their author, Kurt Gödel, ascribed them. Gödel believed that his results provide a strong argument for the objective existence of a rationally organized world of concepts, which can be to some extent described by a deductive system but cannot be changed or manipulated (cf. [12], p. 320)." [0]

You can argue that Godel misinterpreted incompleteness and There is a case to be made for that. Godel probably did not misinterpret his own philosophy about incompleteness.

> Godel's proof itself can be formalized, so I don't see how it places a limitation on formalism in general

It uses formalism to show that formalism is limited and that the positivist notion of truth does not include things which are true but can not shown to be true (within a axiomatic system capable of expressing arithmetic).

[0]: Kurt Gödel and the Logic of Concepts (2024) https://arxiv.org/html/2406.05442v2#bib.bib12

▲

griffzhowl 2 days ago | parent [-]

> It goes what step further, there are statements that are true but can not be proved.

No, this is the misconception. I know it's often stated this way, but it's wrong. Godel showed that given any formal system, you can construct a statement that the system can neither prove nor disprove. But Godel actually proves this statement in his proof, so it's certainly not unprovable in general.

▲

EthanHeilman a day ago | parent [-]

As far as I can tell this is not a misconception, I am just not communicating clearly enough. I figured I could make the point at a higher level.

You can construct a statement in an axiomatic system complex enough to express arithmetic:

1. Which is true,

2. AND which can be proved to be true under the assumption the system is consistent,

3. and which can not be proven true within that axiomatic system because you can't prove consistency of the system itself within the axiomatic system itself.

The crass positivist position would be that such undecidable statements are meaningless, i.e. neither true nor false. The incompleteness theorems provide a strong counter-example: a statement which can not be proved within that axiomatic system, but is true (if the system is consistent). The positivists must then amend their position to include things which can't be proved within the axiomatic system but can be proved true. This resulted in the watered down late-positivism.

	▲	griffzhowl 5 hours ago \| parent [-]
		Yes, the misconception is to think Godel's theorem shows that there are true but unprovable statements. In fact, what it means for a mathematical statement to be true is that it's provable. Godel showed that the concept of provability is much more subtle than following from a single axiom system, but it doesn't show that there's some kind of transcendent form of mathematical truth that doesn't depend on proof, in my view.