Rigorous definition of a type

Question

What is a type in type theory? I tried to find a rigorous definition without luck. And that makes me wonder.. maybe there isn't any rigorous definition?

My aim is to see how homotopy type theory provides a foundation for mathematics. An attempt is given here. Despite the nice resources given there, however, I found that my problem was more basic than knowing what a homotopy type theory is. Rather, it's about type theory: I'm in search of a rigorous definition of type theory.

Now, since this question is close to the fundamentals.. I reckon that I might have to specify what I really need. First of, I know how the basics of type theory works. I know that a type is roughly a collection of things, called terms, whatever these means. I know there might be rules to tell if a given term is of a given type. I know there are types derived from predefined types.. etc. If you ask me to follow the rules and play the game, I think I won't have a problem. What bothers me is that I don't really know what a type is, whenever addressed.

So, really, what is a type? What is a term? What is a function? Are they fundamentally undefined?

My feeling is.. it's necessary to introduce the rules of the game we're playing if one has to more rigorously refine type. And to do that, deductive system and lambda calculus seem to be a must. To define a function, it seems that certain realistic or imaginary machine should be involded.. for example Turing machine. And are there other systems to be introduced, before defining rigorously what a type is? Also, a natural question then arises: can all these systems be rigorously defined?

Remark

I have to admit at the end that I might not fully understand what I'm asking. I know I'm in search of a full and rigorous definition of type.. but you might ask what I mean by "rigorous"? Well.. I don't know. How can I define "rigorous"? How can I define "define"? What is "what"? And what is "what is what"? ..? It might sound like I'm making fun of words, but I'm serious.

EDIT: Zhen Lin asked a great question in the comment, which helped me express my expectation through set theory.

@ZhenLin I'm much comfortable with set theory because I sort of know what are undefined. We start with a set of undefined symbols (characters) and make up strings. There are some symbols that are "special": " ", "(", ")", "$\exists$", "$\forall$, "$\wedge$, "$\to$... etc. There is a list of pre-defined rules, that tell us how to reduce one to another. There is a list of pre-defined axioms that tell us where we could start. There is a list of translation rules that translate what's in it to English. And then we obtain meanings from that..

Related

• What do logicians mean by "type"?

Answer 1

Not "rigorous" but a "motivation"...

See Rob Nederpelt & Herman Geuvers, Type Theory and Formal Proof : An Introduction (Cambridge University Press, 2014), page 33:

In order to get a firmer hold on the desired behaviour of functions, we will introduce types in the present chapter. This is a natural thing to do: functions are usually thought of as acting on objects belonging to a certain collection, e.g. the collection of the natural numbers or the collection of points on a line. Therefore, it is quite customary to talk about a function on a domain, for example the function ‘square’ on the natural numbers.

Hence, the addition of types gives certain restrictions on the input values permitted: a function defined on domain $\mathbb N$ may only take natural numbers as input values, even when it would be quite clear what the output value would be for some ‘illegal’ input value. For example, ‘square’ on $\mathbb N$ permits us to calculate three-squared, but excludes by definition the squaring of three-and-a-half. We could, however, define ‘another’ squaring function on a larger domain, e.g. $\mathbb Q$ or $\mathbb R$, in order to make it applicable to three-and-a-half. On the other hand, such an extension of the domain is often impossible: the function ‘square root’ on the naturals may not be extended to a function ‘square root’ on the integers, since the square root of a negative number is non-existent in the normal conception of what it means to be a root (even when complex numbers are permitted as an answer, the square root of $−1$ does not exist, since both $i$ and $−i$ could serve as an answer).

And see page 34:

we discuss the intended meaning of the types. This is simple:

− type variables are abstract representations of basic types such as nat for natural numbers, list for lists, etcetera.

− arrow types represent function types, such as nat → real (the set of all functions from naturals to reals) or (nat → integer) → (integer → nat) (the set of all functions with input a function from naturals to integers and output a function from integers to naturals).

In a nutshell, it is an abstract representation of a mathematical universe made of objects of different sorts (numbers, lists) and function on them.

Answer 2

Your question is very typical for a small class of individuals. Unfortunately, reduction to "first principles" is something you need to look for in the papers reprinted in sourcebooks, modern commentary written mostly by philosophers, and the arduous task of sifting through bibliographies. If you do so, you will find that different authors will use the same words differently. You will then be faced with deciding upon reconciliations that work for you personally.

With that said, almost all foundational literature begins with "motivation." Rarely does the technical development return to what serves as motivation to recover the heuristic under the formal. In my personal opinion, the HOTT book is utterly flawed for this reason. If you claim a foundation, its explanation does not belong in appendixes.

In so far as formalist foundations are associated with Hilbert, it essentially invokes the paraphrase of natural language fragments. There is no meaningful notion of definition. Its relationship to "language signatures" is closely bound to the study of symbolic algebras pursued in the tradition of British mathematics (de Morgan and Peacock). And, this had been motivated by the desire to do for logic what Newton had done for analytical geometry.

De Morgan speaks of "peculiar symbols," "meanings," and "rules of operation." Formalism is bound to peculiar symbols and rules of operation without meanings. But, de Morgan observes that the sign of equality is a exception. Substitutivity in a calculus requires a warrant.

This leads to the difference between Frege's logicism and Russell's logicism. With respect to intentionality, Frege's logic had been non-classical. Russell's interpretation of definite descriptions as a form of quantifier recovers classical ambivalence. But, this effectively undermines the generally understood role of definition with respect to first principles.

Russell's account of definite descriptions introduces the notion of "self-identity" into the jargon of logic and its defense of the law of identity. It also accounts for Russell's stipulation that "term" is to be identified with "individual." A term can clearly be stipulated to mean something else. But, this lies at the heart of first-order logic. Russell's recovery of classical bivalence depends upon the fact that collections are composed of individuals.

One influence on Russell had been Peano's distinction between membership and inclusion. Earlier authors had not made this distinction. It lies at the heart of extensionality and semantics.

However, although Russell had been committed to a logicist interpretation for the sign of equality, he considered other views. He has a chapter on "quantity and magnitude" in "Principles of Mathematics" in which he considers alternatives. His "relative equality" does not assume the necessity of reflexive equality statements, although they are provable. In a parenthetical remark that follows, he says that reflexive equality statements maybe assumed as a consequence to a "type" stipulation (If A be a number, then A=A).

Backtracking this even further, Aristotle's analysis of logic speaks of genera, species, in individuals. All of it involves "names." Individuals are associated with proper names and are referred to as "primary substances." Other names are "secondary substances." These would be comparable with "types."

You can get from Russell to HOTT by reading Martin-Lof.

Russell's account of foundations is bound to his logical atomism. One need not take that view. Category theory does not. Lawvere makes an oblique comment about how philosophy detoured away from mathematics because of how the logicists deprecated inclusion. Since HOTT uses a categorical notion of set, this is relevant to your question.