MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## categorification of logic

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?

-
I deleted my post because too many people were downvoting it. This is a horrible question that borders on vacuity, and you're using the wrong terminology to boot. You need at least up to first-order logic to define anything of value and interpret any axioms. I mean, if you model a first-order axiom system in category theory, you can't prove anything about the axiom system without first assuming first order logic. – Harry Gindi Dec 16 2009 at 18:38
Harry, what's your problem? I think the question is a very interesting one (as evidenced by the link to my work that David supplied below). And I'm confused by your complaints; it sounds to me like he's asking for categorified first-order logic, not trying to do away with first-order logic. (Although I didn't get a chance to read your deleted post, so maybe you explained there.) – Mike Shulman Dec 16 2009 at 18:45
"You need at least up to first-order logic to define anything of value and interpret any axioms." This is not correct. First order logic is one way of formalizing math. Another way is to work in some topos directly with its objects and arrows. You can work inside an algebraic structure using only equational logic, which is much weaker than first order logic. Linear logic is not even weaker that f.o.l. -- it is simply different. In any case, as I said in my previous comment, any logical system involving types and terms can be turned into a category – SixWingedSeraph Dec 16 2009 at 20:20
No, Harry, I still don't think you were completely right, and you were definitely unnecessarily abrasive. I agree, though, that Colin would benefit from reading some more basic stuff about category theory and what people call "categorical logic." That would probably answer some of his questions automatically, and would give him the terminology and background to ask other questions in an easier-to-understand way. – Mike Shulman Dec 18 2009 at 16:58
@Harry: Michael Makkai and other logicians have been working on categorical model theory and first-order categorical logic for decades now; are you saying that this whole project is a waste of time? – John Goodrick Dec 18 2009 at 22:09

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)
-
 My introduction to categorical logic was from Pitts (1989), Notes on Categorical Logic, which stands up well compared to his later treatments. Link to (large) pdf is at cl.cam.ac.uk/~amp12/papers/index.html – Charles Stewart Jan 14 2010 at 12:46 Lambek & Scott (1986), Introduction to higher order categorical logic, covers an immense amount of ground, and is forefully driven by an agenda in the foundations of mathematics. Not easy going, but indispensible if you really want to get to grips with the subject. – Charles Stewart Jan 14 2010 at 12:50

Try Mike Shulman's page.

-

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/

-
I think the comment "its flavor seems to be more category-theoretic than logical" demonstrates a gulf between the attitudes of people with different backgrounds. To my mind pure category theory is a part of logic. It's about mathematical thought, and mathematical structures, and mathematical language; it's metamathematics. People with a background in "traditional" logic don't tend to see it that way, though. – Tom Leinster Dec 19 2009 at 2:52
@Tom Leinster: I'm sympathetic with the view that category theory is part of logic, in some reasonable sense of the words. But the one time I made a serious attempt to understand Makkai's work, I was made acutely aware of my lack of background in category theory, and the things I had learned in my logic classes didn't seem to be of much help; that's all I meant by the "category-theoretic flavor." – John Goodrick Dec 19 2009 at 16:57
I don't really understand how you can talk about categories (they have an axiomatic definition) without first developing a proof calculus. – Harry Gindi Dec 19 2009 at 22:50
@Harry: the same way people talked about other axiomatically-defined mathematical objects (such as groups or models of non-Euclidean geometry) before modern proof calculi were invented. As far as I know, nothing like what you'd call a proof calculus was rigorously defined before Frege's 1879 Begriffsschrift (but I'd be interested in hearing about an earlier reference), whereas Cayley was already studying abstract groups at least as far back as 1854. – John Goodrick Dec 20 2009 at 17:48
They talked about them informally. To be completely formal, one first needs a proof calculus. – Harry Gindi Dec 22 2009 at 0:18
show 1 more comment