Model theory is applied to axiomatic systems to give them an interpretation. Now consider a logic in axiomatic form. When we consider a model of this logic and some sentence in the logic, each variable in the sentence is interpreted in a some set. From another perspective this appears to be assigning a type to that variable.

Is that the case? Is model theory for logic essentially the same as type theory - but where syntax is separated from semantics - that is we think of type as semantics?


There may be a connection between model theory and type theory if you dig enough, but I don't see the analogy between assigning types to variables and assigning objects to variables. My knowledge of type theory is a bit fragmented, but I would say that, if anything, type theory has closer ties to computability theory or proof theory than it does to model theory.

For one thing, types/terms can be systematically combined in meaningful ways to produce other types/terms, whereas objects in model theory don't combine in this way. Moreover, in model theory, the focus is on models, and which theories are satisfied in which models; it's more concerned with worldly structure, you might say, and less concerned about the particulars of the language (though which language a model is in certainly matters). By contrast, type theory is more concerned with the particulars of the language, and less concerned with the way the world is set up.

That's a very rough (and possibly misleading) characterization, but for instance, in model theory, you might be concerned about determining what the models of the theory of algebraically-closed fields or the theory of divisible ordered groups look like (are there saturated models, prime models, homogeneous models, etc.) or what properties these theories have (are they complete, decidable, categorical, do they have quantifier elimination, etc.). But you wouldn't bother yourself with proof systems in model theory, and in fact you can easily get in model theory by without ever mentioning them! By contrast, type theory might be concerned with naming proofs and showing how to systematically code proofs into terms of a certain type. You wouldn't need to talk about the way the world is, in type theory, but you would need to talk about syntactic functions.

It can also be confusing, because model theory uses the word "type" in a very different unrelated sense from type theory. A type over a parameter set X with respect to a theory T is a set of formulae consistent with T which may use members of X as parameters in the formulae. It then becomes an interesting question in model theory whether or not there are models of T that omit certain "types", or how many types there are with respect to T, or in what way the different types with respect to T are related, etc.

  • Nice answer. I've come across the use you mentioned of type in my cursory reading of type theory - and yes it did confuse me somewhat. – Mozibur Ullah Jun 3 '13 at 5:08

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.