The Worm Calculus

Abstract

We present a propositional modal logic WC, which includes a logical verum constant ⊤ but does not have any propositional variables. Furthermore, the only connectives in the language of WC are consistency-operators ⟨α⟩ for each ordinal α. As such, we end up with a class-size logic. However, for all practical purposes, we can consider restrictions of 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 WC are all of the form A ⊢ B for worms A and B. The main result of the paper says that the well-known strictly positive logic RC, called Reflection Calculus, is a conservative extension of WC. As such, our result is important since it is the ultimate step in stripping spurious complexity off the polymodal provability logic GLP, as far as applications to ordinal analyses are concerned. Indeed, it may come as a surprise that a logic as weak as WC serves the purpose of computing something as technically involved as the proof theoretical ordinals of formal mathematical theories.

Keywords

Provability logic, strictly positive logics, closed fragment, feasible fragments, Reflection Calculus, ordinal notations

Citation

de Almeida Borges, A. & Joosten, J. J. (2018). Bezhanishvili, G., D'Agostino, G., Metcalfe, G., & Studer, T. (Eds.). The Worm Calculus. Advances in Modal Logic 12 (pp. 13–27). College Publications. URL: http://www.aiml.net/volumes/volume12/deAlmeidaBorges-Joosten.pdf

@InProceedings{AlmeidaBorges_Joosten2018_WormCalculus,
  author = "{de Almeida Borges}, Ana and Joosten, Joost J.",
  editor = "Bezhanishvili, Guram and D'Agostino, Giovanna and Metcalfe, George and Studer, Thomas",
  title = "The {W}orm {C}alculus",
  booktitle = "Advances in Modal Logic 12",
  year = "2018",
  pages = "13--27",
  publisher = "College Publications",
  url = "http://www.aiml.net/volumes/volume12/deAlmeidaBorges-Joosten.pdf",
  keywords = "Provability logic, strictly positive logics, closed fragment, feasible fragments, Reflection Calculus, ordinal notations",
  abstract = "We present a propositional modal logic WC, which includes a logical verum constant ⊤ but does not have any propositional variables. Furthermore, the only connectives in the language of WC are consistency-operators ⟨α⟩ for each ordinal α. As such, we end up with a class-size logic. However, for all practical purposes, we can consider restrictions of 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 WC are all of the form A ⊢ B for worms A and B. The main result of the paper says that the well-known strictly positive logic RC, called Reflection Calculus, is a conservative extension of WC. As such, our result is important since it is the ultimate step in stripping spurious complexity off the polymodal provability logic GLP, as far as applications to ordinal analyses are concerned. Indeed, it may come as a surprise that a logic as weak as WC serves the purpose of computing something as technically involved as the proof theoretical ordinals of formal mathematical theories."
}