Foundations of Mathematics should tell us what are true mathematical statements. The last layer of this is the most familiar, the *axioms* that we know are true in advance. But before we use, or even state, these, we must

- Understand how we can build valid mathematical objects, and what are the ones we start with - the
**language**of mathematics. - Which of these are
**statements**-*is*makes no sense –`$1 + 2$`

true?**types**of mathematical objects. - Specify how to make a
*judgement*that one statement is true from knowing other statements are true (the**rules of deduction**).

Given these, we form a *theory* by specifying that some statements, our axioms, are assumed to be true. We then have a meta-mathematical layer of judgements which is the collection of statements that we have judged to be true (more precisely, to have been proved).

We emphasise that this is not the only way in which foundations can be built. Indeed the foundations we consider will have a much richer kind of language (not just a larger vocabulary) and so axioms will play only a minor role - indeed in the pure Type Theoretic foundations we have no axioms.

All foundations we consider will have **rules** giving

- a
**language**describing the objects we consider together with some information about their nature - which we will call**types**. Types are the analogue of*parts of speech*in natural languages. **judgements**we make about these objects; including judgements of types which are required in the rules for forming languages.

The rules must be clearly and unambiguously stated and straightforward to verify, including by a computer program.

While natural langauges have a vocabulary that grows over time, the *parts of speech* remain fixed. However in the higher languages we consider, we can *form* new parts of speech - essentially the part of speech of a word/phrase may be given by a *type-phrase*. Indeed there are three levels of languages we consider, which in terms of *terms* (analogues of words, phrases, sentences etc) and *types* (analogues of parts of speech) are:

**First-order**: a fixed, often finite, set of types.**Higher-order**: types can be built from other types, for example if`$A$`

and`$B$`

are types we can form the*function type*`$A \to B$`

(in programming languages these are often called*generics*).**Dependent types**: types can be formed not just from types but also terms- for instances vectors of a fixed length form a type;
- indeed, types are
*first-class*, i.e., we cna have functions (some of whose) arguments are types and functions whose results are types (or both).

We shall see how to build such a type theory, and how it also forms foundations for *computation*.

We communicate with computers using *programming languages*, which are languages in the above sense. However, with the most common style of programming, so called *imperative programming*, the program to describe a mathematical computation is very different from a mathematical description, as it is a set of instructions to output the result of the described objects.

However, *functional languages*, building on Church’s model of computation, have descriptions that are much closer to mathematical descriptions. For instance, in pseudo-code we may define `factorial(n)`

as

```
$factorial(n)$ := if $n = 0$ then $1$ else $n\cdot factorial(n-1)$
```

which is just as good a mathematical definition as any. Moreg generally, the only form of *looping* or used in functional programming is recursion, and there is no (explicit) *flow of control*.

Indeed the foundations we study are to a substantial extent common for mathematics and computation, with the langauge for computation a restriction of the language used for mathematics. Code for a mathematical object is just an *effective* description of that object, which merely means that it does not invoke axioms (including logical axioms such as the law of excluded middle). This would not be musch use if our foundations were Set Theory, as in set theory we use axioms at the drop of a hat. But in the Type Theoretic foundations we study, we use axioms only if there is a strong reason to use.

Examples such as the factorial function, or typical mathematical problems such as solving equations, give a misleadingly limited view of what we mean by computation. Since computation should include all operations that a computer needs to perform, we should include *interpreters*, i.e. a function *eval* so that

```
eval("$factorial(n)$ := if $n = 0$ then $1$ else $n\cdot factorial(n-1)$")($7$)
```

should give us `$factorial(7)$`

.

We can indeed write such interpreters, but such tasks will lead us to the deep unsolvability results of Turing and Godel.