A calculus for worms

In 2012, Dashkov described a calculus used to reason about a strictly positive fragment of the language of GLP. The sequent-style presentation of this calculus proposed by Beklemishev is called the Reflection Calculus (RC). It is well-known that every closed formula of RC can be equivalently written as a worm. One wonders whether it would be possible to work only with worms, maintaining the same proof power available in RC. The answer is yes. We present a calculus for worms and show that it proves exactly the same conjunction-free closed statements as the Reflection Calculus. We are also currently extending the results to creatures more exotic than worms. Joint work with Joost Joosten.