Anne's First Theorem

Anne teaches mathematics, and our friend Grumio gave her this Christmas present:

He had it produced for Anne by TheoryMine, whose details are here (read the FAQs). A certificate of registry was provided guaranteeing that it is unique and provable, and that it has been recorded under her name in their database.

As most readers of OMF know, a theorem is a mathematical formula for which we have a proof. Both theorems and proofs are within a theory which consists of a set of axioms. A proof is a sequence of formulae, starting with some axioms and ending with the theorem. Each non-axiom formula in this sequence follows from the previous formulae in the sequence. All the axioms in TheoryMine theories are recursive definitions.

Recursion is a mathematical technique that is much used in computer programs. In a recursive definition, the value of a recursive function is defined in terms of values of the same function applied to smaller inputs. This sounds circular, but because the function's inputs get smaller and smaller the computation eventually stops. TheoryMine also uses recursion to define brand new types of input and output for each theory. These are called recursive data-structures.

But never mind about all that; theorems are abstract objects that are not subject to wear and tear. Even diamonds will be destroyed in the heat death of the universe; theorems won't be.

So what a splendid gift they make! No-one could doubt that they are a girl's best friend.