Computational Isomorphisms in Classical Logic

We prove that any pair of derivations, without structural rules, of F ) G and G ) F , where F , G are rst-order formulas `without any qualities', in a constrained classical sequent calculus LK p , denes a computational isomorphism up to an equivalence on derivations based upon reversibility properties of logical rules. This result gives a rationale behind the success of Girard's denotational semantics for classical logic, in which all standard `linear' boolean equations are satised. 1 Introduction 1.1 A patch of paradise to be broadened In recent work [1] devoted to the proof theory of classical logic, we embarked on the project of overcoming the obstacles that prevent cut from being a decent binary operation on the set of classical sequent derivations. To clarify what we mean by decency, let us have a look at the world of simply typed -calculus, which, seen from a normalization-as-computation point of view, is something close to a patch of paradise. danos@logique..