Suppose that we proved $\varphi$ from a theory $T$. Often we ask whether or not we could have proved $\varphi$ with a weaker theory, to find out we usually analyze the proof and try to figure out whether or not a general result would have been true in a weaker theory.

For example, clearly $\sf ZFC$ proves that every infinite set has a countably infinite subset. However when one analyzes the proof it is easy to see that much weaker assumptions suffice, for example $\sf ZF+DC$ - and if one tries harder then one can even show that the even weaker $\sf AC_\omega$ suffices instead of $\sf DC$.

Establishing the fact that the two are not equivalent, and that there are models of $\sf ZF$ in which every infinite set has a countably infinite subset; but $\sf AC_\omega$ fails requires a different approach. But that is not what I am interested in.

I am looking for that "one tries harder" examples, where the fact that $\varphi$ is provable from a much weaker theory required a whole other approach - rather than proof analysis.

Two examples I have in mind are,

1. The fact mentioned above, about countably infinite subsets. The usual proof with the axiom of choice would be to define by induction a sequence. Analyzing that proof would result in $\sf DC$ being sufficient; but if one takes on a different approach and works slightly harder then one can see that $\sf AC_\omega$ is enough.

2. Shelah's proof of Los conjecture, and the generalization of Morley's categoricity theorem (Sh:840). I am unfamiliar with either proof, but here is Shelah's abstract:

The main result is Los conjecture: characterizing in ZF of countable first order T categoricity in some uncountable $\aleph_\alpha$ (or every one). If there are $\aleph_1$ real this is Morley's theorem, the ZFC one. Otherwise, we get a different theorem. The characterization (and the proof) are different. (Taken from here.)

So while the results are similar - under a weaker theory of course - the approach is different.

I am interested in similar examples, preferably with a summary of the argument (in case such summary is possible to give). Other reverse mathematics and proof analysis results are less interesting in this context.

Suppose that we proved $\varphi$ from a theory $T$. Often we ask whether or not we could have proved $\varphi$ with a weaker theory, to find out we usually analyze the proof and try to figure out whether or not a general result would have been true in a weaker theory.

For example, clearly $\sf ZFC$ proves that every infinite set has a countably infinite subset. However when one analyzes the proof it is easy to see that much weaker assumptions suffice, for example $\sf ZF+DC$ - and if one tries harder then one can even show that the even weaker $\sf AC_\omega$ suffices instead of $\sf DC$.

Establishing the fact that the two are not equivalent, and that there are models of $\sf ZF$ in which every infinite set has a countably infinite subset; but $\sf AC_\omega$ fails requires a different approach. But that is not what I am interested in.

I am looking for that "one tries harder" examples, where the fact that $\varphi$ is provable from a much weaker theory required a whole other approach - rather than proof analysis.

Two examples I have in mind are,

1. The fact mentioned above, about countably infinite subsets. The usual proof with the axiom of choice would be to define by induction a sequence. Analyzing that proof would result in $\sf DC$ being sufficient; but if one takes on a different approach and works slightly harder then one can see that $\sf AC_\omega$ is enough.

2. Shelah's proof of Los conjecture, and the generalization of Morley's categoricity theorem (Model theory without choice? Categoricity, J. Symbolic Logic, 74(2), 361–401 Sh:840, arXiv:math/0504196). I am unfamiliar with either proof, but here is Shelah's abstract:

The main result is Los conjecture: characterizing in ZF of countable first order T categoricity in some uncountable $\aleph_\alpha$ (or every one). If there are $\aleph_1$ real this is Morley's theorem, the ZFC one. Otherwise, we get a different theorem. The characterization (and the proof) are different.

So while the results are similar - under a weaker theory of course - the approach is different.

I am interested in similar examples, preferably with a summary of the argument (in case such summary is possible to give). Other reverse mathematics and proof analysis results are less interesting in this context.