Research Project
Reverse Mathematics in Dependent Type Theory
Robin Adams
Dept of Computer Science
Royal Holloway, University of London
EPSRC Post-Doctoral Fellowship (Dec. 2006 - Nov. 2009)
Grant ref. EP/D066638
Abstract of the project proposal
It has been known for over a century that it is possible in principle
to build a machine that would check whether a proof of a mathematical
theorem is correct, if that proof is written in a language designed
for the task, called a language of formal logic (or sometimes system
or theory of formal logic). The study of these languages is the field
of mathematics called mathematical logic. Nowadays, it is possible in
practice. There are several computer programs, called proof checkers,
that check whether a proof written in a particular logical system is
correct. These have proven useful both to research mathematicians, and
to computer scientists for reasoning about programs, when it is
desired to have a proof that a given program has a certain property,
and a cast-iron guarantee that the proof is correct.
Proof checkers
based on the family of systems of formal logic known as dependent type
theories have proven very successful, particularly for these computer
science applications. However, dependent type theory has so far only
been successfully applied to constructive mathematics - a school of
thought in the philosophy of mathematics that rejects many methods of
proof that are accepted in classical mathematics, the practice of
mathematics followed by the mainstream mathematical
community. Constructive mathematics, or constructivism, is only one of
a number of alternatives to classical mathematics. Many such
foundations for mathematics have been proposed, going by such weird
and wonderful names as predicativism, finitism and
ultraintuitionism.
There is a project of research in mathematical
logic called Reverse Mathematics that has conducted an extremely
detailed analysis of several theories of logic of the kind known as
second-order logics, many of which correspond closely to some
foundational scheme in mathematics. This programme has been very
succesful, revealing unsuspected connections between the foundational
schemes, and helping to make more precise what is meant by the
strength of a mathematical theorem.
It is our opinion that Reverse
Mathematics has been hampered by this concentration on second-order
logic. Second-order logic can only talk about two types of
mathematical object: natural numbers, and sets of natural numbers. To
handle other objects, researchers in Reverse Mathematics must pretend
that certain natural numbers are disguised (they prefer the word
'coded'). This is not always possible, and it is often inconvenient
when it is possible. Type theory, in contrast, as its name suggests,
is designed to handle a variety of different types of mathematical
object. We believe it is time for dependent type theory to be applied
outside constructive mathematics, and for Reverse Mathematics to have
a second string to its bow. We therefore feel it is time that these
two strands of research were brought together. We propose to carry out
a programme similar to Reverse Mathematics in dependent type
theory. We shall use Peter Aczel's recent concept of a logic-enriched
type theory: a type theory in which the mechanism for representing
mathematical objects, and the mechanism for reasoning about those
objects, are rigidly separated. It is therefore possible to change the
logic to be classical, predicative, or what you will, without changing
the collection of objects about which one can speak.
We propose to
construct a number of different logic-enriched type theories
corresponding to different foundational schemes in mathematics, and to
investigate which proofs can be formalised within each. We shall adapt
an existing general-purpose proof checker to implement these
theories. We hope that this shall both reveal connections between the
foundational systems of mathematics that are not apparent in Reverse
Mathematics, and be a large step towards the construction of a proof
checker that retains all the strengths of dependent type theory, but
can accept non-constructive proofs.