I've recently been looking at Gödel's incompleteness theorems from a very different angle. I'm not new to these theorems at all, but this is a different perspective which I haven't seen posted here before and wanted to ask about it.
The basic idea is this: we treat so-called "first-order PA" as an incomplete, yet sound and effective proof system for second-order PA. It's not quite the same as something like Henkin semantics: here, we really do interpret the second-order quantifiers as literally quantifying over all first-order predicates, but our proof system only has the ability to substitute in a first-order definable predicate into a second-order sentence and make whatever inferences one can be derive from that. The first incompleteness theorem then shows that this proof system is incomplete and cannot prove everything that is true in second-order PA. The second incompleteness theorem shows that any proof system for second-order PA which is complete is either not sound or not effective.
This perspective leads to some very interesting viewpoints. For instance, the Gödel sentence can be interpreting as saying that the proof system in question is not strong enough to prove the sentence. In other words, the proof system is not strong enough to prove its own lack of strength. We may then ask how we know this sentence is true, and of course the answer is that we don't: if we have inadvertently created an inconsistent theory, the sentence will in fact be false. What we do know is that if and only if the second-order theory is consistent and the proof system is sound, then the sentence is in fact true. Given these additional assumptions, we can then prove the Gödel sentence. In fact, the second incompleteness theorem is basically this, but where we formulate these new additional assumptions in a simpler way (directly asserting there is no natural number encoding a proof of 1=0).
But this is extremely bizarre, because it can be thought of giving us a way to strengthen our proof system "for free!" Basically, what we're saying is, if we start with our second-order proof system, we can simply add an additional inference rule basically stating "we assume this proof system to be sound" and somehow we can then magically prove more theorems which are guaranteed to be true in the second-order theory. This seems nuts.
One question is: does this mean it's a theorem of second-order PA that our proof system is sound? Or a theorem of second-order PA that second-order PA is consistent? Or at least the Gödel-encoded versions of these things? I'm not sure how to make sense of this.
EDIT: Noah Schweber has given some really good insights below into why a first-order perspective is probably a much cleaner way to look at this than the second-order proof-system above. In that view, this question can be rewritten as: when I add $Con(T)$ to some logical theory $T$, why does that really make it stronger? And in what "direction" is it strengthening the theory, rather than adding $~Con(T)$? When does it tend to point things towards a particular choice of "standard model" and why? I've left this question open though as I am also interested in the second-order view (even if it's more limited).
I'm not really sure I understand your overall goal (how does this differ from just the usual first-order "iterated consistency extensions"? why do you say that the second incompleteness theorem, rather than the first, is the one that "shows that any proof system for second-order PA which is complete is either not sound or not effective"? and a couple other confusions). However, focusing on the end of your post, I think the following is important:
More concretely, and abbreviating $(\mathbb{N};+,\times)$ (or similar) by just "$\mathbb{N}$," the set of second-order tautologies (in particular, the set of tautologous second-order implications) in the language of arithmetic isn't a definable-in-$\mathsf{SOL}$ subset of $\mathbb{N}$ (under an appropriate coding system). This is an immediate consequence of three facts:
The finiteness of $\mathsf{PA_2}$ (no need for an induction scheme!).
The categoricity of $\mathsf{PA}_2$ (no nonstandard models!).
Tarski's undefinability theorem (which while usually stated for first-order logic applies more generally).
Let $\varphi$ be the one-second-order-sentence axiomatization of $\mathsf{PA_2}$. Then by the first two bulletpoints above we get $$Th_{\mathsf{SOL}}(\mathbb{N})=\{\psi:\emptyset\models_{\mathsf{SOL}}\varphi\rightarrow\psi\},$$ but the third says that $Th_{\mathsf{SOL}}(\mathbb{N})$ isn't second-order definable in $\mathbb{N}$.
Consequently, we can't even ask in $\mathsf{PA_2}$ whether $\mathsf{PA_2}$ is satisfiable.