Computational isomorphisms in classical logic: (Extended Abstract)

Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Pages (from-to)183 - 195
Number of pages13
JournalElectronic Notes in Theoretical Computer Science
Volume3
DOIs
Publication statusPublished - 1996

Fingerprint

Dive into the research topics of 'Computational isomorphisms in classical logic: (Extended Abstract)'. Together they form a unique fingerprint.

Cite this