"No first-order theory containing a sufficient amount of arithmetic can prove its own consistency". It's the "prove its own" part of Godel's theorem that always confused me. Why do we care so much about PA proving $\textit{itself}$ consistent? Can't we prove it is consistent using our natural language?
Now, I am making the rough claim here that $\mathbb{N}$ exists intuitively in our natural language. Since we know that every satisfiable set of axioms is consistent (equivalent to soundness) and $\mathbb{N}$ satisifies the PA axioms, then the existence of $\mathbb{N}$ says that PA is consistent!
Of course there must be something I'm misunderstanding. The only objection to my 'PA-consistency proof' that I can think of is that formalists would claim that our intuition of $\mathbb{N}$ is actually more dubious than finite manipulations of strings. Therefore we should trust the formal manipulation of strings.
But, I would argue that the only reason they trust those finite manipulations of strings is because there are 'proofs' that $\vdash$ corresponds to $\models$ (completeness and soundness). And these two theorems are 'proved' outside of a formal language using our natural language (they are theorems $\textit{about}$ first-order languages, not theorems $\textit{of}$ first-order languages). So shouldn't a formalist think of formalism as being just as dubious as $\mathbb{N}$?
I hope that all made sense. In short, I am asking why can we not just claim that $\mathbb{N}$ proves PA is consistent based on the soundness theorem?
Also, I would be grateful if someone could give me some insights on how other consistency proofs work for other formal theories. In order for them to all prove their own consistency wouldn't they have to use some kind of self-referencing similar to Godel codes?