The Worm Calculus

Abstract

We present a propositional modal logic $\sf WC$, which includes a logical $verum$ constant $\top$ but does not have any propositional variables. Furthermore, the only connectives in the language of $\sf WC$ are consistency-operators $\langle α\rangle$ for each ordinal $α$. As such, we end up with a class-size logic. However, for all practical purposes, we can consider restrictions of $\sf WC$ up to a given ordinal. Given the restrictive signature of the language, the only formulas are iterated consistency statements, which are called worms. The theorems of $\sf WC$ are all of the form $A \vdash B$ for worms $A$ and $B$. The main result of the paper says that the well-known strictly positive logic $\sf RC$, called Reflection Calculus, is a conservative extension of $\sf WC$. As such, our result is important since it is the ultimate step in stripping spurious complexity off the polymodal provability logic $\sf{GLP}$, as far as applications to ordinal analyses are concerned. Indeed, it may come as a surprise that a logic as weak as $\sf WC$ serves the purpose of computing something as technically involved as the proof theoretical ordinals of formal mathematical theories.