## Relating double-negation translations and focused proof systems

### Encadrement :

Dale Miller, Parsifal team, INRIA-Saclay and LIX/Ecole Polytechnique

### Description du sujet

Double negation translations are means of embedding first-order classical logic into first-order intuitionistic logic. There are many such translations: for an overview, see [FO10]. Such translations have a number of important uses in proof theory [A04] and in programming language theory and implementation (eg, via continuation-passing style translations).

Such translations can be used as a way to provide some constructive content to classical logic proofs. In recent years, another way to approach the possible constructive content of classical logic is via *focused proof systems* for classical logic. A comprehensive and simple approach to focused proofs in classical logic is given by the LKF proof system in [LM09]. In order to use a focused proof system, one must first *polarize* the classical logic formula. There are a great many ways to do such polarization and the allowed proofs in the resulting focused proofs can vary a great deal.

The goal of this internship is to develop a tight relationship between the choices in polarization in LKF and the choices in designing a double negation translation. We search for a means of using LKF to provide a rationale for the design of double negation translation and to provide a uniform proof of their correctness.

It should be possible to continue this work as a PhD student particularly along the line of developing the proof theory of a merging of classical and intuitionistic logic as described in [LM11]. This internship will take place within the funding context of the **ProofCert** project, a recently accepted ERC Advanced Investigator Award. This five year project (2012-2016) provides funding for PhD students covering a broad range to topics in a foundational approach to *proof certificates*.

### Bibliography

The following bibliography is indicative of the kind of papers that will be part of this research effort.

- [A04]
**Forcing in proof theory**by Jeremy Avigad. Bulletin of Symbolic Logic 10(3): 305-333 (2004): pdf.- [FO10]
**On various negative translations**by Gilda Ferreira and Paulo Oliva. Proceedings of Classical Logic and Computation, 2010: pdf.- [LM09]
**Focusing and Polarization in Linear, Intuitionistic, and Classical Logic**by Chuck Liang and Dale Miller.*Theoretical Computer Science*, 410(46), pp. 4747-4768 (2009): doi, pdf.- [LM11]
**Kripke Semantics and Sequent Calculus for Combining Classical and Intuitionistic Logics**by Chuck Liang and Dale Miller. Submitted. Draft dated 6 Oct 2011: pdf.