categorification of logic - MathOverflow

categorification of logic

2009-12-16T12:07:45Z

has there be 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, must of the interesting stuff comes by looking at different cardinalities. First order theory like Lowenheim-Skolem Theorem makes 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.

Anyone aware of categorified logic?

Answer by David Corfield for categorification of logic

2009-12-16T13:53:15Z

Try Mike Shulman's page.

Answer by John Goodrick for categorification of logic

2009-12-18T22:18:02Z

You many also want to look at the work of Michael Makkai on [accessible categories].[1] 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:

http://www.math.mcgill.ca/makkai/

Answer by Andrej Bauer for categorification of logic

2009-12-21T19:11:27Z

The system does not allow me to post urls because I am a "newbie", so they are mangled. I apologize for this. You will have to reconstruct them by removing spaces after periods.

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, see ht tp: //www. tac.mta. ca/tac/reprints/articles/16/tr16abs.html
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 at ht tp://www. itu. dk/~butz/research/publications.html, those might be an easy starting place.
You should definitely consult Andy Pitt'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, see ht tp://www. cl. cam. ac. uk/~amp12/papers/catl/catl.ps. gz)