Type Theories of Natural Numbers: A Study of Conservative Extension
Abstract
We present some possible definitions for what it means for a type theory to be a conservative extension over another type theory. We do so by giving two type theories of natural numbers: T T (N) and T T (N, ×). T T (N) is a type theory that comprises only the natural numbers as a type, while TT(N,×) is an extended theory of TT(N) that includes an additional type constructor that can form pair types. Our aim is to search for a general definition of a conservative extension. Our approach does not only involve judgements in our definition of conservativity, but also convertibility between terms, which corresponds to the process of computation for each type theory. Understanding type theories and their computation have valuable implications in research areas, such as in Computer Science, particular in the context of proof assistants and other fields where type theory is considered.
We prove that TT(N,×) is not a conservative extension over TT(N) in the strongest sense, by giving a counter example, but that it is a conservative extension in three other senses. We do this by defining a translation from TT(N,×) to TT(N), we define terms in TT(N) that will represent terms from TT(N,×), and therefore use the translation to prove conservativity.
Our contribution lies in providing a deeper understanding of the relationships between type theories, specifically focusing on type theories that are fragments of Martin-L ̈of type theory, where Martin-L ̈of type theory serves as an alternative foundation of mathematics. We argue why one of the notions of conservative extension, proposed in this thesis, is the most suitable definition to establish a conservative extension between T T (N) and T T (N, ×). From this notion of conservative extension, we discover that since they are conservative, they denote the same functions, specifically the primitive recursive functions. This motivates us to utilize this definition of conservative extension, because it provides the insight that if two theories are conservative, they denote the same functions. If this is the case in general between type theories then this deserves further research on our notions of conservativity, as it may be helpful for transferring theorems. This could serve as a new feature for proof assistants that are based on a type theory, with a particular focus on conservativity.
These findings prompt further questions: can these definitions of conservative extensions be regarded as a general definition within the context of type theory? Can these definitions be valuable in applications within type theory? Are there any significant implications that arise from conservative extensions in type theories overall? Having an understanding of conservative extensions and their implications has the potential to enhance our understanding of type theory.
Degree
Student essay
Collections
View/ Open
Date
2023-06-30Author
Babunovic´, Aleksandar
Keywords
Logic
Publication type
H2
Language
eng