This is not quite true, Gödel's incompleteness theorems can luckily be formalized in extremely weak fragments of Peano arithmetic such as primitive recursive arithmetic (PRA) with its very limited induction principle. :-)

The only position on the philosophy of mathematics I know which does not accept PRA is ultrafinitism.

Problem with 1st-order PRA is that it is too weak to serve as

foundation of mathematics.

Can you provide a paper or book on this?

It's ok to use logic to prove theorems in logic. We also use thinking to deduce some facts about our thinking. Self-reference is not always paradoxical. In a higher-order logic some self-referential definitions are legitimate.

Yes and then you can do self-referential statements again which leads you to the conclusion that Gödels theorems are provable only in a system that cannot prove its own consistency.

True, but it's not a logical paradox. The fact that a system can't prove its own consistency doesn't imply that this system is inconsistent. The fact that Godel's theorems are provable only in such systems also doesn't imply that they are wrong.

From the common sense the whole situation looks paradoxical, indeed. To prove consistency of some theory we have to use some stronger theory, to prove consistency of that theory we need even stronger theory and so on.

Perhaps, the best way to realize why there is no paradox is the following:

Our memory is finite. As well as our thinking. But the total number of true facts about mathematics is infinite. By constructing theories we are trying to compress the infinite number of true facts into some finite form. Godel's theorem says it's impossible. And it looks quite natural from this perspective.

I never said it is a paradox. I never said that PA or Q is inconsistent. I said that they cannot prove their own consistency by Gödels theorem. Hence we don't know if Gödels theorem was formalized in an inconsistent system.

Honestly it would be weird if the incompleteness theorems don't apply to themselves.

The logical contradiction is that allowing the [Gödel 1931]

proposition I'mUnprovable into foundations makes the

foundations inconsistent.

It's not Peano arithmetic, it is basically 'enough of' arithmetic for Goedel's methods to apply. Robinson arithmetic is weaker than PA but Goedel still applies. Goedel's argument is basically a meta-argument about any mathematical system which is rich enough to describe useful mathematics, it does not rely on any particular axiomatisation, rather it applies to all axiomatisations with a few simple features.

While it is true that Goedel's theorem applies to weak systems such as Robinson Arithmetic (and any decidable extensions there of), The proof of Goedel's result itself requires at least some amount of induction.

As a consequence the minimum system that Goedel's second incompleteness applies to is stronger than the minimum system that the first incompleteness theorem applies to.

I think if Gödels proof needs Q then that is OK.

Q cannot prove its own consistency. Which means there is no way of telling that Gödels theorems are proved in a theory that is inconsistent (where everything is true).

"it does not rely on any particular axiomatisation"

-- OK, what does it rely on then?

The axioms allowing one to express enough of arithmetic for Goedel’s methods to apply. As the comment says.

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”.

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

for the foundation of mathematics.

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

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.

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

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

system for the foundation of mathematics.

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

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.