|
| EPSRC Reference: |
GR/R95975/01 |
| Title: |
CATEGORICAL LOGIC AND PROOF THEORY: REALIZABILITY INTERPRETATIONS FOR CONSTRUCTIVE THEORIES |
| Principal Investigator: |
Dr N Gambino |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Pure Maths and Mathematical Statistics |
| Organisation: |
University of Cambridge |
| Scheme: |
Postdoctoral Research Fellowship |
| Starts: |
01 January 2003 |
Ends: |
31 December 2004 |
Value (£): |
66,191
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
20 Mar 2002
|
Maths Postdoctoral Sift March 2002
|
Deferred
|
|
|
Summary |
Realizability is a technique of proof theory. Its original version was obtained by defining a relation between natural numbers and sentences of arithmetic so that if a number and a sentence are related, then the former can be seen as a proof of the latter. Since then, realizability has been extensively developed and applied to the study of arithmetic and analysis. Recent developments in categorical logic generated a renewed interest in realizability interpretations.
The aim of the proposed research is to extend and apply realizability to a wide class of constructive theories. One reason for the interest in constructive theories is that proofs formalized in them are intended to have computational content. This is usually referred to as the proofs-as-algorithms principle. Realizability provides a means to make this idea mathematically precise. Remarkably, constructive theories are sufficiently expressive to formalize large parts of mathematics. On the whole, constructive theories can be formulated in different settings: set theory, type theory and category theory. Research both in Britain and elsewhere is actively focusing on relating constructive theories formulated in different settings.
The first main goal of the research is to obtain a general account of realizability interpretations using categorical logic. The second main goal is to apply realizability interpretations to obtain proof theoretic results.
|
| Final Report Summary |
Realizability is a technique of proof theory. Its original version was obtained by defining a relation between natural numbers and sentences of arithmetic so that if a number and a sentence are related, then the former can be seen as a proof of the latter. Since then, realizability has been extensively developed and applied to the study of arithmetic and analysis. Recent developments in categorical logic generated a renewed interest in realizability interpretations.
The aim of the proposed research is to extend and apply realizability to a wide class of constructive theories. One reason for the interest in constructive theories is that proofs formalized in them are intended to have computational content. This is usually referred to as the proofs-as-algorithms principle. Realizability provides a means to make this idea mathematically precise. Remarkably, constructive theories are sufficiently expressive to formalize large parts of mathematics. On the whole, constructive theories can be formulated in different settings: set theory, type theory and category theory. Research both in Britain and elsewhere is actively focusing on relating constructive theories formulated in different settings.
The first main goal of the research is to obtain a general account of realizability interpretations using categorical logic. The second main goal is to apply realizability interpretations to obtain proof theoretic results.
Summary of Outcomes
I investigated the interplay between two areas of pure mathematics, category theory and mathematical logic. Category theory allowed me to find an unexpected applications of the notion of 'species of structure' to mathematical logic.
|
| Further Information: |
www.lacim.ugam.ca |
| Organisation Website: |
http://www.cam.ac.uk |
|
|