Developing arithmetic in Gödel's system T

April 11, 2011

This year I’ve been running a reading group on type theory. Our primary text is Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor. The focus of the book is the development of the typed λ-calculus, with a strong proof-theoretic slant, these two perspectives being unified by the Curry-Howard correspondence. It begins by exploring the connections between intuitionistic logic and the simply typed lambda calculus, and works up to a fairly in-depth study of System F.

One of the intermediate steps is the system T, originally developed by Kurt Gödel in his Dialectica interpretation, and reformulated by Tait in 1967. I won’t try to cover the history here—there are plenty of articles out there if you’re interested. (The names of the articles alluded to are given in the references at the end.)

The modern formulation of T is as a typed λ-calculus with natural number and boolean types. In chapter 7 of Proofs and Types, Girard shows how the natural numbers can be represented in T, and provides a definition of addition based on the recursion operator $\mathsf{\text{R}}$. He goes on to say that

Among easy exercises in this style, one can amuse oneself by defining multiplication, exponenential, predecessor etc.

So, let’s amuse ourselves! Thinking about these simple examples is helpful because it gives a working demonstration of how the recursion operator adds power back to the language which was lost when the restrictive type system was introduced.

For example, the untyped λ-calculus allows one to use Church encoding to represent the natural numbers, but in the simply typed lambda calculus one is barred from forming the relevant terms by the requirement that every term be well-typed.

During the reading group meeting where we discussed this chapter, we managed to assemble a working definition for multiplication, which I’ll present below along with the other arithmetical functions Girard suggests. However, before we get onto that, I’m going to briefly sketch how the type of natural numbers $\mathsf{\text{Nat}}$ is defined in T; the introduction and elimination rules for terms of that type, on which everything else is built; and how an addition function can be defined in terms of those rules.

A small niggle: Girard actually talks about an integer type $\mathsf{\text{Int}}$. When one examines the nature of the type it becomes clear that what’s intended is a natural number type, so I’m going to talk solely about natural numbers and call the type in question $\mathsf{\text{Nat}}$, not $\mathsf{\text{Int}}$.

Natural numbers in T

System T is a variant of the simply typed lambda calculus, so it has three sorts of rules: those stating which types exist; those stating which terms of those types can be formed; and reduction rules stating how some terms can be reduced to others. These are spelled out in §3.1 of Proofs and Types, so if any of the following doesn’t make sense, I recommend checking that out (the book is freely available from the link above).

For system T, there are also two constant types, $\mathsf{\text{Nat}}$ and $\mathsf{\text{Bool}}$; here we shall only be concerned with $\mathsf{\text{Nat}}$ so I shall omit the rules mentioning $\mathsf{\text{Bool}}$. The additional term formation rules for system T specify how one can introduce and eliminate terms of $\mathsf{\text{Nat}}$ and $\mathsf{\text{Bool}}$. The introduction rules are:

• $\mathsf{\text{O}}$ is a (constant) term of type $\mathsf{\text{Nat}}$;
• If $t$ is a term of $\mathsf{\text{Nat}}$, then $\mathsf{\text{S}}t$ is a term of type $\mathsf{\text{Nat}}$.

These mirror their equivalents in Peano Arithmetic almost exactly—that is, they represent zero and the successor function. There is also the elimination rule for $\mathsf{\text{Nat}}$, which introduces the recursion operator $\mathsf{\text{R}}$:

• If $u$, $v$, $t$ are of types respectively $U$, $U\to (\mathsf{\text{Nat}}\to U)$ and $\mathsf{\text{Nat}}$, then $\mathsf{\text{R}}uvt$ is of type $U$.

The recursion operator allows us to combine the introduction rules to give recursive definitions of arithmetic operations such as addition and multiplication in a form not too far removed from their counterparts in Peano Arithmetic. Its reduction rule is given by two cases:

• $\mathsf{\text{R}}uv\mathsf{\text{O}}$ reduces to $u$.
• $\mathsf{\text{R}}uv(\mathsf{\text{S}}x)$ reduces to $v(\mathsf{\text{R}}uvx)x$.

The first is the base case, which ensures that the recursion is well-founded. The second rule gives, for the recursive case, a way of eliminating an instance of the recursion operator. The term it reduces to looks more complex than the one we started with, but it’s clear that eventually we’re going to run out of successors and the reduction process will terminate (a proof of this is given in §7.2 of Proofs and Types).

Addition

With the preamble out of the way, we’re finally ready to start defining the usual arithmetic functions within T. The easiest place to start is with the definition of addition.

$x+0=x$

$x+S(y)=S(x+y)$

There’s no recursion operator in sight in this definition, but of course there is recursion occurring. The first equation gives the base case, defining the result when the addition function is used to combine a number $x$ with $0$. The second equation defines the recursive case, giving the result when we add the successor of some number $y$ to some number $x$. The recursion operator $\mathsf{\text{R}}$ has three arguments, and the first two map to these cases: the value of the base case (here it would be $x$) and the function to apply in the recursive case (here, the successor function).

With this in mind, we can formulate an addition function in T pretty straightforwardly. The variables bound by lambda abstractions have been given type annotations, just to make clear how the types of these terms relate to those specified in the introduction and elimination rules for terms of type $\mathsf{\text{Nat}}$. I shall omit these annotations from the definitions in the rest of the article.

$\mathsf{\text{add}}=\lambda x^{\mathsf{\text{Nat}}}.\lambda y^{\mathsf{\text{Nat}}}.\mathsf{\text{R}}x(\lambda z^{\mathsf{\text{Nat}}}.\lambda w^{\mathsf{\text{Nat}}}.\mathsf{\text{S}}z)y$

The second term given to $\mathsf{\text{R}}$ is just a double lambda abstraction over $\mathsf{\text{S}}x$, representing a two-argument function; the second argument (the numbers accumulating on the right of the reduction) will always be thrown away. The type of the term must be, by the definition we gave earlier, $U\to (\mathsf{\text{Nat}}\to U)$. In this case we’re saying that the type $U$ is in fact the constant type $\mathsf{\text{Nat}}$, so the term has a type of $\mathsf{\text{Nat}}\to (\mathsf{\text{Nat}}\to \mathsf{\text{Nat}})$.

I should note that there is no mechanism in T for giving names to definitions (i.e. let binding), so equations like the one given above should simply be seen as expressing abbreviations, not as expressions in the language of T, although the lambda term on the right hand side certainly is.

Multiplication

Again, let’s begin with the definition of multiplication we find in Peano Arithmetic.

$x\cdot 0=0$

$x\cdot S(y)=(x\cdot y)+y$

Here we can see that in the base case, when we combine $0$ with $x$ the result is $0$. In contrast, in the base case for addition when we combine $0$ with $x$ the result is $x$. This is reflected in the following definition of multiplication in T, with $\mathsf{\text{O}}$ as the base case, and addition as the operation applied in the successor case.

$\mathsf{\text{mult}}=\lambda x.\lambda y.\mathsf{\text{RO}}(\lambda z.\lambda w.(\mathsf{\text{add}})xz)y$

Expanding the definition of $\mathsf{\text{add}}$ in $\mathsf{\text{mult}}$ (with some trivial α-conversion and β-reduction), it’s easy to see the double recursion that we also see in the $\mathsf{\text{PA}}$ definitions.

$\mathsf{\text{mult}}=\lambda x.\lambda y.\mathsf{\text{RO}}(\lambda z.\lambda w.\mathsf{\text{R}}x(\lambda u.\lambda v.\mathsf{\text{S}}u)z)y$

Exponentiation

Just as multiplication is built on addition, adding an extra layer of recursion, so exponentiation is built on multiplication. The $\mathsf{\text{PA}}$ equations are

$x^0=1$

$x^{S(y)}=x^y\cdot y$

Again, all we need to do to define this new function is state the base case ($\mathsf{\text{SO}}$, corresponding to the rule that any number raised to exponent 0 is 1) and the function to apply in the recursive case (multiplication).

$\mathsf{\text{exp}}=\lambda x.\lambda y.\mathsf{\text{R}}\mathsf{\text{SO}}(\lambda z.\lambda w.((\mathsf{\text{mult}})xz))y$

Predecessor

The predecessor function is given by the following equations.

$Pred(0)=0$

$Pred(S(x))=x$

Compared to the nested recursions given above, the definition of the predecessor function in T is strikingly simple.

$\mathsf{\text{pred}}=\lambda x.\mathsf{\text{RO}}(\lambda y.\lambda z.z)x$

The insight which allows one to derive it is similarly simple. An application of the predecessor function to some successor (in the case of $\mathsf{\text{O}}$ the predecessor will simply be $\mathsf{\text{O}}$ too) will be of this form: $\mathsf{\text{RO}}(\lambda y.\lambda z.z)(\mathsf{\text{S}}x)$. When we look at the reduced term after one reduction, we have something like $(\lambda y.\lambda z.z)(\mathsf{\text{RO}}(\lambda y.\lambda z.z)x)x$.

Ignore the new occurrence of the recursion operator; just consider it as another term. Instead, look at the whole formula as an application. Clearly, the first argument to the function on the left will always be discarded: the whole term will always reduce simply to $x$, the predecessor of $\mathsf{\text{S}}x$, our initial argument.

References & further reading

• Girard, Lafont and Taylor’s Proofs and Types is the primary reference for this article.
• System T was first introduced by Kurt Gödel in his 1958 Dialectia article ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, which is reproduced (with an English translation) in volume II of his Collected Works, edited by Feferman et al.
• The more modern version of T which Girard et al. work from was first given by William Tait in his 1967 JSL article, ‘Intensional interpretation of functionals of finite type I’.
• From a programming languages perspective, Benjamin Pierce provides a good introduction to the simply typed lambda calculus in chapter 9 of his book Types and Programming Languages.
• A more general introduction to the λ-calculus is Hindley and Seldin’s Lambda-Calculus and Combinators, while Barendregt’s The Lambda Calculus: Its Syntax and Semantics is the definitive reference work in the field.