6
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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.
$\endgroup$
  • 1
    $\begingroup$ 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? $\endgroup$ – Jonathan Gallagher Oct 24 '17 at 19:29
  • $\begingroup$ @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). $\endgroup$ – Neel Krishnaswami Oct 24 '17 at 19:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.