How to insert new theorems in edition 1

[andrejbauer]

The incremental improvements to the book are working very nicely, I think. But the fact that we decided not to change numbering is making it hard to iterate towards a second edition. In fact, it is going to be hard to ever begin working on a second edition because the incremental corrections work so well.

Of course, not changing the numbering was the correct decision to make. People refer to theorems by their numbers. However, let us think about relaxing the scheme so that we can in fact add new theorems. It is simple, really, once we recognize the fact that nothing prevents us from using a dense linear order.

For example, we could insert new theorems in such a way that they would receive numbers between those already in the book. I think it could be made to work. At some point we can "reset" the scheme and announce a 2nd edition, but I suspect it would be better to plan for a neverending stream of improvements.

[andrejbauer]

Now that I think about this, it is not so clear how it cold be done. I was thinking of some sort of "bisection" method. Suppose we introduce new envrionments newthm, newdef and so on for insertion of new items. If three newthm are inserted between 4.2.10 and 4.2.11, they might be numbered 4.2.10.X. But how would we allocate the X's and respect the order in which they were inserted?

One option is to give explicit infromation on the ordering somewhere, but that sounds annoying.

[JasonGross]

One option is to allocate the X's manually (newthm and newdef take X as an argument), and then when you "reset", you remove the manual numbering. Another option is to take a label for the preceeding theorem, and a boolean that says whether to start a new counter or use the previous one. Then you write some LaTeX black magic code to compute the numbers correctly.

[mikeshulman]

For what it's worth, I don't think that the 2nd edition should be just a collection of minor improvements. I'd rather not call anything the 2nd edition until we want to make some more major change, like adding substantial new material or changing the underlying type theory.

However, this is a good idea. But it does seem impossible in principle for LaTeX to tell from three un-annotated newthms in between 4.2.10 and 4.2.11 which of them was inserted first, and without that information there seems no way to allocate numbers to them automatically in a way that will be stable under inserting new ones.

[JasonGross]

Well, LaTeX could use \write18 to call git blame on the input .tex file and parse the output of that to figure out the ordering, but that seems rather insane. Another option if to have travis auto-annotate new theorems with dates (similar to what it does with errata), or to have the makefile pre-process the .tex file using git blame.

[andrejbauer]

I agree there is no automagic. What is the least amount of manual work that is needed? Also, we need a scheme that protects us from ourselves. Here's a possiblity: the new environment newthm takes a fraction between 0 and 1 (I am not kidding). We check that the newthm's appearing between two old thm's are ordered strictly linearly. That is, the fractions appear in a strict increasing order. Thus, between 4.2.10 and 4.2.11 we would have 4.2.10½ and 4.2.10⅔ and so on. This would be kind of crazy but it would work.

I don't like coupling the solution with git. It should be a pure LaTeX solution.

The strict linear order thingy can be checked fairly easily. We remember the last fraction seen. Old environments set it to 0. New environments check that the last fraction seen is strictly greater than the given one.

[mikeshulman]

I actually like the use of fractions: I would prefer 4.2.10½ over 4.2.10.5 because with the latter choice, some theorems are numbered x.x.x and others are numbered x.x.x.x, which seems potentially confusing. Using fractions makes it clear that all theorems come in the same sequence.

At first I thought it would be hard to program TeX to compare fractions, but then I realized it's easy as long as it can multiply and compare integers.

[mikeshulman]

Actually, there is a sensible and quite general way to assign numbers to new theorems. The location of a new theorem to be added in a section defines a cut of the existing theorem numbers in that section, and therefore identifies a unique simplest number inhabiting that cut (in the sense of the surreals). For instance, if a new theorem is added in between 4.2.10 and 4.2.11, then the cut { 1,2,3,...,10 | 11,12,...,n } defines the number 10½, while if a new theorem is added at the end, then the cut { 1,2,3,...,n | } defines the number n+1. With this scheme we'd be okay even if sometime we have to add infinitely many theorems.

One slight problem with it is that if a new theorem is added to a section which previously contained no theorems, then for consistency it should be numbered 1, but the cut { | } defines the number 0. (Of course, this would not be a problem if we had consistently numbered theorems starting from 0 in every section to begin with.) We could assume an implicit "theorem 0" at the very beginning of every section to prevent this, but that would have the additional effect that a new theorem added to section 4.2 before theorem 4.2.1 would become 4.2.½ rather than 4.2.0. I'm not sure whether that's the right thing to do -- should theorem numbers always be positive?

Another question is what to do when multiple theorems are added at the same time. If we add two theorems in between 4.2.10 and 4.2.11 at the same time, the above scheme would require us to first number one of them 4.2.10½ and then the other one either 4.2.10¼ or 4.2.10¾, depending on which order we chose to number them in. But it would arguably be more natural to number them as 4.2.10⅓ and 4.2.10⅔.

[andrejbauer]

When does 1/3 happen? Or do we keep getting dyadics? I like a canonical choice of numbers.

[mikeshulman]

With the surreal scheme, we would never get past dyadics as long as every section contains only finitely many theorems. But we would have to decide what to do about the issues in my second two paragraphs, and the latter might lead to theorems being numbered with thirds. Any thoughts about whether theorem numbers should always be positive?

Another canonical scheme would be:

• if adding n theorems at the end, take the least n positive integers not yet in use.
• if adding n theorems at the beginning (to a section that already contains theorems), take the greatest n integers not yet in use.
• if adding n theorems in between two existing theorems numbered X and Y, divide (Y-X) into n equal parts and use the boundary points.

That way if we add two theorems in between 4.2.10 and 4.2.11, they would be 4.2.10⅓ and 4.2.10⅔, and then if we later add three theorems in between 4.2.10 and 4.2.10⅓ they would be 4.2.10 1/12, 4.2.10 1/6, and 4.2.10 1/4.

[andrejbauer]

But we do not know ahead of time how many theorems will appear between 4.2.10 and 4.2.11. So we really do need to mark theorems so that we can tell in what order they were added.

[mikeshulman]

I meant "if adding n theorems at one time" in the third bullet point.

[andrejbauer]

Farey sequence seems better.

So in your scheme the theorems would be tagged with a "generation"?

[mikeshulman]

Better than what?

As for "generations", well sort of, but not exactly. E.g. if we add one theorem in between 4.2.10 and 4.2.11, and then another one in between 4.2.10 and 4.2.10½, and then another one in between 4.2.10½ and 4.2.11, the resulting sequence of numbers would be indistinguishable from if we added three theorems at once in between 4.2.10 and 4.2.11.

I feel like we are talking past each other about something. I'm not proposing that TeX can automatically calculate these fractions, although I suppose it would be possible -- I was just proposing a way for us to decide canonically on what fractions to give to the newthm command.

[andrejbauer]

Yes, we were talking past each other. I suppose people might find it cute to insert 4.2.10⅛ because it was "just a corollary of 4.2.10".