Stronger theorem not resulting from proof analysis

Question

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.

Answer 1

The following statement has a proof in ZF, which requires thinking harder than the usual proofs in ZFC (or dependent choice):

A function $f: \mathbb R\to \mathbb R$ which is sequentially continuous is continuous.

Note that this is not the same as "sequentially continuous at $x$ implies continuous at $x$", which is not provable in ZF.

See Herrlich's book on AC for this.

Answer 2

Hindman's Theorem is a semi-example. The most common proof is the Galvin-Glazer argument that uses idempotent ultrafilters. Hindman's original proof was a phenomenally complex direct combinatorial construction. Later, other proofs came along using ideas from topological dynamics.

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.

So this is an example where you have to work much, much harder to see that the result is provable in a relatively weak system, but the hard work was not new work tailored for that purpose, it was older work that preceded the better known easier proofs.

Answer 3

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.)

Answer 4

Often we can easily prove something using impredicativity (e.g., by constructing something “from above” by taking the intersection of all solutions), while there may be a more difficult (or at least completely different) construction “from below”.

This will encompass a range of examples. To get things started, I'll add one (anyone: feel free to add more!):

• To prove that the sheafification functor exists (for a small Grothendieck site), we can either use a simple construction involving the corresponding Lawvere–Tierney operator on the subject classifier (impredicative), or we can use a more involved construction assuming WISC (but otherwise predicative).

Answer 5

There are many examples in reverse math where the standard argument requires $\Pi^1_1$-$\mathsf{CA_0}$ but a more careful transfinite recursion goes through in $\mathsf{ATR_0}$. I've written about the Cantor-Bendixson theorem in particular, and a general "length heuristic," at math.stackexchange. (I've also argued there that the $\mathsf{ATR_0}$-provability of open determinacy is not a counterexample to this heuristic, but that's a shakier point.)