# Explicit set of types and terms in MLTT

Whenever I read a presentation of MLTT, especially in the context of the correspondence of MLTT with LCCCs (eg. Seely's paper), they say "the type constructors/formation rules are..." and then list a bunch of rules, and at least one of the rules will refer to terms. For example, in Seely, you have:

If $F$ is a type-valued function constant, and $a_1, a_2, \dots a_n$ are terms of the appropriate types, then $F(a_1, \dots , a_n)$ is a type.

And then after, you get the term formation rules, which refer to types. This is supposed to represent some sort of mutual induction, but if you naively interpret a paper as being a sort of short-hand for formal definitions and proofs in set theory + FOL, then the definition given is circular.

Later, you get,

Let $C(M)$ be the category whose objects are all closed types of M, and morphisms $\mathrm{hom}(A,B)$ are closed terms of type $A \to B$.

A category consists of a set of objects (modulo size issues) and a set of morphisms between each object. Lets say for the sake of argument that I am skeptical that the mutual inductive definitions like Seely's actually give a well-defined set. How do you actually construct the sets of types and terms (more) formally in set theory, and convince me that these actually do form a set?

Not just for the sake of argument, I'm skeptical that the sort of dependent type theory that you can implement on a computer and program with is the same sort of dependent type theory that has this relationship with locally cartesian closed categories.

A general way to see that such inductive definitions are well-founded is to observe that the definitions may be understood as defining a least fixed point of a monotone operator. This approach works for any sort of deductive systems, including ones that have several kinds of judgments, and even for infinitary ones.

Let us first consider a simple example where there is no mutual induction, for instance provability of formulas in first-order logic. Let $F$ be the set of all formulas (or all strings, if you suspect that even the notion of a well-formed formula is susupect) and suppose we would like to define the subset $T \subseteq F$ of all provable formulas. Inference rules are all of the form $$\frac{Q_1 \quad Q_2 \quad \cdots \quad Q_n}{P}$$ which we read as

"If premises $P_1, \ldots, P_n$ are provable then conclusion $Q$ is provable."

Define the set $I$ of all instances of all inference rules whose elements are pairs $(\{Q_1, \ldots, Q_n\}, P)$ where $Q_1, \ldots, Q_n, P \in F$ and there is some inference rule which allows us to conclude from premises $Q_1, \ldots, Q_n$ that $P$. (Note: typically an inference rule is a schema which has many instances. We put these instances in $I$.)

We will exhibit $T$ as the least fixed point of a monotone operator $C : P(F) \to P(F)$ where $P(F)$ is the powerset of $F$. The operator $C$ is defines as $$C(S) = \{ P \in F \mid \exists Q_1, \ldots, Q_n \in S . (\{Q_1, \ldots, Q_n\}, P) \in I\}.$$ It is easy to check that $C$ is monotone and that therefore by Tarski's fixed point theorem it has a least fixed point $T$. The set $T$ is precisely the set of all derivable formulas that we are after.

We may allow infinitary inference rules of the form $$\frac{Q_1 \quad Q_2 \quad Q_n \quad \cdots}{P}$$ and nothing much changes, except that the elements of $I$ are now of the form $(Q, P)$ where $Q$ is an arbitrary set of premises, rather than a finite one. Tarski's fixed point theorem still applies, although it gets harder to compute the fixed point by iteration (we have to go transfinite up the ordinals).

We might face a mutually inductive definition, say of types and terms. The situation is only slightly more complicated in such a case. We deal with two sets of syntactic entities, $F_\mathrm{term}$ and $F_\mathrm{type}$, and two monotone operators $$C_\mathrm{term} : P(F_\mathrm{term}) \times P(F_\mathrm{type}) \to P(F_\mathrm{term})$$ and $$C_\mathrm{type} : P(F_\mathrm{term}) \times P(F_\mathrm{type}) \to P(F_\mathrm{type}).$$ Tarski's fixed-point theorem still applies because we can combine these into a single monotone operator $$C = \langle C_\mathrm{term}, C_\mathrm{type} \rangle : P(F_\mathrm{term}) \times P(F_\mathrm{type}) \to P(F_\mathrm{term}) \times P(F_\mathrm{type}).$$ The least fixed point $(T_\mathrm{term}, T_\mathrm{type})$ gives both terms and types simultaneously.

One may also observe that a product of powers is isomorphic to a power of a sum, $$P(F_\mathrm{term}) \times P(F_\mathrm{type}) \cong P(F_\mathrm{term} + F_\mathrm{type})$$ and reduce the mutually inductive case back to the ordinary one.

One may object that I am shooting a sparrow with a cannon ball. Do we really need general powersets and Tarski's fixed-point theorem? Well, yes if we want to show that in general there is never a problem. In a specific case a lesser fixed point theorem will suffice. For instance, all formal systems that occur in practice are finitary and the set $I$ is primitive recursive, so a fairly weak induction principle on natural numbers will suffice to establish the existence of a least fixed point.

How do you actually construct the sets of types and terms (more) formally in set theory, and convince me that these actually do form a set?

It's essentially the same argument that BNF grammars define sets.

1. Start with the set of untyped terms (conventionally dubbed the preterms), and the set of untyped contexts (sequences $x_1:A_1, \ldots, x_n:A_n$ where the $x_i$ are variables and $A_i$ are preterms).

2. Think of each judgement form as a predicate. Think of $\Gamma \vdash e : A$ as a three-argument predicate on precontexts, preterms, and preterms, $\Gamma \vdash A \mbox{ type}$ as a two-argument predicate on preterms, $\Gamma \vdash e \equiv e' : A$ as a four-place predicate and so on.

3. Interpret each rule of MLTT as a predicate transformer. So a rule like $$\frac\Gamma \vdash e : \Sigma x:A.B} \Gamma \vdash \pi_1 e : A}$$ is defining a new predicate $\vdash'(\_, \_, \_)$ from the old predicate $\vdash(\_, \_, \_)$ such that $\vdash'(\Gamma, \pi_1 e, A)$ holds when $\vdash(\Gamma, e, \Sigma x:A.B)$ holds.
4. Observe that every rule is a Horn clause without negation.
5. As a result, the predicate transformer induced by the interpretation of a rule is monotone on the inclusion order on the lattice of sets of terms (or tuples of contexts and terms; or tuples of contexts, terms and terms; and so on).
6. Furthermore, the pointwise union of monotone predicate transformers is also monotone. So we can interpret all of the rules as jointly defining a monotone predicate transformer.
7. By the Knaster-Tarski theorem, there is a least fixed point to the this lattice.
8. That fixed point gives you the set of well-typed terms, contexts, etc.
• In the argument sketched above, termination of type checking, and strong normalization of beta reduction seem to not play a role. Would this argument allow one to define the set of types when one takes types modulo $\equiv$, or in the face of the rules for type equality which depends on term equality? – Jonathan Gallagher Oct 24 '17 at 19:29
• @JonathanGallagher: This argument just establishes that the rules defining the set of derivation trees are well-founded, which seemed to be what was worrying Daniel. With a bit of care/encoding it could even be made to work in Peano or Heyting arithmetic. In the presence of universes, establishing more substantial properties like consistency or normalization requires a much stronger metalogic. You need inductive-recursive definitions to interpret type theory in itself, and I don't know how to interpret induction-recursion in anything less than bounded IZF (topos logic). – Neel Krishnaswami Oct 24 '17 at 19:55