The Worm Calculus
Ana de Almeida Borges, Joost J. Joosten

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 , which includes a logical constant but does not have any propositional variables. Furthermore, the only connectives in the language of 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 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 are all of the form for worms and . The main result of the paper says that the well-known strictly positive logic , called Reflection Calculus, is a conservative extension of . As such, our result is important since it is the ultimate step in stripping spurious complexity off…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Semantic Web and Ontologies · Logic, programming, and type systems
