Florence Clerc was an intern with the Parsifal team during summer 2012. On Friday, November 30 at 10:00 she will speak at the Deducteam seminar in room Verte 1 at INRIA, 23 avenue d’Italie (metro place d’Italie) on the 5th floor.
Embedding constructiveness into classical logic via double negation translations or polarization
Florence Clerc (INRIA and LIX, Ecole polytechnique)
Abstract: Although originally developed as a tool for proving the consistency of classical logic with respect to constructive reasoning, double negation translations have recently been used to embed classical reasoning into intuitionistic proofs. Such translations can then be used to associate constructive functions to classical proofs. In this paper, we show that if we pick a particular double negation translation from a set of known translations, it is possible to establish an isomorphism between the cut free classical sequent proofs of formula B and the intuitionistic sequent calculus proofs of the translation of B. In order to get such a strong correspondence of proofs, this isomorphism is constructed between focused sequent proofs in these two logics. Using the LJF and LKF focused proof systems of Liang & Miller (2009), we can show that focused cut-free classical proofs of a certain polarization of B are isomorphic to a certain double negation translation. In particular, we describe the polarization of classical proofs needed to exactly model the Kuroda translation.
