Moving focusing proof systems to arithmetic

Encadrement :

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

Description du sujet

The logic MALL (multiplicative additive linear logic) is an elegant, small logic for which provability is decidable. Girard extended MALL to a fully expressive and undecidable logic by adding the exponentials (!, ?). While this approach to logic has been successful and broadly employed, there are reasons to look elsewhere for means to extend MALL. In particular, Baelde (2012) recently studied the addition of least and greatest fixed points to MALL and developed numerous aspects of its proof theory.

This internship is proposed in order to investigate the proof theory of fixed points within intuitionistic and classical logics. While Baelde's paper starts this exploration, more can be done.

  1. The LKU proof system of Liang & Miller (2011) provides a single framework for specifying focused proof systems (and their cut-elimination theorems) for classical logic, intuitionistic logic, and MALL. This framework is currently playing an important role in the ProofCert project within the Parsifal team at INRIA-Saclay. This internship should propose how to integrate least and greatest fixed points into the LKU framework with the hope of respecting and unifying the previous results involving fixed points and proof theory.
  2. There should be a number of ways to apply the proof theory of fixed points the theory of arithmetic in both a classical setting (Peano arithmetic) and an intuitionistic setting (Heyting arithmetic). For example, focusing proof system come equipped with a polarization of connectives. A formula that is a purely positive fixed point expression is related to a number of notions in arithmetic. For example, a recursively enumerable predicate can be shown to coincide exactly to a predicate defined using such an expression. The existence of a decidable predicate provides a version of the excluded middle that is again a purely positive fixed point expression. The special class of Σ01 in the arithmetical hierarchy of formulas is again exactly those formulas in classical logic that can be polarized purely positively.
  3. Several other connections between focusing and computation should be possible. One particular concept that should be interesting applications to theorem proving and model checking is likely to be the following: Assume P(x) is a predicate of one argument for which it has already been proved that the set { x | P(x) } is a singleton. It is then the case that the "positive" formula [ ∃ x. P(x) ∧ Q(x) ] is equivalent to the "negative" formula [ ∀ x. P(x) ⊃ Q(x) ]. Such an ability to shift polarization flexibly should impact the design and application of proof search mechanisms. Such singleton predicates appear every time a predicate is used to encode a function.

This internship can be expanded into a PhD topic by developing various of the research avenues described in the ProofCert proposal. The possible applications of this topic are broad: they range from providing a proof theory for constructive and classical arithmetic to providing a framework for mixing model checking and inductive theorem proving: see Miller (2011, 2012).


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

[Baelde 2012]
Least and greatest fixed points in linear logic by David Baelde. ACM Trans. on Computational Logic, 13(1), 2012. (doi, pdf).
[Liang & Miller, 2011]
A Focused Approach to Combining Logics by Chuck Liang and Dale Miller. Annals of Pure and Applied Logic, 162(9), 2011. (doi, pdf).
[Miller 2011]
Communicating and trusting proofs: The case for foundational proof certificates by Dale Miller. To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science in Nancy, France, 19-26 July 2011. Draft dated 23 July 2012: pdf.
[Miller 2012]
A proposal for broad spectrum proof certificates by Dale Miller. CPP 2011: First International Conference on Certified Proofs and Programs, 7-9 December 2011, Taiwan. Draft dated 30 October 2011: (pdf). Slides: pdf. See also the description of the panel on Communicating and trusting proofs held during this meeting.
[Troelstra 1973]
Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, A. S. Troelstra, Lecture Notes in Mathematics 344, 1973.

Dale Miller