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:


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.