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…
Tag: sequent calculus
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…
Checking proofs with very low complexity
The very notion of mathematical proof is founded upon the idea that a proof is ‘routine’ to check. While it may be difficult to actually prove a mathematical theorem, a proof should allow us to verify its truth . But exactly how much effort is required to check a proof, in terms of computational complexity?…
