Computational isomorphisms in classical logic

Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx

Research output: Contribution to journalArticlepeer-review

Abstract

All standard ‘linear’ boolean equations are shown to be computationally realized within a suitable classical sequent calculus . Specifically, 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.
Original languageEnglish
Pages (from-to)353 - 378
Number of pages26
JournalTheoretical Computer Science
Volume294
Issue number3
DOIs
Publication statusPublished - Feb 2003

Keywords

  • Classical logic
  • Proof theory
  • Linear logic

Fingerprint Dive into the research topics of 'Computational isomorphisms in classical logic'. Together they form a unique fingerprint.

Cite this