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.

1. Is it correct?

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

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

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

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

• If the morphisms are isomorphisms then it's quite boring. Instead you might want to consider homomorphisms (yes, this notion is not the sole property of group theorists or algebraists). Simply functions from one structure to another which preserve the interpretation to a sufficient degree (much like homomorphisms between groups). – Asaf Karagila Jul 28 '14 at 1:13
• Yes, thank you. That's what I had in mind. I edited the question. – Borbei Jul 28 '14 at 1:16
• Well, nothing I can count as an answer, but I should point out that vector spaces have quite complicated theories in some sense. You need to decide whether or not you have a two-sorted structure with vectors and a field; or if you prefer an infinite language with a function symbol for each scalar and then add infinitely many axioms describing the relations between those functions. Topological spaces don't have a simple and obvious first-order theory either, since axioms of topology are really third-order over the space (unions of open sets), so to remedy that you need to make things [...] – Asaf Karagila Jul 28 '14 at 1:38
• [...] a bit more complicated. Of course if you have a metric space, then you can alleviate some of that by using the metric to do certain things. But since you would often want additional properties which the metric don't usually describe in first-order (e.g. local compactness) you again need to make things more complicated. – Asaf Karagila Jul 28 '14 at 1:40

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