<p>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.</p>

<p>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</p>

<blockquote>
  <p>"If premises $P_1, \ldots, P_n$ are provable then conclusion $Q$ is provable."</p>
</blockquote>

<p>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 <em>schema</em> which has many <em>instances</em>. We put these instances in $I$.)</p>

<p>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 <a href="https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem" rel="nofollow noreferrer">Tarski's fixed point theorem</a> it has a least fixed point $T$. The set $T$ is precisely the set of all derivable formulas that we are after.</p>

<p>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).</p>

<p>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 <em>two</em> sets of syntactic entities, $F_\mathrm{term}$ and $F_\mathrm{type}$, and <em>two</em> 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.</p>

<p>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.</p>

<p>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 <em>in general</em> 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.</p>

CC BY-SA 3.0
2017-10-26T15:17:55.973Z
2017-10-26T16:01:55.407Z
2017-10-26T16:01:55.407Z
Andrej Bauer
<blockquote>
  <p>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?</p>
</blockquote>

<p>It's essentially the same argument that BNF grammars define sets.</p>

<ol>
<li><p>Start with the set of untyped terms (conventionally dubbed the <em>preterms</em>), 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).</p></li>
<li><p>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. </p></li>
<li>Interpret each rule of MLTT as a <em>predicate transformer</em>. 
So a rule like 
$$
  \frac{\displaystyle \Gamma \vdash e : \Sigma x:A.B}
       {\displaystyle \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. </li>
<li>Observe that every rule is a Horn clause without negation. </li>
<li>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). </li>
<li>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.</li>
<li>By the Knaster-Tarski theorem, there is a least fixed point to the this lattice.</li>
<li>That fixed point gives you the set of well-typed terms, contexts, etc.</li>
</ol>

CC BY-SA 3.0
2017-10-24T19:29:36.643Z
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
CC BY-SA 3.0
2017-10-24T19:55:22.330Z
@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
CC BY-SA 3.0
2017-10-24T13:10:37.730Z
2017-10-24T13:10:37.730Z
Neel Krishnaswami
<p>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:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>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.</p>

<p>Later, you get,</p>

<blockquote>
  <p>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$.</p>
</blockquote>

<p>A category consists of a <em>set</em> of objects (modulo size issues) and a <em>set</em> 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?</p>

<p>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.</p>

<type-theory><ct.category-theory><dependent-type>
Explicit set of types and terms in MLTT
Daniel Satanove
# Explicit set of types and terms in MLTT

(Asked by: username_0 on 2017-10-23)

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.

**Tags:** type-theory, ct.category-theory, dependent-type

---

## 2 answers

### Answer by username_1 on 2017-10-26. Score: 4 | Accepted answer

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](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_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.


---

### Answer by username_2 on 2017-10-24. Score: 7

> 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{\displaystyle \Gamma \vdash e : \Sigma x:A.B}
   {\displaystyle \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.

> **Comments:**
> **username_3**: 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?  
> **username_2**: @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).  

---

