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

Question

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?

Thanks in advance.

Answer 1

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.

Answer 2

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.