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.
