# Are mathematical objects a type according to type-theory?

I've been thinking about mathematical objects as a metaphysical trope, and the idea of them existing as a type has a few issues for me.

Mainly the response to this question is similar to what I've been looking at, but I have a few questions based on this.

Why can unique mathematical objects have "copies" or exist in multiples? (PhilSE)

Mainly, how do we perform operations on 'types' and how does this differ from the 'instances' and 'concepts'.

• This question needs to be more carefully thought out and re-written. I have no idea what you think a type is or why two types couldn't be added, or why you think "the 'object' is a type" or why you think we need to push concepts in between types and objects. In logic, a type is usually viewed as a set or class, but as far as I know, no one says "mathematical objects are a type". Commented May 3, 2022 at 15:36
• @DavidGudeman doesn’t type theory say so? It is an alternative foundation to mathematics than set theory. If realists can say and mean numbers are sets in some platonic sense, can’t a type realist say the same about types? Commented May 3, 2022 at 15:42
• @JKusin, I've always found type theories ugly so I haven't spent a lot of time on them, but I believe that depending on what type theory you mean, types might be syntactic objects or sets or classes of sets/functions/predicates. If types are sets, then sets can be used to represent numbers, and in that usage they can be added. But beyond that, a type theory that classes all mathematical objects as one type would be trivial, so I don't think the question was about type theory. Commented May 3, 2022 at 15:51
• I think the best way to understand this is that there exists objects and 'references' which can belong to types, but it's something I've heard about treating numbers as 'tropes' and types that instances belong to. Commented May 3, 2022 at 18:47
• @DavidGudeman my issue with why we can't add types is do we add the 'types' or the instance? I'm just trying to understand things I have learnt where people talk about instantiating mathematical objects. Commented May 3, 2022 at 18:49

Only if one wants to simulate mathematical objects with software. To philosophers, mathematical objects are not a species of type, rather types are a species of mathematical object in the same way sets are species of mathematical objects. But to a software engineer, to claim that mathematical objects are data types is a perfectly sensible claim. A computer scientist can then turn around and create a data model and write a program and use primitive types of the language to design a data model and instantiate objects that represent mathematical objects. Doing so well is usually called a computer algebra system. Thus, a mathematical object can be implemented as an extended data type on a system of primitive types which can be considered philosophically to be mathematical objects themselves. Reread that last sentence because it's a bit trippy.

Given the criticism from philosophical novices not familiar with types, type theory is essentially an evolved form of set theory originally crafted to avoid Russell's paradox which was quite the inconvenient hiccup in theory at the beginning of the 20th century. This is done by defining differences among the objects involved and setting restrictions on their relations. The short version is that when you let a mathematical set contain itself, all philosophical hell breaks loose. By differentiating sets as types, and then placing restrictions on types, then sets and elements in the traditional sense can be easier to use pragmatically. So much more pragmatically that modern programming languages and compilers express philosophies on the use of type theory often defined by BNF to describe relations between objects.

What prefigures an understanding of this answer is that this philosophical analysis is predicated in a largely mathematically constructivist fashion. This means that mathematical 'objects' are not so much disembodied, Platonic entities, that are metaphysically presupposed to have some objective existence, but rather are constructions of language subject to truth-conditional rules themselves constructed out of language.

From a nominalist position, if tokens are compared, it is imperative to understand the relation between them in what in computer science is often called a schema in the data community. Type theory provides a mathematical characterization that serves as the basis for data models such as ERMs and techniques for mapping them such as ORM much in the way relational algebra serves as a basis for query languages. But all of this is based on an implicit understanding about the relations that inhere to a set of tokens which in philosophy brings to mind the dichotomy of the type and the token.

Once one has a software system that has a compiler, one can simply choose to implement a data model of mathematical objects and define their types with primitive types! So, I think it's fair to say that most philosophers would consider the claim 'a type is a species of mathematical object' metaphysically a necessity, but the claim 'a mathematical object is a species of type (in the context of a software construct)' a contingent claim.

How does one perform operations on types? I will create a partial answer:

(a): first, there are many type theories. So, lets fix one, perhaps Martin- Lof's. So we gain access to, say, function types, unit types, finite types, etc. I will take for granted that these are mathematical objects- literally objects studied by mathematicians. They may not be under your preferred definition of mathematical object.

(b) Now say that we wish to perform an operation on a type. It is a rule of Martin Lof's type theory that if A is a type under context Gamma, and B is a type under context Delta, then A X B is a type under context Gamma, Delta. So we have just performed an operation on types, namely we have constructed the product type. One more example: lets take the naturals to be a type, and bool to be a type. We can construct an object- the "even" predicate- that takes all evens to true, and all odds to false. Such a predicate has type Nat -> bool. So, in some sense, we have just created a new type. So we perform operations on types just like we perform other operations in math- according to the rules.

(c): Further, by Curry Howard isomorphism, propositions are types. In fact, a proof object of some proposition P- perhaps the paradigmatic instance of a mathematical object, is a term of type P. So mathematical objects may be types or they may be terms with a type in a given type theory. It is is also possible that mathematical objects cannot be constructed- consider the propostion False.

(d): OP has noted that none of this answers the question of mathematical objects as a metaphysical trope, nor as instances, nor as concepts- all of which are distinct. No doubt there is an answer, however, it will likely not be mathematical- since tropes and concepts at least, are not studied by mathematicians. For other readers, note that type theory as above is not about the distinction between types and tokens, either.

• *but how do we get those rules? well, we wish to avoid circularity, so we construct an ascending chain of universes, such that types cannot range over themselves. we wish to be able to to harness the computational power of decidability, so we add in the notion of bools. Etc... Commented May 6, 2022 at 16:49