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.
-
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.
-
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.
-
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).
Bibliography
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