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…
LK vs LJ: An origin story for linear logic
In his 1987 TCS paper [2], Girard credits semantic considerations related to coherent models as the origin of the key observation behind linear logic: the intuitionistic implication should be split into two connectives . To the extent that it makes sense to propose an alternative origin story for linear logic, it is interesting to note…
Confluence in the sequent calculus
In this blog post, we give an insight into the confluence of the sequent calculus, a property mainly considered since the discovery of the so-called Curry-Howard correspondence [1]. Confluence is often thought to be part of the well-understood folklore. For people already aware of the links between intuitionism and computation, it may feel natural and…
New results about logics using proof systems other than sequent calculus
Many new results and new insights about classical and non-classical logics have been obtained using the sequent calculus, e.g. Gentzen’s consistency argument; interpolation, decidability, complexity for modal and substructural logics; (what else?). I would like to identify new results and insights about logics that were obtained using proof systems—other than the sequent calculus—that utilised some…
