nLab internal logic



Categorical algebra

Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




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 strict 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, if we assume that the ambient category has additional structure, 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 CC are:

  • the objects AA of CC are regarded as collections of things of a given type AA

  • the morphisms ABA\to B of CC are regarded as terms of type BB containing a free variable of type AA (i.e. in a context x:Ax:A)

  • a subobject ϕA\phi \hookrightarrow A is regarded as a proposition (predicate): by thinking of it as the sub-collection of all those things of type AA for which the statement ϕ\phi is true

    • the maximal subobject is hence the proposition that is always true; this is the logical object of truth A\top \hookrightarrow A

    • the minimal subobject is hence the proposition that is always false; this is the logical object of falsity A\bottom \hookrightarrow A

    • one proposition implies another if as subobjects of AA they are connected by a morphism in the poset of subobjects: ϕψ\phi \Rightarrow \psi means ϕψ\phi \hookrightarrow \psi

  • Logical operations are implemented by universal constructions on subobjects.

and so on.

  • A dependent type over an object AA of CC may be interpreted as a morphism BAB\to A whose “fibers” represent the types B(x)B(x) for x:Ax:A. This morphism might be restricted to be a display map or a fibration.

Once we formalize the notion of “logical theory”, the construction of the internal logic can be interpreted as a functor LangLang from suitably structured categories to theories. The morphisms of theories are “interpretations”, and so an internalization of some theory TT (such as the “theory of groups”) into a category CC is a morphism of theories TLang(C)T\to Lang(C).

Moreover, the functor LangLang has a left adjoint functor: the syntactic category SynSyn of a theory. Thus, a model of TT in CC is equally well a functor Syn(T)CSyn(T)\to C. Frequently, this adjunction is even an equivalence of categories; see relation between type theory and category theory.

Kinds of internal logics in different categories

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 SynLangSyn \dashv Lang).

Lawvere (or “finite product”)category with finite products
cartesian/essentially algebraic (or “left exact” or “finite limit”)finitely complete category
minimal logiccartesian closed category
regularregular category
coherentcoherent category
disjunctivepre-lextensive category
geometricinfinitary coherent category (aka geometric category)
constructive first-orderHeyting category
classical first-orderBoolean category
extensional dependent typeslocally cartesian closed category
constructive higher orderelementary topos
classical higher orderBoolean topos
linear logicsymmetric monoidal category
cohesive modal logiccohesive topos

Each type of logic up to and including “geometric” can also be described in terms of sketches. Not coincidentally, the corresponding types of category up to and including “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.

Internal first-order logic

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 A,B,CA,B,C. 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 A×BA\times B and the unit type 11.

    • The theory will also generally contain function symbols such as f:ABf:A\to B, each with a source and target that are types. For example, the theory of a monoid has one type MM, one function symbol m:M×MMm:M\times M\to M, and one function symbol e:1Me:1\to M. Function symbols of source 11 are also called constants.

    • The theory may also contain relation symbols R:AR:A, each equipped with a type. For example, the theory of a poset has one type PP and one relation :P×P\le:P\times P. The most basic relation symbol, which most theories contain, is equality = A:A×A=_A:A\times A on a type AA.

  • Finally the theory may contain logical axioms of the form Γ|φψ\Gamma | \varphi \vdash \psi. Here φ\varphi and ψ\psi are first-order formulas built up from terms and relation symbols using logical connectives and quantifiers such as ,,,,,¬,,\top,\bot,\wedge,\vee,\Rightarrow,\neg,\forall,\exists, and Γ\Gamma is a context which declares the type of every variable occurring in φ\varphi and ψ\psi.

For example, the theory of a group has one type GG, three function symbols m:G×GGm:G\times G\to G, i:GGi:G\to G, and e:1Ge:1\to G, and axioms

x:G,y:G,z:G|m(m(x,y),z)=m(x,m(y,z)) x:G|m(x,i(x))=em(i(x),x)=e x:G|m(x,e)=xm(e,x)=x.\array{ x:G,y:G,z:G | \top \vdash m(m(x,y),z) = m(x,m(y,z))\\ x:G | \top \vdash m(x,i(x)) = e \;\wedge\; m(i(x),x) = e\\ x:G | \top \vdash m(x,e) = x \;\wedge\; m(e,x) = x. }

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 PP, one relation :P×P\le:P\times P, and axioms

x:P|xx x:P,y:P|xyyxx=y x:P,y:P,z:P|xyyzxz.\array{ x:P | \top \vdash x\le x\\ x:P,y:P | x\le y \;\wedge\; y\le x \vdash x=y\\ x:P,y:P,z:P | x\le y \;\wedge\; y\le z \vdash x\le z. }

Categorical semantics

Now suppose that we have a category CC with finite limits and we want to interpret such a theory internally in CC. 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 CC. Then for each function symbol in the theory we choose a morphism in CC. And finally, for each relation in the theory we choose a subobject in CC. (We always interpret the relation of equality on a type AA by the diagonal AA×AA\hookrightarrow A\times A in CC.) Thus, for example, to interpret the theory of a group in CC we must choose an object GG and morphisms m:G×GGm:G\times G\to G, i:GGi:G\to G, and e:1Ge:1\to G, while to interpret the theory of a poset, we must choose an object PP and a subobject []P×P[\le] \hookrightarrow P\times P.

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 CC. For example, given an object GG and a morphism m:G×GGm:G\times G\to G, there are two evident morphisms G×G×GGG\times G\times G \to G which are the interpretations of the two terms m(m(x,y),z)m(m(x,y),z) and m(x,m(y,z))m(x,m(y,z)).

We then define, inductively, an interpretation of every logical formula? that can be constructed from the theory by a subobject in CC. The idea is that if x:Ax:A is a variable of type AA and φ(x)\varphi(x) is a formula with xx as its free variable, then the interpretation of φ(x)\varphi(x) should be the “subset” {xA|φ(x)}\{x\in A | \varphi(x)\} of AA. The base case of this induction is that if tt is a term interpreted by a morphism ABA\to B and R:BR:B is a relation symbol, then R(t)R(t) is interpreted by the pullback of the chosen subobject RBR\hookrightarrow B representing RR along the morphism t:ABt:A\to B. The building blocks of logical formulas then correspond to operations on the posets Sub(A)Sub(A) of subobjects in CC, as follows.

Logical operatorOperation on Sub(A)Sub(A)
conjunction: \wedgeintersection (pullback)
truth: \toptop element (AA itself)
disjunction: \veeunion
falsity: \botbottom element (strict initial object)
implication: \RightarrowHeyting implication
existential quantification: \existsleft adjoint to pullback
universal quantification: \forallright 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 RAR\subset A under a function f:ABf:A\to B can be defined as

{bB|(aA)(aRf(a)=b)},\{b\in B | (\exists a\in A)(a\in R \;\wedge\; f(a)=b)\},

while its “dual image” (the right adjoint to pullback) can be defined as

{bB|(aA)(f(a)=baR)}.\{b\in B | (\forall a \in A)(f(a)=b \Rightarrow a\in R)\}.

Of course, not in all finitely complete categories CC do all these operations on subobjects exist. Moreover, in order for the relationship with logic to be well-behaved, any of the 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 Sub(A)Sub(A) always have finite intersections (given by pullback), including a top element (given by AA itself). Thus in any such category, we can interpret logical theories that use only the connectives \wedge and \top. 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 f *:Sub(B)Sub(A)f^*:Sub(B)\to Sub(A) along any map f:ABf:A\to B has a left adjoint, usually written f\exists_f, 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 \wedge, \top, and \exists.

Actually, some instances of \exists can be interpreted in any category with finite limits: if ff is itself a monomorphism, then f *f^* always has a left adjoint, given simply by composition with ff. On the logical side, this means that we can interpret “provably unique existence” in any category with finite limits. Logic with \wedge, \top, 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 \vee and \bot to regular logic. Likewise, in an infinitary-coherent (or “geometric”) category we can interpret geometric logic, which adds infinitary disjunctions iφ i\bigvee_i \varphi_i 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 AA which are disjoint (their intersection is initial), then their coproduct is also their union in Sub(A)Sub(A). Therefore, in a lextensive category we can interpret disjunctive logic, which is cartesian logic plus \bot 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 f *:Sub(B)Sub(A)f^*:Sub(B)\to Sub(A) also have right adjoints, usually written f\forall_f, and it is easy to see that this implies that each Sub(A)Sub(A) is also a Heyting algebra, hence has an “implication” \Rightarrow as well. (We define “negation” by ¬φφ\neg \varphi \equiv \varphi \Rightarrow \bot.) 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 CC consists of a choice of objects, morphisms, and subobjects for the types, function symbols, and relation symbols as above, such that for each axiom Γ|φψ\Gamma | \varphi \vdash \psi, we have [φ][ψ][\varphi]\le [\psi] in Sub([Γ])Sub([\Gamma]). Here, [Γ][\Gamma] is the product of the objects that correspond to the types of the variables in Γ\Gamma, [φ][\varphi] and [ψ][\psi] are the interpretations of the formulas φ\varphi and ψ\psi as subobjects of [Γ][\Gamma], and \leq is the relation of subobject inclusion.

It is easy to verify that a model of the theory of a group in CC is precisely an internal group object in CC, as usually defined. For instance, the validity of the axiom

x:G,y:G,z:G|m(m(x,y),z)=m(x,m(y,z))x:G,y:G,z:G | \top \vdash m(m(x,y),z) = m(x,m(y,z))

means that the equalizer of the two morphisms G×G×GGG\times G\times G \to G must be all of G×G×GG\times G\times G, or equivalently that those two morphisms must be equal. The same happens in most other cases.

The internal logic as a functor

As described above, a model of a given theory TT in a category CC consists of an assignment

types of TT\toobjects of CC
function symbols of TT\tomorphisms of CC
relation symbols of TT\tosubobjects in CC
axioms of TT\tocontainments in CC

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 CC (which may be regular, coherent, geometric, Heyting, etc.), we define its internal type theory (with first-order logic) Lang(C)Lang(C) to be the theory whose

  • types are the objects of CC;
  • function symbols are the morphisms on CC;
  • relation symbols are the subobjects in CC;
  • axioms are the containments in CC.

Now a model of TT in CC can be described simply as a morphism of theories (a “translation” or “interpretation”)

TLang(C).T \to Lang(C).

The functor Lang:CategoriesTheoriesLang : Categories \to Theories has a left adjoint, the syntactic category of a theory. Thus we have a chain of natural isomorphisms

Theories(T,Lang(C))Models(T,C)Categories(Syn(T),C)). Theories(T,Lang(C)) \cong Models(T,C) \cong Categories(Syn(T),C)).

Soundness and internal reasoning

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 φψ\varphi\vdash \psi and ψχ\psi\vdash \chi deduce φχ\varphi\vdash\chi) are internally valid, in the sense that if the premises are satisfied in some model CC (in the example, if [φ][ψ][\varphi]\le [\psi] and [ψ][χ][\psi]\le [\chi]) then so is the conclusion (in the example, [φ][χ][\varphi]\le [\chi]). 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

x:G,y:G,z:G|m(x,y)=em(x,z)=ey=z.x:G,y:G,z:G | m(x,y)=e \;\wedge\; m(x,z)=e \vdash y=z.

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 ¬¬φ\neg\neg\varphi is, in general, distinct from that of φ\varphi, and that φ¬φ\varphi\vee \neg\varphi 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 CC is a different statement from its being internally projective, meaning that “XX 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.

Completeness, syntactic categories, and Morita equivalence

The converse of the Soundness Theorem is called the Completeness Theorem, and states that if a sequent φψ\varphi\vdash\psi 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 C T=Syn(T)C_T = Syn(T) of a theory TT was mentioned above, as the left adjoint to the “internal logic functor” LangLang. By the Yoneda lemma, the syntactic category C TC_T contains a “generic” model of the theory. Moreover, by the construction of C TC_T (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 C TC_T, and hence provable from TT.

The universal property of C TC_T 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 TT lives in a sub-fragment of geometric logic (such as regular, coherent, lextensive, or geometric logic), then the Grothendieck topos of sheaves on C TC_T for its appropriate (regular, coherent, extensive, or geometric) coverage contains a TT-model which is generic for models in Grothendieck toposes: any TT-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 C TC_T completely determine the TT-models in any category DD 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 TTT\to T' between theories, in this sense, induces a functor from TT'-models in DD to TT-models in DD, for any category DD with suitable structure, in a way which is natural in DD. In particular, theories which are “Morita equivalent” in this sense have naturally equivalent categories of models in all categories DD 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 SetSet.) Moreover, the fact that the syntactic category is defined “syntactically” means that a morphism TTT\to T' actually induces a “translation” of the types, functions, and relations of TT into those of TT'.

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 SetSet.)

Kripke–Joyal semantics

To be written, but see Kripke-Joyal semantics.

Dependent type theory

We now consider the internal language of a locally cartesian closed category as a dependent type theory.

Material to be moved here from relation between type theory and category theory.

Higher-order logic

To be written, but see Mitchell–Bénabou language for the version in a topos.


Internal logic in SetSet

The topos Set in classical mathematics of course has as its internal logic the “ordinary” logic. This is reproduced by following the abstract nonsense as follows:

the terminal object of Set is the one-element set *{*}, the subobject classifier in Set is the two-element set Ω={true,false}\Omega = \{true, false\} equipped with the map

T:*Ω T : {*} \to \Omega

that picks the element truetrue in Ω\Omega. The Heyting algebra of subobjects of the terminal object is the poset

L={*} L = \{ \emptyset \hookrightarrow {*} \}

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 *trueΩ{*} \stackrel{true}{\to} \Omega and *falseΩ{*} \stackrel{false}{\to} \Omega, so that we can also write our poset of subobjects of the terminal object as

L={falsetrue}. L = \{ false \to true \} \,.

The logical operation =AND\wedge = AND is the product in the poset LL. Indeed we find pullback diagrams in LL

true×true=true true truetrue×false=false false truefalse×false=false false false. \array{ true \times \true = true &\to& true \\ \downarrow \\ true } \;\;\; \;\;\; \;\;\; \array{ true \times false = false &\to& false \\ \downarrow \\ true } \;\;\; \;\;\; \;\;\; \array{ false \times false = false &\to& false \\ \downarrow \\ false } \,.

The logical operation =OR\vee = OR is the coproduct in the poset LL. Indeed we find pushout diagrams in LL

true true truetrue=true false true truefalse=true false false falsefalse=false. \array{ && true \\ && \downarrow \\ true &\to& true \coprod \true = true } \;\;\;\; \;\;\; \;\;\; \array{ && false \\ && \downarrow \\ true &\to& true \coprod false = true } \;\;\;\; \;\;\; \;\;\; \array{ && false \\ && \downarrow \\ false &\to& false \coprod false = false } \,.

The logical operation ¬=NOT\not = NOT is given by the internal hom into the initial object in LL:

¬=hom(,false):L opL. \not = hom(-, false) : L^{op} \to L \,.

We find the value of the internal hom by its defining adjunction. For hom(true,false)hom(true,false) we have

Hom L(true,hom(true,false))Hom L(true×true,false)=Hom L(true,false)= Hom_L(true, hom(true,false)) \simeq Hom_L(true \times true, false) = Hom_L(true, false) = \emptyset


Hom L(false,hom(true,false))Hom L(false×true,false)=Hom L(false,false)=* Hom_L(false, hom(true,false)) \simeq Hom_L(false \times true, false) = Hom_L(false, false) = {*}

from which we deduce that

hom(true,false)=false. hom(true,false) = false\,.

Similarly for hom(false,false)hom(false,false) we have

Hom L(true,hom(false,false))Hom L(true×false,false)=Hom L(false,false)=* Hom_L(true, hom(false,false)) \simeq Hom_L(true \times false, false) = Hom_L(false, false) = {*}


Hom L(false,hom(false,false))Hom L(false×false,false)=Hom L(false,false)=* Hom_L(false, hom(false,false)) \simeq Hom_L(false \times false, false) = Hom_L(false, false) = {*}

from which we deduce that

hom(false,false)=true. hom(false,false) = true \,.

This way all the familiar logical operations are recovered from the internal logic of the topos Set.

Internal logic in a sheaf topos on open subsets

Let XX be a topological space and Op(X)Op(X) its category of open subsets and Sh(X):=Sh(Op(X))Sh(X) := Sh(Op(X)) the Grothendieck topos of sheaves on XX.

We discuss the internal logic of this sheaf topos (originally Tarski, 1938).

The terminal object is the sheaf represented by XX: the one that is constant on the one-element set

X:U*. X : U \mapsto {*} \,.

The subobjects of this object are the representable presheaves

hom(,V):U{* |ifUV otherwise hom(-,V) : U \mapsto \left\{ \array{ {*} & | if U \subset V \\ \emptyset & otherwise } \right.

for VOp(X)V \in Op(X).


In the presheaf topos PSh(Op(X))=Func(Op(X) op,Set)PSh(Op(X))= Func(Op(X)^{op},Set), the subobjects of 11 are arbitrary sieves in Op(X)Op(X), not just representables. For instance, for any two open sets UU and VV there is a sieve consisting of all open sets contained in either UU or VV, which doesn’t necessarily contain UVU\cup V. It’s only in the sheaf topos Sh(X)Sh(X) that the representables are precisely the subobjects of 11.

The poset of subobjects formed by these is just the category of open subsets itself:

L=Op(X). L = Op(X) \,.
  • The logical operation ANDAND is the product in Op(X)Op(X): this is the intersection of open subsets.

  • The logical operation OROR is the coproduct in Op(X)Op(X): this is the union of open subsets.

  • The internal hom in Op(X)Op(X) is given by

    hom(U,V)=(U cV) hom(U,V) = (U^c \vee V)^\circ

    (the interior of the union of the complement of UU with V).

    So negation is given by sending an open subset to the interior of its complement:

    ¬U=hom(U,)=(U c) =(U c) . \not U = hom(U,\emptyset) = (U^c \vee \emptyset)^\circ = (U^c)^\circ \,.

In particular we find that in the internal logic of PSh(X)PSh(X) the law of the excluded middle fails in general, as in general we do not have that

(¬U)U=true (\not U) \vee U = true

because ¬UU=(U c) U=X\U\not U \vee U = (U^c)^\circ \cup U = X \backslash \partial U is the total space XX without the boundary (frontier) of UU, and not true=Xtrue = X, all of the total space.

Thus, the internal logic of this sheaf topos is (in general) intuitionistic logic. As remarked above, this is the case in many toposes.



Most books on topos theory develop some internal logic, at least in the context of a topos. For example:

is comprehensive.

Phoa has a presentation of the internal logic of a topos over a dependent type theory, as opposed to other systems which use simple type theory. This is system is not minimal, but close to what is used in practice PS.

The book

works in the even more general context of fibrations, allowing us to associate to each object AA an arbitrary poset instead of Sub(A)Sub(A).

The book

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.

A discussion of dependent type theory as the internal language of locally cartesian closed categories is in

  • R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)

The observation that the poset of open subsets of a topological space serve as a model for intuitionistic logic is apparently originally due to

  • Alfred Tarski, Der Aussagenkalkül und die Topologie, Fundamenta Mathemeticae 31 (1938), pp. 103–134.


Discussion of fundamental constructions of algebraic geometry from the perspective of the internal logic of the sheaf topos over a scheme (Zariski topos, etale topos) is in

Last revised on January 27, 2024 at 14:37:26. See the history of this page for a list of all contributions to it.