|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
One of the most important observations of category theory is that large parts of mathematics can be internalized in any category with sufficient structure. The most basic examples of this involve algebraic structures; for instance, a group can be defined in any category with finite products, and an internal category can be defined in any ambient category with pullbacks. For such algebraic (or even essentially algebraic) structures, which are defined by operations with equational axioms imposed, it suffices for the ambient category to have (usually finite) limits.
However, it turns out that if we assume some additional structure on the ambient category, then much more of mathematics can be internalized, potentially including fields, local rings, finite sets, topological spaces, even the field of real numbers. The idea is to exploit the fact that all mathematics can be written in the language of logic, and seek a way to internalize logic in a category with sufficient structure.
The basic ideas of the internal logic induced by a given category is this:
the maximal subobject is hence the proposition that is always true, this is the logical object of truth .
the minimal subobject is hence the proposition that is always false, this is the logical object of falsity .
and so on.
Once we formalize the notion of “logical theory”, the construction of the internal logic can be interpreted as a functor from suitably structured categories to theories. The morphisms of theories are “interpretations”, and so an internalization of some theory (such as the “theory of groups”) into a category is a morphism of theories .
Moreover, the functor has a left adjoint functor: the syntactic category of a theory. Thus, a model of in is equally well a functor . Frequently, this adjunction is even an equivalence of categories; see relation between type theory and category theory.
There are many different kinds of of “logical theories”, each of which corresponds to a type of category in which such theories can be internalized (and yields a corresponding adjunction ).
|finite product theory||category with finite products|
|finite limit (aka “left exact” or “cartesian”)||finitely complete category|
|disjunctive||lextensive category (aka finitary disjunctive category)|
|geometric||infinitary coherent category (aka geometric category)|
|dependent types||locally cartesian closed category|
|higher order||elementary topos|
|linear logic||symmetric monoidal category|
Each type of logic up through “geometric” can also be described in terms of sketches. Not coincidentally, the corresponding types of category show up through “geometric” fit into the framework of familial regularity and exactness. Sketches can also describe theories applicable to categories not even having finite products, such as finite sum sketches, but the type-theoretic approach taken on this page requires at least finite products (or else something closely akin, such as a cartesian multicategory).
However, there are other sorts of internalization that do not fit in this framework. For instance, to describe a monoid internal to a monoidal category, one needs an internal linear logic. See internalization for a discussion of the more general notion in the context of doctrines.
We begin with the interpretation of internal first-order logic, which is the most used in toposes and related categories.
In this section, what we mean by a theory is a type theory without dependent types, but with a dependent logic. This entails the following.
The signature of the theory consists of
Various types . For example, the theory of a group has only one type (group elements), but the theory of a-ring-and-a-module has two types (ring elements and module elements). There are also generally type constructors that build new types from basic ones, such as product types and the unit type .
The theory will also generally contain function symbols such as , each with a source and target that are types. For example, the theory of a monoid has one type , one function symbol , and one function symbol . Function symbols of source are also called constants.
The theory may also contain relation symbols , each equipped with a type. For example, the theory of a poset has one type and one relation . The most basic relation symbol, which most theories contain, is equality on a type .
Finally the theory may contain logical axioms of the form . Here and are first-order formulas built up from terms and relation symbols using logical connectives and quantifiers such as , and is a context which declares the type of every variable occurring in and .
For example, the theory of a group has one type , three function symbols , , and , and axioms
This is an equational theory?, meaning that each axiom is just one or more equations between terms that must hold in a given context. For a different sort of example, the theory of a poset has one type , one relation , and axioms
Now suppose that we have a category with finite limits and we want to interpret such a theory internally in . We identify the aspects of the theory with structures in the category by what is called categorical semantics:
First, for each type in the theory we choose an object of . Then for each function symbol in the theory we choose a morphism in . And finally, for each relation in the theory we choose a subobject in . (We always interpret the relation of equality on a type by the diagonal in .) Thus, for example, to interpret the theory of a group in we must choose an object and morphisms , , and , while to interpret the theory of a poset, we must choose an object and a subobject .
Of course, this is not enough; we need to say somehow that the axioms are satisfied. We first define, inductively, an interpretation of every term that can be constructed from the theory by a morphism in . For example, given an object and a morphism , there are two evident morphisms which are the interpretations of the two terms and .
We then define, inductively, an interpretation of every logical formula? that can be constructed from the theory by a subobject in . The idea is that if is a variable of type and is a formula with as its free variable, then the interpretation of should be the “subset” of . The base case of this induction is that if is a term interpreted by a morphism and is a relation symbol, then is interpreted by the pullback of the chosen subobject representing along the morphism . The building blocks of logical formulas then correspond to operations on the posets of subobjects in , as follows.
|Logical operator||Operation on|
|truth:||top element ( itself)|
|falsity:||bottom element (strict initial object)|
|existential quantification:||left adjoint to pullback|
|universal quantification:||right adjoint to pullback|
The fact that existential and universal quantifiers can be interpreted as left and right adjoints to pullbacks was first realized by Bill Lawvere. One way to realize that it makes sense is to notice that in Set, the image of a subset under a function can be defined as
while its “dual image” (the right adjoint to pullback) can be defined as
Of course, in not all finitely complete categories do all these operations on subobjects exist. Moreover, in order for the relationship with logic to be well-behaved, any of these operations we make use of must be stable under (preserved by) pullbacks. (Pullbacks of subobjects correspond to “innocuous” logical operations such as adding extra unused variables, duplicating variables, and so on, so they should definitely not affect the meaning of the logical connectives. However, in linear logic such operations become less innocuous.)
In any category with finite limits, the posets always have finite intersections (given by pullback), including a top element (given by itself). Thus in any such category, we can interpret logical theories that use only the connectives and . This includes both the theories of groups and posets considered above.
In a regular category, the existence of pullback-stable images implies that the base change functor along any map has a left adjoint, usually written , and that these adjoints “commute with pullbacks” in an appropriate sense (given by the Beck-Chevalley condition. Thus, in a regular category we can interpret any theory in so-called regular logic, which uses only , , and .
Actually, some instances of can be interpreted in any category with finite limits: if is itself a monomorphism, then always has a left adjoint simply given by composition with . On the logical side, this means that we can interpret “provably unique existence” in any category with finite limits. Logic with , , and “provably unique existence” is called cartesian logic or finite-limit logic.
A coherent category is basically defined to be a regular category in which the subobject posets additionally have pullback-stable finite unions. Thus, in a coherent category we can interpret so-called coherent logic, which adds and to regular logic. Likewise, in an infinitary-coherent (or “geometric”) category we can interpret geometric logic, which adds infinitary disjunctions to coherent logic. Geometric logic is especially important because it is preserved by the inverse image parts of geometric morphisms, and because any geometric theory has a classifying topos.
On the other hand, in a lextensive category, we do not have images or all unions, but if we have two subobjects of which are disjoint (their intersection is initial), then their coproduct is also their union in . Therefore, in a lextensive category we can interpret disjunctive logic, which is cartesian logic plus and “provably disjoint disjunction.” Likewise, in an infinitary-lextensive category we can interpret “infinitary-disjunctive logic.”
Finally, in a Heyting category the base change functors also have right adjoints, usually written , and it is easy to see that this implies that each is also a Heyting algebra, hence has an “implication” as well. (We define “negation” by .) Thus, in a Heyting category we can interpret all of (finitary, first-order) intuitionistic logic.
Now that we know how to interpret logic, we can say that a model of a given theory in consists of a choice of objects, morphisms, and subobjects for the types, function symbols, and relation symbols as above, such that for each axiom , we have in . Here, is the product of the objects that correspond to the types of the variables in , and are the interpretations of the formulas and as subobjects of , and is the relation of subobject inclusion.
It is easy to verify that a model of the theory of a group in is precisely an internal group object in , as usually defined. For instance, the validity of the axiom
means that the equalizer of the two morphisms must be all of , or equivalently that those two morphisms must be equal. The same happens in most other cases.
As described above, a model of a given theory in a category consists of an assignment
|types of||objects of|
|function symbols of||morphisms of|
|relation symbols of||subobjects in|
|axioms of||containments in|
This is a sort of heteromorphism in that it changes the name of things as it operates on them. We can describe it more simply as a “translation of theories” as follows.
Given a category (which may be regular, coherent, geometric, Heyting, etc.), we define its internal type theory (with first-order logic) to be the theory whose
Now a model of in can be described simply as a morphism of theories (a “translation” or “interpretation”)
The functor has a left adjoint, the syntactic category of a theory. Thus we have a chain of natural isomorphisms
Internal logic is not just a way to concisely describe internal structures in a category, but also gives us a way to prove things about them by “internal reasoning.” We simply need to verify that the “usual” methods of logical reasoning (for example, from and deduce ) are internally valid, in the sense that if the premises are satisfied in some model (in the example, if and ) then so is the conclusion (in the example, ). This is called the Soundness Theorem.
It then follows that if we start from the axioms of a theory and “reason normally” within type theory, which in practice amounts to pretending that the types are sets, the function symbols are functions, and the relation symbols are subsets, then anything we prove will still be true when the theory is interpreted in an arbitrary category, not just Set. For example, by easy equational reasoning from the theory of a group, we can prove that inverses are unique, which is expressed by the logical sequent
It follows that this is also true, suitably interpreted, as a statement about internal group objects in any category.
There are (at least) three caveats. Firstly, we must take care to use only the rules appropriate to the fragment of logic that is valid in the particular categories we are interested in. For example, if we want our conclusions to be valid in any regular category, we must restrict ourselves to reasoning “within regular logic.” Most mathematicians are not familiar with making such distinctions in their reasoning, but in practice most things one would want to say about a regular theory turn out to be provable in regular logic. (We will not spell out the details of what this means.) And once we are in a Heyting category, and in particular in a topos, this problem goes away and we can use full first-order logic.
The second, more important, caveat is that the internal logic of all these categories is, in general, constructive. This means that, among other things, the interpretation of is, in general, distinct from that of , and that is not always valid. So even if we believe that classical logic (including the principle of excluded middle and even the axiom of choice) is “true,” as many mathematicians do, there is still a reason to look for proofs that are constructively acceptable, since it is only these which are valid in the internal logic of most categories. If the category is Boolean and/or satisfies the internal axiom of choice, however, then this problem goes away, but these fail in many categories in which one wants to internalize (such as many Grothendieck toposes).
The third caveat is that one must take care to distinguish the internal logic of a category from what is externally true about it. In general, internal validity is “local” truth, meaning things which become true “after passing to a cover.” This is particularly important for formulas involving disjunction and existence. For example, an object’s being projective in the category is a different statement from its being internally projective, meaning that “ is projective” is true in the internal logic. Another good example can be found in the different notions of finite object in a topos. This problem goes away if the ambient category is well-pointed, but well-pointed categories are even rarer than Boolean ones satisfying choice; the only well-pointed Grothendieck topos is Set itself.
The converse of the Soundness Theorem is called the Completeness Theorem, and states that if a sequent is valid in every model of a theory, then it is provable from that theory. This is noticeably less trivial. In classical first-order logic, where the only models considered are set-valued ones, the completeness theorem is usually proven using ultraproducts. However, in categorical logic there is a more elegant approach (which additionally no longer depends on any form of the axiom of choice).
The syntactic category of a theory was mentioned above, as the left adjoint to the “internal logic functor” . By the Yoneda lemma, the syntactic category contains a “generic” model of the theory. Moreover, by the construction of (see syntactic category), the valid sequents in this model are precisely those provable from the theory. Therefore, if a sequent is valid in all models, it is in particular valid in the generic model in , and hence provable from .
The universal property of is also sometimes useful for semantic conclusions. For instance, sometimes one can prove something about the generic model and then carry it over to all models.
Furthermore, if lives in a sub-fragment of geometric logic (such as regular, coherent, lextensive, or geometric logic), then the Grothendieck topos of sheaves on for its appropriate (regular, coherent, extensive, or geometric) coverage contains a -model which is generic for models in Grothendieck toposes: any -model in a Grothendieck topos is its image under the inverse image of a unique geometric morphism. This topos is called the classifying topos of the theory.
The syntactic category of a theory can be considered as the “extensional essence” of that theory, since functors out of completely determine the -models in any category with suitable structure. It therefore makes sense, in some contexts, to define a morphism of theories to be a functor between their syntactic categories, and an equivalence of theories (sometimes called a Morita equivalence) to be an equivalence between their syntactic categories.
A morphism between theories, in this sense, induces a functor from -models in to -models in , for any category with suitable structure, in a way which is natural in . In particular, theories which are “Morita equivalent” in this sense have naturally equivalent categories of models in all categories with suitable structure; so they have the same “meaning” even though they may be presented quite differently. (Note that this is a much stronger sort of equivalence than merely having equivalent categories of models in some particular category, such as .) Moreover, the fact that the syntactic category is defined “syntactically” means that a morphism actually induces a “translation” of the types, functions, and relations of into those of .
By first applying various “completion” processes to syntactic categories before asking about equivalence, we obtain coarser notions of equivalence, which only induce equivalences of models in more restricted sorts of categories. For instance, if we compare the exact completions of syntactic categories of regular theories, we obtain a notion of equivalence that induces equivalences of categories of models in all exact categories (not necessarily all regular ones). Likewise for coherent theories and pretoposes, and for geometric theories and infinitary pretoposes. Note, though, that the infinitary-pretopos completion of a (small) geometric theory is in fact already a (Grothendieck) topos, and coincides with the classifying topos considered above. Thus, passage to classifying toposes is also an instance of this construction, and an equivalence of classifying toposes means that two theories have equivalent categories of models in all toposes. (This is still much stronger than just having equivalent categories of models in .)
To be written, but see Kripke-Joyal semantics.
Material to be moved here from relation between type theory and category theory.
consisting only of the two trivial subobjects of , the point itself and the empty set, and the unique inclusion morphism between them. These are classified, respectively, by the truth values and , so that we can also write our poset of subobjects of the terminal object as
from which we deduce that
Similarly for we have
from which we deduce that
We discuss the internal logic of this sheaf topos (originally Tarski, 1938).
In the presheaf topos , the subobjects of are arbitrary sieves in , not just representables. For instance, for any two open sets and there is a sieve consisting of all open sets contained in either or , which doesn’t necessarily contain . It’s only in the sheaf topos that the representables are precisely the subobjects of .
The logical operation is the product in : this is the intersection of open subsets.
The logical operation is the coproduct in : this is the union of open subsets.
The internal hom in is given by
(the interior of the union of the complement of with V).
So negation is given by sending an open subset to the interior of its complement:
In particular we find that in the internal logic of the law of the excluded middle fails in general, as in general we do not have that
because is the total space without the boundary (frontier) of , and not , all of the total space.
Most books on topos theory develop some internal logic, at least in the context of a topos. For example:
Goldblatt, Topoi: the categorial analysis of logic
Part D of
works in the even more general context of fibrations, allowing us to associate to each object an arbitrary poset instead of .
is arguably all about this subject (although you wouldn't know it until about Chapter VIII), but from a different perspective. In particular, Taylor allows us to replace having all pullbacks with pullbacks along a pullback-stable class of display morphisms.
The observation that the poset of open subsets of a topological space serve as a model for intuitionistic logic is apparently originally due to