What does it mean when a proof of a theorem actually proves a stronger result?

Question

Many times, in math textbooks, the author says something along the lines of, "This proof of the theorem actually proves a stronger result...". I am a little confused as to what that means, formally. Formally, a proof is a sequence of either axioms or justified steps, culminating in the last step, which is called a theorem. So, I am a little confused what authors of math textbooks actually mean by that. It can't simply be something like, "Theorem $S$ implies theorem $S'$", because in a theory $T$, every theorem implies every other theorem in that theory. So, my real question is, has anyone formalized what it means for a proof of a theorem to actually prove a stronger result than the theorem itself? Or, is this, in fact, one of those notions in math books which has no adequate formalization, and is just one those things that are "You know them when you see them"?

Answer 1

It is quite common with complete induction. You want to proof A(n) for all natural numbers n. To do this you prove A(0) and you proof that A(n) implies A(n+1). And sometimes this doesn’t work because A(n) does almost but not quite imply A(n+1).

As an example, say you want to show that f(n) <= n. But f(n+1) is a tiny bit larger than f(n)+1, so the induction step doesn’t work.

However if you take the stronger statement f(n) <= n - 1/n, you might be able to prove that because f(n+1) may now be a tiny bit larger than f(n)+1, and the induction step still works.

Answer 2

Let's suppose that the theorem you intended to prove was this:

Theorem: $P$ implies $Q$.

And let's say that the proof went like this:

Step 1: $P$ implies $X$

Step 2: $X$ implies $Q$.

QED

But now someone thinks to ask: In Step 2, is the converse true? In other words, does $Q$ imply $X$? And they notice: No! $Q$ does not imply $X$.

In that case the proof of the theorem actually proves a stronger result: the implication $P \implies X$ is stronger than the implication $P \implies Q$.

Answer 3

It just means that the theorem is a corollary of an in essence different result.

The different result is stronger or more general.

Here's a perfect example, from my own work: group isomorphisms preserve element order