3 Predicate Logic

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" ($\mathrm{\forall }$) and "there exists" ($\mathrm{\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 $\mathrm{\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:

$\mathrm{\forall }a,b,c\in \mathbb{Z},((a\mid b)\wedge (a\mid c)\to (\mathrm{\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 $\mathrm{\forall }$-introduction is used. The second one is more obvious, for the subformula $\mathrm{\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 $\mathrm{\forall }$) but it is not written down explicitly.

Here we see the simplest, most direct method to prove a $\mathrm{\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 $\mathrm{\forall }$-introduction should work, which we can keep in mind for later.

There are also two nearly-identical places where an informal version of $\mathrm{\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 $\mathrm{\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 $\mathrm{\exists }$-elimination should work in general.

There is no use of $\mathrm{\exists }$-introduction, or $\mathrm{\forall }$-elimination in this proof. It is worth thinking about what these should look like. We can see a use of $\mathrm{\exists }$-introduction if we try to prove a specific divisibility statement, for example $3\mid 6$. This expands to $\mathrm{\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 $\mathrm{\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 $\mathrm{\forall }$ and $\mathrm{\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 $\mathrm{\forall }$ and $\mathrm{\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 $\mathrm{\forall }XT$ 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 $\mathrm{\forall }XT$ 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 $\mathrm{\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 $\mathrm{\exists }XT$ 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 $\mathrm{\forall }X$, we use generalization: we prove the statement without the quantifier, treating $X$ as an unknown. To use a $\mathrm{\forall }X$, we substitute some specific $a$ for $X$.

$${\displaystyle \frac{\mathrm{\Gamma }⊢T}{\mathrm{\Gamma }⊢\mathrm{\forall }XT}({\mathrm{\forall }}_I){\displaystyle \frac{\mathrm{\Gamma }⊢\mathrm{\forall }XT}{\mathrm{\Gamma }⊢T[X\mapsto a]}({\mathrm{\forall }}_E)}}$$

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 $\mathrm{\exists }X$, we must have a proof of the statement when $X$ is some specific $a$; to use a $\mathrm{\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$.

$${\displaystyle \frac{\mathrm{\Gamma }⊢T[X\mapsto a]}{\mathrm{\Gamma }⊢\mathrm{\exists }XT}({\mathrm{\exists }}_I){\displaystyle \frac{\mathrm{\Gamma }⊢\mathrm{\exists }XT\mathrm{\Gamma },T⊢V}{\mathrm{\Gamma }⊢V}({\mathrm{\exists }}_E)}}$$

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 $\mathrm{\forall },\mathrm{\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 $\mathrm{\forall },\mathrm{\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. $\mathrm{\forall },\mathrm{\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 $\mathrm{\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 $\mathrm{\Gamma }\models T$ if for all models and all valuations that make the formulas in $\mathrm{\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 $\mathrm{\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 $\mathrm{\Gamma }\models T$, then $\mathrm{\Gamma }⊢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 $\mathrm{\Gamma }⊢T$, then $\mathrm{\Gamma }\models 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 $\mathrm{\forall }$ and $\to$ (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.)

$${\displaystyle \frac{x\notin \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x\Rightarrow \text{Type}}({\text{Var}}_{\mathit{wf}}){\displaystyle \frac{\mathrm{\Gamma }⊢T\Rightarrow \text{Type}\mathrm{\Gamma }⊢W\Rightarrow \text{Type}}{\mathrm{\Gamma }⊢T\to W\Rightarrow \text{Type}}({\Rightarrow }_{\mathit{wf}})}}$$

If $\mathrm{\Gamma }⊢T\Rightarrow \text{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 $\text{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 $\mathrm{\forall }XW$, our human-readable notation will be $\mathrm{\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 $\mathrm{\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 $\mathrm{\forall }$ initially, and will add $\mathrm{\exists }$ later on. Look at the interpretation of $\mathrm{\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$, $\mathrm{\forall }$ becomes implication ($\to$). 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 $\mathrm{\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 $\mathrm{\Pi }X:T.W$, and calls these "Pi-types". But since our primary motivation is the study of logic, we will stick with $\mathrm{\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.

$${\displaystyle \frac{\mathrm{\Gamma }⊢T\Leftarrow \text{Type}\mathrm{\Gamma },x:T⊢W\Leftarrow \text{Type}}{\mathrm{\Gamma }⊢\mathrm{\forall }x:T.W\Rightarrow \text{Type}}({\mathrm{\forall }}_{\mathit{wf}})}$$

$${\displaystyle \frac{\mathrm{\Gamma }⊢\mathrm{\forall }x:T.W\Leftarrow \text{Type}\mathrm{\Gamma },x:T⊢t\Leftarrow W}{\mathrm{\Gamma }⊢\lambda x.t\Leftarrow \mathrm{\forall }x:T.W}({\mathrm{\forall }}_I)}$$

In general, the type $T$ may contain references to variables in $\mathrm{\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\notin \mathrm{\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 $\mathrm{\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 $\mathrm{\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$, $\mathrm{\forall }$-elimination generalizes implication-elimination.

$${\displaystyle \frac{\mathrm{\Gamma }⊢f\Rightarrow \mathrm{\forall }x:T.W\mathrm{\Gamma }⊢t\Leftarrow T}{\mathrm{\Gamma }⊢ft\Rightarrow W[x\mapsto t]}({\mathrm{\forall }}_E)}$$

It’s convenient to be able to collapse adjacent for-alls together in human-readable notation, as in $\mathrm{\forall }(x:T)(y:W).S$ or $\mathrm{\forall }xy: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, $\lambda x.x$, as $A\to A$. But it could also be typed as $B\to B$, and $C\to C$, and so on. We can go further: it can be typed as $(A\to B)\to (A\to B)$. For any type $T$, no matter how complex, $\lambda x.x$ can be typed as $T\to T$.

Since $\mathrm{\forall }$ is in our language, we can write one function $\lambda y.\lambda x.x$ encompassing all of these, whose type is $\mathrm{\forall }T.(T\to 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 $\mathrm{\forall }T\to (T\to T)$ is not complete according to our syntax for $\mathrm{\forall }$. We have to specify the domain of quantification of $T$. Clearly, it is $\text{Type}$, and the complete term is $\mathrm{\forall }(T:\text{Type}).(T\to T)$. In order to be able to say this, we have to add $\text{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 $\text{Type}$ has type $\text{Type}$. That is, $\text{Type}:\text{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 $\text{Type}:\text{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 $\text{Type}:\text{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 $\text{Type}$ as a constant to Proust’s term language will be straightforward. But adding code implementing the rules for $\mathrm{\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 $\text{Type}$, we don’t have any other type constants. The base types we used in propositional logic are gone (as is the ${\text{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\to (A\to B)\to B$ from propositional logic becomes $\mathrm{\forall }AB:\mathrm{Type}.A\to (A\to B)\to B$, and the proof term $\lambda x.\lambda f.fx$ from propositional logic becomes $\lambda A.\lambda B.\lambda x.\lambda f.fx$. (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 $\mathrm{\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 $\mathrm{\forall }$ and for $\lambda$; 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 $\lambda$.

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 $\lambda x.x$ and $\lambda 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 $\lambda x.x$ and $\lambda 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 $\lambda 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{array}{rl}x[x\mapsto s]& =s\\ y[x\mapsto s]& =y\end{array}$$

Substitution into an application just substitutes into the two parts.

$$\begin{array}{rl}(t_1{t}_2)[x\mapsto s]& =(t_1[x\mapsto s])(t_2[x\mapsto s])\end{array}$$

We can’t do the same for lambda, because again there are two cases. If we are substituting for $x$ into a $\lambda 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 $\lambda x.b$, nothing should change in the body $b$. The $\lambda x$ introduces a new local name $x$ and a new local scope.

Even this does not handle all cases involving free variables. Consider $(\lambda x.y)[y\mapsto x]$. Going ahead and substituting would give $\lambda x.x$, which is not right. The substitution $y\mapsto x$ is referring to a version of $x$ outside the scope of the $\lambda 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 $\lambda x.y$ as $\lambda z.y$ for some choice of $z$, and then do the substitution, giving $\lambda 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 $\lambda x$ to $z$, but in general, if $y$ is replaced by a more complex expression $t$ (that is, we are rewriting $\lambda 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 $(\lambda x.yz)[y\mapsto x]$. If we first changed $\lambda x.yz$ to $\lambda z.yz$, and continued with $(yz)[y\mapsto x]$, we would end up with $\lambda z.xz$, which is incorrect. But if we chose $w$ instead of $z$ to replace $x$ in $\lambda x$, we would end up with $\lambda w.xz$, 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 $\lambda x$. Consider $(\lambda x.\lambda z.x)[y\mapsto x]$. If we first changed $\lambda x.\lambda z.x$ to $\lambda z.\lambda z.z$, and then continued with $(\lambda z.x)[y\mapsto x]$, we would get $\lambda z.\lambda z.z$, which is not correct. If we instead choose $w$ as the new variable, we get $\lambda w.\lambda z.w$, which is correct.

Here are all the rules summarized.

$$\begin{array}{rl}(\lambda x.t)[x\mapsto s]& =\lambda x.t\\ (\lambda x.t)[y\mapsto s]& =\lambda x.(t[y\mapsto s])\\ & x\text{not free in}s\\ (\lambda x.t)[y\mapsto s]& =\lambda z.((t[x\mapsto z])[y\mapsto s])\\ & x\text{free in}s,z\text{not free in}s\text{or}t,z\text{not a binder in}t\end{array}$$

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 $fa$ steps to $fb$. 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 $\mathrm{\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 $\lambda x.\lambda y.y$ or $\lambda \mathrm{\_}.\lambda y.y$ (which are the same, in a sense to be formalized below), but we can’t write $\lambda x.\lambda \mathrm{\_}.\mathrm{\_}$ (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. $\lambda x.\lambda y.x$ becomes $\lambda .\lambda .1$, and $\lambda x.\lambda y.y$ becomes $\lambda .\lambda .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 $\lambda x.t$ and $\lambda 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(\mathrm{mod}4)$. But we typically go further and say things like $(1+6)\equiv (2+1)(\mathrm{mod}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.

$${\displaystyle \frac{\mathrm{\Gamma }⊢f\Rightarrow \mathrm{\forall }x:T.W\mathrm{\Gamma }⊢t\Leftarrow T}{\mathrm{\Gamma }⊢ft\Rightarrow W[x\mapsto t]}({\mathrm{\forall }}_E)}$$

In our code so far, we synthesize the type of $f$, verify with a match that it is of the form $\mathrm{\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).

$${\displaystyle \frac{\mathrm{\Gamma }⊢\mathrm{\forall }(x:T)\to W\Rightarrow \text{Type}\mathrm{\Gamma },x:T⊢t\Leftarrow W}{\mathrm{\Gamma }⊢\lambda x.t\Leftarrow \mathrm{\forall }x:T.W}({\mathrm{\forall }}_I)}$$

The code synthesizes the type of $\lambda 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 $\mathrm{\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 $\mathrm{\forall }(x_1:T).W$, we can check if $x$ satisfies the side conditions with respect to $\mathrm{\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.