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
$1 + 2$ true? makes no sense – types of mathematical objects.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
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:
$A$ and $B$ are types we can form the function type $A \to B$ (in programming languages these are often called generics).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.