# When is the higher-order theory of a model categorical?

I'm interested in (classical) type theories $L$ with the following property. For $M$ any model of $L$ (in Set), let $T(M)$ be the type theory of $M$, i.e., the strongest extension of $L$ satisfied by $M$. The property is: for each model $M$ of $L$, $T(M)$ is categorical. In other words, for any $L$-models $M$ and $M'$, if $T(M) = T(M')$ then $M \cong M'$.

First, is there a standard name for this property? The intuitive idea is that $L$ has enough expressive power to completely describe its models. For now, I'm just going to call these theories "expressive enough".

Some examples: Any categorical theory is expressive enough. Any theory with only finite models is expressive enough. I'm pretty sure the theory of compact metric spaces is expressive enough (since the theory of a compact metric space $M$ determines a sequence of finite metric spaces that converges on $M$).

Second (a bit vaguely), is there something usefully general to say about which theories are "expressive enough"?

Third, I'm specifically interested in the constraints on this property from incompleteness. Intuitively there is a trade-off for theories between being expressively powerful and being easy to state. From Gödel we know that no categorical theory that extends Robinson arithmetic Q is recursively axiomatizable. Does this extend in some natural way to "expressive enough" theories that extend Q? Can we replace "extends Q" with something more general?

(I'm also interested in variations on this question: does it make a difference if we restrict attention to models within some cardinal? Is it more interesting if we use other logics besides type theory? But no equational theory with models with more than one element, and no first-order theory with infinite models, is "expressive enough".)

• I think you are looking for something along the lines of stability theory en.wikipedia.org/wiki/Stable_theory – UserB1234 Aug 7 '14 at 17:28
• Also, nowadays it more customary to call $M$ an $L$ structure, rather than a model. So this would probably be phrased: Let $M$ be an $L$ structure and let $T(M)$ be its $L$ theory.. – UserB1234 Aug 7 '14 at 21:15