Homotopical inductive types
Lead Research Organisation:
University of Leeds
Department Name: Pure Mathematics
Abstract
Over the past few years, new surprising connections have emerged between two traditionally distant areas of mathematics: mathematical logic (which is generally concerned with the study of the forms of reasoning used in mathematics) and homotopy theory (which is interested in understanding and classifying various notions of space). These connections are useful because they provide a clear
geometric intuition that helps us to work with a class of logical systems, known as type theories. On that basis, the Fields medallist Vladimir Voevodsky has formulated an ambitious research programme, called the Univalent Foundations of Mathematics programme, that seeks to develop a new foundations of mathematics on the basis of type theories that include new axioms motivated by homotopy theory.
The proposed research seeks to advance our understanding of the type theories proposed by Voevodsky in order to develop the Univalent Foundations programme. Our first goal is to understand better the relationship between the type theories introduced by Voevodsky and axiomatic set theories, which represent the more traditional approach to foundations of mathematics. In particular, we want to clarify the logical status of the Univalence Axiom, a new axiom which allows us to treat objects that share all structural properties as equal. Furthermore, we wish to gain further insight into a variation, again motivated by homotopy theory, over the standard way of defining types.
geometric intuition that helps us to work with a class of logical systems, known as type theories. On that basis, the Fields medallist Vladimir Voevodsky has formulated an ambitious research programme, called the Univalent Foundations of Mathematics programme, that seeks to develop a new foundations of mathematics on the basis of type theories that include new axioms motivated by homotopy theory.
The proposed research seeks to advance our understanding of the type theories proposed by Voevodsky in order to develop the Univalent Foundations programme. Our first goal is to understand better the relationship between the type theories introduced by Voevodsky and axiomatic set theories, which represent the more traditional approach to foundations of mathematics. In particular, we want to clarify the logical status of the Univalence Axiom, a new axiom which allows us to treat objects that share all structural properties as equal. Furthermore, we wish to gain further insight into a variation, again motivated by homotopy theory, over the standard way of defining types.
Planned Impact
The modern world relies in an essential way on computer systems to run important tasks in a variety of areas: from finance and medicine to transport and energy. When computer systems are used in safety-critical applications (such as controlling the functioning of a nuclear power station or coordinating the signal system of a train network), it is essential that their correctness is established without doubt, and not merely indicated by tests.
One successful approach to the verification of software correctness has been to develop integrated software systems, known as proof assistants, in which it is possible to write computer programs, specify requirements, and formally prove that these requirements hold. Thus, these systems give us a way of creating correct-by-construction programs, which is beneficial also in economic terms since it eliminates the difficult process of debugging. The development of proof assistants involved a combination of ideas of mathematical logic and computer science, in a way that is reminiscent of the very origin of computer programming. Indeed, proof assistants are also used in the formalisation of mathematical proofs, so as to guarantee their correctness.
The proposed research focuses on logical systems, known as type theories, which are at the core of some of the most powerful proof assistants (such as the Coq system). In particular, we seek to advance our understanding of a new class of type theories which have been recently formulated by the Fields medallist Vladimir Voevodsky, thanks to the discovery of surprising connections between
mathematical logic and homotopy theory (an area of mathematics that studies general notions of space).
Our proposed research will benefit directly the academic communities working in mathematical logic, homotopy theory and higher-dimensional category theory by improving our understanding of this new class of type theories and of the connections between these subjects. Our work is likely to impact also the ongoing design of new proof assistants based on these new type theories, since it aims to obtain precise information on their expressive power. These new proof assistants, in turn, will benefit society in general by facilitating the creation of correct-by-construction computer programs.
One successful approach to the verification of software correctness has been to develop integrated software systems, known as proof assistants, in which it is possible to write computer programs, specify requirements, and formally prove that these requirements hold. Thus, these systems give us a way of creating correct-by-construction programs, which is beneficial also in economic terms since it eliminates the difficult process of debugging. The development of proof assistants involved a combination of ideas of mathematical logic and computer science, in a way that is reminiscent of the very origin of computer programming. Indeed, proof assistants are also used in the formalisation of mathematical proofs, so as to guarantee their correctness.
The proposed research focuses on logical systems, known as type theories, which are at the core of some of the most powerful proof assistants (such as the Coq system). In particular, we seek to advance our understanding of a new class of type theories which have been recently formulated by the Fields medallist Vladimir Voevodsky, thanks to the discovery of surprising connections between
mathematical logic and homotopy theory (an area of mathematics that studies general notions of space).
Our proposed research will benefit directly the academic communities working in mathematical logic, homotopy theory and higher-dimensional category theory by improving our understanding of this new class of type theories and of the connections between these subjects. Our work is likely to impact also the ongoing design of new proof assistants based on these new type theories, since it aims to obtain precise information on their expressive power. These new proof assistants, in turn, will benefit society in general by facilitating the creation of correct-by-construction computer programs.
Organisations
People |
ORCID iD |
Michael Rathjen (Principal Investigator) | |
Nicola Gambino (Researcher) |
Publications
Cook J
(2016)
Advances in Proof Theory
Cook J
(2016)
Classifying the Provably Total set Functions of KP and KP(P)
in The IfCoLog Journal of Logics and their Applications
Dihoum E
(2019)
Preservation of choice principles under realizability
in Logic Journal of the IGPL
Gambino N
(2017)
On operads, bimodules and analytic functors
in Memoirs of the American Mathematical
Society
Gambino Nicola
(2014)
On operads, bimodules and analytic functors
in arXiv e-prints
RATHJEN M
(2021)
LIFSCHITZ REALIZABILITY AS A TOPOLOGICAL CONSTRUCTION
in The Journal of Symbolic Logic
Rathjen M
(2016)
Concepts of Proof in Mathematics, Philosophy, and Computer Science
Rathjen M
(2016)
Proof Theory of Constructive Systems: Inductive Types and Univalence
Rathjen M
(2017)
Feferman on Foundations
Rathjen M
(2019)
The scope of Feferman's semi-intuitionistic set theories and his second conjecture
in Indagationes Mathematicae
Rathjen M
(2018)
Lifschitz Realizability as a Topological Construction
RATHJEN M
(2016)
INDEFINITENESS IN SEMI-INTUITIONISTIC SET THEORIES: ON A CONJECTURE OF FEFERMAN
in The Journal of Symbolic Logic
Rathjen M
(2016)
Remarks on Barr's theorem: Proofs in geometric theories
Rathjen M
(2017)
Long Sequences of Descending Theories and other Miscellenia on Slow Consistency
in IfCoLog Journal of Logics and their Applications
Rathjen M
(2020)
Power Kripke-Platek set theory and the axiom of choice
in Journal of Logic and Computation
Rathjen Michael
(2014)
Indefiniteness in semi-intuitionistic set theories: On a conjecture of Feferman
in arXiv e-prints
Swan A
(2016)
An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof
in Journal ofLogic & Analysis
Van Der Meeren J
(2014)
Well-partial-orderings and the big Veblen number
in Archive for Mathematical Logic
Description | We have developed technical tools for dealing with infinitary intuitionistic derivations and extracting computational information from them in the presence of strong axioms such as Powerset and Exponentiation and used them to determine the strength of type theories with the type of propositions. We also proved several of Feferman's conjectures pertaining to the indeterminacy of iconic set-theoretic statements in semi-intuitionistic set theories. |
Exploitation Route | They will provide answers concerning the strength of current proof assistants. |
Sectors | Creative Economy |
Description | Results about the indefinitness of the continuum problem in semi-intuitionistic set theories have stirred a lot of interest in set theory and the philosophy of mathematics. |
First Year Of Impact | 2014 |
Sector | Other |
Impact Types | Cultural |
Description | A new dawn of intuitionism |
Amount | $743,694 (USD) |
Organisation | The John Templeton Foundation |
Sector | Academic/University |
Country | United States |
Start | 12/2017 |
End | 08/2020 |