TL;DR: Dag Normann and I have obtained LOTS of equivalences between the second-order Big Five of Reverse Mathematics and third-order theorems from mainstream analysis about (possibly) discontinuous functions, working in Kohlenbach’s higher-order Reverse Mathematics. We also show that slight generalisations or variations of the aforementioned third-order theorems fall FAR outside of the Big Five. Our…
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…
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…