The Worm Calculus

TL;DR

This paper introduces the Worm Calculus, a propositional modal logic with a unique language of iterated consistency statements called worms, and shows it is a conservative extension of Reflection Calculus, simplifying the analysis of ordinal proof theories.

Contribution

It establishes that the weak Worm Calculus is a conservative extension of Reflection Calculus, aiding in simplifying ordinal analysis related to provability logic.

Findings

Worm Calculus is a conservative extension of Reflection Calculus.

The logic simplifies the complexity of polymodal provability logic.

It enables computation of proof-theoretic ordinals using a weak logic.

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 \alpha \rangle$ for each ordinal $\alpha$. 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.