13
$\begingroup$

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?

Improve this question
$\endgroup$
11
  • 9
    $\begingroup$ 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.) $\endgroup$
    – Mike Shulman
    Commented Dec 16, 2009 at 18:45
  • 9
    $\begingroup$ "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 $\endgroup$
    – SixWingedSeraph
    Commented Dec 16, 2009 at 20:20
  • 2
    $\begingroup$ What is a topos and how can we deduce things from its axioms? Surely we need the ability to make logical inference in a formal setting... $\endgroup$
    – Harry Gindi
    Commented Dec 16, 2009 at 21:32
  • 7
    $\begingroup$ 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. $\endgroup$
    – Mike Shulman
    Commented Dec 18, 2009 at 16:58
  • 6
    $\begingroup$ @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? $\endgroup$
    – John Goodrick
    Commented Dec 18, 2009 at 22:09

5 Answers 5

Reset to default
9
$\begingroup$

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.)
Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ 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 $\endgroup$
    – Charles Stewart
    Commented Jan 14, 2010 at 12:46
  • 1
    $\begingroup$ 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. $\endgroup$
    – Charles Stewart
    Commented Jan 14, 2010 at 12:50
6
$\begingroup$

Try Mike Shulman's page.

Improve this answer
$\endgroup$
3
$\begingroup$

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

Improve this answer
$\endgroup$
3
$\begingroup$

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/

Improve this answer
$\endgroup$
6
  • 2
    $\begingroup$ 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. $\endgroup$
    – Tom Leinster
    Commented Dec 19, 2009 at 2:52
  • 1
    $\begingroup$ @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." $\endgroup$
    – John Goodrick
    Commented Dec 19, 2009 at 16:57
  • $\begingroup$ I don't really understand how you can talk about categories (they have an axiomatic definition) without first developing a proof calculus. $\endgroup$
    – Harry Gindi
    Commented Dec 19, 2009 at 22:50
  • 5
    $\begingroup$ @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. $\endgroup$
    – John Goodrick
    Commented Dec 20, 2009 at 17:48
  • $\begingroup$ They talked about them informally. To be completely formal, one first needs a proof calculus. $\endgroup$
    – Harry Gindi
    Commented Dec 22, 2009 at 0:18
1
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.