# What's the difference between a logic, an internal logic (language) of a category, an internal logic of a topos and a type theory?

maybe this question doesn't make sense at all. I don't know exactly the meaning of all these concepts, except the internal language of a topos (and searching on the literature is not helping at all).

However, vaguely speaking by a logic I mean a pair $(\Sigma, \vdash)$ where $\Sigma$ is a signature (it has the types, functionals and relational symbols) and a consequence operator $\vdash$.

By an internal logic in a category I mean viewing each object as a type and each morphism as a term.

So what's the difference between a logic, an internal logic (language) of a category, an internal logic (language) of a topos and a type theory? Furthermore why the interchanging in the literature between the word "logic" and "language" when dealing with the internal properties of a category? Moreover, how higher order logic, modal logic and fuzzy logic suit in these concepts stated above?

The internal logic of a topos is an instance of the internal logic of a category (since toposes are special kinds of categories). The internal logic of toposes (instead of an arbitrary category) can also be interpreted with the Kripke-Joyal semantics. For more on this, check part D of Johnstone's Elephant and chapter VI of Mac Lane's and Moerdijk's Sheaves in Geometry and Logic, lecture notes by Thomas Streicher, and of course the nLab articles on these matters.

I don't know the term "internal logic of a type theory". But check the (very accessible) introduction of the HoTT book on how type theory and logic are related.

The terms "internal logic" and "internal language" are often used synonymously. Personally, I prefer "internal language", since this stresses that one can use it not only to reason internally, but also to construct objects and morphisms internally.

The internal language of a topos $\mathcal{E}$ is higher-order in the sense that, because of the existence of a subobject classifier, every object $X \in \mathcal{E}$ has an associated power object $\mathcal{P}(X) \in \mathcal{E}$ which one can quantify over in the internal language. (In the special case $\mathcal{E} = \mathrm{Set}$, the internal language is really the same as the usual mathematical language and $\mathcal{P}(X)$ is simply the power set of $X$.) In an arbitrary category, power objects need not exist, such that their internal language is (at best) first-order. Generally, richer categorical properties allow you to interpret greater fragments of first-order logic, this is neatly explained in Johnstone's part D.

Any Lawvere-Tierney topology in a topos gives rise to a modal operator in its associated internal language. (These operators can have concrete geometric meanings, for instance "on a dense open set it holds that" or "on an open neighbourhood of a point $x$ it holds that".)

I don't know of a direct relationship between fuzzy logic and the internal language of toposes, see an older question here.

• On little clarification, because this might give the impression that, as soon as you have a subobject classifier, you get power objects. You also need exponentials (i.e., Cartesian closure). Aug 15, 2014 at 21:55
• Thanks for the answer. But HoTT book deals only with a specific kind of type theory where types correspond to homotopy type of topological spaces. Furthermore, I still confused by the fact that there is no standard definition of a logic and dealing with signatures is not exact "logic", it's just a "interpretation" in a linguistic sense of a "logic". Moreover in a topos or a category it's not clear exact where is the signature of a logic (in the sense I have cited in my question). It's not clear too why there are more logics than categories. Aug 16, 2014 at 1:30
• @user40276: I'm not quite sure whether I understand you correctly. Let $\mathcal{C}$ be a category. Then the signature induced by $\mathcal{C}$ has all objects of $\mathcal{C}$ as sorts (this is terminology from the Elephant, in your question you said type), all morphisms as function symbols and all subobjects as relations. Andreas: You are quite right, of course. Aug 21, 2014 at 11:05
• Ok, so, for instance, a predicate symbol would be a subobject (in the case of first order logic)? Furthermore, I still confused by the fact that some references says that an internal language defines a theory and not a logic? Aug 21, 2014 at 12:49
• Yes, you are right that a predicate symbol would be a subobject. Nov 3, 2014 at 14:28

Your definition of logic is pretty much correct. A logic contains both the language which the signature $$\Sigma$$ generates and the deductive system defined by $$\vdash$$.

A type theory is a logic with different sorts of individuals (called "types") and constructions that generate new types from existing ones, like product and arrow types.

An internal logic is a type theory derived from a category and the internal language is the language part of that logic. Specifically, the atomic sorts of the internal language are the objects of the category. Since a topos is a specific category of categories, the internal logic of a topos is the derived type theory.

The modalities of modal logic can sometimes be related to operators on subobjects in a category, but only if they preserve logical equivalence: $$\alpha\iff\beta$$ should imply $$\Box\alpha \iff \Box \beta$$. Otherwise, the induced function of subobjects is not well-defined.

Fuzzy logic is misnamed. It is more like a model theory than a logic.

• Thanks for the answer. In an arbitrary category there is no power object nor subobject classifies, so I don't know how can you create $\forall$ and $\exists$ as adjoint functors. Aug 22, 2014 at 16:55
• Nobody said the internal logic of an arbitrary category was any good. That's why we like topoi, or at least Cartesian closed categories, so much. Aug 23, 2014 at 0:46
• Every part of the logic requires some structure on the category for a sound interpretation. Not much is needed for a poset of subobjects, however. If a category has pullbacks, then each morphism induces an inverse image map between these posets. If a category has Cartesian products then quantifiers are adjoints to the inverse image maps of these products. Aug 23, 2014 at 7:41
• So not every logic can be encoded as a category? If the answer is yes, it's kind of weird because I can always pick the free topos generated by some signature. Aug 26, 2014 at 17:14
• @user40276: youtube.com/watch?v=j4XT-l-_3y0. I would say that is a category of theories in higher order constructive logic L and a category of categories C and some bifunctor $L\to C$ that reflects equivalences of categories. Aug 28, 2014 at 8:32