Main statement as theorem or corollary

Question

In a text there will often be a few important results that are usually called Theorems. Intermediate statements are called Lemmas, and statements that follow immediately from previous results are called Corollaries.

There is a problem here, however. Especially in the context of theorem provers: A Theorem $A$ is often proved using induction. In order to perform this induction, the statement of the theorem needs to be strengthened to $B$ (otherwise the induction will not 'go through'). The original statement $A$ of the theorem will then follow trivially from $B$. We now have three possible naming conventions for this:

• Call $B$ a Lemma and $A$ a Theorem. This is attractive, because $A$ is the main statement of interest. The problem is, however, that the proof of $A$ is mainly done in $B$, which is now called an 'unimportant' Lemma.

• Call $B$ a Theorem and $A$ a Corollary. This is attractive because $A$ follows immediately from $B$, hence a Corollary. Also, it makes clear that the proof of $B$ contains a lot of important steps. However, when looking over the text quickly, one might miss the main statement $A$, because it is phrased as a simple consequence of $B$.

• A third option is to not have $B$ at all but only state Theorem $A$, and then perform the strengthening of the statement 'inline' in the proof via a cut. This is also inconvenient because it hides the technique used to prove $B$, which may be very important.

I would be interested in how this is commonly solved.

Answer 1

Another approach is to present both as theorems, but to present only A as a `marquee result' in the introduction, mentioning that it follows from the stronger but more technical B.

Answer 2

In my opinion, the best thing to do is to be honest and to explain that $A$ is the statement of main interest and that one is forced to prove the stronger statement $B$ just for technical reasons.

So I would call the statements Theorem $B$ and Corollary $A$ (since $A$ descends from $B$, after all), or maybe Theorem $B$ and Theorem $A$ if I intend to further emphasize the importance of $A$.

I think it is also convenient to write a remark explaining why the proof argument does not work for $A$; in this way, the reader will be motivated not to skip the proof of $B$.

Answer 3

I would state the main result up front, along the lines of:

In this paper we prove the following theorem:

Theorem A: (statement of theorem A)

Then go on with the explanation of the proof, including introducing B:

In order to enable the use of induction, we strengthen (A) to give:

Theorem B: (statement of theorem B)

Then establish the base and inductive cases, plus anything else you need to prove B. Then you can finish with:

Theorem A follows simply as a corollary.

Answer 4

As you said, we call something a theorem to highlight it as an important result (irrespective of how hard it was to prove), whereas a lemma is an intermediate result on the way to a theorem.

By this criterion, then we should certainly have Theorem A. Whether to call B a theorem or a lemma is a judgement call on whether the generalization is of sufficient interest to be important in its own right ($\implies$ theorem), or whether it is really just a technical detail to make the proof go through ($\implies$ lemma).

Answer 5

You say "Especially in the context of theorem provers: ..." then go on to describe conflating content and presentation. The content is a dependency tree of theorems. The presentation uses words like "lemma", "theorem", and "corollary" to help organize the information for a reader.

If we are "in the context of theorem provers", we are discussing content, so the resolution is straightforward: everything is a theorem. Perhaps one wants to allow some presentation markup in one's theorem prover, but mixing content and presentation is an anti-pattern.

(In the context of presentation, the situation you are describing is the familiar pattern of having a denouement corollary after some complicated (sequence of) theorem(s) in the preceding work. Then the labelling indicates the amount of work the reader should expect to expend to understand the object. Until theorem provers start proving theorems about the difficulty in understanding a statement and proof assuming a reader model, this is not in the context of theorem provers.)