Computational isomorphisms in classical logic

All standard ‘linear’ boolean equations are shown to be computationally realized within a suitable classical sequent calculus LK p η. Specifically, LK p η can be equipped with a cut-elimination compatible equivalence on derivations based upon reversibility properties of logical rules. So that any pair of derivations, without structural rules, of F⇒G and G⇒F, where F, G are first-order formulas ‘without any qualities’, defines a computational isomorphism.

Authors

• Vincent Danos
• Jean-Baptiste Joinet
• Harold Schellinx

Keywords

• Proof theory
• Linear logic
• Classical logic