26
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ It seems to me that you inverted $A$ and $B$ at the end of the first and second point. $\endgroup$ – Francesco Polizzi Jan 15 '18 at 14:31
  • $\begingroup$ Yes, sorry about that. I've fixed it. $\endgroup$ – Lasse Jan 15 '18 at 14:36
  • 3
    $\begingroup$ Crossposted to MSE: math.stackexchange.com/questions/2598088/… Please don’t do that, as it leads to duplicated effort. $\endgroup$ – Jeremy Rickard Jan 15 '18 at 17:06
  • $\begingroup$ Isn't everything a "corollary"...? $\endgroup$ – Najib Idrissi Jan 16 '18 at 10:37
  • $\begingroup$ Well, technically yes. But from a style perspective something is usually only a corollary, if it follows almost directly from the preceding lemma/theorem. $\endgroup$ – Lasse Jan 16 '18 at 18:00
28
$\begingroup$

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.

$\endgroup$
13
$\begingroup$

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

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Yes that is certainly true. But using this rationale, one might never actually use a corollary, because presumably one would not state a trivial truth if it is not important. So then all corollaries would become theorems. $\endgroup$ – Lasse Jan 15 '18 at 14:38
  • 1
    $\begingroup$ A corollary is also a term to highlight an important result, but one which follows quickly from a theorem, whereas a theorem is usually a culmination of a bunch of lemmas. $\endgroup$ – Doris Jan 15 '18 at 14:56
  • $\begingroup$ Also a corollary is always a corollary of something, and in my experience always appears right after the thing it is a corollary of. So if statement A is in the introduction, say, and statement B is in a later section, you shouldn't call A a corollary. $\endgroup$ – Doris Jan 15 '18 at 14:58
2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Not everyone agrees with you that mixing content and presentation is an anti-pattern. For example, Knuth specificly invented literate programming to mix content and presentation. Theorem provers like Coq consciously support literate programming, and therefore have styling options. $\endgroup$ – Lasse Jan 16 '18 at 17:50
  • $\begingroup$ Having said that, after one proofs something in a theorem prover, often one wants to write a paper. In this paper, you would like to follow the structure of the formal proof as precisely as possible, for easy of comparison. So in my opinion, this problem also transfers to a paper setting. But do I understand from the text in your parenthesis, that you advocate using a theorem for B and a corollary for A? $\endgroup$ – Lasse Jan 16 '18 at 17:52
  • $\begingroup$ @Lasse : Knuth eventually backed away from literate programming, realizing the intersection of good programmers and good writers is effectively empty. (There's a Knuth quote to this effect which I am too lazy to find.) $\endgroup$ – Eric Towers Jan 17 '18 at 0:47
  • $\begingroup$ @Lasse : Yes, my test in parentheses recommends using the common idiom of technical theorem followed by gee-whiz corollary. $\endgroup$ – Eric Towers Jan 17 '18 at 0:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.