This book, Type Theory and Formal Proof: An Introduction, is a gentle, yet profound, introduction to systems of types and their inhabiting lambda-terms. The book appears shortly after Lambda Calculus with Types (Barendregt et al., 2013). Although these books have a partial overlap, they have very different goals. The latter book studies the mathematical properties of some formalisms of types and lambda-terms. The book in your hands is focused on the use of types and lambda-terms for the complete formalisation of mathematics. For this reason it also treats higher order and dependent types. The act of defining new concepts, essential for mathematical reasoning, forms an integral part of the book. Formalising makes it possible that arbitrary mathematical concepts and proofs be represented on a computer and enables a machine verification of the well-formedness of definitions and of the correctness of proofs. The resulting technology elevates the subject of mathematics and its applications to its maximally complete and reliable form.

The endeavour to reach this level of precision was started by Aristotle, by his introduction of the axiomatic method and quest for logical rules. For classical logic Frege completed this quest (and Heyting for the intuitionistic logic of Brouwer). Frege did not get far with his intended formalisation of mathematics: he used an inconsistent foundation. In 1910 Whitehead and Russell introduced types to remedy this. These authors made proofs largely formal, except that substitutions still had to be understood and performed by the reader.

Type constructors

In the previous chapter we introduced the possibility of constructing generalised terms, by abstracting a term from a type variable. For example, the term λx : σ · x (which is the identity on the fixed type σ) can be generalised to the term λα : * · λ x : α · x (the ‘polymorphic’ identity, i.e. the identity on variable type α, abstracted from this α).

In a similar manner, there is a natural wish to construct generalised types. For example, types like β → β, γ → γ, (γ → β) → (γ → β), …, all have the general structure ◇ → ◇, with the same type both left and right of the arrow. Abstracting over ◇ makes it possible to describe the whole family of types with this structure.

In order to handle this, we introduce a generalised expression that embodies the essence of this structure: λα : * · α → α. This is itself not a type, but a function with a type as a value. It is therefore called a type constructor. Only when we ‘feed’ it with e.g. β, γ or (γ → β), we obtain types:

(λα : * · α → α) β → β β → β,

(λα : * · α → α) γ → β γ → γ,

(λα : * · α → α) (γ → β) → β (γ → β) → (γ → β).

Descriptive versus primitive definitions

As we have explained before, our intention is to switch over from λC to an extended formal system with definitions that can be fruitfully used for the formalisation of mathematical texts (including logic).

In the previous chapter we have defined the system λD0, an extension of λC with definitions as ‘first class citizens’. We have based λD0 on so-called descriptive definitions. The word ‘descriptive’ means that each defined constant is connected to an explicit definiens, giving a formal description of what the constant represents. The new name (the constant), so to say, ‘stands for’ the ‘describing’ expression to which it has been coupled in its definition.

When it comes to mathematics (and logic) in general, there is still one thing that we miss: the possibility to express so-called primitive notions, necessary for the incorporation of axioms and axiomatic notions. These appear as soon as we go beyond the so-called constructive logic (cf. Sections 7.4 and 11.8), or when we incorporate mathematics in a style based on axioms, as often happens.

The constants introduced in primitive definitions – as opposed to those in descriptive definitions – are not accompanied by a descriptive expression. These so-called primitive constants are only provided with a type to which the constant belongs, but there is no further restriction or characterisation. Consequently, primitive constants cannot be unfolded, simply because there is nothing to unfold them to.

Input–output behaviour of functions

Many functions can be described by some kind of expression, e.g. x2 + 1, that tells us how, given an input value for x, one can calculate an output value. In the present case this proceeds as follows: first determine the square of the input value and consequently add 1 to this. The so-called ‘variable’ x acts as an arbitrary (or abstract) input value. In a concrete case, for example when using input value 3, one must replace x with 3 in the expression. Function x2 + 1 then delivers the output value 32 + 1, which adds up to 10.

In order to emphasise the ‘abstract’ role of such a variable x in an expression for a function, it is customary to use the special symbol λ: one adds λx in front of the expression, followed by a dot as a separation marker. Hence, instead of x2 + 1, one writes λx · x2 + 1, which means ‘the function mapping x to x2 + 1’. This notation expresses that x itself is not a concrete input value, but an abstraction. As soon as a concrete input value comes in sight, e.g. 3, we may give this as an argument to the function, thus making a start with the calculation.

The nature of definitions

In the ‘real world’ of logical and mathematical texts, definitions are indispensable. This is particularly the case when the amount of ‘knowledge’ begins to grow.

Therefore we aim at an extension of λC with definitions. In the present chapter we start with an overview of what definitions are and how they are used. Gradually, we shall transform the definitions to a more formal format, in order to be able to incorporate them in λC. The derivation system that we eventually obtain when extending λC with definitions, we call λD, to be described in Chapter 10. A simpler precursor shall be named λD0; see Chapter 9. In the following sections we describe and discuss the essential features of definitions, and how they can be formalised.

We first ask ourselves: what is the use of a definition? The main reason for introducing a definition is to denote and highlight a useful concept. Both logic and mathematics are based on certain notions, most of which are composed from other ones. It is very convenient to single out the noteworthy notions by giving them names.

We start with a number of examples of definitions as they occur in mathematics books.

Examples 8.1.1 (1) ‘A rectangle is a quadrilateral with four right angles.’ Here the notion that we want to single out is ‘a quadrilateral with four right angles’. We give it the name ‘rectangle’.

Dealing with subsets in λD

In type theory, sets are not directly represented, although we have often treated sets as types (i.e. objects of type *) in the previous chapters. We wrote *s instead of * to underline this. However, types and sets have very different backgrounds. In Chapters 2 to 6, we introduced types as formal expressions, in order to eliminate undesired properties from the (‘free’) untyped lambda calculus. Sets, on the other hand, are mathematical constructs, meant to enable us to talk about collections of mathematical objects.

Until now, considering sets as types has worked out fine. But we may expect serious problems when it comes to subsets. The reason is that the Uniqueness of Types property (see e.g. Lemma 10.4.10) conflicts with the ‘natural’ view on subsets. For example, let S be a set and T a proper subset of S. Now let c be an element of S. In type theory this could be expressed as c: S. But what if we wish to express that c is also an element of the subset T? Then c: T doesn't work, because types S and T are different, hence Uniqueness of Types would be violated.

As another example, let P be a property of elements in S. Then one can form the set {x ∈ S | P x} of all elements of S satisfying P.

The Peano axioms for natural numbers

In the previous chapters we have become acquainted with the use of λD for doing mathematics, by selecting a few examples and investigating the issues that we came across.

Let's now make a fresh start by thoroughly exploring the most fundamental entities in mathematics: natural and integer numbers. This will not be easy, since in the process of development we have to pretend that we ‘know nothing’ about subjects we are so familiar with. As a consequence, we have to build up our knowledge from scratch, which may seem cumbersome, but it is also quite interesting, since we are obliged to scrutinise the foundations of mathematics.

In the present section, we start with the basis: natural numbers. Integers will be the main topic of following sections.

In Chapter 1 we saw how natural numbers, and operations on naturals such as addition and multiplication, can be coded in untyped lambda calculus, as so-called Church numerals (see Exercise 1.10). There also exist encodings of these notions in typed lambda calculi: in the chapter about λ2 we have discussed the so-called polymorphic Church numerals; see, for example, Section 3.8 and Exercise 3.13. (For Church numerals in λ→: see Section 2.14.)

Therefore, it would be a type-theoretically justified choice to introduce the natural numbers in this manner. This can be done by writing down the appropriate definitions, since λ2 is a subsystem of λD.