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
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.