Computational isomorphisms in classical logic
Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx · Electronic Notes in Theoretical Computer Science · 1996
We prove that any pair of derivations, without structural rules, of F ⊢ G and G ⊢ F, where F, G are first-order formulas ‘without any qualities’, in a constrained classical sequent calculus LKηp, define 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 satisfied.