[kaba0]

I’m not too knowledgeable on the topic, but Gödel’s proof uses a smaller logic system — on which a meta-language can be used to prove consistency/completeness. It is precisely about not being able to prove these properties “from within”.

[ProfHewitt]

As explicitly stated in the title [Gödel 1931] for a system

for the foundation of mathematics.

[erichahn]

Which one? I don't think so tbh because his proof uses PA.

[ProfHewitt]

The reason that [Gödel 1931] was influential was that it

claimed to prove incompleteness for a system for the

foundations of mathematics.

1st-order systems such a PA were introduced later and

quickly shown to be inadequate for the foundations of mathematics.

[kyberias]

It's very easy for you to check this from his 1931 article.

[ProfHewitt]

Yes, it is very easy to check that [Gödel 1931] was for a

system for the foundation of mathematics.

[erichahn]

If you figure this out correctly you can claim the third incompleteness theorem. (If I am right)

[ProfHewitt]

Results in [Gödel 1931] depend on existence of proposition

I'mUnprovable. Since, the proposition doesn't exist in

foundations, the results in [Gödel 1931] do not hold for foundations.