Is category theory as philosophically intuitive as basic logic?

So far as I understand, category theory can be used as foundations of mathematics as in that the rest of logic can be defined through categorical ideas.

However is category theory as natural a starting point as logic when one wishes to think mathematically?

I’ve often seen that logic is studied outside the context of mathematics in the humanities. However, I never heard of anyone who is in fields related to the humanities speaking about category theory. I'm trying to figure out if this is because of category theory being relatively new mathematics or because it is a less natural/more convoluted starting point to the study of the world.

• Category theory uses basic logic, so it is not the "starting point" anyway. And ZFC set theory, which is a more apples to apples comparison for foundations, is not much taught in humanities either. For applications of category theory to arts, see Mannone. Commented Mar 28 at 11:02
• Type theory is the 'internal logic' of certain categories, and type theory can be used in place of FOL. Cf. e.g. Mike Shulman's article "From Set Theory to Type Theory" and Lambek and Scott's "Reflections on a Categorical Foundation of Mathematics". Commented Mar 28 at 11:14
• I don't think category theory provides what can legitimately be called a foundation of mathematics because it only describes structures; it does not build up those structures like set theory does. What it does can be better described as providing insight into mathematics than a foundation for mathematics. Commented Mar 28 at 15:27
• To nip off the motte-and-bailey argument in the final paragraph, an example of category theory in the humanties is Montague semantics for natural languages. Let answers focus on the relationship between category theory and logic. Commented Aug 25 at 16:09
• @DavidGudeman: To summarize McLarty 2004 (PDF), it's known that ZFC is bi-interpretable with ETCS plus an Axiom of Replacement. ETCS is wholly structural; it may be stated topos-theoretically as studying "the well-pointed topos with NNO and Choice", a common description of the category of ZFC-style sets. This leads to neutral set theory. Commented Aug 25 at 16:16

Disclaimer: all of the following are what I think to be true but am not certain.

Is category theory as philosophically intuitive as basic logic?

Lawvere first suggested that category theory could be an alternative to set theory as a foundation of mathematics. Set theory can be written in the specification language of first order logic. The same is true for category theory. Lawvere developed a set of axioms which would be written in a formal logic. These axioms define the structure of categories, but they are themselves defined in logic. So it might be a misunderstanding to think that category theory is meant to replace logic.

So far as I understand, category theory can be used as foundations of mathematics as in that rest of logic can be defined through categorical ideas.

There might be some truth to this. You would probably want to check out topos theory. I don’t know enough about it yet, but in topos theory, a category has an “internal logic”. Thus, a category is a structural way of representing a given logic (intuitionistic, regular, minimal, higher order, etc.)

However is category theory as natural starting point as logic when one wishes to think mathematically?

Category theory is more abstract. It tends to be harder upfront, but divinely illuminating, and simplifying, over time. From what I have seen, those people who are partial to category theory do not merely just like category theory, they revere it. Once you go categorical, you don’t go back. Any question you are pursuing with set theory can be categorified, and it gives you a completely different view on the same phenomenon. https://ncatlab.org/nlab/show/horizontal+categorification

Ive often seen that logic is studied outside the context of mathematics in humanities. However I never heard about anyone who is in fields related to humanities speaking about category theory.

It is happening right now in the world as we speak. People like David Spivak have suggested that category theory has potential as a way to model ontologies: https://arxiv.org/abs/1102.1889 Many extremely good category theorists right now are working on categorical data science. Spivak has worked at the company Uber to implement more categorical data structures into their operations. Categorical data is a revolution, because it allows data to be way more inter-operable, and it facilitates expressing things in a compositional way, so that there is a strong computable structure relating the concepts being modeled. String diagrams, a category-theoretic visual diagram, are being used to model systems in general and verify properties about them.

I'm trying to figure out if this is because of category theory being relatively new mathematics or while is a less natural/more convoluted starting point to the study of the world.

You could argue that category theory is less naturally intuitive, at first. It was only invented in the 1950’s. One mathematician has said “what mathematics is to the world, category theory is to mathematics”. The key thing is in doing the mental work to understand some of the concepts, what you gain is unbelievable levels of generalization, which results both in much deeper, universal knowledge (as in, instead of knowing something about one particular member of a class of mathematical objects, you can know something about the class of all of them), but also ultimately much simpler understanding too.

• Lawvere started writing about category theory no earlier than the late 60s and 70s. Eilenberg, McLane, and others were already using it in the 1950s. Commented Mar 28 at 11:14
• Comments to various points above: CT as "foundational" language compared to Set Theory (and not so much to logic). Commented Mar 28 at 12:25
• "However is category theory as natural starting point..." For old math practiotioners (like me) set theory is more "natural" compared to CT as well as standard predicate logic presentation is more "natural" wrt old type-theoretic one (that of Church; very cumbersoime). But things changed: modern (Martin-Lof) TT is much more simple (Natural Deduction presentation...) and computation-oriented; thus, more friendly for "youngs". Commented Mar 28 at 12:28
• "logic is studied outside the context of mathematics in humanities. Correct, but only a small part of ST can be applied in humanities, and similar for CT. Commented Mar 28 at 12:29

Surprisingly, category theory corresponds to formal logic, so the answer is necessarily yes and the fusion of techniques is known as categorical logic (WP, nLab). In the next two paragraphs, I'll crib from the computational trilogy tables and also a page specifically relating type theory and category theory.

For example, here's a basic warmup in sentential logic. We have sentences P, Q, S, etc. We also have implications, like an implication PQ from P to Q. For any two implications like PQ and QR, where the target of one implication is the source of another, we have a syllogism leading to the implication PR. Every sentence P has an implication called its "identity", PP, and syllogism with identity doesn't do anything. For now, suppose there is at most one implication between any two sentences.

In category theory, this sort of logic corresponds to a thin category (WP, nLab); replace "sentences" by "objects", "implications" by "morphisms" (or "arrows", etc.) and "syllogism" by "composition". In this sense, any non-bogus intuition about traditional logic is directly portable to categorical logic.

For example, where's modus ponens? Normally our logic of syllogisms will admit that, if P is a sentence and PQ is an implication, then Q is a sentence too. This is also admitted in category theory. But the existence of target objects is not as difficult as the existence of implications, so this usually leads to a desire for a trivially-true sentence 1 and a desire to deduce facts by syllogizing elementarily-true implications 1P with transformative implications PQ to obtain non-trivial elementary truths 1Q. Category theory does all of that too, and has a notion of generalized elements.

I think that the intuition complaints start when considering features of category theory which aren't used often enough by logicians to have classical names. The simplest example is likely via commutative diagrams (WP, nLab). A diagram is, intuitively, a tool for making schematic claims; a diagram is a schema over some objects and arrows along with some requirements for how they interrelate.

For example, let us return to sentential logic and consider a diagram over some object P containing the single sentence P and the identity implication PP. This diagram is known to category theorists as "the walking object", because for any choice of sentence, we can construct the diagram above it by highlighting its identity implication. A logician might scoff at the silly nomenclature, not realizing that we can make walking isomorphisms, walking binary operators, walking algebriac theories, walking equivalences and walking adjunctions/Galois connections, walking first-order theories, etc.