I am thrilled to announce that my theorem has been confirmed via proof by induction and proof by rippling at the University of Edinburgh. Per the long-standing tradition in mathematics that the author of a new theorem has the authority to name it, I have recorded my theorem as “The Thompson Postulate.”
Thank you, thank you. It is a great honor and I promise that although I now join the ranks of other great minds like, Gauss, Fermat and Pythagoras, I won’t let it go to my head.
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. The axioms used in my theory were 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.
Coming up with a mathematical theory isn’t that hard – people do it every day. It’s proving the theory that is challenging. My theory was proved two ways. The first was proof by induction. A proof by induction is just like an ordinary proof in which every step must be justified. However it employs a neat trick which allows you to prove a statement about an arbitrary number n by first proving it is true when n is 1 and then assuming it is true for n=k and showing it is true for n=k+1. The idea is that if you want to show that someone can climb to the nth floor of a fire escape, you need only show that you can climb the ladder up to the fire escape (n=1) and then show that you know how to climb the stairs from any level of the fire escape (n=k) to the next level (n=k+1).
The second was proof by rippling. Rippling refers to a group of meta-level heuristics, developed primarily in the Mathematical Reasoning Group in the School of Informatics at the University of Edinburgh and most commonly used to guide inductive proofs in automated theorem proving systems. Rippling may be viewed as a restricted form of rewrite system, where special object level annotations are used to ensure fertilization upon the completion of rewriting, with a measure decreasing requirement ensuring termination for any set of rewrite rules and expression.
The challenge in developing a theorem is to assure that the theorem is not trivially true, which mine is not. There are two senses in which my theorem is not trivially true. Firstly, note that some mathematical theories are inconsistent i.e. the axioms contradict each other. In such theories all formulae are theorems, which is clearly undesirable. However, it is a well-established mathematical result that theories consisting only of recursive definitions are inherently consistent. So my theorem is not trivial in this sense. The second sense in which my theorem is not trivially true is that it cannot be directly derived by a simple calculation. In particular, it is not true by simple rewriting from other known theorems.
Now, I probably need to right-size expectations by saying that my theorem will not earn me the Fields Medal (it’s the Nobel Prize of math), but it’s interesting to me and technically speaking, the notion of interesting initially developed in Conjecture Synthesis for Inductive Theories (Journal of Automated Reasoning) which was then further developed in Scheme-Based Synthesis of Inductive Theories (LNCS, Volume 6437) ensures that standard orderings, using known theorems as rewrites, cannot prove the new theorem: that there is no direct symbolic calculational proof of the new theorem (hence, interesting).
So, with no further ado, I present (the quite official) The Thompson Postulate:
Let
T3 = Cf(T3, ℕ) | Ce(Bool, ℕ)
T12 = Cv(T12) | Cu(Bool, Bool)
fια : T3 × T12 → T3
fια(Ce(x, y), z) = Ce(x, y)
fια(Cf(x, y), z) = Cf(fια(x, z), y)
then
fια(x, y) = x
# # #
bloomfield knoble creates marketing plans, strategy, creative design, collateral, Power Point presentations, email templates, videos, audio, music videos, television commercials, letterhead, identity, gift cards, SWOT analyses, brochures, letter templates, software applications, web applications, multimedia productions, Flash content, streaming videos, logo designs, widgets, technical consulting.