# Stronger theorem not resulting from proof analysis

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.

Probably the most famous example in reverse math is Ramsey's Theorem for pairs. The usual proof goes through in $ACA_0$, and iterates to give Ramsey's Theorem for n-tuples. But Seetapun gave a very different proof of Ramsey's Theorem for pairs shows that the statement is weaker than $ACA_0$. (And Seetapun's argument only works for pairs.)
Blass, Hirst and Simpson have analyzed the original Hindman proof to conclude that Hindman's Theorem is provable in $\mathrm{ACA}_0^+$, a relatively weak subsystem of second-order arithmetic. On the other hand, the Galvin-Glazer proof cannot even be formulated in second-order arithmetic since idempotent ultrafilters are higher order objects. Some arguments from topological dynamics can be formulated in second-order arithmetic but none have given better bounds than Hindman's original proof.