A post by Anupam and Sonia in 2022 ignited a surge of interest from the modal logic and proof theory communities: until then, it was commonly believed that different inuitionistic versions of modal logic agreed on their -free parts, but this turns out to be false. After 23 comments, 3 papers, 1 further blog post,…
Anupam Das
Exponentials vs fixed points in linear logic
It has been known for a while that the exponential modalities of linear logic may be simulated by least and greatest fixed point operators. However it is apparently not widely known whether this simulation was faithful. In this post we explain that this is not the case, using only first principles of linear logic.
Brouwer meets Kripke: constructivising modal logic
Intuitionistic logic and modal logic each admit meaningful projections of classical theories. While intuitionistic logic can interpret classical logic by a host of translations, thus yielding computational interpretations, modal logic can be employed to understand notions of provability and truth. However, the enrichment of intuitionistic logic by modalities is far less canonical than its classical…
Deterministic – nondeterministic pairs in proof theory
This is meant to be a light post, posing a perhaps naive question. One of the hallmarks of computational proof theory is the association between arithmetic theories and complexity classes, in terms of their provably recursive functions. But is there a general rule for identifying the provably recursive functions of a class of induction invariants?