3 Predicate Logic

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

Basically, we is OK, but we better pay attention to detail.
(Wake Up, Essential Logic, 1979)

Propositional logic is simple and clean and can be a lot of fun, but it’s not expressive enough to make the kind of statements about mathematics and computer science that we want to make. Predicate logic adds the quantifiers "for all" (\(\forall\)) and "there exists" (\(\exists\)), and a notion of what they might be quantifying over. This is messier, but we can accomplish more with it.

To strengthen our intuition before going into the formalism, let’s revisit the examples from the Waterloo math course that we used at the beginning of the previous chapter.

The course notes define divisibility as follows: "We write \(m \mid n\) when there exists an integer \(k\) so that \(n = km\)." More formally, we can say "\(m \mid n\) is shorthand for \(\exists k \in \mathbb{Z}, ~n=km\)."

We looked at the following theorem:

Divisibility of Integer Combinations (DIC): Let \(a\), \(b\) and \(c\) be integers. If \(a \mid b\) and \(a\mid c\), then for any integers \(x\) and \(y\), \(a \mid (bx+cy)\).

We rewrote it in English like this:

"For all \(a,b,c\in\mathbb{Z}\), if \(a \mid b\) and \(a\mid c\), then for all \(x,y\in\mathbb{Z}\), \(a \mid (bx+cy)\)."

and then in logical notation like this:

\(\forall a,b,c\in\mathbb{Z}, ((a \mid b) \land (a\mid c) \ra (\forall x,y\in\mathbb{Z}, a \mid (bx+cy)))\).

Here is the proof of DIC as it appears in the course notes (also quoted in the Introduction chapter):

"Assume that \(a\mid b\) and \(a\mid c\). Since \(a\mid b\), there exists an integer \(r\) such that \(b=ra\). Since \(a \mid c\), there exists an integer \(s\) such that \(c = sa\). Let \(x\) and \(y\) be any integers. Now \(bx + cy = (ra)x + (sa)y = a(rx + sy)\). Since \(rx + sy\) is an integer, it follows from the definition of divisibility that \(a \mid (bx + cy)\)."

There are two places where an informal version of \(\forall\)-introduction is used. The second one is more obvious, for the subformula \(\forall x,y\in\mathbb{Z}, a \mid (bx+cy)\). The informal proof of that starts with "Let \(x\) and \(y\) be any integers." There is an implicit "Let \(a,b,c\) be any integers" at the beginning of the entire proof (because the entire DIC formula starts with a \(\forall\)) but it is not written down explicitly.

Here we see the simplest, most direct method to prove a \(\forall\) statement, which is sometimes called "generalization" (our math course calls it "the select method"). It amounts to just taking the quantifier off and manipulating the rest of the statement, treating the formerly-quantified variable as an unknown symbolic quantity. This is done so often in mathematics that we don’t think about it any more. In this case, we remember that \(x\) and \(y\) are integers, and proceed to use properties of integers in the next sentence. That tells us something about how formal \(\forall\)-introduction should work, which we can keep in mind for later.

There are also two nearly-identical places where an informal version of \(\exists\)-elimination is used. This happens when we use the divisibility property. The first one is "Since \(a\mid b\), there exists an integer \(r\) such that \(b=ra\)." The definition \(a\mid b\) expands to \(\exists k, b=ka\). What the proof does is give the name \(r\) to what this statement refers to as \(k\), and then use the property \(b=ra\) in the rest of the proof. Again, this tells us something about how \(\exists\)-elimination should work in general.

There is no use of \(\exists\)-introduction, or \(\forall\)-elimination in this proof. It is worth thinking about what these should look like. We can see a use of \(\exists\)-introduction if we try to prove a specific divisibility statement, for example \(3\mid 6\). This expands to \(\exists k, 6=3k\). To prove this, we exhibit a specific \(k\), namely \(k=2\), and then show that \(6=3\cdot 2\). This is too trivial to require a proof in our informal setting, but the property being witnessed by our choice of \(k\) could in general be more complex.

How might we use or eliminate a for-all statement? The entire DIC formula is one. If we wanted to use this result, we would provide instantiations for \(a,b,c\). For example, they could be \(5,6,7\) respectively. That is not a very useful thing to do, because we are not going to be able to prove that \(5\mid 6\), so we won’t be able to make use of the right-hand side of the implication. But if we chose \(5,10,15\), we could conclude that \(\forall x,y\in\mathbb{Z}, 5 \mid (10x+15y)\). Furthermore (and this is important), if we wanted a self-contained proof of this specific statement, we could take the general proof and substitute \(5,10,15\) for \(a,b,c\) everywhere, and get a valid proof of the specific statement. Again, you should remember this for later.

Two more things to note. We didn’t have to choose numbers to instantiate \(a,b,c\). We could have used any expressions that would evaluate to integers. And there is nothing special about the names \(a,b,c\). We could systematically replace them with \(d,e,f\) respectively, and the theorem would still be valid, because the resulting proof would work. In a sense, it’s the same theorem and the same proof, even though we have made a syntactic change. Something similar holds when we use a there-exists statement. We will need to use these ideas in our formalization.

For the idea of using the quantifiers \(\forall\) and \(\exists\), and indeed for many of the ideas of formal logic that we are studying, we are indebted to Gottlob Frege. (Not those precise symbols; they are due to Gentzen and Peano, respectively.) His Begriffsschrift ("Concept Notation", 1879) introduced a language for discussing logic, which he then used to try to formally describe mathematics in his subsequent work. Frege’s notation for proofs was rather awkward, and his habit of criticising other mathematicians for insufficient rigour and clarity (a prominent example being David Hilbert, a significant figure in the formalist movement) could not have been endearing. At the time, his work was mostly ignored.

In 1902, as Frege was about to publish the second volume of his massive work Grundgesetze der Arithmetik ("Basic Laws of Mathematics"), he received a letter from the British philosopher and logician Bertrand Russell, pointing out a contradiction in his logical system as laid out in the first volume. In modern terms, Frege’s system allowed the formation of a set from a predicate, a logical statement with a variable. Given a predicate \(P(x)\), one could form the set \(\{e \mid P(e)\}\). Russell’s observation was devastatingly simple: if the predicate \(P(x)\) says "\(x \notin x\)", then trying to figure out the value of the predicate on the resulting set gives a contradiction.

Frege did not know how to fix his system. He could not make the contradiction go away without making the system useless for describing mathematics. His final years were not happy ones. Russell’s solution was type theory, elements of which we have already been using. Russell and Alfred North Whitehead used it to publish their own massive three-volume work on the foundations of mathematics, Principia Mathematica (1910-1913). This was very influential work, but the system was overly complicated, and was gradually refined by subsequent researchers. Alonzo Church’s version of simple type theory using the lambda calculus (1940) is now the standard. Among Bertrand Russell’s subsequent achievements were being jailed for pacifism during World War I, and being awarded the Nobel Prize for Literature in 1950. That’s an inadequate summary of his complex and fruitful life, and once again I urge you to do some tangential reading.

It is traditional, in a course like this, to cover classical first-order predicate logic. However, the logical systems described above are not first-order; they are higher-order, as are the systems on which the proof assistants we are aiming for are based. Since Proust is designed to demystify proof assistants, it is also based on a higher-order system. We will not skip first-order logic entirely, as it is extensively used, and is the basis for modern foundations of mathematics. However, since our time is limited, I will just sketch the ideas rather than present them in detail.

It will take a bit of time before I can define "first-order" and "higher-order", and explain why I’m going quickly over material that everyone else does slowly, but the following analogy may provide motivation. In studying functional programming using HtDP or FICS, we start with first-order functions which can only be applied and cannot be used as arguments. We can do a lot with them; in fact, many programming languages, such as C, only have first-order functions. But when we get to lambda and higher-order functions, suddenly our programming language becomes a lot more expressive, and things get a lot more interesting. Something similar happens in logic, though we may not get enough experience in first-order logic for you to see this.

3.1 First-order logic

From propositional logic, we retain the logical connectives and the idea of variables, though how we use variables will change. We add the quantifiers \(\forall\) and \(\exists\), and we add ways to work with variables to create propositions (to which the logical connectives can be applied).

In mathematics, we typically say things like "For all natural numbers \(n\)," but the domain over which we are quantifying ("natural numbers", in this case) is not part of the language of first-order logic. As we’ll see, the domain and its properties have to be dealt with in a roundabout fashion.

Since variables now represent objects in the domain being quantified over, a variable by itself is not a logical formula, and we have have to remove the grammar rule that says so. We get propositions (to which the logical connectives can be applied) by adding relational symbols, such as \(<\). For example, we might say \(A < B\), which is a proposition. But applying relational symbols only to variables does not seem to give us a rich enough language to do what we want. To enrich the language further, we add functional symbols, so we can create expressions.

What relational and functional symbols should we use? It depends on the domain being quantified over, and it’s hard to throw in everything that might be used by mathematicians (who keep making up new symbols to talk about their new areas of study).

For this reason, the language of first-order logic is really a family of languages. Each language in the family has a fixed set of function and relation symbols. Since a function is a special kind of relation, the function symbols are actually redundant, but they certainly help with expressivity. Similarly, we can add named constants (since a constant is just a function with no arguments).

As an example, we could talk about arithmetic by using the functions \(+\) and \(\cdot\), the constants \(0\) and \(1\), and the relations \(<\) and \(=\).

With the informal example above, we saw that to use a statement of the form \(\forall X~T\) that we have proved, we substitute some specific expression \(a\) for \(X\) everywhere in \(T\), giving us a statement that we can regard as proved. This should remind you of the way we handled implication in propositional logic. But there we talked about substituting a proof into another proof that used assumptions. Here we are substituting into a formula to get another formula. We can create a notation for this: \(T[X\mapsto a]\). It turns out that substitution is a bit tricky to define precisely, which we won’t do until we get to higher-order logic. Since we’re just skimming first-order logic, we can make do with an intuitive notion for a while longer.

Recall that the BHK interpretation gives meanings to each of the logical connectives in terms of what they say about proofs. Putting this together with the discussion above, we arrive at the following interpretation of the for-all quantifier.

"A proof of \(\forall X~ T\) is a construction which permits us to transform an object \(a\) into a proof of \(T[X\mapsto a]\)".

In the example in the informal reasoning at the beginning of the chapter, we saw that to prove a \(\exists\) statement, we needed to exhibit a witness and a proof that the witness has the property claimed by the statement. Here is the corresponding BHK interpretation.

"A proof of \(\exists X~T\) is an object \(a\) and a proof of \(T[X\mapsto a]\)."

As we saw with the propositional connectives, the inference rules come in introduction and elimination flavours. For each quantifier, there is one introduction rule and one elimination rule. To create a \(\forall X\), we use generalization: we prove the statement without the quantifier, treating \(X\) as an unknown. To use a \(\forall X\), we substitute some specific \(a\) for \(X\).

\[\ir{(\forall_I)}{\Gamma\vdash T}{\Gamma\vdash\forall X~T} ~~~~ \ir{(\forall_E)}{\Gamma\vdash\forall X~T}{\Gamma\vdash T[X\mapsto a]}\]

Do not take these rules too seriously, as there are important technical side conditions on them that I am leaving out for now. To create a \(\exists X\), we must have a proof of the statement when \(X\) is some specific \(a\); to use a \(\exists X\), we need some way of concluding some \(V\) from the statement without the quantifier (once again, treating \(X\) as an unknown), and then the existence lets us conclude \(V\).

\[\ir{(\exists_I)}{\Gamma\vdash T[X\mapsto a]}{\Gamma\vdash\exists X~T} ~~~ \ir{(\exists_E)}{\Gamma\vdash\exists X~T ~~~ \Gamma,T\vdash V}{\Gamma\vdash V}\]

There is a pleasing symmetry to these rules. You should be able to see how the rules correspond to the way quantification is used in the proofs you have seen. Though I have presented these right after a discussion of the BHK intuitionistic interpretation, there is no difference between classical and intuitionistic logic in the treatment of these quantifiers. The difference is on the propositional level, whether LEM or one of its equivalents is considered valid.

The classical semantics for first-order predicate logic extends the semantics for classical propositional logic. Recall that the Boolean valuation was the way we defined truth in classical propositional logic. We can continue to use this idea if we figure out how to assign a truth value to the subformulas which are connected by the logical connectives. Those subformulas involve \(\forall,\exists\) and the chosen set of function and relation symbols, as well as possibly more logical connectives.

The traditional way to define the classical semantics is in terms of models. A model is a domain of quantification (over which \(\forall,\exists\) scope) together with an interpretation for each of the function and relational symbols. For example, for the language we proposed to talk about arithmetic, the domain of quantification could be the integers, \(+\) could be interpreted as addition, and so on. \(\forall,\exists\) are interpreted as "for all" and "there exists" in the usual mathematical sense.

However, in this particular instance (and typically in general) this is not the only model possible. We could make the domain be the Boolean values \(\{0,1\}\), \(+\) could be interpreted as Boolean OR, and \(\cdot\) as Boolean AND. (In fact, this language, with this second interpretation, is used to talk about Boolean functions in circuit design and computer architecture.)

It’s not very satisfying to say that the interpretation of something we are trying to make precise is our old informal notion. But there is a more immediate problem: if multiple interpretations are possible, then how can we hope to prove a theorem about the integers if it might also be a theorem about the Boolean values, or some other domain we haven’t thought about? You can probably think of theorems that hold for Boolean values that do not hold for the natural numbers, and vice-versa.

The traditional way to handle this is to use the \(\Gamma\) that appears in the "proves" and "entails" relation. We originally added this to hold the assumptions that pile up when proving implications. But we can throw in formulas that represent properties of our chosen domain. For arithmetic, we could add the commutative and distributive laws, among others.

Given a model, a valuation is a map from variables to elements of the domain, and this is extended to give a truth value to formulas in the obvious way. That is, the value of a function expression is the interpretation of the function symbol applied to the (recursively defined) values of the argument expressions. The value of a relation expression is 1 if the relation holds among the values of the argument expressions; otherwise it is 0. And connectives work as in the semantics of classical propositional logic. We write \(\Gamma\vDash T\) if for all models and all valuations that make the formulas in \(\Gamma\) true, \(T\) is made true.

For classical propositional logic, there are only a finite number of valuations to check for any sequent, but this is clearly not the case for predicate logic, because of that "for all models" phrase. It’s not even clear how one might go about figuring out what possible models there might be for a given \(\Gamma\). So it is perhaps a bit surprising to learn that classical predicate logic is complete, as was first proved by Kurt Gödel in 1929. That is, if \(\Gamma\vDash T\), then \(\Gamma\vdash T\).

The proofs of completeness (for there are several ways to do it) are fairly involved, and are typically covered in senior-level logic courses in mathematics departments. Fortunately, soundness for both classical and intuitionistic predicate logic (if \(\Gamma\vdash T\), then \(\Gamma\vDash T\)) remains an easy induction on the proof tree. Both Heyting algebras and Kripke models can be extended to provide complete semantics for intuitionistic predicate logic.

We saw with classical propositional logic that there was an algorithm to decide whether a formula was provable or not: the formula has a fixed number of variables, so try all valuations on those, and if each one makes the formula true, then by completeness, it is provable. The proof of completeness I sketched in the previous chapter also yields an algorithm to construct the proof for a formula.

There is no obvious algorithm for predicate logic (how does one "try all models"?) and indeed one can prove that there is no such algorithm for predicate logic, whether classical or intuitionistic. This was first shown by Alonzo Church in 1936, in the work for which he invented the lambda calculus. Later that year, Alan Turing gave a different proof using a different model of computation, which we now call a Turing machine, for which he showed that the halting problem is undecidable.

Turing’s proof is simple enough that it can be understood by anyone who knows a bit of Racket, since the main requirement is understanding how programs can themselves be manipulated as data. It’s a bit of a tangent, but if you haven’t seen it, I’ve put a writeup of it on this auxiliary page.

Both Church and Turing were primarily motivated by this question of constructive provability, which had been formulated by David Hilbert, vaguely in 1900 and more precisely in 1924. In fact, the result holds even for formulas of a special form using only \(\forall\) and \(\ra\) (and therefore only intuitionistic rules, since there is no negation). The basic idea is that given a program in some model of computation, one can build a first-order formula that can be proved if and only if the program halts. In effect, the formula describes the computation of the program.

The logical system I have just described is called first-order because the quantification is only over objects in the domain. One cannot quantify over sets, or functions, or relations. Yet we do this kind of thing in mathematics all the time, which is why Frege and Russell used higher-order logical systems.

There are some interesting limitations on the expressiveness of first-order predicate logic. One cannot throw in enough rules to ensure that the language of arithmetic only admits the usual model of the integers. One can add enough to rule out, for example, the model of Boolean values, but there will always be models that look similar to the natural numbers we know and love but are not quite the same. One cannot express the concept that the domain is finite, or countable. So, for example, there is an uncountable model (has the same cardinality as the real numbers) in which exactly the logical statements that hold for the integers hold in that model. This is both fascinating and somewhat disturbing.

So why did first-order logic become the standard? There is no simple reason for this, just as there is no simple reason that Java and C++ dominate computing. The metamathematics of first-order logic is quite interesting, especially the rich field known as model theory. First-order logic has proved sufficient to define set theory, and thus the foundations of mathematics. There is a paper linked on the Resources page which provides much insight into the history of logic, if you wish to learn more.

For computer scientists, there are additional frustrations. We’ve seen how our proof terms for propositional logic provide useful computational tools like lambda and pairs, even though we haven’t yet used them for actual computation. In first-order logic, we don’t directly construct useful datatypes. Instead, we add rules that describe the properties of these datatypes and draw conclusions from them. In contrast, the development below will continue the introduction/elimination approach, with familiar constructors for datatypes. Furthermore, propositions will also become objects on which computations can be performed. All of this improves expressivity relative to first-order logic.

If we wanted to spend time on first-order predicate logic, we could define proof terms for it, extending what we did for propositional logic. But there are many technical details, some of which are glossed over in informal presentations, but which implementations cannot neglect. Much of this work would have to be replicated in a slightly altered fashion when moving to higher-order logic.

Instead, let’s jump ahead to higher-order logic, and bring Proust along with us.

3.2 Higher-order logic

We hope to be able to prove theorems about user-defined computations, as we did in the Introduction with append. It follows that things we have been keeping on the left-hand (term) side of the \(t:T\) colon, like constructors for values and functions, are going to show up on the right-hand (type) side of the colon, because that’s where our logical formulas live. In preparation for this, we will go back to the very first version of Proust, that only handled implication in propositional logic, and refactor it to mix terms and types, while retaining the same behaviour. Instead of having terms and types separate in the grammar and in the program design, we handle them both with one nonterminal and the same functions.

This grammar by itself lets us put expressions on the right-hand side of a colon that are not valid types, such as ((λ x => x) : (λ y => y)). Previously the parse-type function would report an error if given (λ y => y), but we will also merge the parse functions for terms and types, as well as the pretty-print functions. We move the responsibility for reporting invalid types into type-synth. If we let Type be the type of valid types, we have the following rules derived from our previous grammar for types. Since position will no longer differentiate a variable from a base type, we use the context to disambiguate. (This is an awkward choice, and it’s only temporary.)

\[\ir{(\textrm{Var}_\mathit{wf})}{x \not\in \Gamma}{\Gamma \vdash x \Ra \textrm{Type}} ~~ \ir{(\Ra_\mathit{wf})}{\Gamma \vdash T \Ra \textrm{Type} ~~~ \Gamma \vdash W \Ra \textrm{Type}}{\Gamma \vdash T \ra W \Ra \textrm{Type}}\]

If \(\Gamma \vdash T \Ra \textrm{Type}\) is valid, we say that \(T\) is a well-formed type. Implementing this requires a new structure to be added to Proust to represent \(\textrm{Type}\).

(struct Type () #:transparent)

Here are the new type checking and synthesis functions.

If we were going no further, this would be an inferior design, as it mixes together things that can and should be kept separate. But they cannot be kept separate in what we are about to do.

The code is linked in the Handouts chapter as proust-pred-start.rkt. You should look at it to make sure that all the merged functions make sense to you.

We have a different implementation of something we could do before (propositional logic with only implication) but nothing new yet. In the next subsection, we will start in on higher-order predicate logic, by starting to work on adding for-all. This is where we seriously depart from a conventional treatment, but the result will be a small language with considerable power, even without the rest of the logical connectives.

3.2.1 Rules for universal quantification

We want to be able to quantify over more than a single, unspecified domain. But we can’t quantify over just anything; we run the risk of introducing Russell’s paradox. The solution we adopt is based on Russell’s solution: we quantify over things that are typeable. Instead of \(\forall X~W\), our human-readable notation will be \(\forall X:T . W\), meaning \(X\) is quantified over type \(W\).

We now slightly change the BHK interpretation to take the new idea into account, with the added clarification in bold below:

"A proof of \(\forall X:T . W\) is a construction which permits us to transform an object \(x\)
of type \(T\) into a proof of \(W[X\mapsto x]\)".

We will be focussing on \(\forall\) initially, and will add \(\exists\) later on. Look at the interpretation of \(\forall\), and consider what happens when \(W\) does not mention \(X\). We have not defined substitution formally, but it should be clear that any reasonable definition must leave \(W\) unchanged when substitution for \(X\) is done but \(X\) does not occur in \(W\). Under these circumstances, the interpretation becomes "... a construction which permits us to transform an object \(x\) of type \(T\) into a proof of \(W\)." But an object \(x\) of type \(T\) is, by the Curry-Howard correspondence, a proof of \(T\). In other words, in the case where \(W\) does not mention \(X\), \(\forall\) becomes implication (\(\ra\)). Implication is a special case of for-all!

This suggests that the proof term for creating a for-all formula should act like the proof term for creating an implication, that is, it should be some sort of generalized lambda. But what kind of generalization? Let’s look at the BHK interpretation again, rephrased to make the Curry-Howard connection more explicit:

"A proof of \(\forall X:T . W\) is a function that transforms a proof \(x\) of \(T\) into a proof of \(W[X\mapsto x]\)".

The only change to our earlier notion of lambda needed here is that the type of the result can depend on the value of the argument. This is known as a dependent type. It is not common in programming languages, because of the complexity it brings to the type system, but it is just the right idea for a proof assistant. (Haskell will have optional dependent types in an upcoming release.) The idea is useful even when \(W\) does not have a logical interpretation, and we will see examples of this below. Type theory often uses the notation \(\Pi X:T.W\), and calls these "Pi-types". But since our primary motivation is the study of logic, we will stick with \(\forall\).

The for-all introduction rule resembles the implication introduction rule (which it replaces, being more general) but because of the mingling of terms and types, we do have to check for well-formed types.

\[\ir{(\forall_\mathit{wf})} {\Gamma\vdash T\La\textrm{Type} ~~~ \Gamma,x:T\vdash W\La\textrm{Type}} {\Gamma\vdash\forall x:T . W \Ra \textrm{Type}}\]

\[\ir{(\forall_{I})} {\Gamma\vdash \forall x:T . W \La\textrm{Type} ~~~ \Gamma,x: T\vdash t\La W} {\Gamma\vdash\la x.t\La\forall x:T. W}\]

In general, the type \(T\) may contain references to variables in \(\Gamma\), which was not possible when we separated terms and types. But in the recursive application, we add \(x:T\) to the context. As a consequence, the items in a context are now ordered by time of addition. That is, contexts are no longer sets, but sequences. A later element of the sequence can refer to an earlier variable.

Fortunately, we already represented sets as lists in Proust, so they are already sequences. But the previous side condition \(x \not\in\Gamma\) is going to take more work to ensure. We can’t just rely on the "first occurrence" behaviour of assoc as we did before. A new binding for \(x\) might refer to \(y\) earlier in the context, and that might refer to the earlier binding of \(x\) to a different type. But that earlier binding will never be produced by assoc. Notice also that the variable \(x\) is the same in both the lambda term and the for-all type. We’re going to want more flexibility than that. We’ll return to these points when discussing the implementation.

How do we use or eliminate a for-all? Is it like using or eliminating an implication? Again, yes. Remember our discussion of \(\forall\)-elimination for the DIC example above. We can pick a specific value (or a term of the right type) to substitute for the variable of the for-all, and get a specific statement. But we can also get a proof of the specific statement by substituting the specific value for the variable in the proof of the general statement.

The proof term for \(\forall\)-elimination is function application, just as it was for implication elimination. We apply the lambda which proves the for-all to a specific value of the right type, in accordance with the BHK interpretation, and get a proof for that value. This involves substituting the specific value for the variable in the body of the lambda to get a specialized proof term. The difference from implication-elimination is that we must substitute to compute the correct result type as well. Since the substitution has no effect if \(W\) does not mention \(x\), \(\forall\)-elimination generalizes implication-elimination.

\[\ir{(\forall_{E})} {\Gamma\vdash f\Ra\forall x:T . W ~~~ \Gamma\vdash t\La T} {\Gamma\vdash f~t\Ra W[x\mapsto t]}\]

It’s convenient to be able to collapse adjacent for-alls together in human-readable notation, as in \(\forall (x:T) (y:W) . S\) or \(\forall x~y:T . W\). Once again, in Proust we have to add enough parentheses to facilitate parsing, and we can’t use dot as it has a special meaning in Racket. But we can make choices that facilitate writing proofs.

We’ve introduced quantification over a type, but we can also consider quantification over all types. Previously, we typed the identity function, \(\la x .x\), as \(A \ra A\). But it could also be typed as \(B \ra B\), and \(C \ra C\), and so on. We can go further: it can be typed as \((A\ra B)\ra (A \ra B)\). For any type \(T\), no matter how complex, \(\la x.x\) can be typed as \(T\ra T\).

Since \(\forall\) is in our language, we can write one function \(\la y. \la x. x\) encompassing all of these, whose type is \(\forall T ~.~ (T \ra T)\). This is known as the polymorphic identity function, since it can be applied to elements of many different types (after first being applied to the type of the element).

But \(\forall T \ra (T \ra T)\) is not complete according to our syntax for \(\forall\). We have to specify the domain of quantification of \(T\). Clearly, it is \(\textrm{Type}\), and the complete term is \(\forall (T : \textrm{Type}) ~.~ (T \ra T)\). In order to be able to say this, we have to add \(\textrm{Type}\) to our language of terms, as a constant. If we do this, it has to have a type itself.

For the sake of simplicity, we are going to say that \(\textrm{Type}\) has type \(\textrm{Type}\). That is, \(\textrm{Type}:\textrm{Type}\) should typecheck. This was the decision taken by Per Martin-Löf in his first version of intuitionistic type theory (1971), and is the decision taken by the Haskell implementors in upcoming releases, as well as by several tutorials on the subject from which I am drawing. However, this is not a good decision from the point of view of proof assistants. Jean-Yves Girard proved in his PhD thesis (1972) that this results in an inconsistent logic.

The form of \(\textrm{Type}:\textrm{Type}\) is reminiscent of the self-reference in Russell’s paradox, but the proof of inconsistency is not as direct. It is a roundabout construction that we are not likely to encounter. Nonetheless, any implementation of dependent types that has the goal of being logically consistent must avoid this choice. The solution is not difficult, but it will be a distraction to us at this point. The proofs we are interested in will work both with \(\textrm{Type}:\textrm{Type}\) and with the more complicated solution that avoids inconsistency. For those interested, I will sketch below (section 3.2.7, optional) how to fix this issue, but for now, let’s not worry about it.

Another deviation from rigourous correctness I will make at this point is that I will stop writing out all the inference rules. Some of them will be inherent in the code, which can be easier to understand than an equivalent set of rules. I’ve already been doing this in a sneaky fashion; lookup judgments, even in our most basic propositional system, require formal rules, but I have simply used Racket’s association list lookup function. This means you have to pay even more attention to the code. Don’t just trust me or past users; use your own critical facilities.

Challenge: keep track of all changes and additions to the inference rules. Some of the references in the Resources chapter can help with verifying your work.

Adding \(\textrm{Type}\) as a constant to Proust’s term language will be straightforward. But adding code implementing the rules for \(\forall\) requires a precise definition of substitution, which I have been putting off. I will put it off a little longer, in order to discuss other consequences of moving to dependent types.

Besides \(\textrm{Type}\), we don’t have any other type constants. The base types we used in propositional logic are gone (as is the \(\textrm{Var}_\mathit{wf}\) rule). We can translate theorems of propositional logic into theorems of predicate logic by quantifying over the base types, which will then be interpreted as type variables. For example, the theorem \(A \ra (A \ra B) \ra B\) from propositional logic becomes \(\forall A~B:\mathrm{Type}~.~ A \ra (A \ra B) \ra B\), and the proof term \(\la x. \la f.f~x\) from propositional logic becomes \(\la A. \la B. \la x. \la f.f~x\). (You may wish to verify this by drawing a proof tree on paper.)

We don’t have the other logical connectives yet, but their rules in predicate logic are straightforward adaptations of their rules in propositional logic. In this manner, predicate logic subsumes all of propositional logic, and our implementation can be extended in a similar fashion.

To facilitate the discussion, let’s postulate an additional type constant \(\mathrm{Bool}\), the type of Booleans. We’re going to add this later, and we don’t need any properties of it now, except that \(\mathrm{Bool}:\mathrm{Type}\) holds. We can apply the polymorphic identity function defined above to it. Informally using the name \(\mathit{id}\) as shorthand for the full definition of the polymorphic identity function, we would form the expression \(((\mathit{id}~\mathrm{Type})~\mathrm{Bool})\). Intuitively, this expression should evaluate to just \(\mathrm{Bool}\).

We can show that \(((\mathit{id}~\mathrm{Type})~\mathrm{Bool}) : \mathrm{Type}\) holds. Because we have mingled terms and types, an expression like \(((\mathit{id}~\mathrm{Type})~\mathrm{Bool})\) can indeed show up to the right of a colon, in "type-land". That is, we might need to determine whether or not some other expression \(e\) has type \(((\mathit{id}~\mathrm{Type})~\mathrm{Bool})\). This should have the same answer as whether or not \(e\) has type \(\mathrm{Bool}\).

That is our intuition, but is it justified? Recall the BHK interpretation of for-all:

"A proof of \(\forall X:T . W\) is a function that transforms a proof \(x\) of \(T\) into a proof of \(W[X\mapsto x]\)".

Looking at the effect of applying such a function to such an \(x\) on the type level, we see a single step of computation in the lambda calculus: applying a lambda to an argument means substituting the argument for the variable of the lambda everywhere in the body of the lambda. This is not a coincidence. Alonzo Church, the creator of the lambda calculus, was a logician, and he defined the lambda calculus for logical purposes. We are fortunate that our chosen implementation language happens to be based on the lambda calculus, so the intuitive notion of computation we get from it is just what is required here.

To summarize, we’ve just seen a need for computation to take place during typechecking (though we’re still vague on exactly where that happens). We want to introduce computation anyway, because we want to prove theorems about programs, but even if we didn’t have this ambition, we’d still have to talk about it, because we are using dependent types. The computation that takes place during typechecking and the computations we will define in order to prove theorems about them will use the same model, which is based on substitution, just as with our mental model of Racket function application.

A conventional treatment of first-order logic doesn’t have to talk about computation, but it does have to discuss substitution. Some treatments try to get away with just the intuitive idea of substitution, but this can lead to problems even with on-paper proofs. Furthermore, to add computation to first-order logic, the system must be expanded with rules for the computational model, whereas here we’ve already done the work.

It all hinges on substitution, and the time has come to be precise about that.

3.2.2 Substitution and computation

The issues with substitution are the same for \(\forall\) and for \(\la\); both are binding constructs, giving a local meaning to their variables. It is probably easier for computer scientists to understand the issues when explained using \(\la\).

We did not give a computational meaning to proof terms when discussing propositional logic. They were just concise representations of proof trees. But the computational meaning is familiar to you from learning Racket, even if the syntax is different. You know that \(\la x.x\) and \(\la y.y\) are syntactically distinct (our representations of them are not structurally equal, as checked by Racket’s function equal?) but they really both represent the identity function. The names of parameters are not important to the computation (though proper naming of parameters is important for human readers). But \(\la x.x\) and \(\la x.y\) are not the same function. The first is the identity function, which always produces its argument, and the second is the function which ignores its argument and produces \(y\) (sometimes called the "constant-y" function).

You might object to \(\la x.y\), because \(y\) is free, that is, it is not bound by a lambda and doesn’t have an apparent meaning. In Racket, we tend to not have to worry about free variables, as every variable must have a binding or meaning somewhere (otherwise Racket would complain about an undefined identifier). Furthermore, the notion of substitution discussed in HtDP and FICS doesn’t substitute inside the body of lambdas, as tends to be common practice in programming languages. When a substitution does happen, it is a substitution of a value (not a more complicated expression) for a variable. Once again, this is done for practical purposes (it is more efficient). Consequently, in Racket (and many other languages), substitution involving closed terms always produces a closed term. This makes substitution simpler.

Here, we are taking off binders when forming the premise of a use of the for-all introduction rule, and later we’ll encounter situations in which we have to substitute under binders also. So we can’t avoid dealing with free variables. This is one source of the technical side conditions I left out when describing the inference rules for first-order logic. It’s unavoidable even in a conventional presentation done correctly.

Let’s try to define substitution for lambdas in a way that respects our intuition above. The definition will be recursive in the structure of expressions, so we can implement it using structural recursion. What should happen when substituting into a variable? There are two cases, depending on whether or not the variable being substituted into is equal to the variable being substituted for.

\begin{align*}x[x \mapsto s] &= s\\ y[x \mapsto s] &= y\end{align*}

Substitution into an application just substitutes into the two parts.

\begin{align*}(t_1~t_2)[x \mapsto s] &= (t_1[x \mapsto s]) (t_2[x \mapsto s])\end{align*}

We can’t do the same for lambda, because again there are two cases. If we are substituting for \(x\) into a \(\la y.b\), where \(y\) is different from \(x\), then we should go ahead and substitute into the body \(b\). But we are substituting for \(x\) into a \(\la x.b\), nothing should change in the body \(b\). The \(\la x\) introduces a new local name \(x\) and a new local scope.

Even this does not handle all cases involving free variables. Consider \((\la x.y)[y\mapsto x]\). Going ahead and substituting would give \(\la x.x\), which is not right. The substitution \(y\mapsto x\) is referring to a version of \(x\) outside the scope of the \(\la x\), but naive substitution puts the \(x\) being substituted into a scope in which \(x\) has a different meaning. This problem is called variable capture, because the \(x\) in the substitution is being "captured" by the lambda, changing its meaning.

What we need to do is first rewrite \(\la x.y\) as \(\la z.y\) for some choice of \(z\), and then do the substitution, giving \(\la z.x\), which has the right behaviour. The same issue would arise if what was being substituted for \(y\) was a more complex expression \(s\), where \(x\) is free in \(s\). So \(z\) has to be chosen so that it doesn’t occur free in \(s\).

In the example, we just changed the \(x\) in \(\la x\) to \(z\), but in general, if \(y\) is replaced by a more complex expression \(t\) (that is, we are rewriting \(\la x . t\)), we have to go through \(t\) and make the same substitution. What conditions does the choice of \(z\) have to satisfy with respect to \(t\)?

We can’t choose a \(z\) that is free in \(t\). Consider \((\la x . y ~ z)[y \mapsto x]\). If we first changed \(\la x . y ~ z\) to \(\la z . y ~ z\), and continued with \((y~z)[y \mapsto x]\), we would end up with \(\la z . x ~ z\), which is incorrect. But if we chose \(w\) instead of \(z\) to replace \(x\) in \(\la x\), we would end up with \(\la w . x ~ z\), which is correct.

There is one more condition on the choice of \(z\), which is that it cannot occur as a binder in the body of the \(\la x\). Consider \((\la x . \la z . x)[y\mapsto x]\). If we first changed \(\la x . \la z . x\) to \(\la z . \la z . z\), and then continued with \((\la z . x)[y\mapsto x]\), we would get \(\la z . \la z . z\), which is not correct. If we instead choose \(w\) as the new variable, we get \(\la w . \la z . w\), which is correct.

Here are all the rules summarized.

\begin{align*}(\lambda x. t)[x \mapsto s] &= \lambda x. t\\ (\lambda x. t)[y \mapsto s] &= \lambda x. (t[y \mapsto s])\\ &~~~~x~\mbox{not free in}~s\\ (\lambda x. t)[y \mapsto s] &= \lambda z. ((t[x\mapsto z])[y \mapsto s])\\ &~~~~x~\mbox{free in}~s,~z~\mbox{not free in}~s~\mbox{or}~t,~z~\mbox{not a binder in}~t\end{align*}

If you have not seen this definition before, you are probably glad to have been spared it until now. You may be asking yourself, how do we know we have gotten it right, that we haven’t missed some other case or other side condition? One answer is that we can formally prove that this definition has the properties we want of substitution, and that theorems about the ways we use substitution (for example, in computation) can also be proved formally. Some of the references in the Resources chapter do this.

3.2.3 Implementing computation

We don’t have a use for computation in propositional logic, but let’s add it to proust-pred-start.rkt, which currently only handles propositional logic. To avoid confusion, we’ll strip out all the types (hence all the logic!) and call it proust-just-comp.rkt. This may seem alarming, but types play no role in computation. Types can tell us something about the result of computation, since typically we define types so that if an expression has type \(T\), then when we evaluate it, the result should also have type \(T\). But the process of evaluation does not involve types.

In order to implement substitution, we need ways to check if a variable is free in a term and if a variable is a binder in a term. The simplest way to do this is to just descend through the term recursively, looking for places it might be free or a binder, respectively. Since these searches are very similar, we combine them into a single function.

The definition of substitution in the previous subsection, in mathematical form, says that the variable \(z\) we introduce to avoid capture substitution must not be a binder in the term being substituted into. In an implementation, we actually have to generate a specific variable. Again, we take a simple but possibly inefficient approach: we stick an underscore on the end of the variable we have to change (\(x\) in the rules above) and redo the test, repeating until it works. In practice, we have to strike a balance between not enough rewriting, which will lead to bugs, and too much rewriting, which will lead to unreadable error messages or results.

Because some of the side conditions require looking at more than one expression, the helper function refresh consumes a variable x and a list of expressions. The side condition helper function sc-helper has as its last parameter a Boolean value specifying whether or not to check if x occurs as a binder in an expression.

Challenge: Racket has a function called gensym which creates a symbol guaranteed not be in use. Both this and our simpler option change the name, and we’d want to change it back in the pretty-printing. Racket also has support for sets as a datatype, allowing us to calculate the set of free variables in a term only once. Use these ideas to improve the efficiency and usability of substitution.

We could define computation using inference rules, and that is what we would do if we wanted a mathematically precise definition. If an expression is a lambda applied to an argument subexpression, then one step of computation consists of substituting the argument for the variable of the lambda, in the body of the lambda. But we also need rules to allow subexpressions to step. For example, if \(a\) steps to \(b\), then \(f~a\) steps to \(f~b\). Then we can define multiple steps as either zero steps or one step followed by multiple steps, and finally define a full computation as reducing an expression by stepping until it cannot be reduced further.

That doesn’t give us much guidance on implementation, and it’s easy to construct an inefficient algorithm. We fared better with bidirectional typing because it used structural recursion, but computation doesn’t. Thinking directly about a Racket implementation will be more fruitful.

If we want to reduce an expression, there are three cases. A variable cannot be reduced further. To reduce a lambda, reduce its body. To reduce an application, reduce the expressions in function position and argument position. If the expression in function position reduces to a lambda, do the substitution, then reduce the result (this is not structural recursion). The Racket code is a direct translation of this paragraph.

The code reduces in the bodies of lambdas, even though I said above that this is not done in most programming languages. I’ll discuss the reasons for this below. The full code is linked in the Handouts chapter as proust-just-comp.rkt.

3.2.4 Back to predicate logic

When we move back to our previous setting, namely trying to add rules for for-all to our minimal propositional system with only implication, we have to add to some of the code above. Here is the grammar so far.

To replace the dot in our human-readable for-all notation, I have chosen single right-arrow (made with a hyphen and greater-than characters) because for-all generalizes implication (also retained for convenience and readability). Previously, we extended this grammar to allow the removal of parentheses on multiple applications and multiple arrows. We can do that, and in addition, allow multiple arguments in for-alls and lambdas.

Since implication is now redundant, we can remove it as an AST node type, but leave it in the user term language, to be desugared by the parser (as we did with negation) into an instance of \(\forall\) with an underscore ("don’t care") as the binding variable. We’ll also allow underscore as a binding variable in a lambda, but it can’t be used as an occurrence of a variable. That is, we can write \(\la x . \la y . y\) or \(\la ~\_ . \la y . y\) (which are the same, in a sense to be formalized below), but we can’t write \(\la x . \la ~\_ ~.~ \_\) (the rightmost use of underscore isn’t allowed).

The Arrow data structure, being now used for for-all, is now more general, so we need to put more information (the name of the variable) into the AST node.

(struct Arrow (var domain range) #:transparent)

We need to change the parsing and pretty-printing functions (not further described here; the full code is linked below).

Extending substitution to the syntax not present in proust-pred-start.rkt is not difficult. The code for for-all resembles the code for lambda; the code for annotation and the function type resemble the code for function application.

Since the sc-helper function that does most of the work in checking side conditions works by structural recursion on the AST, it also has to handle all the possibilities.

For reduction, all the added code resembles the code for function application, except for the annotation case, where the type annotation is simply dropped.

We still have to nail down the role of reduction in typechecking. But there are some lessons to be learned from substitution. We sometimes have to change the name of a variable introduced by a binder to avoid variable capture. As a result of these rewritings, we may compute a lambda or for-all that doesn’t look exactly like we expect, but is the same up to the choices of variable names. We should regard these as the same. This is known as alpha-equivalence.

We need to use this notion when we check types for equality, notably in the "turn" rule, where to check a type, we synthesize it and then compare to what we thought it should be. We used structural equality before, but we really should use alpha-equivalence.

A typical treatment of these issues usually mentions alpha-equivalence, but uses it to gloss over difficulties in substitution, assuming a human reader knows how to tweak things to avoid difficulty. (This is sometimes known as the Barendregt convention, after an author who has published extensively on the lambda calculus.)

But in implementing these ideas on a computer, we have to get all the details straight. To the best of my knowledge, no mathematician before Church (1936) really took these matters seriously. Much of Curry’s work deals with a setting where lambda is absent, replaced by specific combinators (which consume and produce functions). For example, we can have a combinator which composes two functions. This avoids the complications of naming (and definitely simplifies metamathematical proofs), at the cost of making "programming" more difficult.

Another solution to this problem was pioneered by de Bruijn, who replaced names by a number indicating lexical depth. \(\la x. \la y. x\) becomes \(\la . \la . 1\), and \(\la x . \la y. y\) becomes \(\la . \la . 0\). This is hard for humans to read, and the definition of substitution is a bit more complicated, but this representation (called de Bruijn notation) is used a lot in real implementations of statically-typed functional programming languages. It also simplifies the metamathematics (proofs of theorems like soundness). There are a number of hybrid and alternative approaches. This topic gets a lot of attention in programming language research circles, and we will look at it again in a later, optional chapter.

We need to write code to decide the alpha-equivalence of two expressions. Having defined substitution and variable-refreshing, we could use simultaneous almost-structural recursion on the two expressions, similar to checking for structural equality. When we reach, say, a \(\la x.t\) and \(\la y.w\), we compute a new variable \(z\) fresh for both \(t\) and \(w\), and continue the recursion on \(t[x\mapsto z]\) and \(w[x\mapsto z]\).

But there is a simpler and more direct approach. Instead of renaming with a fresh \(z\), we maintain an association list of correspondences between binders in the first expression and binders in the second. In the situation above, we add the association of \(x\) and \(y\) to the list, and continue recursion on the bodies \(t\) and \(w\). When the recursion bottoms out with a use of variables, either they must be associated in the list (because they were bound at the same point in the recursion) or they must be the same variable (which occurs free at the same point in both expressions).

That last definition is there because we are about to use an even more expansive notion of equivalence, and we will change the definition of equiv?.

Racket’s and form is not a function, but a macro, because it does short-cutting: if the first argument evaluates to false, it will not evaluate the second argument. So this implementation of alpha-equivalence might stop early, if it detects a mismatch. As stated earlier, here we prioritize readability above efficiency, but such considerations are important in systems intended for real use.

Alpha-equivalence is analogous to modular arithmetic, where instead of being restricted to statements like \(7 = 7\), we can say \(7 \equiv 3 \pmod 4\). But we typically go further and say things like \((1 + 6) \equiv (2 + 1) \pmod 4\). The analogue in our typechecking situation (where instead of addition, we have function application) is to consider two types equal exactly when, after reducing each one, they are alpha-equivalent. If we don’t do the reductions, then our code might consider two different ways of describing the same type as unequal, and this will limit the usefulness of our system.

(define (equiv? e1 e2) (alpha-equiv? (reduce e1) (reduce e2)))

This definition of type equivalence, called definitional equality, has proved very useful in practice, but it is not the only choice that can be made at this point.

Once again, there are opportunities for improving efficiency. Fully reduced expressions can be quite large, and it might be better to reduce on the fly, since the equivalence check might stop early.

The one place we are using type equivalence so far is the turn rule. But there may be other places where reduction might be needed. Here is the rule for for-all elimination again.

\[\ir{(\forall_{E})} {\Gamma\vdash f\Ra\forall x:T. W ~~~ \Gamma\vdash t\La T} {\Gamma\vdash f~t\Ra W[x\mapsto t]}\]

In our code so far, we synthesize the type of \(f\), verify with a match that it is of the form \(\forall x:T. W\), and then check that \(t\) has type \(T\). We have no guarantee that the synthesis algorithm produces fully-reduced types. We could try to ensure this, but it could be tricky to maintain as we add features, and it could be inefficient. Instead, we’ll reduce the synthesized type before doing the match.

Here is another example of the same issue, in the rule for for-all introduction (leaving off the side conditions).

\[\ir{(\forall_{I})} {\Gamma\vdash \forall (x:T)\ra W \Ra\textrm{Type} ~~~ \Gamma,x: T\vdash t\La W} {\Gamma\vdash\la x.t\La\forall x:T. W}\]

The code synthesizes the type of \(\la x.t\), and then verifies with a match that it is an arrow type before continuing. Once again, we should reduce the synthesized type before the match. In general, if we synthesize a type (or the user provides one), and we need it to be of a certain form, we should reduce it first before verifying.

We will use full reduction in our implementation, but more efficient methods are available here also. We could reduce just far enough to see that the top constructor is for an arrow type, and not fully reduce its subexpressions. Stated in more generality, this is known as reduction to weak head normal form (WHNF), and it is an important technique in programming languages. Being aware of weak reduction can help us to understand what full-featured proof assistants like Agda or Coq are doing in certain situations.

We are almost ready to write the full code for type checking and synthesis. There were three issues we put off until later, and the time has arrived to deal with them. One was that whenever we add a variable \(x\) to a context \(\Gamma\), we must check that it is not already there. If it is, we refresh it with respect to the context and whatever else it must not clash with. This is a generalization of our previous function refresh, and the definitions required are short.

The second issue had to do with the new rule for checking the type of a lambda, which you can see just above. We’d like to relax the condition that \(x\) is the binder in both the lambda and the for-all, that is, we’ll allow alpha-equivalent variations. It’s simplest and often the most natural to have them be the same variable when writing a term annotated with its type directly by hand. But this rule could be used in a recursive check where the type has been subject to renaming or otherwise generated by code.

If instead the type is \(\forall (x_1:T). W\), we can check if \(x\) satisfies the side conditions with respect to \(\Gamma\) and the type, and if so, just alpha-rename \(x_1\) to \(x\) in the type. But if not, then we need to freshen \(x\) with respect to the context, the term, and the type, and then replace \(x\) with the fresh variable in both the term and the type.

The third issue is the use of underscores, which requires some special cases. If one of the term or type has an underscore as variable and the other does not, then we try to use the actual variable to replace the underscore (checking the requisite conditions), and if we can’t, we freshen and substitute into both, as above.

Here’s the code. Parts of it look long, but they are mostly just variations on the same basic idea, trying to minimizing the amount of rewriting done.

This code is not practically usable without definitions. Testing it would require building up successively larger expressions using cut and paste.

3.2.5 Adding definitions

When developing Proust for propositional logic, we used holes, which were very convenient for interactive development. They are also convenient for predicate logic, as we will see when looking at Agda and Coq, but it is considerably more difficult to add them. I will defer a principled treatment of holes in the context of dependent types to a later, optional chapter.

We could put in holes just as we did for propositional logic, and let them typecheck as anything. But we cannot do refinement in the same way. It is no longer the case that we can fill in one hole with anything that has the type we associated with the hole during typechecking. In the presence of dependent types, there can be also be dependencies between holes. Handling these dependencies can be complicated, and neglecting them can lead the user into blind alleys.

Global definitions can serve as a partial substitute, so at least we can build up terms incrementally. They also reduce the size of terms by shrinking repeated subexpressions.

We’ll implement definitions with two global association lists, one for definitions (mapping names to terms) and one for the types of defined terms (mapping names to types). There are more efficient ways to do this, but once again this is easy to code and understand. You will miss holes when you do the exercises, but they return with even more sophistication with Agda and Coq, which we will get to soon.

Refactored Proust for propositional logic interpreted a symbol not in the current context as a propositional variable. But in Proust for predicate logic, the only variables are the ones introduced by binding forms. So if a symbol is not in the context or global definitions, it has no meaning, and an error must be raised.

We need to add a line in type-synth looking up the type of a variable that might be a global definition (after first looking for it in the context).

Fully reducing an expression means expanding definitions, so we need something similar there. But reduce does not have the context as an argument, and that must be added.

The full code is available in proust-pred-forall.rkt, with the beginnings of a test suite that also shows how one might use Proust to prove theorems in predicate logic.

For propositional logic, there was a clear correspondence between the tree structure of a proof built by inference rules and the tree structure of the concise proof term we used. That correspondence no longer holds for our proof terms for predicate logic. The computational steps (reductions) are not explicitly represented in the proof terms. They are verified when the proof term is typechecked.

The omission of the computations in our proof terms makes them more concise than proof trees. Informal proofs are also more concise, with the brain of the expert reader filling in what’s left out. But it’s not as easy to get a machine to check an informal proof. Here the omissions correspond nicely to what a machine can do, and furthermore, the computations take place in a simple computational model that we understand (one very similar to what we have been using to construct our proof assistant), so the proof terms remain comprehensible to us.

3.2.6 Simulating other features

This subsection and the next one are optional reading.

Alonzo Church, in his 1936 work, argued that the lambda calculus was a general model of computation by showing how it could simulate Booleans, pairs, and arithmetic. That was in an untyped setting. That implementation cannot be tweaked to typecheck in the simply-typed lambda calculus, or in the version of the lambda calculus corresponding to first-order quantification. John Reynolds showed how to extend the simply-typed lambda calculus with quantification over types so that Church’s implementation would typecheck. This can be done in the higher-order language we are now working with.

As you can imagine, this involves heavy use of lambda, and this provides further justification for our decision to reduce applications of lambda anywhere in the expression. Otherwise, in the simulation of arithmetic, the simulation of \(1 + 1\) is not the same as \(2\); each results in a lambda, and reduction only at the root of each expression does not make the bodies identical. This will also be an issue when we add the natural numbers in a direct fashion via new constructs with introduction and elimination rules, as we will do shortly.

You are familiar with Booleans from prior programming experience, as well as our discussion of the Boolean interpretation. The general idea of Church’s encodings is to encode values by their eliminators. How do we eliminate or use a Boolean value? With an if-then-else. That is, a Boolean value b will be encoded by the function that consumes two things and produces the first if b is true and the second if it is false.

This leads to the following definitions in the untyped lambda calculus:

\begin{align*}\textrm{true} &= \lambda x. \lambda y. x\\ \textrm{false} &= \lambda x. \lambda y. y\\ \textrm{if} &= \lambda b. \lambda t. \lambda f.~ b~t~f\end{align*}

We can use polymorphism to define typed versions of these in Proust. First of all, we need a type that works for both \(\textrm{true}\) and \(\textrm{false}\). This one does.

(def 'bool '((∀ (X : Type) -> (X -> X -> X)) : Type))

That might seem a bit generous, but it is possible to show that versions of \(\textrm{true}\) and \(\textrm{false}\) are the only values of this type. Here are those versions.

And we can now easily type a version of \(\textrm{if}\).

This, in turn, can be used to code Boolean functions.

The same ideas can be made to work for the logical connectives, pairs, and natural numbers. I’ll sketch the ideas, and you can work out the details as a challenge.

Logical AND (\(\land\)) will be a function consuming two types and producing a type.

(def 'and '(? : (Type -> (Type -> Type))))

Using the general idea that an encoding of a datatype is the type of an eliminator, we would like the replacement for ? to be the type of an AND eliminator. But there are two eliminators for AND. So we use polymorphism to generalize the type to encompass both.

(def 'and '((λ p => (λ q => (∀ (c : Type) -> ((p -> (q -> c)) -> c))))

: (Type -> (Type -> Type))))

Now you can finish the definitions of conj (which is \(\land\)-intro), proj1 (which is \(\land\)-elim0), proj2 (which is \(\land\)-elim1), and the proof that AND is commutative, by filling in the holes below.

(def 'conj '(? : (∀ (p : Type) -> (∀ (q : Type) -> (p -> (q -> ((and p) q)))))))

(def 'proj1 '(? : (∀ (p : Type) -> (∀ (q : Type) -> (((and p) q) -> p)))))

(def 'proj2 '(? : (∀ (p : Type) -> (∀ (q : Type) -> (((and p) q) -> q)))))

(def 'and-commutes '(? : (∀ (p : Type) -> (∀ (q : Type) -> (((and p) q) -> ((and q) p))))))

Next, you will tackle natural numbers. How might we use or eliminate a natural number? By iterating. A general form of iteration using a natural number \(n\) would consume a function and a base value to which the function should be applied \(n\) times. Using this idea, fill in the holes in the following definitions.

(def 'nat '((∀ (x : Type) -> ((x -> x) -> x -> x)) : Type))

(def 'z '(? : nat))

(def 's '(? : (nat -> nat)))

(def 'one '((s z) : nat))

(def 'two '((s (s z)) : nat))

(def 'plus '(? : (nat -> (nat -> nat))))

You should be able to prove that, for example, ((plus one) one) equals two, though since we have not implemented equality in Proust’s term language yet, all you can do is show that these two are equal using equiv?. But you will not be able to prove facts about this version of the natural numbers that require induction.

If you’re still curious, you might figure out how to tackle logical OR, logical NOT, and lists. (The eliminator of a list is its foldr function specialized to that list.)

These simulations are intellectually interesting, but they can be inefficient (especially the natural numbers), and they are somewhat awkward to use. Furthermore, there are certain things we would like to prove but cannot (for example, that simulated 0 is not equal to simulated 1). For these reasons, it makes sense to add these features directly, which we do below. As we will see, Agda and Coq provide a general mechanism to define new recursive datatypes. Rather than leap to this level of generality, we will create each of our datatype additions to Proust individually, to gain intuition before moving to these languages and their more general settings.

3.2.7 Neither proof nor assistant

We designed Proust as a proof assistant, but it cannot reliably prove things because of \(\textrm{Type}:\textrm{Type}\), and it does not offer interactive development of proofs by refining holes. The first of these is relatively easy to fix, but the second is not. In this subsection (which is also optional reading), I will briefly discuss this.

The easiest (but not most general) way to fix \(\textrm{Type}:\textrm{Type}\) is to create another type for \(\textrm{Type}\), by declaring \(\textrm{Type}:\textrm{Kind}\). We’re going to leave \(\textrm{Kind}\) out of our language of proofs and only use it internally in Proust. Both \(\textrm{Type}\) and \(\textrm{Kind}\) are called sorts. What we have is a two-sorted type system.

A for-all type (or Arrow type in Proust’s code) can quantify over something whose type is a sort (previously it had to be \(\textrm{Type}\)). The body of the for-all has to synthesize in a context where the quantified variable is added (as before), but now the result has to be a sort (previously it had to be \(\textrm{Type}\)), and the whole for-all type types as that sort (previously it typed as \(\textrm{Type}\)). The only other place where \(\textrm{Kind}\) has to be handled is in reduce.

That’s the extent of the changes, only a few lines, but a bit hard to motivate. The result is a two-sorted pure type system that implements the Calculus of Constructions in its original form. This turns out to not be quite enough when one starts to seriously work through proofs, and one runs across situations where it would be nice to quantify over \(\textrm{Kind}\). The solution is another construction originally used by Russell: a universe hierarchy (sometimes called ramified types). We could say \(\textrm{Type_0}:\textrm{Type_1}\), \(\textrm{Type_1}:\textrm{Type_2}\), and so on. The \(\textrm{Type}\) and \(\textrm{Kind}\) rules above are adjusted so that a for-all type lives in the universe which is just large enough to contain what it quantifies over and what its body produces. This can also be done in a few lines of code.

Challenge: adapt proust-pred-forall-works.rkt to implement each of these ideas.

Both Coq and Agda maintain a universe hierarchy, and hide the details from the user until they become relevant. We would do this in Proust as well if our goal was a fully-usable proof assistant. Certain concepts (equality, for example) show up in multiple universes, and it would be nice to just implement them once. This is known as "universe polymorphism".

Bringing back holes and refinement is not a matter of a few lines of code. The basic idea is to replace each hole with a metavariable, and then collect equations relating these metavariables during typechecking. This is also done in Hindley-Milner type inference (as implemented in OCaml and Haskell), and the algorithm to solve the equations is called unification. In the case of Hindley-Milner type inference, the algorithm is more or less the obvious one. If \(\textrm{Nat}\ra X = Y \ra \textrm{Bool}\), then \(X = \textrm{Bool}\) and \(Y = \textrm{Nat}\). More generally, an equation implies more equations between subterms, which eventually become as simple as the above example.

But that is first-order unification, with a fixed set of type constructors. If a metavariable could show up in constructor position, we have higher-order unification, which is undecidable. This is roughly what happens when dependent types are involved. Coq and Agda use algorithms that are not guaranteed to work, but which mostly work well in practice. At times they will report a "cannot unify" error. Sometimes this is because the equations cannot be solved, and sometimes it is because the algorithm is inadequate.

A later, optional chapter will expand on the last two paragraphs, and the Resources chapter has suggestions if you wish to read more about these topics from primary sources.

3.2.8 Equality, Booleans, and arithmetic

It’s worth summarizing what Proust code needs to be added to when we add a new feature.

• Parsing, pretty-printing;

• Alpha equivalence;

• Substitution, free variable check;

• Reduction;

• Type checking and synthesis.

First, let’s add the equality relation, because without some relation, we can’t form logical statements about values. The equality relation is the most general and useful, though perhaps not the easiest to add. The code is available in proust-pred-eq.rkt.

We have two notions of equality already: structural equality (equal? in Racket) and definitional equality (equiv? in Proust). To these we will add propositional equality, which is how we talk about equality in propositions, and how references to it are interpreted. Our implementation of this adds syntax to let user code access our previously-internal notion of definitional equality. In our term language, we will use the traditional infix \(=\) for equality.

We parse this sort of expression into a new two-field Teq structure. Type expressions using equality are validated with the following inference rule.

\[\ir{(=_\mathit{wf})}{\Gamma\vdash t\Ra T ~~~\Gamma\vdash w\La T}{\Gamma\vdash (t = w)\Ra \textrm{Type}}\]

This is what the code does. But if the turn rule is used for \(\Gamma\vdash w\La T\), it will be as if the following inference rule is used (writing \(\equiv\) for definitional equality), which may be clearer:

\[\ir{(=_\mathit{wf})}{\Gamma\vdash t\Ra T ~~~\Gamma\vdash w\Ra W ~~~T\equiv W } {\Gamma\vdash (t = w)\Ra \textrm{Type}}\]

The term for equality introduction is formed by a new infix constructor with one argument, eq-refl, which witnesses reflexivity (\(x\) is equal to \(x\)). We synthesize the type of \(x\) (but make no use of it) to confirm the well-formedness of the type we are synthesizing (\(x = x\)).

\[\ir{(=_I)}{\Gamma\vdash x \Ra T}{\Gamma\vdash (\textrm{eq-refl}~x)\Ra (x = x)}\]

At first glance, eq-refl seems useless. What good is a proof of \(x = x\)? But remember that we are exposing definitional equality, which is more general than structural equality. If we have two expressions e1 and e2, which both reduce to the same expression e3 in a given context, then the type (e1 = e2) will be well-typed in that context, and the term (eq-refl e3) will be a value of that type. In fact, so will (eq-refl e1) and (eq-refl e2). This is another situation where the computational steps built into our typechecking will make proof terms shorter.

How do we use an equality in an informal proof? We do substitution of "equals for equals". For example, we might have the equality \(3=1+2\), and we might then substitute the expression \(1+2\) for \(3\) in some logical formula.

We don’t yet have natural numbers or addition implemented in our system. But we’re used to thinking about them, so let’s derive the elimination principle for equality by starting with the above example, and gradually generalizing it.

If we just wanted to use the equality \(3=1+2\), we might have some logical formula \(S\) in which we might want to substitute \(1+2\) for \(3\). It is tempting to write this as \(S[3\mapsto 1+2]\). But our definition of substitution does not allow an expression like \(3\) to appear on the left-hand side of \(\mapsto\); it has to be an variable. Furthermore, we might not want to substitute for every occurrence of \(3\), but just for some of them. For example, if \(S\) is \(3+3=6\), we might wish to substitute to get \((1+2)+3=6\).

So let’s construct a formula \(P\) which looks like \(S\), but it uses a fresh variable \(x\) at the places where we have an occurrence of \(3\) that we want to substitute for. Then \(S\) is \(P[x\mapsto 3]\), and the result of the replacement of those occurrences of \(3\) by \(1+2\) would be \(P[x\mapsto 1+2]\). For our example, \(P\) would be \(x+3=6\).

Another way of thinking of this is that \(P\) is like a function that consumes an \(x\) of type \(\textrm{Nat}\) and produces a logical formula. In other words, \(P\) has type \(\textrm{Nat} \ra \textrm{Type}\). (This is even more general, since not all types are logical formulas, but that extra generality will come in handy.) We can ensure this interpretation if we put a \(\la x\) in front of the formula using the fresh variable \(x\). This avoids having to deal with fresh variables directly (our notions of alpha-equivalence and careful substitution will handle that for us).

We can now try to write out the type of the equality eliminator as specialized for this particular equality. If we have a proof of \((P~3)\), and a proof of \(3=1+2\), we can prove \((P~(1+2))\). This works for any \(P: \textrm{Nat} \ra \textrm{Type}\). So the type of the equality eliminator (which we will call \(\textrm{eq-elim}\)) will be:

\[\forall P: (\textrm{Nat} \ra \textrm{Type}) ~.~ (P~3)\ra (3=1+2) \ra (P~(1+2))\]

Now let’s generalize. Instead of just \(1+2\), we can use any expression \(y\) that types as \(\textrm{Nat}\), and work with a proof of \(3=y\). This gives us a more general type for the equality eliminator, namely:

\[\forall P: (\textrm{Nat} \ra \textrm{Type})~.~ (P~3)\ra \forall y: \textrm{Nat}~.~ (3=y) \ra (P~y)\]

We can similarly generalize \(3\) to an arbitrary expression \(x\) that types as \(\textrm{Nat}\), and work with a proof of \(x=y\), giving us:

\[\forall (x: Nat)~(P: \textrm{Nat} \ra \textrm{Type})~.~ (P~x)\ra \forall y: Nat~.~ (x=y) \ra (P~y)\]

Finally, we generalize to equalities over arbitrary types instead of just our not-yet-existent \(\textrm{Nat}\).

\[\forall (A:\textrm{Type})(x:A)(P: A\ra \textrm{Type})~.~ (P~x) \ra \forall y:A ~.~ (x=y)\ra (P ~y)\]

So, to use or eliminate a proof of an equality, we provide \(A,x,P\), a proof of \((P~x)\), \(y\), and a proof of \((x=y)\), and get a proof of \((P~y)\). Another way to view this is a statement that if \((x=y)\), then any property \(P\) that holds for \(x\) also holds for \(y\). If you squint hard enough, you can convince yourself that this is an induction principle for the set of \(y\) that are equal to \(x\). If you can’t, don’t worry about this; the point is that equality can be treated as just another datatype, which is what Agda and Coq do.

Since we have to write out an explicit proof term using this eliminator in Proust, we can make it a little less tedious by synthesizing the type \(A\) from \(x\). This means that in the term language, the equality eliminator has five arguments instead of six. Here is the grammar rule:

And here is the inference rule:

\[\ir{(=_\mathit{elim})}{\Gamma\vdash x\Ra A ~~ \Gamma\vdash P \La A \ra \textrm{Type} ~~ \Gamma\vdash\mathit{px} \La (P~x) ~~ \Gamma\vdash y \La A ~~ \Gamma\vdash q\La(x = y)} {\Gamma\vdash(\textrm{eq-elim}~x~P~\mathit{px}~y~q) \Ra (P~y)}\]

How do we use such a rule in practice? Here is one possible approach. Suppose we have a proof \(w\) of an equality \(e_1 = e_2\), and a proof \(t\) of a logical statement \(s_1\) containing one or more occurrences of \(e_1\) as a subexpression. We want to selectively replace some (perhaps all) of those occurrences of \(e_1\) in \(s_1\) with \(e_2\), yielding a new logical statement \(s_2\) for which we’d like a proof. To form the \(P\) argument to \(\textrm{eq-elim}\), we find a fresh variable \(z\), replace with \(z\) each occurrence of \(e_1\) in \(s_1\) which we want substituted, and wrap the result in \(\la z\). This ensures that \((P~e_1)\) is \(s_1\) and \((P~e_2)\) is \(s_2\). The desired proof of \(s_2\) will be \((\textrm{eq-elim}~e_1~P~t~e_2~w)\).

There are a lot of changes to the code, but most of them are straightforward as we go through the checklist: parsing, pretty-printing, alpha equivalence, substitution, and the free variable check. The two interesting changes involve type synthesis and reduction. The code for type synthesis essentially checks the various parts of the type signature we have figured out for the eliminator. (There are other changes to type-synth, for example, to synthesize the type of an equality, but they are more straightforward.)

Following a suggestion of Astra Kolomatskaia, we type the application of Eq-elim not as (P y) but as (Pann y), where Pann is P annotated with its (checked) type. The reason for this is that in practice, P will often be a lambda, and this saves the user the burden of annotating it.

How do these new sorts of terms behave under reduction, which is where computation takes place? The result of reducing (Eq-refl x) is (Eq-refl (reduce x)). What about (Eq-elim x P px y peq)? We start by reducing peq. If the result is of the form (Eq-refl z), then both x and y must be definitionally equal to z. The result is supposed to be a proof of (P y). Given what we have learned, px is that proof, and we reduce that. On the other hand, if peq does not reduce to an application of Eq-refl, then we reduce the other arguments and wrap them up in Eq-elim again.

The code so far is linked in the Handouts chapter as proust-pred-eq.rkt. We can’t do much with this yet, because we don’t have many datatypes to work with. We do have the identity function, and the simulation of Booleans, which we can use in a few simple equalities.

Exercise 10: State and prove the properties that equality is symmetric and transitive. \(\blacksquare\)

Our definition of propositional equality in terms of definitional equality is not the only possibiity, and working with it for a while will raise questions in one’s mind. For example, it does not capture the mathematical notion that two functions are equal if and only if they are pointwise equal. Equivalence classes are used a lot in higher mathematics, and one might want a definition of equality that could more easily accommodate user-defined equivalence classes and the notion of quotients on sets. Homotopy type theory is one currently popular approach that provides an interesting alternative to what I have presented here.

We can do more with equality when we add more datatypes, which we will do right now.

To add Booleans directly (as opposed to simulations), we add to the term language the constants true, false, and Bool (which is the type of true and false). We parse these into new zero-field structures in an AST.

The introduction rules for these are pretty straightforward.

\[\ir{(\textrm{Bool}_\mathit{wf})}{}{\Gamma\vdash\textrm{Bool}\Ra\textrm{Type}} ~~~ \ir{(t_I)}{}{\Gamma\vdash\textrm{true}\Ra\textrm{Bool}} ~~~ \ir{(f_I)}{}{\Gamma\vdash\textrm{false}\Ra\textrm{Bool}} ~~~\]

Let’s think about the eliminator for Boolean values. In the simulation above, we used if-then-else. But I warned you that those simulations were limited. Here’s the definition we used in the simulation. Focus on the type.

This is very much a computational definition. In effect, the eliminator consumes a Boolean value (the test of the if), and two values of the same type X (the "then" and "else" clauses) and produces one of them (which has type X). We are working on a proof assistant, so we also need ways of proving things about Boolean values. But the computational aspect is more familiar to us, so let’s stick with it for a bit.

Do the two clauses (then-else) need to have the same type? That is the practice in most statically-typed programming languages, but we have dependent types in our language, which most languages do not.

Suppose we try to have the two clauses produce different types, say T and W respectively. Then what would the result type be? It would depend on the value of the Boolean test. That’s where dependent types can be useful. If the Boolean test value is b, then the result type is something like "if b then T else W".

To express this using dependent types, we need to create a function \(P:\textrm{Bool}\ra\textrm{Type}\), such that \(P~\textrm{true} = T\) and \(P~\textrm{false} = W\). Then the type of the result is simply \(P~b\).

So the type of the eliminator seems to be \(\forall (P:\textrm{Bool}\ra\textrm{Type})~(b:\textrm{Bool})~.~ T \ra W \ra (P~b)\).
Substituting for \(T\) and \(W\), we get
\(\forall (P:\textrm{Bool}\ra\textrm{Type}) ~(b:\textrm{Bool})\ra (P~\textrm{true}) \ra (P~\textrm{false}) \ra (P~b)\).
Bringing the \(\forall b\) closer to where \(b\) is used, we get
\(\forall (P:\textrm{Bool}\ra\textrm{Type}) ~.~ (P~\textrm{true}) \ra (P~\textrm{false}) \ra \forall b:\textrm{Bool}~.~(P~b)\).

We did this from a computational point of view, to make if-then-else more general, and we still have to figure out how to implement it. What about the ability to prove things? It turns out that this eliminator is exactly what is needed.

The function \(P:\textrm{Bool}\ra\textrm{Type}\) can be viewed as describing a property of Booleans. Given a particular Boolean value \(b\), \(P~b\) is a type, which could be a logical statement, stating that \(P\) holds for \(b\). That logical statement may or may not be provable. The conclusion of the eliminator is \(\forall (b:\textrm{Bool})\ra(P~b)\). This is saying that the property holds for all Booleans. So the eliminator is giving us a way of proving for-all statements quantified over Booleans. Looking at the premises of the eliminator, we see that in order to prove such a statement, we need to show that \(P\) holds for arguments \(\textrm{true}\) and \(\textrm{false}\).

This seems like common sense. To prove that something holds for all members of a finite set (example: Booleans), show that it holds for each member of that set. The eliminator is formalizing this intuition. It can be viewed as an induction principle for Booleans. You know induction primarily as a way of proving for-all statements about the natural numbers. But the idea can be generalized to other types, even types such as Boolean that have a simple non-recursive definition (in effect, the definition only has base cases). Although this eliminator seems straightforward, the equivalent cannot be proved for our simulation of Booleans (another reason to add them directly).

We’ll call the elimination form in the term language Bool-ind, and it will have four arguments: \(P\), the terms of type \(P~\textrm{true}\) and \(P~\textrm{false}\), and \(b\) of type \(\textrm{Bool}\).

\[\ir{(\textrm{Bool}_\mathit{E})} {\Gamma\vdash P\La\textrm{Bool}\ra\textrm{Type} ~~ \Gamma\vdash\mathit{tp}\La(P~\textrm{true}) ~~\Gamma\vdash\mathit{fp}\La(P~\textrm{false}) ~~ \Gamma\vdash b\La\textrm{Bool}} {\Gamma\vdash(\textrm{bool-ind}~P~\mathit{tp}~\mathit{fp}~b)\Ra(P~b)}\]

Again, most of the changes resulting from this addition to the grammar are straightforward, though we have to go through the checklist and make sure they’re all done. The interesting ones are type synthesis and reduction. The additional code for type synthesis pretty much checks the type signature we worked out for the eliminator.

What would the result of reducing (Bool-ind P tp fp b) be? If reducing b does not yield one of true or false, all we can do is reduce the other arguments and then wrap them up again in a Bool-ind structure (in other words, use structural recursion). But if it yields true, then the result should have type (P true), that is, it should be the reduction of tp. The other case should now be obvious.

The similarity of the handling of the eliminator for equality and the eliminator for Booleans should now be more evident, and can serve as a guide for future additions. This code is linked in the Handouts chapter as proust-pred-bool.rkt.

Exercise 11: Define the Boolean \(\mathit{and}\) function, and prove that for all Booleans \(b\), \(\mathit{and}~b~b=b\). \(\blacksquare\)

This is the third time we have implemented computation in Proust, and it should now be clear what they have in common. Computation happens when an eliminator for a type is directly applied to a constructor for that type. With a for-all type, the eliminator is function application, and the constructor is lambda. If a lambda is directly applied to an expression, we substitute the expression into the body of the lambda and continue to reduce. Similarly, reduction makes computational progress when the eliminator eq-elim is applied to a proof of equality that is of the form (eq-refl x), and when the eliminator Bool-ind is applied to a Boolean expression that is either true or false. This pattern will continue with later additions.

With Booleans, we started with a computational notion, to generalize if-then-else to the dependent setting, and came up with an eliminator that is useful for proving things. We could also have gone the other way, starting with an induction principle for Booleans and specializing it to a form that is computationally useful. That approach will pay off as we move to natural numbers, because if you had ever seen induction before this stroll, chances are it was for natural numbers. I will sketch the ideas for the implementation of proust-pred-nat.rkt and you will complete it as an exercise.

We saw induction on lists in the Introduction chapter. Induction on natural numbers is even simpler. To prove a property holds for all natural numbers, prove that it holds for zero, and prove that for all \(n\), if the property holds for \(n\), then it holds for \(n+1\). The reason that induction makes sense as a proof technique is because the natural numbers can be viewed as the smallest set containing 0 and closed under adding 1 (successor). In fact, this is how we will represent the natural numbers, and how Agda and Coq do.

This idea goes back to Hermann Grassman (1861), though it was made famous by Giuseppe Peano (1889), building on work of Dedekind and Peirce. We won’t have pattern matching in Proust, (though it is a major feature in both Agda and Coq), so our definition of plus will not look the same. It will be essentially the same, only expressed differently.

We add the Z and S structures to Proust; these serve as introduction forms for natural numbers, which we will type as Nat. I’m deliberately leaving out inference rules here; I want you to write them out and convince yourself of their correctness before doing the implementation.

For the eliminator, we can reason as follows: to prove a property of a natural number n, it suffices to prove it for Z and show that successor preserves the property, that is, for any natural number \(k\), if \(k\) has the property, then so does the successor of \(k\). As we saw above, "a property" is a function \(P : \textrm{Nat}\ra\textrm{Type}\). The induction principle for natural numbers, expressed in our language, looks like this:

\[\forall P: (\textrm{Nat}\ra \textrm{Type}) ~.~ (P~\textrm{Z}) \ra (\forall k:\textrm{Nat}~.~ (P~k) \ra (P~(\textrm{S}~k))) \ra (\forall n:\textrm{Nat}~.~ (P~n))\]

We define an eliminator Nat-ind with arguments P, zc and sc (zero case and successor case), and n. As with Booleans, the code for type synthesis does the checking expected from the signature. Details are left for you to implement in an exercise below. Notice in particular that if you are constructing the expected type of sc, the variable of quantification k should be fresh with respect to P.

What about reduction? Reducing (Nat-ind P zc sc (Z)) should clearly result in zc (reduced). What about (Nat-ind P zc sc (S m)) for some m? To get the required proof of (P (S m)), we need to get a proof of (P m) with the recursive application (Nat-ind P zc sc m), then apply (sc m) to this, according to the induction principle. This is a bit more complicated than the cases we’ve seen, but along the same lines.

I promised that if we focussed first on proving things, a computationally useful principle would result. The behaviour of Nat-ind under reduction should be reminiscent of structural recursion on a natural number. The computation of plus in Racket given above has a zero case and a successor case. We can define a single abstract function for this, much as we did when we defined foldr for structural recursion on lists. Here is an iterator for natural numbers, which we can use to define plus.