How do you use category theory as a foundation for logic? What does it mean to be a foundation for logic as opposed to a foundation for math?
My question is similar to this question but is specifically about category theory as a foundation for logic (and what that means).
By logic, I specifically mean things like propositional calculi, predicate logics, modal logics, and other things that are formalisms for manipulating things that can bear truth values. I'm intending this question to be related to, but different from treating category theory as a foundation for math. I'm pretty sure this is the sort of thing that the excerpt in question means by logic, unless I'm fundamentally misreading it.
This answer to this question includes an interesting excerpt (emphasis mine).
Now, it was discovered that category theory can be used also as a
foundation for logic and there are many differences between
categorical logic and classical logic. Here again one formalism may be
better suited than another, depending on the purpose. For instance, it
would seem that for constructive and intuitionistic logic topos theory
provides a very natural setting, more so than classical set theory
would. For classical logic it is debatable how much merit there is in
adopting the topo theoretic approach. Classical techniques such as
Cohen forcing can be understood quite nicely via topos theory but one
may argue that the insight provided is not significant enough to
justify abandoning standard techniques for new ones. It's a matter of
taste.
I'm trying to understand what this means. I'm used to thinking of logic as being a foundation rather than having a foundation.
If pressed, though, I'm somewhat familiar with three approaches to explaining something I might loosely call the foundation of logic.
-
Model theory, where we build structures out of sets in a specific set theory (usually ZFC) and throw more set theory at the problem when we need things like tuples or symbols. I don't know if set theory is special here. Maybe you can use something else like second-order arithmetic.
-
Type theory, where we have individual terms and those terms, in some sense, are proofs. All of our inference rules transform the terms in addition to the types. In this setting, I think, logic is what you get when you ignore everything that appears to the left of a colon.
-
Games. I've seen a few things here and there on game semantics. The core analogy of game semantics makes a huge amount of intuitive sense to me, but I haven't read much about it besides a few articles.
Type theory has a deep connection to category theory that you obtain by noticing that terms are like arrows and types are like objects, and then seeing where that analogy takes you. I don't understand this analogy beyond a superficial level.
Best Answer
This not a full answer, but the point I want to make would not fit in a comment.
I think there are two conceptions of "logic" at play here, depending on what you want to use it for.
1. Logic as a foundation
This is the way you mentioned you are familiar to thinking about it, and I believe it is the most common use of logic. It makes perfect sense if you think as logic as a framework in which the maths happens, but then if you want it to be foundational, this framework needs to be specified outside of the realm of maths, as a primary notion. I have never been completely convinced that category theory really has a claim in that, even though some people say it does. I think there is an important caveat though that I will develop in point 3.
2. Logic as a tool to study mathematical objects
Another approach to logic, that I think is very common among logician, but maybe fairly less known to other mathematicians, is the use as logic tools in order to study the maths themselves. In this approach you really are free to set yourself up inside any foundational system that suits you, and develop all the arguments you want within this framework. With this description one shall ask "what is the difference with just doing normal maths", and indeed, there is no difference, except for the fact that logic wants to study the objects through the lens of formal systems. Let me give you an example of this approach, and how category theory plays a role in it
An example - Algebraic theories: Among all the mathematical structures that you might want to study (groups, rings, fields, vector spaces, algebras, topological spaces,...) You could isolate some of them which you can define using only certain kinds of formulas. In the example of algebraic theories, you want to restrict to first order formulas satisfying with only functions symbols, and satisfying some extra properties (see https://en.wikipedia.org/wiki/Algebraic_theory) for all the precise details. For instance, groups or fields are algebraic theories, whereas topological spaces are not. You can then study the properties of the mathematical things that can be defined as algebraic theories, and it turns out they have some properties, like they all have a notion of free thing.
Why category theory helps: In this approach to logic category theory can help in the sense that it can provide a nice way to encode the properties that you might want to study. Here I chose my example carefully to be algebraic theories, because these can be represented with a categorical gadget called a Lawvere theory (https://ncatlab.org/nlab/show/algebraic+theory). It is not important for my point that you go through the exact details on how these two notions correspond, although it is pretty interesting (I recall that there is a nice video of Emily Riehl explaining this in an introductory way). The point is, using objects and morphisms of a category, you can encode formulas that define a mathematical structure.
Quick recap: In this second approach that I have presented, logic is not used as a foundation for maths. Instead, you start by picking your favourite foundations, and then you study the relation between the mathematical structures and the formulas defining them whithin this foundations. Note that in this second approach I purposefully avoided using the word axiom - even though people would still use it for this. It's something I realised recently but there are two meanings of this word, depending on which approach you work with. In the foundational approach, an axiom is a fundamental truth that you take for granted to start reasoning (probably what you have in mind). But in the logic as a tool approach, people use axiom all the time to talk about the defining formulas of a structure (e.g. the axioms of groups). It's a bit anecdotal, but pondering a bit about why we use axioms in these two different ways helped me separate things a bit more formally.
3. Bootstrapping logic
Okay, so now comes my important caveat. You might wonder what would happen if you try to "bootstrapp" the first approach into the second approach. What I mean by that is that with my second approach, I am allowed to study mathematical structures defined by some formulas within a foundational framework. Now what if I were to plug in as formulas the axioms of my foundational structure? I would end up with a view of my foundational structure within my foundational structure. It is my understanding that it is not a very rare thing to consider. In particular, you could define the entire set theory but viewed within the foundational framework of set theory. To differentiate the two, I will say that the foundational framework is the meta-theory.
Now recall that category theory may help you express logic within a foundational framework. So in the meta-theory, we can define the categories (let's call them meta-categories, that's a name I just made up, to emphasize that they are categories defined in a foundational framework of the meta-theory). Now we can repeat the story of approach 2. We consider the formulas defining our structure (now I'll call them axioms, and just to be completely thorough about it, I'll call the formulas defining the meta-theory the meta-axioms). These formulas can usually be encoded using the meta-categories.
A notion that arises in such approach is that of a topos. From a logical point of view, it encodes axioms of things that behave a lot like sets do, and in particular the sets are a topos. Here I mean the sets as defined in the theory, not the one of the meta-theory. With this third view, you can see logic as a way to develop all the maths that you would like (within a fixed meta-theory), and you could develop all of it with only the (meta-)categories. So in this sense, (meta-)categories are a foundational framework for maths (within a fixed meta-theory).
Conclusion
The third part of my point is an approach that I know to be quite studied, and it works pretty well. In fact that is what most of the categorical is about. I want to add that I have read the claim that category theory could be a foundational framework, and I am never sure in which of the two above meaning it is meant to be. I have never seen any convincing argument to define category theory alone as a foundation for maths in a vacuum. That would imply defining categories as a primitive language, independently of set theory (or independently of type theory), but that does not mean it cannot be done. However, as I have described, you really can understand category theory as a foundation for maths internal to a fixed meta-theory!