Relations between Theories and Categories I'm just toying around with some thoughts, trying to grock some concepts:
It seems that every formal theory induces a locally small category via interpretations: its objects are structures that satisfies the sentences of that theory (e.g. models), and its morphism are logical homomorphisms. 


*

*Is it correct? 

*What about the opposite? Is it true that every locally small category induces a formal theory? If so, are there known algorithms to construct such a theory from an explicitly given category?

*If so, functors can be regarded as relations between theories. But this doesn't really sits well with my intuition. For example, there is a covariant functor between the category of pointed manifolds and linear spaces, but I'm used to think about it as, roughly, a some kind of an embedding. Not as a way to relate the mathematical theory differential geometry with the theory of linear algebra. What's a good mental model for thinking about it? 

*Is it possible to prove results using this correspondences, in a way that "bypasses" Godel's incompleteness theorem? E.g. by proving that the category induced by a theory has an initial object in which some categorical property holds, we can deduce the truthness of a statement in this theory (since it's true in every model). Can it happen that such a true statement be unprovable in the theory, in the regular sense? Can a similar strategy be used to prove an independence of an axiom? 

*Is there a categorical difference between first vs. second order logic? I'd guess it has something to do with large categories on the one hand, and Lowenheim–Skolem theorem on the other, but I haven't got far with this idea.
Related: (a) Comparing Category Theory and Model Theory (with examples from Group Theory). (b) A logic that can distinguish between two structures
 A: Here are some partial answers:


*

*A good definition of arrows for $\mathrm{Mod}(T)$ is elementary embeddings of models.

*It turns out that "being the category of models of a first-order theory" is not a property of a category.  Let me explain: let C be the discrete category with an uncountable infinity of objects.  Question: is C the category of models of a theory?  Answer: well, it could be, but you've got to add more information -- you've got to put a topology on C.  e.g. if you make C into the Cantor space, then the answer is Yes, it's the category of models of a propositional theory with a countable number of propositional constants.  If you equip C with a different topology, then it will correspond to the models of a different theory.   

*Every interpretation between theories corresponds to a functor; but not every functor corresponds to an interpretation between theories.  You need to specify some conditions on the functor -- it needs to preserve the relevant structure.  The requirements are spelled out in Makkai and Reyes' book, First Order Categorical Logic

*It's difficult to prove model-theoretic properties using categorical methods.  But some progress in this direction was made in Makkai and Reyes' book.  

*Higher-order logic needs topos theory.  See the book, Introduction to Higher Order Categorical Logic by Lambek and Scott.
