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.
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 language | English |
---|---|
Pages (from-to) | 183 - 195 |
Number of pages | 13 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 3 |
DOIs | |
Publication status | Published - 1996 |