{
  "id": "1803.10543",
  "version": "v2",
  "published": "2018-03-28T11:45:33.000Z",
  "updated": "2019-06-18T16:47:08.000Z",
  "title": "The Worm Calculus",
  "authors": [
    "Ana de Almeida Borges",
    "Joost J. Joosten"
  ],
  "journal": "Advances in Modal Logic 12 (2018) 13-27",
  "categories": [
    "math.LO"
  ],
  "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.",
  "revisions": [
    {
      "version": "v2",
      "updated": "2019-06-18T16:47:08.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "worm calculus",
      "propositional modal logic",
      "polymodal provability logic",
      "propositional variables",
      "iterated consistency statements"
    ],
    "tags": [
      "journal article"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}