Goldblatt. Topoi: The Categorial Analysis of Logic

Javascript Interactive Higher-Order Theorem Prover

Automated Reasoning in Higher Order Logic

This page was created and is maintained by Chad E Brown.

Goldblatt. Topoi: The Categorial Analysis of Logic. (Available via Amazon)

Chapter 2: What Categories Are. In set theory, functions are represented by a set of ordered pairs. This conflates the notion of a function with its graph. Also, while we can recover the image of a function, we cannot recover a general codomain (contrast the function 1:A->A with i:A->B where A is a subset of B; these functions are represented as the same sets). An alternative to such a representation is to note certain properties of functions (associativity, identity) and axiomatize these properties. Doing so, we obtain the concept of a category. Many examples of categories are structured sets with structure-preserving functions between them.

[pp. 25-26, "The pathology of abstraction"] This process of abstraction is common in mathematics. We examine specific situations, recognize common features, and present an axiomatic description of an "abstract" concept. Then we search for more examples of the abstract concept. This provides an interaction between generalizing and specializing. If possible, we prove representation theorems which tell us every model of our abstract concept is (equivalent to) one of a specific class of models (e.g., Cayley's theorem for groups, Stone's theorem for boolean algebra). In the case of category theory, the axioms are so weak that we get a wide class of models. In many models, the objects are not sets at all and the arrows are not functions.

A few examples of categories which do not have sets as objects and functions as arrows are 1, 2[0->1], and 3 [0->1->2]. These categories are examples of preorders: categories in which there is at most one arrow between any two objects (identity corresponds to reflexivity and composition corresponds to transitivity). Given any collection of objects, the discrete category with those objects has only identity arrows. All the examples so far in this paragraph have been preorders. The natural numbers N gives an example of a category (with one object and natural numbers as arrows and addition as composition) which is not a preorder. In general, monoids correspond to one-object categories.

Matrices over a commutative ring K form the arrows of a category Matr(K) where the objects are natural numbers and an nxm matrix is an arrow from m to n. Composition is given by matrix multiplication.

From a given category, we can form subcategories. A subcategory is full if whenever a and b are objects of the subcategory, all arrows from a to b are in the subcategory. Examples are the full subcategories of Set: Finset (finite sets) and Nonset (nonempty sets). A full subcategory of Finset is Finord (objects are the elements of omega).

From given categories, we can form product categories and arrow categories. We can also form, what Goldblatt calls "comma categories", but are known to me as slice categories. Note that a slice category is a (not full in general) subcategory of the arrow category. Instead of considering objects f:A->B and arrows <h,k>:f->g; with gh=kf, we restrict ourselves to f:A->B (with fixed B) and arrows <h,1_B>:f->g; with gh=1f.

Chapter 3: Arrows instead of Epsilon. We can reformulate set-theoretic constructions in categorial terms. Injections become monics, surjections become epics. Isos are arrows with inverses. (A group is a monoid with every arrow iso.) Epi + monic does not in general imply iso. (Consider any nontrivial preorder or the monoid N.) A skeletal category is one in which isomorphic objects are equal (e.g., Finord). A poset is a skeletal preorder.

The empty set becomes an initial object. One element sets become terminal objects. In a poset, an initial object is the bottom and a terminal object is the top. In Grp and Mon, the trivial group/monoid is both terminal and initial (a "zero" object). In the arrow category Set^2, the empty function null:null->null is initial and any !:{*_1}->{*_2} is terminal. In a slice category C/A, !:null->A is initial and 1:A->A is terminal.

In the basic language of categories, we can form the dual of any statement Sigma by reversing composition and interchanging references to dom's and cod's to obtain Sigma^op. The concepts initial and terminal are dual in this sense. We can also construct the dual category C^op of any category C by reversing the arrows. C^op^op = C. If C is discrete, C^op = C. Any statement Sigma is true in C iff Sigma^op is true in C^op. This leads to the principle of duality: if we have proven Sigma holds in all categories, then so does Sigma^op.

Cartesian products become categorial products given (up to isomorphism) by a universal mapping property. In Finord, a product is the usual multiplicative product. In a preorder, a product is a greatest lower bound. The notion of product can be generalized to finite products, which can be constructed from binary products (and the terminal object for the product of zero objects). Dual to products are coproducts. In Set, coproducts are disjoint unions. In preorders, coproducts are least upper bounds. In Finord, coproducts correspond to sums.

From two functions f,g:A->B we can form the subset E={x : f(x) = g(x)} of A. In categorial terms this gives an equalizer of f and g. Every equalizer is monic [we may call such monics "regular"]. Not all monics are equalizers. (Consider any nontrivial preorder [here equalizers are all identities] or the monoid N [here there are no equalizers].) Epic equalizers are iso. Since in any topos all monics are equalizers (of the characteristic function of the subobject given by the monic and the characteristic function of the full subobject [=true!]), we have in any topos epi+monic = iso.

We can unify the notions of terminal objects, products and equalizers as the more general notion of limits of diagrams. A limit is a universal cone over a diagram. We also have the dual notion of colimits (co-universal co-cones over a diagram) which unifies the notions of initial objects and coproducts.

Dual to equalizers are coequalizers. In Set, these are given by equivalence classes. The universal mapping property allows us to define a function on equivalence classes by defining it on the original elements and showing they respect the equivalence relation.

Pullbacks of two arrows with a common codomain is probably the most important categorial construction. In Set, the pullback of f and g can be defined as {<x,y> : f(x) = g(y)} with projection arrows. A special case is when g:C->B is an inclusion function with C a subset of B. In this case we can describe the pullback as the inverse image f^{-1}(C) with inclusion into the domain of f and f restricted to f^{-1}(C). In any category, we can form the "kernal relation" of any f:A->B by pulling back f along itself. [In terms of generalized elements, <x,y> is in this relation iff f(x) = f(y).] In Mon [or Grp or Vect] we can obtain the kernel of f:M->N (as a subobject of M) by pulling back !:0->N along f. In a preorder, pullbacks are products (greatest lower bounds). In any category with a terminal object 1, the product of A and B is the pullback of !:A->1 and !:B->1. In any category, equalizers i of f and g can be characterized as pullbacks <i,i> (i.e., where both "projections" are equal) of <f,g>. Also, an arrow f:A->B is monic iff <1_A,1_A> is the pullback of <f,f>. The pullback of a monic is monic. Also, we have the famous pullback lemma.

A category is complete if it has all limits, co-complete if it has all colimits, bi-complete if it is complete and co-complete, finitely complete if it has all finite limits, finitely co-complete if it has all finite colimits, and finitely bi-complete if it is finitely complete and finitely co-complete. A category is finitely complete if it has a terminal object and pullbacks.

An example of a categorial construction which is not a limit is exponentiation. In set, this corresponds to B^A = {f:A->B} with ev:B^A x A->A given by ev(f,a)=f(a). The UMP of the construction gives a unique transpose g~:C->B^A for every g:CxA->B. Goldblatt defines a Cartesian closed category to have all finite limits and exponents, as opposed to McLarty who defines a Cartesian closed category to have all finite products and exponents. Finord is Cartesian closed and exponentiation is exponentiation on the natural numbers. A chain (linearly ordered poset) is a CCC with exponents given by q^p = 1 if p<=q and = q if q<p.

For Cartesian closed categories, we have 0xA is initial for all A, an arrow A->0 implies A is initial, we can only have a zero object if the category is degenerate (all objects are isomorphic), any arrow 0->A is monic, A^1 is isomorphic to A, A^0 and 1^A are terminal. A consequence is that Mon and Grp are not CCC, because both have zero objects but are not degenerate.

Chapter 4: Introducing Topoi. Subobjects are given by equivalence classes of monics. A subobject classifier is an object Omega and arrow true:1->Omega satisfying the Omega-axiom: for each monic f:a>->d there is exactly one arrow (the characteristic arrow of f) Chi_f:d->Omega so that <!,f> is the pullback of <true,Chi_f>. As usual, subobject classifiers are unique up to a unique commuting isomorphism. So, the subobjects of d correspond to arrows d->Omega. An elementary topos is a category which is finitely complete, finitely co-complete, has exponentiation, and has a subobject classifier. Actually, finite co-completeness is implied by the other conditions.

Examples of topoi are Set, Finset and Finord. From any two topoi E1 and E2, we can build the product topoi E1xE2 by "doubling up" the constructions.

The arrow category of Set is a topos with subobject classifier given by Omega = {0,0.5,1}->{0,1} taking 0|->0, 0.5|->1, 1|->1 and true:1->Omega given by the pair of arrows taking singletons to 1. Given f:A->B, g:C->D, the exponent g^f:E->F is given by E = {<h:A->C,k:B->D> : gh=kf}, F = D^B, and g^f(<h,k>) = k. Evaluation ev:g^f x f -> g is given by <u:ExA->C,v:FxB->D> where u(<h,k>,x)=h(x) and v(k,y) = k(y). <u,v>:g^f x f -> g since g(u(<h,k>,x)) = g(h(x)) = k(f(x)) = v(k,f(x)) = v(g^f x f (<h,k>,x)).

The fundamental theorem of Topoi states that if E is a topos, then every slice E/I is a topos. So, every Set/I is a topos. We can reinterpret Set/I as the category Bn(I) of bundles indexed by I. That is, the objects p:A->I in Set/I correspond to a collection of disjoint sets {A_i} (determined by p^-1(i), also given {A_i} we can reconstruct A and p). Each set A_i is a stalk or fibre over i. Each member of A_i is a germ at i. The whole {A_i} is a bundle of sets over the base space I. Arrows from {A_i} to {B_i} are collections of functions {f_i:A_i->B_i} (corresponding to commuting functions in Set/I). The terminal object of Set/I is 1:I->I which corresponds to the bundle {{i}_i} (a bundle of terminals from Set). The product is given by a bundle of products of the fibres in Set, which is precisely the pullback in Set. The pullback in Bn(I) is a bundle of pullbacks from Set. Exponentials {A_i}^{B_i} are given by a bundles of function spaces {A_i^{B_i}} and evaluation is given by a bundle of evaluation functions {ev:A_i^{B_i} x B_i -> A_i}.

The subobject classifier is given by a bundle of subobject classifiers from Set. The true arrow picks out the element 1 from each stalk {0,1}_i. In general, such arrows are sections: in terms of Set/I we have s:I->A is a section of a bundle f:A->I if fos = id_I. Such an s:I->A corresponds to an arrow in Bn(I) from {{i}_i} (terminal) to {A_i}--i.e., a global element of {A_i}. That is global elements of Bn(I) are bundles of global elements in Set. Elements of Omega (arrows 1->Omega) are the "truth values" of the topos. Truth values correspond to subobjects of 1. In the case of Bn(I), the subobjects of {{i}_i} correspond to the subsets of I (in particular, there are 2^|I| of them).

Sheaves are bundles with a topological structure. In particular, a sheaf over a topological space I is a pair (A,p) where A is a topological space and p:A->I is a continuous local homeomorphism (every point has an open neighborhood which p maps homeomorphically onto its image). The category Top(I) of sheaves over I with arrows from (A,p) to (B,q) given by continuous functions k:A->B so that p = kq. Such a k must be open. The terminal object is id:I->I.

The subobject classifier is given as follows. Let O be the open subsets of I. For each i in I define O_i = {U in O : i in U} (i.e., neighborhoods of i) and define U to be i-equivalent to V if there is a W in O_i so that U intersect W = V intersect W. (So, U and V look equal "locally" around i.) Omega is taken to be the projection onto I from I^. Here I^ is the union of Omega_i = {<i,[U]_i> : U in O} over i in I where [U]_i is the i-equivalence class of U (with topology on I^ generated from basic sets [U,V] = {<i,[U]_i> : i in V in O and U subset of V}). The stalks corresponding to p:I^->I are the Omega_i's. The idea is that all sets containing i are i-equivalent, all the sets separable from i are i-equivalent, and inbetween we have equivalence classes those sets for which i is on the boundary of U and "look the same" near i. Maps from the terminal object (id:I->I) to the subobject classifier Omega:I^->I is a continuous section s:I->I^ (with ps = id:I->I). We can show that such sections correspond to open sets in O. Given U open in O, S_U:I->I^ by S_U(i) = <i,[U]_i> is a continuous section. Note [U]_i = [I]_i = O_i iff i in U, so we can recover U from S_U. In fact, for any section s, we can define U = {i : s(i) = <i,[I]_i>} and show U is open and s = S_U.

The truth arrow is given by the section T:I->I^ satisfying T(i) = <i,[I]_i>. The characteristic function for an open subset A of B (with q:B->I) is given by Chi:B->I^ satisfying Chi(b) = <q(b),[q(A intersect S_b)]_q(b)> where S_b is a neighborhood of b on which q is a local homeomorphism. This measures the extent to which b is in A.

Other examples of topoi are given by monoid actions. Given a monoid M (with operation * and identity e), an M-set is a pair (X,lambda) where X is a set and lambda:MxX->X is a monoid action (satisfying lambda(e,x) = x and lambda(mp,x) = lambda(m,lambda(p,x))). Consider, the monoid of natural numbers N. An N-set X is a set where each each x in X is associated with a sequence nx (where 0x = x). Arrows between M-sets are those preserving the action. Any singleton M-set (with the only action possible) is terminal. Products are Cartesian products with action given componentwise. Pullbacks are fibred products of sets with action given componentwise. Let L_M be the left ideals of M (e.g., L_N = {[>=n] := {m>=n} : n in N}; M is a group iff all we have are the empty and full ideals). Let Omega = (L_M,omega) where omega:M x L_M -> L_M by omega(m,B) = {n : nm in B} (e.g., omega:N x L_N -> L_N is given by omega(m,[>=b]) = {n in N: n >= b-m}). The truth arrow T:1->Omega takes the singleton to the largest left ideal M. The characteristic function of X sub-M-set of Y is given by Chi:Y->L_M where Chi(y) = {n : ny in X} (so that y is in X iff Chi(y) = M).

Exponents of M-sets X and Y are given by E = {f:MxX->Y : f(kn,kx) = kf(n,x) forall k and n in M and x in X} with action (mf)(n,x) = f(nm,mx) [slight change from Goldblatt]. ev:ExX->Y is given by ev(f,x) = f(e,x). The transpose of g:ZxX->Y is given by g~:Z->E where g~(z)(m,x) = g(mz,x).

Actually, the topos of M-sets is a special case of topoi of the form Set^C^op where C is small. (The category of M-sets can be represented as Set^M since a functor F:M->Set determines a set X and an action given by bijections lambda_m:X->X for each m in M.) The subobject classifier of the topos Set^C^op is given by Omega(A) = {S : S is a sieve on A} where a sieve on A is a collection of arrows S, all with codomain A, so that s o f is in S whenever s is in S and f is composable with s. (Compare sieves with right ideals of a monoid.) On arrows, we have Omega(g:A->B)(S' [sieve on B]) = {s : gos in S'} [sieve on A].

Another special case of such topoi are Set^P where P is a preorder. The subobject classifier in this case is given by Omega(p) = {S subset of P : x in S implies x>=p and y>=x in S implies y in S}.

In a topos, we can form power objects Omega^A which correspond to power sets. The pullback of true:1->Omega along ev:Omega^A x A->Omega gives the subobject epsilon_A>->Omega^A x A. This subobject has the property that for every "relation" r>->BxA, there is a unique f_r:B->Omega^A so that r is the pullback of epsilon_A along f_r x 1_A. (That is, we can Curry relations to be functions into the power object.) In general, a power object of A is an object P(A) and subobject eps_A>->P(A) x A satisfying the above property. Every topos has power objects, as shown above. On the other hand, given power objects we can recover Omega as the power object of 1. Also, power objects can be used to construct exponentials. Thus we have a category C is a topos iff it is finitely complete and has power objects.

Lawvere has suggested that the Omega-axiom of subobject classifiers is a form of the ZF Comprehension principle. Given any function phi:B->2={0,1}, Comprehension [or, separation] allows us to form the set {x in B : phi(x) = 1}. In a general topos, given an arrow phi:B->Omega, we have a unique subobject A>->B of B obtained by pulling back true along phi. Furthermore, global elements y:1->B are members of A iff phi o y = true o !.

Chapter 5: Topos Structure: First Steps. In a topos, all monics are equalizers [are regular monics]. In fact, f:A>->B is the equalizer of Chi_f:B->Omega and true!:B->Omega. It follows that an arrow in a topos is iso iff it is epic and monic.

In a topos we can factor any arrow f:A->B into f = im f o f* where im f is monic and f* is epic (called an "epi-monic factorization"). This factorization is unique up to a unique commuting isomorphism. In Set it is trivial to find such a factorization (A-f->f(A)>->B). There are two "arrows-only" approaches. 1) Obtain f* as the coequalizer of p and q where <p,q> is the kernel pair of f (i.e., <p,q> is the pullback of <f,f>). In Set, this corresponds to forming the equivalence relation R_f = {<x,y> : f(x)=f(y) in A} and then the quotient A/R_f. 2) Obtain im f as the equalizer of p and q where <p,q> is the pushout of <f,f>. In Set, this corresponds to forming the R = f(A) disjoint-union (B' x {0}) disjoint-union (B' x {1}) where we write B = f(A) disjoint-union B'. Here, p,q:B->R both send p(a)=a=q(a) if a is in f(A), but p(b)=(b,0) and q(b)=(b,1) if b is in B'. Then we form f(A)>->A by equalizing p and q. Goldblatt chooses the second approach so that he can use previously proven results to show f* (given uniquely by the UMP of equalizers) is epic and that the factorization is unique.

First, if f = v u and v is monic, then im f <= v. This follows since v must equalize two arrows s and t (since we are in a topos) and we can show s o im f = t o im f. Next, f* must be epic, because im f* must be iso (im f o im f* <= im f is obvious, and im f <= im f o im f* since f = im f im f* f** [use above with v = im f im f*) which implies the pushout <p,q> of <f*,f*> must have p=q (since im f* equalizes p and q). So, we have the epi-monic factorization f = im f o f* and given any epi-monic factorization f = u o v, there is a unique k satisfying v o k = im f and u = k o f*, k is monic since v o k = im f is monic, and k is epic since k o f* = u is epic, so k is iso.

Without proof, Goldblatt states the results for topoi: Pullbacks preserve epics, coproducts preserve pullbacks.

Since a topos is Cartesian closed, only degenerate topoi (all objects isomorphic) can have an arrow x:1->0 (an element of an initial object 0). [Note: All degenerate topoi are equivalent to 1, since it must have a terminal object and all objects are isomorphic to this terminal object.] By "non-zero" we mean an object which is not initial. By "non-empty" we mean an object A for which there is an element x:1->A. In Set, an object is non-zero iff it is non-empty. In Set^2, however, <null,{0}> is non-zero but empty (since there is no arrow from <{0},{0}> to <null,{0}>). We have already noted that non-empty object must be non-zero unless the topos is degenerate.

A topos is well-pointed if it satisfies the extensionality principle for arrows: for every f,g:A->B with f not equal to g, there is an x:1->A so that f o x is not equal to g o x. Set is well-pointed, but Set^2 is not (consider two arrows from <null,{0}> to <null,{0,1}>). If a topos is well-pointed, then every non-zero object is non-empty (consider the characteristic arrows Chi_{0>->A},Chi_{id:A>->A}:A->Omega which are distinct if A is non-zero since 0 is not isomorphic to A).

The arrow false is defined to be the characteristic arrow of 0>->1. In Set^2, false takes <0,0> to <0,0> where true takes <0,0> to <1,1>. In Bn(I), false takes i to <0,i> where true takes i to <1,i>. In Top(I), false takes i to <i,[empty]_i> where true takes i to <i,[I]_i>. In M-set, false takes 0 to the empty left-ideal where true takes 0 to the full left-ideal. The characteristic arrow of any 0>->A is given by false!:A->Omega. In a nondegenerate topos, true is not false.

The elements of Omega are called "truth values". If true and false are the only truth values of a nondegenerate topos, then the topos is bivalent (two-valued). Every well-pointed topos is bivalent. The idea of the proof is that arrows 1->Omega correspond to monics with codomain 1, and for any monic g:A>->1 we must have A initial (so the characteristic arrow is false) or A terminal (so the characteristic arrow is true). If A is not initial, then since the topos is well-pointed there is an element x:1->A and we must have gx=id_1. So, g must be epic (since it has a right inverse). Since g is monic and epic, it is iso [since we are in a topos] and A is isomorphic to 1 (so, A is terminal).

Arrows f:A->B and g:C->B are called disjoint if <0->A,0->C> is the pullback of <f,g>. (In Set, this means Im f intersect Im g is empty.) A sum (f,g):A+C->B of disjoint monics f:A>->B and g:C>->B is monic. We can prove this fact using the fact that an arrow h is monic iff <id,id> is the pullback of <h,h>. Applying this to f and g, using f and g disjoint, and using the fact that coproducts preserve pullbacks, we have <0->A + id_C,(0->C,id_C)> is the pullback of <(f,g),g>. Using the isomorphism between 0+C and C, we have <i:C->A+C,id_C> is the pullback of <(f,g),g>. The same process yields <i:A->A+C,id_A> is the pullback of <(f,g),f>. Again, using the fact that coproducts preserve pullbacks, <id_{A+C},id_{A+C}> is the pullback of <(f,g),(f,g)>, so that (f,g) is monic.

The map (true,false):1+1->Omega is monic in every topos. This follows since true and false are disjoint monics (the disjointness pullback is precisely the definition of false). If it is also epic (hence, iso), then we say the topos is classical. Set is classical. In fact, every well-pointed topos is classical. Since true and false are the only elements of Omega (since well-pointedness implies bivalence), f o (true,false) = g o (true,false) implies f o true = g o true and f o false = g o false implies f = g (by well-pointedness). So, (true,false) is epic.

So, every well-pointed topos is both bivalent and classical. In fact, a topos is well-pointed iff it is [nondegenerate] classical and every non-zero object is non-empty. The proof of "if" is in Chapter 7.

Set^2 is classical but not bivalent. 1+1 is <{0_0,0_1},{0_0,0_1}>. Omega is <{0,1},{0,1}>. There are four truth values, i.e., arrows from <{0},{0}>->Omega. (true,false):1+1->Omega is the componentwise isomorphism taking each 0_0 to 1 and each 0_1 to 0.

The arrow category of Set is neither classical nor bivalent. 1+1 is id:{a,b}->{a,b}. Omega takes {0,0.5,1} to {0,1}. (true,false) is the pair of functions taking a to 0 and b to 1. This is not an isomorphism (since an isomorphism in this category must be a pair of bijective maps). There are three arrows from 1 to Omega (truth values) corresponding to the pairs (0,0), (0.5,1), and (1,1).

Let M_2 be the monoid 2={0,1} with multiplication. M_2-Set is bivalent but nonclassical. The left ideals of M_2 are empty, {0}, and 2. This gives a subobject classifier {empty,{0},2} with action 0*empty = empty, 0*{0} = 2, 0*2 = 2, and 1*B=B for each B. The map (true,false):{a,b}->L_{M_2} takes a to 2 and b to 0. This is not epic since it cannot distinguish between composition with f:L_{M_2}->L_{M_2} with f(empty)=empty, f({0})=2, and f(2)=2, vs. composition with the identity arrow. M_2-Set is bivalent since given h:{0}->{empty,{0},2} equivariant, we must h(0)=empty (so h is false) or h(0)=2 (so h is true). h(0) cannot be {0} because equivariance implies h(0) = h(0*0) = 0 * h(0) which is either empty or 2. Now that we know M_2-Set is bivalent, the f above and the identity arrow can be used to check directly that M_2-Set is not well-pointed, since the two arrows agree on all elements--i.e., true and false.

Also, every nonzero M_2-Set object is nonempty. Given a nonzero X, pick some x in X and let y = 0 * x. Then y is a fixed point of the action: m*y = m*0*x = 0*x = y. For any such fixed point, we can define the element y':{0}->X by y'(0) = y. Equivariance follows since y'(m*0) = y = m*y = m*y'(0). (In fact, all elements are given by such fixed points.)

Actually, M-Set is classical iff M is a group. If M-Set is classical, then (true,false):{a,b}->L_M must be a bijection, so that L_M has two elements (which can only be empty and M), so that M is a group. If M is a group, then L_M = {empty,M} and (true,false) is an equivariant bijection, hence iso.

Using [global] elements, we can define what it means to say an arrow is surjective or injective. In a well-pointed topos, an arrow is surjective iff epic, and an arrow is injective iff monic. It is straightforward to show that surjectivity implies epic (using well-pointedness). Then, assuming f:A->>B epic and given y:1->B, to show surjectivity we must find an x:1->A so that f o x = y. We can find such an x by forming the pullback <p,q> of <f,y>. p is epic as the pullback of f epic [we are in a topos]. The domain C of p must be nonzero (or p would be monic, hence iso, hence 0 would be isomorphic to 1 and the topos would be degenerate). So, there must be a z:1->C. Let x = q o z (note that we only used every nonzero object has an element). Showing monics are injective is trivial (and works in any category). Finally, if f:A->B is injective and f o g = f o h for g,h:C->A with g not equal to h, then by well-pointedness we have x:1->C with g o x not equal to h o x. But f o g o x = f o h o x and injectivity of f imply g o x = h o x, giving a contradiction.

The arrow f:L_{M_2}->L_{M_2} in M_2-Set considered above is surjective and injective, but is neither epic nor monic. Also, (true,false) in M_2-Set is surjective but not epic.

Chapter 6: Logic Classically Conceived. We can axiomatize classical propositional logic CL (with implies, and, or, and not as primitive) with detachment (modus ponens) as the sole rule of inference. We can define truth table semantics and prove soundness and completeness. Such truth table semantics are actually given by the Boolean Algebra 2={0,1}. We can define such a semantics for any Boolean Algebra B (complemented distributed [bounded] lattice) and prove soundness and completeness for models in this B. Thus, a sentence is provable in CL iff it is valid in every Boolean Algebra (this version of completeness can be proven by constructing the Lindenbaum Algebra).

implies:Omega x Omega->Omega is the characteristic arrow of |<=|>->Omega x Omega

or:Omega x Omega -> Omega is the characteristic arrow of the im f >->Omega x Omega

In terms of Set, the image of f is {<1,0>,<1,1>,<0,1>} where <1,1> is the image of two elements in Omega + Omega.

In Set and Finset, these correspond to the classical truth functions. In Bn(I) we get copies of the classical truth functions for each i in I. In M-Set, and and or are given by intersection and union. For each left ideal B, not(B) is the ideal {m : m*B = empty} (note: not(empty) = M, not(M) = empty; if M is commutative, then not(B) = empty for every nonempty B). For left ideals B and C, implies(B,C) is the ideal {m : m*B subset m*C}. In particular, for M_2-Set we have Omega given by left ideals {empty,{0},2} and truth functions: not(2) = not({0}) = empty; not(empty) = 2; implies(B,2) = implies(B,B) = 2; implies(2,{0}) = {0}; implies(empty,{0}) = 2; implies(2,empty) = implies({0},empty) = empty. Note that or(not({0}),{0}) = {0} so that excluded middle fails.

We can use these truth arrows to define a semantics for propositional logic in any topos E. Validity in Set, Finset, or Finord corresponds to validity in the Boolean Algebra 2 which corresponds to CL-provability. Validity in Bn(I) corresponds to validity in the Boolean Algebra P(I) which corresponds to CL-provability. In any topos, the truth arrows behave like the classical truth functions on the elements true,false:1->Omega. It follows that any sentence valid in any particular [nondegenerate] topos is CL-provable (so we have completeness). We do not have soundness since excluded middle need not hold for all truth values 1->Omega. For example, excluded middle fails in the arrow category of Set. We do have that if E is a bivalent topos, then E|=alpha iff CL|-alpha. However, bivalence does not characterize classical logic. M_2-Set is bivalent, but is nonclassical. Set^2 is not bivalent, but is classical (and Set^2|=alpha iff CL|-alpha).

Chapter 7: Algebra of Subobjects. We can define operations on the poset Sub(d) by composing characteristic arrows with the arrows not, and, or, implies. In Set, this agrees with the usual notion of complements, intersections, union, and -A or B. In any topos, f "meet" g (given by characteristic arrow and o <Chi_f,Chi_g>) is also given by the pullback of f and g. In any topos, given a pullback <u,f> of <v,g> we can factor the pullback into two pullbacks <u,f*> of <h,g*> and <h,im f> of <v,im g>. Such a factorization allows us to prove that the "join" of f and g (given by characteristic arrow or o <Chi_f,Chi_g>) is the same subobject as im (f,g).

These characterizations of "meet" and "join" allow us to prove that Sub(d) is a lattice with meets and joins given by these operations. Also, 1_d represents the top of Sub(d) and 0_d:0->d represents the bottom. f:a>->d is equivalent to 1_d iff f is iso. f meet its "pseudocomplement" -f is equivalent to 0_d. However, we do not have f join -f is necessarily equivalent to 1_d. For example, in M_2-Set we have the subobject true:1>->Omega given by {{0,1}} and the subobject false:1>->Omega given by {empty} so that true join[union in M_2-Set] false is {empty,{0,1}} which is smaller than the top subobject given by {empty,{0},{0,1}}. In any topos, -true is false (look at the characteristic arrows), so that in M_2-Set we have true join -true is not 1_Omega. So, false is not the Sub(Omega)-lattice complement of true. But in any topos, false is the only possible complement for true, since if f is a complement of true, then f must be the characteristic arrow of some 0:0->A, which allows us to factor f through false by the definition of false as the characteristic arrow of 0:0>->1. The conclusion is that if true join false is not the top of the lattice, then Sub(Omega) cannot be a Boolean Algebra.

A topos is Boolean if every Sub(d) is a Boolean Algebra. This following are equivalent for a topos E:

Most of this theorem follows easily from the earlier results. To prove "(7) => (1)" we take f:a>->d and show f join -f is the top of the lattice. This follows from (f,-f) epic (so that im (f,-f) [i.e., f join -f] is iso). (f,-f) is epic as the pullback of (i_1,i_2) = 1_{1+1}. This is a pullback since i_1:1->1+1 is a subobject classifier.

If E is Boolean, then E|=alpha or -alpha for any sentence alpha. Actually, all we use is that Sub(1) is a Boolean Algebra. In fact, for any nondegenerate topos E, the following are equivalent:

Sub(1) may be a Boolean Algebra and E may not be Boolean (consider M_2-Set which is bivalent [so that Sub(1) is a Boolean Algebra] but not classical).

Sub(Omega) is a Boolean Algebra iff (EM) or o <1_Omega,not> = true! holds. (EM does not hold in M_2-Set.)

The implies arrow induces the "relative pseudocomplement" (r.p.c.) operation on each Sub(d). The operation satisfies:

(1) h subobject of rpc(f,g) iff f meet h subobject of g. (Compare this to the deduction theorem.)

In Sub(d), rpc(1,1) and rpc(0,1) and rpc(0,0) are all 1 [top] while rpc(1,0) is 0 [bottom]. In general rpc(f,g) is the largest element x so that f meet x is a subobject of g (i.e., it really is the relative pseudocomplement). In a Boolean Algebra, rpc(f,g) must be -f join g. This gives three more characterizations of Boolean topoi. For a topos E, the following are equivalent:

We can use these results to verify the truth tables for the operations on true,false:1->Omega (since they correspond to lattice operations on Sub(1)).

Also, we can now show that a classical topos in which every nonzero object is nonempty is well-pointed. Given f,g:a->b distinct, let h:c>->a be the equalizer and -h:-c>->a be its complement. Using E Boolean (since classical) we have that -c is 0 iff h is iso (in which case f and g are not distinct). So, -c is nonzero, hence nonempty giving an element y:1->-c, and we can distinguish f and g using the element -h o y:1->a.

In any topos, we have, in terms of [global] elements, x is in f meet g iff x is in f and x is in g. The same does not necessarily hold for join [with or] or pseudocomplement [with not].

A topos is extensional if for any f,g:a>->d, f is a subobject of g iff forall x:1->a x in f implies x in g. A topos is extensional iff well-pointed. (We can distinguish between f and g by taking an element of 1 which is not in the equalizer of f and g. To show the converse, assume well-pointedness and that every x in f is in g. Then show Chi_{f meet g} = Chi_f using bivalence (which follows from well-pointedness) and well-pointedness.

A topos satisfies "x in -f iff x is not in f" for all x and f iff it is bivalent.

A topos is disjunctive (satisfies "x in f join g iff x in f or x in g") iff it satisfies y join z = true iff y = true or z = true (forall y,z:1->Omega). Every bivalent topos satisfies this condition, but not every disjunctive topos is bivalent. For example, the arrow category of Set is disjunctive but not bivalent (it has three truth values). However, we do have that any Boolean nondegenerate topos is disjunctive iff bivalent.

Chapter 8: Intuitionism and its Logic. Dedekind and Peano reduced the reals to rationals, the rationals to integers, and the integers to naturals. Peano, of course, gave axioms satisfied by the naturals. The existence of such reductions suggested Frege and Russell's "logicist" thesis that all of mathematics can be reduced to logic.

Cauchy's concepts of limits, etc., removed references to infinity using epsilon-delta-N style definitions. Cantor's set theory, on the other hand, treated infinity as a legitimate mathematical object. Kronecker rejected infinite sets and even irrational numbers as mystical, not mathematical. According to Kronecker, objects cannot be said to exist unless they can be produced. Poincare believed impredicative definitions were the source of the paradoxes discovered at the turn of the century and held that such definitions were inadmissible.

Kronecker and Poincare were the first to express the constructivist attitude. Brouwer carried the attitude much further by developing his philosophy of intuitionism. Brouwer rejected nonconstructive arguments (as did Kronecker and Poincare) but also denied the validity of traditional logic. In particular, arguments by contradiction and use of excluded middle are unacceptable. This can be attributed to a difference between the classical and intuitionistic interpretation of "or" and "not". Given the constructive intuitionistic interpretation of these propositional functions, excluded middle does not hold. According to Brouwer, logical laws were abstracted from mathematical deductions dealing with the finite. They were then (incorrectly according to Brouwer) accepted a priori and applied to the world of the infinite. Brouwer's solution is to return to the source of mathematical truth--the intuition. For Brouwer, mathematics is an activity. This activity may be paralleled by language, but cannot be captured by the language (leading to his rejection of formalism--including any attempts to formalize intuitionism!).

In 1930, Heyting produced an axiomatic system for the propositional content of intuitionism. [Actually, Kolmogorov had introduced a different such system in 1925 and showed how to interpret classical propositional logic in intuitionistic propositional logic.] Heyting acknowledged that, according to intuitionistic philosophy, his axiomatic system is an imperfect tool for describing intuitionistic propositional logic and may not completely capture those sentences which are intuitionistically true. Heyting's system IL is CL without excluded middle.

Tarski and Stone independently discovered that an algebra of open sets of a topological space can be used to give a semantics for IL. By a process of abstraction, we are led to the notion of Heyting Algebras. A Heyting Algebra is a bounded lattice with relative pseudo-complements. The pseudo-complement of a relative to b is the greatest x such that x meet a <= b (denoted by "a=>b"). A special case is the pseudo-complement of a which is the greatest x such that x meet a = 0 (denoted by a' or -a). (Actually, we can talk about relatively pseudo-complemented lattices without 0, in which case pseudo-complements do not make sense.)

Examples include any Boolean Algebra (where pseudo-complements are the same as complements and relative pseudo-complements are given by -a join b), the left ideals of a monoid (where the pseudo-complement of B is given by {m : m*B is empty}), the open sets of a topological space (where the pseudo-complement of G is given by int(-G) and the pseudo-complement of G relative to H is int(-G union H)), and Sub(d) in any topos (where pseudo-complements are given by taking f to -f and relative pseudocomplements are given by taking f and g to rpc(f,g)). In Top(I), pseudo-complements and relative pseudo-complements are given by taking pseudo-complements and relative pseudo-complements of each germ.

In a Boolean Algebra, we have --x = x, but in a Heyting Algebra we may not have this. For example, in Sub(Omega) of M_2-Set we have true is not --true. -true is false (this is generally true in a topos). However, -false corresponds to the set {{0},{0,2}} where true corresponds to the set {{0,2}}. In general in a Heyting Algebra, we have x <= --x. We also have --x <= x iff the algebra is Boolean. The equation --x = x can be represented in a topos as the equation not o not = id_Omega. For any topos E, the following are equivalent:

Now, given any Heyting Algebra, we can define a valuation from propositional sentences into the algebra (as we did with Boolean Algebras except now using pseudo-complements and relative pseudo-complements for negation and implication). For a Heyting Algebra H, a sentence alpha is H-valid (denoted H|=alpha) if it maps to true under every valuation into H. A sentence is HA-valid if it is H-valid for every Heyting Algebra H. A sentence alpha is HA-valid iff IL|-alpha. (The completeness direction can be shown using the Lindenbaum algebra for IL.)

Returning to topos semantics for propositional logic, and noting that Sub(1) must be a Heyting Algebra, we have for any topos E: E|=alpha iff Sub(1)|=alpha. Soundness of topos semantics for IL follows immediately. Note that topological semantics are equivalent to topos semantics for topoi of the form Top(I). [Completeness follows.] It is also now obvious why a topos is sound for CL iff Sub(1) is a Boolean Algebra.

We know that any poset can be thought of as a category. Thought of as a category, a Heyting Algebra is precisely a Cartesian closed and finitely co-complete poset. Relative pseudo-complements correspond to exponents.

In 1965, Kripke introduced a semantics for IL modified from semantics for modal logic. A Kripke model is given by a poset P (also called a "frame", representing possible stages of knowledge) and the set P+ of hereditary subsets of P (i.e., A is in P+ iff A is a subset of P and for any x and y with x in A and x <= y we have y is in A). A valuation V maps propositional constants to hereditary subsets of P (members of P+). For M=(P,V), we define M|=_p alpha (alpha is true in M at p) inductively starting with M|=_p pi iff pi is in V(pi) for propositional constants pi. Then conjunction is given by and; disjunction is given by or. M|=_p -alpha iff there is no q>=p so that M|=_q alpha (we cannot learn alpha at some later stage). Similarly, M|=_p alpha=>beta iff there is no q>=p so that M|=_q alpha but not M|=_q beta (at every later stage if M models alpha, then it models beta). Then, we say M|=alpha if for every p M|=_p alpha.

Taking the poset 2={0<1} and letting V(pi) = {1}, we have not M|=_0 pi and not M|=_i -pi (for i=0,1) so that not M|=_0 pi \/ -pi (excluded middle fails). We do have M|= --pi (this follows from not M|=_i -pi for all i). It follows that we do not have M|= --pi => pi.

We can remove references to p in P by inductively defining M(alpha) as a member of P+ (so that M|=_p alpha iff p is in M(alpha) and M|=alpha iff M(alpha) = P). P+ is a Heyting Algebra and the resulting operations can be used to define M(alpha) inductively from V. So, Kripke validity is a special case of Heyting Algebra validity. Soundness of Kripke validity with respect to IL follows. To prove completeness, we could use Stone's representation theory; Kripke used a semantic tableau technique; Henkin introduced the frame of all "full" sets. A set of sentences Gamma is full if it includes every theorem of IL, if alpha is in Gamma and IL|-alpha=>beta then beta is in Gamma, there is some alpha not in Gamma, and if alpha \/ beta is in Gamma then alpha is in Gamma or beta is in Gamma. The poset of all full sets gives a "canonical" model M_IL for IL. Lindenbaum's lemma states that IL|-alpha iff alpha is in every full set. It follows that IL|-alpha iff M_IL|=alpha. The completeness of Kripke semantics, hence Heyting Algebra semantics, follows.

Kripke semantics can be used to characterize the validity of certain sentences by conditions on frames. P|=(alpha => beta) \/ (beta => alpha) iff the poset P is weakly linear (p<=q and p<=r imply q<=r or r<=q). P|=alpha \/ -alpha iff P is discrete (p<=q iff p=q). P|=-alpha \/ --alpha iff P is directed (p<=q and p<=r imply there is an s with q<=s and r<=s).

Kripke semantics is also related to topological semantics, since P+ gives a topology on P. The Heyting Algebra on P+ induced by the poset P is the same as the Heyting Algebra induced topologically.

An alternative to Kripke semantics is due to Beth. Beth semantics can be described using Kripke models, but M|=_p alpha is interpreted differently. A path through p in a poset P is a maximal linear chain in P. A bar for p is a subset of B so that every path through p intersects B. Beth semantics interprets conjunction, negation, and implication as in Kripke semantics. The differences are: M|=_p pi iff there is a bar B for p with B subset of V(pi) (where pi is a propositional constant); M|=_p alpha \/ beta iff there is a bar B for p with M|=_q alpha or M|=_q beta for each q in B.