Reverse Mathematics in Coq
This is a Korea-France research project on reverse
mathematics. It is part of the STAR Project sponsored by the National
Research Foundation on the Korean side and
Ministry of Foreign and European Affairs on the French side.
Besides two leaders of the project,
Gyesik Lee
on the Korean side and
Hugo
Herbelin
on the French side, more researchers are
involved, above all Laurent Bienvenu, Sungwoo Park, Keiko Nakata, and
some students.
The main goal of the research is to develop and implement formal
systems that support doing “reverse mathematics” in the proof
assistant Coq.
The program called “reverse mathematics” is a
foundation of mathematics that focuses on the analysis of the logical
force of the most standard mathematical theorems. The logical
framework in which mathematics is put down is one of the subsystems of
second-order arithmetic, including the so-called “big
five”: RCA0, WKL0,
ACA0, ATR0,
Π11-CA0.
The best reference is the book by
Stephen Simpson,
Subsystems of Second
Order Arithmetic.
On the other hand, the past 40 years have seen the link between logic
and computing, and more specifically between proofs and programs. The
link got
more intimate with the development of type theory by P. Martin-Löf in the course of
80 years which is both a logic system and a
programming language
and by the development of linear logic by J.-Y. Girard
whose associated concept of
polarity allows a detailed analysis of computational properties of the
basic concepts of mathematical logic.
The correspondence between proofs and programs has helped
to develop the software Coq which is one of the
most-used proof assistants in the formalization of mathematics
or
of specification of programming languages.
The logic of Coq
is a type theory called the Calculus of Inductive Constructions (CIC).
Since its introduction by H. Friedman in 1975, the research program of
reverse mathematics has been extremely productive.
It has in particular shown that the big five are sufficient
for the formalization of the majority of standard mathematical theorems.
However, the
framework remained that of classical logic.
Moreover, reverse mathematics
has confined itself to the language of arithmetic
which is not so efficient in practice.
One of the goals of our project is
to reformulate the languages
of reverse mathematics in a way that the new languages become both finer (thanks to analysis in
terms of polarization) and more useful in
practice (thanks to the use of concepts from type theorie such as
inductive types, dependent products).
The success of Coq in the history of the formalization of mathematics shows that the
goal is very natural.
Another goal is to integrate the new languages into Coq so that
it can serve the research on reverse mathematics.
We will then be able to provide a concrete framework which
any logician or mathematician interested in formalizing the results of
reverse mathematics can use.
Some concrete topics are as follows:
- giving a uniform view of the "big five"
- interpreting the "big five" subsystems as subsystems of Coq's
Calculus of Inductive Constructions
- studying the relations between Simpson's subsystem of second-order
arithmetic and Martin-Löf's type theory
- providing restricted versions of Coq that exactly express the
strength of the "big five"
- formalizing some proofs of Simpson's book in these versions of Coq
- understanding how conservation/absoluteness results adapt to proofs
(i.e. whether the size of proofs is changed)
A
workshop on reverse mathematics and Type Theory will be held
in the period of 25 ~ 29 March, 2013 in Seoul, Korea.
Everyone who is seriously interested in the subject of the workshop
is welcome to the meeting. Registration is required although there is no registration fee.
If you intend to attend the workshop, please send an email to
the local organizer including
full name, position, and affiliation.