Language and logic

In a sense, the theory is logic free. Unlike our account of typed logic, we do not start with propositions and truth. Instead we begin with more elementary parts of language, in particular, with a theory of computational equality of terms (or expressions). In Principia these elementary ideas are considered as part of the meaning of propositions. We separate them more clearly. We examine the mechanism of naming and definition as the most fundamental and later build upon this an account of propositions and truth.

This analysis of language draws on the insights of Frege, Russell, Brouwer, Wittgenstein, Church, Curry, Markov, de Bruijn, Kolmogorov, and Martin-Löf, and it draws on technical advances made by numerous computer scientists and logicians. We can summarize the insights in this way. The notion of computability is grounded in rules for processing language ([25], [39], [79]). In particular, they can be organized as rules for a basic (type free) equality on expressions closely related to Frege's theory of identity in [45]. The rules explain when two expressions will have the same reference if they have any reference. (We call these computation rules, but they could also be considered simply as general rules of definitional equality as in Automath.) DeBruijn showed that to fully understand the definitional rules, we need to understand how expressions are organized into contexts in a tree of knowledge as we discussed in section 2.12.

Frege not only realized the nature of identity rules, but he explained that the very notion of an object (or mathematical object) depends on rules for equality of expressions which are intended to denote objects. The equality rules of a theory serve to define the objects and prepare the ground for a referential language, one in which the expressions can be said to denote objects.

Frege also believed that the equality rules were not arbitrary but expressed the primitive truths about abstract objects such as numbers and classes. We build on Brouwer's theme that an understanding of the natural numbers ${{\mathbb{N} }}$ is an especially clear place to begin, and we try to build as much as possible with them. Here the insights of [19] (see [115]) show how to connect intuitions about number to the rules for equality of expressions. Brouwer shows that the idea of natural number and of pairing numbers are meaningful because they arise from mental operations. Moreover, these are the same abilities needed to manipulate the language of expressions (see [24]).²⁷

So like Frege and Brouwer (and unlike formalists), we understand type theory to be referential, that is, the theory is about mathematical objects, and the meaningful expressions denote them.

Following Russell, we believe that a referential theory is created by classifying expressions into types. Not every expression is meaningful, for example, school children know that 0/0 is not. We sometimes say that the meaningful expressions are those that refer to mathematical objects, but this seems to presuppose that we know what such objects are. So we prefer to say that the task of type theory is to provide the means to say when an expression is meaningful. This is done by classifying expressions into types. Indeed to define a type is to say what expressions are of that type. This process also serves to define mathematical objects.²⁸

Martin-Löf suggested a particular way of specifying types based on ideas developed by W. W. Tait [109,110]. First designate the standard irreducible names for elements of a type, say $t_1, t_2, \ldots$belong to T. Call these canonical values. Then based on the definition of evaluation, extend the membership relation to all t' such that t' evaluates to a canonical value of T; we say that membership is extended by pre-evaluation.