| EPSRC Reference: |
EP/D066638/1 |
| Title: |
Reverse Mathematics in Dependent Type Theory |
| Principal Investigator: |
Adams, Dr R |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Royal Holloway, Univ of London |
| Scheme: |
Postdoc Research Fellowship |
| Starts: |
16 October 2006 |
Ends: |
15 October 2009 |
Value (£): |
225,677
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Logic & Combinatorics |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
17 Feb 2006
|
PDRF - Theoretical Computer Science
|
Deferred
|
|
|
Summary on Grant Application Form |
|
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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
|