Categorification of logic Has there been an effort to categorify first order logic? More particularly, structures in the sense of logic.
If so, then every structure of a first order theory is a category. So in particular, the universe of categories must be a (meta)-category itself. So I have another question: is there a development of a model theory of categorified logic?
The idea is like this: In modern set-theoretic based model theory, most of the interesting stuff comes by looking at different cardinalities. Theorems in first-order logic, like the Lowenheim–Skolem Theorem, make it easy to move up and down cardinalities, and after all, the category SET is equivalent to CARDINALS. Very much this equivalence dictates the model theory.
So the universe of categories CAT, and whatever is a skeletal equivalent of it, will dictate the model theory of categorified logic.
Is anyone aware of categorified logic?
 A: Honestly, I think your motivation is a bit misdirected, but apart from the answers already given, you should look at the general topic of categorical logic. Within that, there are category-theoretic treatments of fragments of first-order logic (such as regular logic and coherent logic), as well as full first-order logic, which goes under the name of hyperdoctrine, as introduced by William Lawvere around 1969.
References:


*

*Adjointness in foundations, F. William Lawvere, Dialectica, 23 (1969). Available in TAC reprints.

*Peter Johnstone's "Sketches of an elephant" is a book on topos theory but contains a lot of background in categorical logic, including first-order logic done categorically.

*Carsten Butz has some lecture notes on categorical logic, those might be an easy starting place.

*You should definitely consult Andy Pitts's chapter on categorical logic in: A. M. Pitts, Categorical Logic. Chapter 2 of S. Abramsky and D. M. Gabbay and T. S. E. Maibaum (Eds) Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, Oxford University Press, 2000. (A preliminary version appeared as Cambridge University Computer Laboratory Tech. Rept. No. 367, May 1995.)

A: Try Mike Shulman's page.
A: You may also want to look at the work of Michael Makkai on accessible categories.  My best understanding is that these are an attempt to generalize categories of models of first-order theories by distilling their essential category-theoretic properties.
(Perhaps this is essentially the same as Mike Shulman's project?  To be honest, my knowledge of categorial logic is very limited, mostly I'm just aware that it exists, and its flavor seems to be more category-theoretic than logical so it's hard for me to digest.)
Also possibly relevant are some of the papers on Makkai's webapge:
https://www.math.mcgill.ca/makkai/
A: This question is very old, but maybe people still fall into it from time to time.
I recently spent a bit of time gathering material for an introduction to categorical logic. It is mostly designed for bachelor and master students.
https://diliberti.github.io/Read/Read.html
A: Christian Lair found accessible categories under the french name "catégorie modélables" around the 80's : http://www.numdam.org/article/DIA_1981__6__A5_0.pdf
One year after (1982) he wrote a paper with René Guitart which express 1st order formulas in the language of (co)limits :
http://www.numdam.org/article/DIA_1982__7__A4_0.pdf
I hope this help.
