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…
Category: Uncategorized
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…
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?
