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?
Linear inferences of size 7
In Anupam’s recent post, he introduced the linear inferences switch and medial. By computational search it had been shown that all linear inferences with 6 or fewer variables are derivable from these two inferences. He also gave an 8 variable linear inference which is not derivable from switch and medial and posed the question of…