Connectives of linear logic are sometimes classified as canonical or not. This refers to the possibility (or not) to characterise a connective (up to logical equivalence) by means of its introduction rules. The standard claim is that all linear-logic connectives, but the exponential ones, are canonical. We want to stress that this claim strongly depends, not only on linear logic itself, but on the way rules are constructed. This means in particular that canonicity is not an intrinsic property of connectives but depends on how they are presented: canonicity is not canonical…
Tag: sequent calculus
Notation for focused proof systems
Standardized notation can be helpful, especially after a topic has matured. For example, Gentzen used as an infix symbol to build sequents from lists of formulas. While one also sees used, it seems that in recent years, has become the standard, especially when proof theory is applied to type theory (where is invariably used) and…
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…
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…