6
$\begingroup$

Usually when formalizing a system of type theory, from what I've seen, authors usually either simply take the basic ideas of working with derivations, rules, and judgements as basic notions, explaining them informally, and define the type theory by giving a list of relevant rules, or formalize it in set theory (e.x. "a type theory consists of a set R of rules such that...").

However, oftentimes people will talk about models of type theories, for example, from ncatlab:

The models of ML type theory depend crucially on whether one considers the variant of extensional type theory or that of intensional type theory.

The models of the extensional version are (just) locally cartesian closed categories.

What is meant by this? Presumably, there is some way of actually formalizing type theory as an honest to goodness model-theoretic theory (either first order, or perhaps second order I imagine), so that a model of the system of type theory in question means the usual thing in model theory.

My question is: Are there any common approaches in the literature for defining type theory as an honest to goodness theory, and thus making the use of the term "model" the same as the model-theorists notion, or does "model of a type theory" mean something different? Is there even a formal definition of what "model of a type theory" or "theory of type theories" means in general in the literature, or are these definitions simply understood in an ad-hoc way, and only fully specified when talking about specific type theories (i.e. "models of MLTT", "models of HOTT")? If the latter is the case, restricting to particular type theories, have notions like "the theory of MLTT" or "the theory of HOTT", for example, been formalized in the usual model-theoretic context?

$\endgroup$
6
$\begingroup$

This question is actually a little difficult because what the best answer is is still a subject of ongoing research and debate.

First of all, dependent type theory is definitely not a first order theory so it needs a different kind of "model" to the usual notion from first order logic model theory. Now the problem is not that there is no good notion of model for type theory, but that there are several, and they have different pros and cons and it isn't clear which is the best way or if we have even discovered the best way yet.

All of these notions are based on the basic idea that there should be a category where contexts in type theory are interpreted as objects in the category, and each object comes equipped with a notion of type and term that are used to interpret types and terms in dependent type theory. The oldest kind of model is know as contextual category, from Cartmell, Generalised algebraic theories and contextual categories. These have the advantage of being very close to the syntax of type theory, but have a somewhat technical definition and so can be difficult to work with. At the other extreme are locally cartesian categories. These have a relatively easy definition using well studied ideas from category theory, but with two main disadvantages. Firstly, just to interpret type theory into a locally cartesian closed category is highly non trivial (see Hofmann, On the Interpretation of Type Theory in Locally Cartesian Closed Categories). Secondly, in a general locally cartesian closed category there is only really one way to interpret identity types, and using this interpretation one always gets a model of extensional type theory. This second point makes locally cartesian closed categories not so useful for HoTT, where it is important that the identity types are not extensional. In between contextual categories and locally cartesian closed categories there are several definitions including categories with families, categories with attributes and comprehension categories, that try to find a balance.

See the nlab page on Categorical Models of Dependent Types for more information.

A question of ongoing research is what kind of model should play the role of locally cartesian closed category for intensional dependent type theory. There is general consensus that this should be done using ideas from homotopical algebra such as weak factorisation system, and then interpreting identity type using the ideas in Awodey and Warren, Homotopy theoretic models of identity types. For instance, there is a general "coherence theorem" in Lumsdaine and Warren, The local universes model: an overlooked coherence construction for dependent type theories, that shows how to interpret intensional type theory in a number of categories. These include locally cartesian closed categories that also come equipped with a kind of structure from homotopical algebra known as right proper model structure.

$\endgroup$
4
$\begingroup$

Your understanding is a little backwards: first- and second-order logic are special cases of type theories, it's just that they are usually untyped, i.e. they have a single type, which is usually called a sort or a universe of discourse. The notion of a "model of type-theory" applies to first- and second-order logic: models of first-order logic are Heyting categories, while models of second-order logic are toposes.

How does this align with usual model theory? A first-order theory is a first-order logic supplemented with some signature and axioms. The model of a first-order theory (in the type-theoretic sense) is then a Heyting category supplemented with a sound (with respect to the axioms) interpretation of the signature inside the Heyting category. In particular, when you restrict your type-theoretic models so that the ambient category is the category of sets, you recover the notion of a model from classical model theory.

Why are models of type theories categories? It is because we can think of type theories/first- and second-order logic as presentations of categories by generators (the logical and non-logical signature of the type /first-/second-order theory) and relations (the inference rules/logical and non-logical axioms). That is to say, the data that goes into specifying type/first-/second-order theory is the same data that specifies categories, so categories are simply type theories, but seen from a different point of view. (One caveat to that: I think type theories in computer science are slightly more general and perhaps somewhat ahead of the categorical/model-theoretic picture).

Note that model theory itself is only coherent with, but not dependent on the type theory (i.e. on the inference rules of the logic). Rather, model theory begins by deciding to interpret propositions as characteristic morphisms to some object of truth values, and how the latter sits in the ambient category in which you're doing the model theory determines the type theory you're interpreting (e.g. this is how continuous logic and its funky inference rules arise from continuous model theory where we decide models to be metric spaces rather than sets and truth-values to be non-negative reals).

$\endgroup$
  • $\begingroup$ Thank you! That way of looking at things is helpful. However, I'd still like to know whether or not there is a general notion of "type theory" and hence "models of type theory", I've seen a few definitions for specific cases in the literature (such as dependent type theories), but never something general enough to cover arbitrary type theories. $\endgroup$ – Nathan BeDell Mar 14 '17 at 1:11
  • $\begingroup$ I do recall reading that the term "type" as it is used in model theory is different from the notion used when discussing "type theory" proper, so perhaps as you suggest, they are not fundamentally different notions, but the more general notion of "type theory" is a generalization of the model-theoretic notion. $\endgroup$ – Nathan BeDell Mar 14 '17 at 1:13
  • 2
    $\begingroup$ I spell out the "type theories as presentations of categories" in a decent amount of detail in my blog post Category Theory, Syntactically which may be of interest. $\endgroup$ – Derek Elkins Mar 14 '17 at 1:14
  • 2
    $\begingroup$ @Sintrastes the "types" of type theory or called sorts in classical logic, they are the domains over which variables ranger over; the "types" in model theory are (roughly) sets of formulas that describe elements of some particular structure -- they are a notion orthogonal to the types of type theory. Regarding the general notion of "type theory", that's the same question as asking for a general notion of "logic" (since type theories are perhaps generalized logics); whatever the answer, it should account for the varieties of logics that exist (linear logics, substructural logics, etc) $\endgroup$ – Vladimir Sotirov Mar 14 '17 at 1:29
  • $\begingroup$ @vladimirsotirov I don't know if it's the same question, but definitely a related one. What I'm really looking for is a general version of the Curry-Howard-Lambek correspondence for suitably defined general conceptions of "logic" and "type theory" -- the existence of such a theorem, if true, I think should characterize the notions I am looking for, but I do not know if this has been accomplished. It might be promising to try to construct a notion of type theory corresponding to the general notions of natural deduction studied in the proof-theoretic semantics literature, but I don't know. $\endgroup$ – Nathan BeDell Mar 14 '17 at 1:46

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.