In this question I asked yesterday I put forward two interpretations of a statements such as "System X is consistent". (a) we can think of it as saying no finite sequence of applications of logical rules to the axioms of the system will result in a contradiction and (b) we can view it as a proof in some given formal System Y (where Y could or could not be the same as X) of some appropriate formalization of a sentence like "there doesn't exist a proof of 0 = 1 in System X". Taking the example of PA (Peano Arithmetic) we see that in sense (b), its consistency has been proved in various formal systems, such as ZF as well as much weaker systems. Godel's second incompleteness theorem says that we cannot prove consistency of System X in sense (b) in System X for sufficiently strong systems.
Now the question is why would we trust any proof of consistency of System X in sense (b) in System X. The mere fact we are trying to prove consistency suggests we doubt it in some sense, further if we have System X is inconsistent it is trivial to prove that it is consistent in sense (b). So let System Z be some formal system for which Godel incompleteness does not apply. Say there is some proof the consistency of System Z in System Z. Would that proof be expressing anything meaningful? It seems any proof undertaken in System Z implicitly assumes the consistency of System Z and we could not know, if System Z were to be inconsistent, if your consistency proof was subtly exploiting that inconsistency.
Thus we are forced to ask what the implications of 2nd incompleteness are. I see the import of 2nd incompleteness is this: "we cannot bootstrap consistency proofs". That is we cannot take some exceedingly simple system, System A, that we believe we can take to be manifestly consistent, and from that construct a chain of stronger systems B, C, D, …, PA, …, ZF, … s.t. $\vdash_A$ Cons(B), $\vdash_B$ Cons(C), …
Edit: At Carl Mummert's request I am adding a direct statement of a question. The most pertinent question is: Does $\vdash_X$ Cons(X) have semantic content? That is does proving the consistency of a System X in System X mean anything, P2 argues why I don't believe it does. P3 then endeavors to understand what the semantic content of Godel's Second Incompleteness Theorem is. So a secondary question is: does that analysis make sense, or does 2nd incompleteness say more?
Best Answer
You are correct in your explanation of why no proof of self-consistency can ever be trusted. If a proposed nice formal system $S$ (that interprets PA and has a proof verifier program) proves its own consistency, then the incompleteness theorems tell us that in fact it is not consistent. Even more so, $S$ itself knows this fact. This is completely contrary to what Hilbert expected.
Symbolically we can prove Godel's second incompleteness theorems expressed in provability logic: $ \def\nn{\mathbb{N}} \def\con{\text{Con}} \def\sound{\text{Sound}} $
In general, $\con(S)$ does not say that $S$ is consistent, but merely says that $S$ is arithmetically consistent, namely that $S$ does not prove $(0=1)$.
If $S$ proves $(0=1)$, then $S$ is useless because it proves every false arithmetical sentence. So for $S$ to be useful it must not prove $(0=1)$, in which case $\con(S)$ is a true arithmetical sentence, and hence by (GI*) $S$ must not prove the true arithmetical sentence $\con(S)$.
So it is not that $S ⊢ \con(S)$ has no semantic content. It is a statement about finite strings, and if it is true then it tells us via (GI*) that $S ⊢ 0=1$. You must distinguish carefully between the meaningfulness of "$S ⊢ \con(S)$" and the meaninglessness of asserting "$\con(S)$" just because $S$ proves it (which is of course stupid even if the incompleteness theorems did not hold).
But your explanation of "we cannot bootstrap consistency proofs" is incorrect. You are essentially trying to assert:
This is erroneous; you need $A$ to be arithmetically sound (or at least $Σ_1$-sound) before you can go from "$A ⊢ \con(B)$" to "$B$ is consistent"! So it is not enough to start from a consistent $A$. It is true that if $B$ interprets $A$, then $A$ cannot prove $\con(B)$ by (GI*), but that fact does not permit you to make the above assertion.
It is not possible to replace "consistent" by "arithmetically sound" either, because arithmetical soundness is not itself an arithmetical property. So I think there is not much you can say about bootstrapping that requires invoking (GI*).
That said, there are things you can say based on either (GI*) or (GI). For example, either of them suffice to show that $□P→P$ cannot be an axiom for every $P$. Note the relation with Lob's theorems (L*) and (L). This shows that every useful nice formal system $S$ cannot have an internal self-proof-to-truth assumption. Perhaps this is a better way to understand the impact of incompleteness. Note that $S$ can still have the rule ( if $⊢ □P$ then $⊢ P$ ). In fact, this rule is redundant if $S$ is $Σ_1$-sound.
More interestingly (as shown in the linked post), although $S$ proves $P∨¬P$ for every $P$, it may not prove $□P∨□¬P$, nor even $□P∨□¬P∨□¬(□P∨□¬P)$. And (as shown in the other post on that thread), $S$ cannot even have an internal self-consistency-implies-proof-to-truth assumption, namely that $S$ cannot always prove $¬□(0=1)∧□P→P$ without also proving $□(0=1)$ and rendering it all meaningless.