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.