Reprints in Theory and Applications of Categories, No. 11, 2005, pp. 1–35.

AN ELEMENTARY THEORY OF THE CATEGORY OF SETS (LONG VERSION) WITH COMMENTARY

F. WILLIAM LAWVERE

Received by the editors 2005-04-01. Transmitted by M. Hyland, A. Kock, R. Rosebrugh. Reprint published on 2005-05-23. 2000 Mathematics Subject Classification: 18B05, 00A30, 03A05. Key words and phrases: Category of sets, Axiom of choice, Mathematical logic and foundations. This article is an expanded version of ‘An elementary theory of the category of sets’, Proceedings of the National Academy of Science of the U.S.A 52, 1506–1511. Article and commentary \begin{matrix}c \\ ◯ \end{matrix}F. William Lawvere and Colin McLarty. Permission to copy for private use granted.

ETCS and the Philosophy of Mathematics

Colin McLarty

Philosophers and logicians to this day often contrast “categorical” foundations for mathematics with “set-theoretic” foundations as if the two were opposites. Yet the second categorical foundation ever worked out, and the first in print, was a set theory—Lawvere’s axioms for the category of sets, called ETCS, (Lawvere 1964). These axioms were written soon after Lawvere’s dissertation sketched the category of categories as a foundation, CCAF, (Lawvere 1963). They appeared in the PNAS two years before axioms for CCAF were published (Lawvere 1966). The present longer version was available since April 1965 in the Lecture Notes Series of the University of Chicago Department of Mathematics.^{1} It gives the same definitions and theorems, with the same numbering as the 5 page PNAS version, but with fuller proofs and explications.

Lawvere argued that set theory should not be based on membership (as in Zermelo Frankel set theory, ZF), but on “isomorphism-invariant structure, as defined, for example, by universal mapping properties” (p. 1). He later noticed that Cantor and Zermelo differed over this very issue. Cantor gave an isomorphism-invariant account of sets, where elements of sets are “mere units” distinct from one another but not individually identifiable. Zermelo sharply faulted him for this and followed Frege in saying set theory must be founded on a membership relation between sets.^{2}

Paul Benacerraf made the question prominent for philosophers one year after (Lawvere 1964). The two were no doubt independent since philosophers would not look in the PNAS for this kind of thing. Benacerraf argued that numbers, for example, cannot be sets since numbers should have no properties except arithmetic relations. The set theory familiar to him was ZF, where the elements of sets are sets in turn, and have properties other than arithmetic. So he concluded that numbers cannot be sets and the natural number structure cannot be a set.

Benacerraf wanted numbers to be elements of abstract structures which differ from ZF sets this way:

in giving the properties (that is, necessary and sufficient) of numbers you merely characterize an abstract structure—and the distinction lies in the fact that the “elements” of the structure have no properties other than those relating them to other “elements” of the same structure. (Benacerraf 1965, p. 70)

1Date verified by Lawvere through the University of Chicago math librarian.

2Zermelo’s complaint about Cantor and endorsement of Frege are on (Cantor 1932, pp. 351, 440-42).

See (Lawvere 1994).

The sets of ETCS are abstract structures in exactly this sense. An element x ∈ S in ETCS has no properties except that it is an element of S and is distinct from any other elements of S. The natural number structure in ETCS is a triad of a set N, a selected element 0 ∈ N, and a successor function s:N→N. Then N, 0, s expresses the arithmetic relations as for example m = s(n) says m is the successor of n. But N, 0, s simply have no properties beyond those they share with every isomorphic triad.^{3} So in relation to 0 and s the elements of N have arithmetic relations, but they have no other properties.

Lawvere carefully says ETCS “provides a foundation for mathematics … in the sense that much of number theory, elementary analysis, and algebra can apparently be developed within it.” This aspect relies entirely on the elementary axioms. But he did not claim that such formal adequacy makes ETCS a formalist or logicist starting point for mathematics, as if there was no mathematics before it. He says that ETCS condenses and systematizes knowledge we already have of “the category of sets and mappings… denoted by S” (pp. 1-2). This aspect deals with models and metatheorems for the axioms. Gödel’s theorem says we will never have a proof-theoretically complete description of this category. Lawvere gives various metatheoretic proofs about categorical set theory based on this and on the Löwenheim-Skolem theorem. Yet he takes it that there are sets, we know much about them apart from any formalization, and we can learn much from seeing how formal axioms describe them. The category exists objectively in mathematical experience as a whole—not in a platonic heaven, nor in merely subjective individual experience. This historical (and dialectical) realism continues through all his work and gets clear recent statements in (Lawvere & Rosebrugh 2003) and (Lawvere 2003).

Of course the category of sets is not the only one that exists. It is not the only one formally adequate as a “foundation” nor the first to be described that way. Lawvere concludes this paper, as he also does the PNAS version, by saying that more powerful foundations would be more naturally expressed in the category of categories (p.32, or (Lawvere 1964, p. 1510)).

References.

Benacerraf, Paul (1965), ‘What numbers could not be’, Philosophical Review 74, 47–73.

Cantor, Georg (1932), Gesammelte Abhandlungen mathematischen und philosophischen Inhalts, Julius Springer, Berlin.

Lawvere, F. William (1963), Functorial Semantics of Algebraic Theories, PhD thesis, Columbia University. Republished in: Reprints in Theory and Applications of Categories, No. 5 (2004) pp 1-121, available on-line at http://tac.mta.ca/tac/reprints/articles/5/tr5abs.html.

Lawvere, F. William (1964), ‘An elementary theory of the category of sets’, Proceedings of the National Academy of Science of the U.S.A 52, 1506–1511.

3For a precise statement and proof see (McLarty 1993).

Lawvere, F. William (1966), The category of categories as a foundation for mathematics, in S.Eilenberg et al., eds, ‘Proceedings of the Conference on Categorical Algebra, La Jolla, 1965’, Springer-Verlag, pp. 1–21.

Lawvere, F. William (1994), ‘Cohesive toposes and Cantor’s “lauter Einsen”’, Philosophia Mathematica 2, 5–15.

Lawvere, F. William (2003), ‘Foundations and applications: Axiomatization and education’, Bulletin of Symbolic Logic 9, 213–24.

Lawvere, F. William & Robert Rosebrugh (2003), Sets for Mathematics, Cambridge University Press.

McLarty, Colin (1993), ‘Numbers can be just what they have to’, Noûs 27, 487–98.

Author Commentary

F. William Lawvere

Saunders Mac Lane wisely insisted on this more complete version of the work that was summarized in the brief article he communicated in October 1964 to the Proceedings of the National Academy of Science. Accordingly, this manuscript, with its relatively complete proofs and extensive remarks on the metamathematical status of the work, was deposited in the University of Chicago mathematics library at the end of April 1965. I hope that the present publication, made possible thanks to Colin McLarty’s efforts in TEX and thanks to the editors of TAC, will assist those who wish to apply the Elementary Theory of the Category of Sets to philosophy and to teaching.

Of course, the central theory is more fully developed in the joint textbook with Robert Rosebrugh Sets for Mathematics (and even bolder metamathematical comments are offered in its appendix). However, the present document may still be of interest, at least historically, giving as it does a glimpse of how these issues looked even as the crucial need for elementary axiomatization of the theory of toposes was crystallizing. (In July 1964 I noted in Chicago that sheaves of sets form categories with intrinsic properties just as sheaves of abelian groups form abelian categories; in January 1965 Benabou told me that Giraud had axiomatized “toposes”; in June 1965 Verdier’s lecture on the beach at LaJolla made clear that those axioms were not yet “elementary” though extremely interesting....).

Among mathematical/logical results in this work is the fact that the axiom of choice implies classical logic. That result was later proved by Diaconescu under the strong hypothesis that the ambient category is a topos (i.e. that the notion of arbitrary monomorphism is representable by characteristic functions) but in this work it is shown that the topos property is itself also implied by choice. Specifically, characteristic functions valued in 2 are constructed by forming the union (proved to exist) of all complemented subobjects that miss a given monomorphism, and then using the choice principle to show that there is no excluded middle. (Presumably with modern technology this calculation could be carried out with more general generators than 1).

This elementary theory of the category of sets arose from a purely practical educational need. When I began teaching at Reed College in 1963, I was instructed that first-year analysis should emphasize foundations, with the usual formulas and applications of calculus being filled out in the second year. Since part of the difficulty in learning calculus stems from the rigid refusal of most textbooks to supply clear, explicit, statements of concepts and principles, I was very happy with the opportunity to oppose that unfortunate trend. Part of the summer of 1963 was devoted to designing a course based on the axiomatics of Zermelo-Fraenkel set theory (even though I had already before concluded that the category of categories is the best setting for “advanced” mathematics). But I soon realized that even an entire semester would not be adequate for explaining all the (for a beginner bizarre) membership-theoretic definitions and results, then translating them into operations usable in algebra and analysis, then using that framework to construct a basis for the material I planned to present in the second semester on metric spaces.

However I found a way out of the ZF impasse and the able Reed students could indeed be led to take advantage of the second semester that I had planned. The way was to present in a couple of months an explicit axiomatic theory of the mathematical operations and concepts (composition, functionals, etc.) as actually needed in the development of the mathematics. Later, at the ETH in Zurich, I was able to further simplify the list of axioms.

April 1, 2005

An Elementary Theory of the Category of Sets (Long Version)

F. William Lawvere ^{4}

The elementary theory presented in this paper is intended to accomplish two purposes. First, the theory characterizes the category of sets and mappings as an abstract category in the sense that any model for the axioms which satisfies the additional (non-elementary) axiom of completeness (in the usual sense of category theory) can be proved to be equivalent to S. Second, the theory provides a foundation for mathematics which is quite different from the usual set theories in the sense that much of number theory, elementary analysis, and algebra can apparently be developed within it even though no relation with the usual properties of ∈ can be defined.

Philosophically, it may be said that these developments partially support the thesis that even in set theory and elementary mathematics it is also true as has long been felt in advanced algebra and topology, namely that the substance of mathematics resides not in Substance (as it is made to seem when ∈ is the irreducible predicate, with the accompanying necessity of defining all concepts in terms of a rigid elementhood relation) but in Form (as is clear when the guiding notion is isomorphism-invariant structure, as defined, for example, by universal mapping properties). As in algebra and topology, here again the concrete technical machinery for the precise expression and efficient handling of these ideas is provided by the Eilenberg-Mac Lane theory of categories, functors, and natural transformations.

The undefined terms of our theory are mappings, domain, co-domain, and composition. The first of these is merely a convenient name for the elements of the universe over which all quantifiers range, the second two are binary relations in that universe, and the last is a ternary relation. The heuristic intent of these notions may be briefly explained as follows: a mapping f consists of three parts, a set S, a set S′, and a “rule” which assigns to every element of S exactly one element of S′. The identity rule on S to S determines the domain of f and the identity rule on S′ to S′ determines the codomain of f. Thus every mapping has a unique domain and codomain, and these are also mappings. Mappings which appear as domains or codomains are also called objects and are frequently denoted by capital letters to distinguish them from more general mappings. If A, f, B are mappings, and if A is the domain of f while B is the codomain of f, we denote this situation by A →^{f} B.

4Work partially supported by AF Contract No. AFOSR-520-64 at the University of Chicago and partially by a NATO Postdoctoral Fellowship at the ETH, Zurich.

A binary operation called composition is defined in the obvious way for precisely those pairs of mappings f, g such that the codomain of f is the domain of g. The result of such composition is denoted by juxtaposition fg, and we have

\xymatrix{A \ar[r]^{f} & B \ar[r]^{g} & C & ⇒ & A \ar[r]^{fg} & C} .

It is clear that composition is associative insofar as it is defined, and that objects behave as neutral elements with respect to composition.

The heuristic class of all mappings, with the above described domain, codomain, and composition structure, will be denoted by S. The axioms of our theory may be regarded as a listing of some of the basic and mathematically useful properties of S. There are three groups of axioms and two special axioms.

The first group of axioms (to which we do not assign numbers) consists of the axioms for an abstract category in the sense of (Eilenberg and Mac Lane 1945). We take these axioms as known but note that these axioms are obviously elementary (first-order) and that they have been stated informally in the third paragraph. We remark that a map A→^{f} B in a category is called an isomorphism if there exists a map B →^{g} A in the category such that fg = A and gf = B; g is then a uniquely determined isomorphism called the inverse of f.

The second group of axioms calls for the existence of solutions to certain “universal mapping problems”. As usual in such situations, it will be clear that the objects and operations thus asserted to exist are actually unique up to an isomorphism which is itself uniquely determined by a “naturalness” condition suggested by the structure of the particular axiom. This naturalness condition is simply that the isomorphism in question commutes with all the “structural maps” occurring in the statement of the universal mapping problem.

Axiom 1. All finite roots exist. Explicitly, this is guaranteed by assuming, in the sense explained below, that a terminal object 1 and an initial object 0 exist; that the product A×B and the coproduct (sum) A+B of any pair of objects exists; and that the equalizer E →^{k} A and the coequalizer B →^{q} E^{∗} of any pair A⇉ \begin{matrix}f \\ g \end{matrix} B of maps exist.

Axiom 2. The exponential B^{A} of any pair of objects exists. The defining universal mapping property of exponentiation, discussed below, is closely related to the concept of λ-conversion and requires, in essence, that for each object A, the functor ( )^{A} is co-adjoint to the functor A × ( ).

Axiom 3. There exists a Dedekind-Pierce object N. This plays the role of our axiom of infinity; the defining property of the natural numbers is here taken to be the existence and uniqueness of sequences defined by a very simple sort of recursion, as explained below.

We now explain in more detail the universal properties associated with the terminology occurring in the existential axioms above. A terminal object is an object 1 such that for any object A there is a unique mapping A→1. An initial object is an object 0 such that for any object B there is a unique mapping 0→B. It is clear that in our heuristic picture of S, any singleton set is a terminal object and the null set is an initial object. (More precisely, we refer here to the identity mappings on these sets.) Because nothing of substance that we wish to do in our theory depends on the size of the isomorphism classes of objects, we find it a notational convenience to assume that there is exactly one terminal object 1 and exactly one initial object 0; however, we do not make this convention a formal axiom as it can be avoided by complicating the notation somewhat.

Definition 1. x is an element of A, denoted x ∈ A, iff 1→^{x} A.

Remark 1: Elementhood, as defined here, is a special case of membership, to be defined presently. Neither of these notions has many formal properties in common with the basic relation of the usual set theories; x ∈ y ∈ z, for example, never holds except in trivial cases. However, we are able (noting that the evaluation of a mapping at an element of its domain may be viewed as a special case of composition) to deduce the basic property required by our heuristic definition of mapping, namely that if A→^{f} B then

∀x [x ∈ A ⇒ ∃!y [y ∈ B & xf = y]]

We must still describe the universal mapping properties of product, coproduct, equalizer and coequalizer in order to explicate our first axiom. Given two objects A and B their product is an object A × B, together with a pair of mappings

\xymatrix{ & A \\ A × B \ar[ur]^{p_{A}} \ar[dr]_{p_{B}} \\  & B}

such that for any object X and pair of mappings

\xymatrix{ & A \\ X \ar[ur]^{f_{A}} \ar[dr]_{f_{B}} \\  & B}

there is a unique mapping X →^{h} A × B such that hp_{A} = f_{A} and hp_{B} = f_{B}, i.e. such that the following diagram commutes:

\xymatrix{ &  & A \\ X \ar[urr]^{f_{A}} \ar[drr]_{f_{B}} \ar@{-->}[r]^{h} & A × B \ar[ur]_{p_{A}} \ar[dr]^{p_{B}} \\  &  & B}

We use the notation h = ⟨f_{A}, f_{B}⟩. Thus taking X = 1, we deduce that the elements x of A × B are uniquely expressible in the form x = ⟨x_{A}, x_{B}⟩ where x_{A} ∈ A and x_{B} ∈ B. Returning to consideration of an arbitrary X and pair of maps f_{A}, f_{B} it then follows that the “rule” of ⟨f_{A}, f_{B}⟩ is given by

x⟨f_{A}, f_{B}⟩ = ⟨xf_{A}, xf_{B}⟩ for all x ∈ X.

The “structural maps” p_{A} and p_{B} are called projections. There are unique natural (commuting with projections) isomorphisms

A × 1 ≅ A ≅ 1 × A
(A × B) × (C × D) ≅ (A × C) × (B × D) .

Given mappings A→^{f} A′, B →^{g} B′, there is a unique natural mapping

\xymatrix{A × B \ar[r]^{f×g} & A′ × B′}

and this product operation on mappings is functorial in the sense that given further mappings A′ →^{\overline{f}} A′′, B′ →^{\overline{g}} B′′, one has

(f \overline{f}) × (g \overline{g}) = (f × g)(\overline{f} × \overline{g})

The coproduct A + B of two objects is characterized by the dual universal mapping property

\xymatrix{A \ar[dr]_{i_{A}} \ar[drr]^{f_{A}} \\  & A + B \ar@{-->}[r]^{h} & X \\ B \ar[ur]^{i_{B}} \ar[urr]_{f_{B}}}

∀X ∀f_{A} ∀f_{B} ∃!h [i_{A}h = f_{A} & i_{B}h = f_{B}] (where the quantifiers range only over diagrams of the above form). Here the structural maps i_{A} and i_{B} are called injections. In the usual discussions of S and hence in our theory, the coproduct is called the sum. The functorial extension of this operation from objects to all mappings follows just as in the case of the product operation, but the deduction of the nature of the elements of A + B is not so easy; in fact we will find it necessary to introduce further axioms to describe the elements of a sum. This is not surprising in view of the great variation from category to category in the nature of coproducts. Suffice it for the moment to note that the existence of sums in S can be verified by one of the usual “disjoint union” constructions; the universal mapping property corresponds to the heuristic principle that a mapping is well defined by specifying its rule separately on each piece of a finite partition of its domain.

The equalizer of a pair of mappings A⇉ \begin{matrix}f \\ g \end{matrix} B is a mapping E →^{k} A such that kf = kg and which satisfies the universal mapping property: for any X →^{u} A such that uf = ug there is a unique X →^{z} E such that u = zk. It follows immediately that the elements a of A such that af = ag are precisely those which factor through k, and the latter are in one-to-one correspondence with the elements of E. It also follows that k is, in a sense to be defined presently, a subset of A; clearly it is just the subset on which f and g agree. The equalizer construction, like the coequalizer to be described next, has certain functorial properties which we do not bother to state explicitly.

The coequalizer of a pair of mappings A ⇉ \begin{matrix}f \\ g \end{matrix} B is a mapping B →^{q} E^{∗} such that fq = gq and which satisfies the dual universal mapping property:

\xymatrix{A \ar[r]^{f} \ar[r]_{g} & B \ar[dr]_{u} \ar[r]^{q} & E^{∗} \ar@{-->}[d]^{z} \\  &  & X}

∀X ∀u [fu = gu ⇒ ∃! z [u = qz] ]

(where the quantified variables range only over diagrams of the sort pictured). As in the case of sums, an elementwise investigation of coequalizers is not immediate; the discussion of the elements of E^{∗} can be reduced to the consideration of the pairs of elements of B which are identified by q, but the latter is non-trivial. However, using our full list of axioms we will be able to prove a theorem to the effect that q is the quotient map obtained by partitioning B in the finest way which, for each a ∈ A, puts af and ag in the same cell of the partition.

This completes the explication of our axiom “finite roots exist” except for the remark that in category theory “finite roots” refers to a more general class of operations including inverse images and intersections and their duals as well as more complicated constructions.

However, all these can be proved to exist (within the first order language) once the existence of the six special cases we have assumed is affirmed.

Before proceeding to the discussion of the exponentiation axiom, let us note that the usual formal definition of mapping can be dualized. The usual notion of a mapping f from A to B describes f as a subset of A×B, namely the graph g of f in the diagram below.

\xymatrix{ &  & A \\ A \ar[urr]^{A} \ar[drr]_{f} \ar[r]^{g} & A × B \ar[ur]_{p_{A}} \ar[dr]^{p_{B}} \\  &  & B}

Dualizing the diagram, we obtain the cograph g^{∗} of f defined to make the following diagram commutative.

\xymatrix{A \ar[dr]_{i_{A}} \ar[drr]^{f} \\  & A + B \ar@{-->}[r]^{g^{∗}} & B \\ B \ar[ur]^{i_{B}} \ar[urr]_{B}}

This suggests the alternative concept of a mapping from A to B as a partition of the disjoint union with the property that each cell in the partition contains exactly one member of B. The concept of cograph corresponds to the intuitive diagrams sometimes used to represent mappings in which both A and B are displayed (disjointly!) and a line is drawn from each member of A to its image in B; two members of A + B can then be thought of as identified if they can be connected by following these lines.

Whatever formal definition is taken, it is intuitively clear that for each pair of sets A, B there exists a set whose elements are precisely the mappings from A to B or at least “names” for these mappings in some sense. This is one of the consequences of our axiom that “exponentiation exists”.

The meaning of the exponentiation axiom is that the operation of forming the product has a co-adjoint operation in the sense that given any pair of objects A, B there exists an object B^{A} and a mapping A × B^{A} →^{e} B with the property that for any object X and any mapping A × X →^{f} B there is a unique mapping X →^{h} B^{A} such that (A × h)e = f. This universal mapping property is partly expressed by the following diagram.

\xymatrix{A × X \ar[dd]_{A} \ar@{-->}[dd]^{h} \ar[ddr]^{f} \\ × \\ A × B^{A} \ar[r]_{e} & B}

Here the structural mapping e is called the evaluation map. By taking X = 1, and noting that the projection A × 1→A is an isomorphism, it follows immediately that the elements of B^{A} are in one-to-one correspondence with the mappings from A to B. Explicitly, a mapping A →^{f} B and its “name” [f] ∈ B^{A} are connected by the commutativity of the following diagram.

\xymatrix{A × 1 \ar[r]^{p_{A}} \ar[d]_{A×[f]} & A \ar[d]^{f} \\ A × B^{A} \ar[r]_{e} & B}

It follows immediately that for a ∈ A, A→^{f} B, one has

⟨a, [f]⟩e = af ,

i.e., the rule of the evaluation map is evaluation.

When extended to a functor in the natural (i.e., coherent with evaluation) fashion, exponentiation is actually contravariant in the exponent. That is, given A′ →^{f} A, B →^{g} B′, the induced map goes in the direction opposite of f:

\xymatrix{B^{A} \ar[r]^{g^{f}} & B^{′A′}}

Functoriality in this case just means that if A′′ →^{\overline{f}} A′, B′ →^{\overline{g}} B′′ are further mappings then (g\overline{g})^{(\overline{f}f)} = (g^{f})(\overline{g}\overline{f}). The rule of g^{f} is of course that for A→^{u} B,

[u](g^{f}) = [fug] .

A simple example of such an induced map is the “diagonal” B →B^{A} which is induced by A→1 and B →^{B} B and which assigns to each b ∈ B the “name” of the corresponding constant mapping A→B.

Also deducible from the exponentiation axiom is the existence, for any three objects A, B, C, of a mapping

\xymatrix{B^{A} × C^{B} \ar[r]^{γ} & C^{A}}

such that for any A→^{f} B, B →^{g} C one has

⟨[f], [g]⟩γ = [fg]

(Of course the usual “laws of exponents” can be proved as well.)

Another consequence of the exponentiation axiom is the distributivity relation

A × B + A × C ≅ A × (B + C)

Actually a canonical mapping from the left hand side to the right hand side can be constructed in any category in which products and coproducts exist; in a category with exponentiation the inverse mapping can also be constructed. A related conclusion is that if q is the coequalizer of f with g, then A × q is the coequalizer of A × f with A × g. Both these conclusions are special cases of the fact that for each A the functor A × ( ), like any functor with a co-adjoint, must preserve all right hand roots. We remark that in the usual categories of groups, rings, or modules, exponentiation does not exist, which follows immediately from the fact that distributivity fails.

The third axiom asserts the existence of a special object N equipped with structural maps 1→^{0} N →^{s} N with the property that given any object X and any x_{0} ∈ X, X →^{t} X there is a unique N →^{x} X such that the following diagram commutes:

\xymatrix{ & N \ar[r]^{s} \ar[dd]^{x} & N \ar[dd]^{x} \\ 1 \ar[ur]^{0} \ar[dr]_{x_{0}} \\  & X \ar[r]^{t} & X}

As usual, the universal mapping property determines the triple N, 0, s up to a unique isomorphism. A mapping N →^{x} X is called a sequence in X, and the sequence asserted to exist in the axiom is said to be defined by simple recursion with the starting value x_{0} and the transition rule t. Most of Peano’s postulates could now be proved to hold for N, 0, s but we delay this until all our axioms have been stated because, for example, the existence of an object with more than one element is needed to conclude that N is infinite. However we can now prove the

Theorem 1 (Primitive Recursion). Given a pair of mappings

\xymatrix{A \ar[r]^{f_{0}} & B}
\xymatrix{N × A × B \ar[r]^{u} & B}

there is a mapping

\xymatrix{N × A \ar[r]^{f} & B}

such that for any n ∈ N, a ∈ A one has

⟨0, a⟩f = af_{0}
⟨ns, a⟩f = ⟨n, a, ⟨n, a⟩f⟩u

(It will follow from the next axiom that f is uniquely determined by these conditions.)

Proof. In order to understand the idea of the proof, notice that primitive recursion is more complicated than simple recursion in essentially two ways. First, the values of f depend not only on n ∈ N but also on members of the parameter object A. However, the exponentiation axiom enables us to reduce this problem to a simpler one involving a sequence whose values are functions. That is, the assertion of the theorem is equivalent to the existence of a sequence

\xymatrix{N \ar[r]^{y} & B^{A}}

such that 0y = [f_{0}] and such that for any n ∈ N, a ∈ A, one has

⟨a, (ns)y⟩e = ⟨n, a, ⟨a, ny⟩e⟩u

where e is the evaluation map for B^{A}.

The second way in which primitive recursion (and the equivalent problem just stated) is more complicated than the simple recursion of our axiom is that the transition rule u depends not only on the value calculated at the previous step of the recursion but also on the number of steps that have been taken. However, this can be accomplished by first constructing by simple recursion a sequence whose values are ordered pairs in which the first coordinate is used just to keep track of the number of steps. Thus the proof of this theorem consists of constructing a certain sequence

\xymatrix{N \ar[r]^{x} & N × B^{A}}

and then defining y as required above to be simply x followed by projection onto the second factor. That is, we define by simple recursion the graph of y.

Explicitly, the conditions on the sequence x are that

0x = ⟨0, [f_{0}]⟩0

and that for each n ∈ N and a ∈ A

(ns)xp_{N} = ns
⟨a, (ns)xp_{B^{A}}⟩e = ⟨n, a, ⟨a, nxp_{B^{A}}⟩e⟩u

By our axiom, the existence of such x is guaranteed by the existence of a mapping

\xymatrix{N × B^{A} \ar[r]^{t} & N × B^{A}}

such that for any n ∈ N, h ∈ B^{A}, a ∈ A

⟨n, h⟩tp_{N} = ns
⟨a, ⟨n, h⟩tp_{B^{A}}⟩e = ⟨n, a, ⟨a, h⟩e⟩u

But such a t can be constructed by defining

t = ⟨p_{N}s, t_{2}⟩

where N × B^{A} →^{t_{2}} B^{A} is the mapping corresponding by exponential adjointness to the composite

\xymatrix{A × N × B^{A} \ar[r] & N × A × A × B^{A} \ar[r] & N × A × B \ar[r]^{u} & B}

where the first is induced by the diagonal map A → A × A and where the second is induced by the evaluation map A × B^{A}→B. (Here we have suppressed mention of certain commutativity and associativity isomorphisms between products.) This completes the proof of the Primitive Recursion theorem.

Our first three axioms, requiring the existence of finite roots, exponentiation, and the Dedekind-Pierce object N, actually hold in certain fairly common categories other than S, such as the category C of small categories and functors or any functor category S^{ℂ} for a fixed small category ℂ (examples of the latter include the category S^{𝔾} whose objects are all permutation representations of a given group 𝔾 and whose maps are equivariant maps as well as the category S^{2} whose objects correspond to the mappings in S and whose maps are commutative squares of mappings in S). However, these categories do not satisfy our remaining axioms.

We state now our two special axioms

Axiom 4. 1 is a generator. That is, if A⇉ \begin{matrix}f \\ g \end{matrix} B then

f ≠ g ⇒ ∃a [a ∈ A & af ≠ ag]

In other words, two mappings are equal if they have the same domain and codomain and if they have the same value at each element of their domain. We mention the immediate consequence that if A has exactly one element then A = 1.

Axiom 5(Axiom of Choice). If the domain of f has elements, then there exists g such that fgf = f.

Remark 2: This axiom has many uses in our theory even at the elementary level, as will soon become apparent. That, in relation to the other axioms, the axiom of choice is stronger in our system than in the usual systems is indicated by the fact that the axiom of choice (as stated above) is obviously independent. Namely, the category O of partially ordered sets and order-preserving maps is a model for all our axioms (even including the final group of axioms not yet described) with the exception that the axiom of choice is false in O. To see the latter we need only take f to be the “identity” map from a set with trivial partial ordering to the same set with a stronger ordering. Most of the basic theorems that we will prove fail in O.

Proposition 1. 2 is a cogenerator.

Proof. Here we define 2 = 1+1, and by the statement that 2 is a cogenerator we mean that if A ⇉ \begin{matrix}f \\ g \end{matrix} B are different then there is B →^{u} 2 such that fu ≠ gu. Since 1 is a generator we are immediately reduced to the case where A = 1 and f, g are elements of B. By the universal property of sums there is an induced map 2 →^{h} B which by the axiom of choice has a “quasi-inverse” u

[figure: 1; i_{0}; f; 2; h; B; huh = h; 1; i_{1}; g]

But this u clearly separates f, g if they are different, since

fu = gu ⇒ fuh = guh ⇒ i_{0}huh = i_{1}huh ⇒ i_{0}h = i_{1}h ⇒ f = g

In order to state our next proposition, we must define subset, inclusion, and member.

Definition 2. a is a subset of A iff a is a monomorphism with codomain A.

Here a monomorphism a is a mapping such that

∀b ∀b′ [ba = b′a ⇒ b = b′]

By the axiom of choice it is clear that in S (indeed in any model of our theory) every monomorphism, except for trivial cases, is a retract, i.e. has a right inverse. Also, since 1 is a generator, it suffices in verifying that a is a monomorphism to consider b, b′ which are elements of the domain of a. Note that the subset is a itself, not just the domain of a. The domain of a is an object, and an object in S is essentially just a cardinal number, whereas the notion of subset contains more structure than just number. Namely, a subset of A involves a specific way of identifying its members as elements of A, hence the mapping a.

Remark 3: A mapping A→^{f} B is an epimorphism iff

∀y ∈ B ∃x ∈ A [xf = y] ,

a monomorphism iff

∀x ∈ A ∀x′ ∈ A [xf = x′f ⇒ x = x′] ,

an isomorphism iff it is both an epimorphism and a monomorphism. The proof (using the axiom of choice) is left to the reader. (The concept of epimorphism is defined dually to that of monomorphism.)

Definition 3. x is a member of a [notation x ∈ a] iff for some A (which will be unique) x is an element of A, a is a subset of A, and there exists \overline{x} such that \overline{x}a = x.

\xymatrix{ & 1 \ar@{-->}[dl]_{\overline{x}} \ar[dr]^{x} \\ • \ar[rr]_{a} &  & A}

Note that \overline{x} is an element of the domain of a and is uniquely determined. Note also that x is an element of a iff x is a member of a and a is an object; the use of the same notation for the more general notion causes no ambiguity.

Definition 4. a ⊆ b iff for some A, a and b are both subsets of A and there exists h such that a = hb.

\xymatrix{• \ar@{-->}[rr]^{h} \ar[dr]_{a} &  & • \ar[dl]^{b} \\  & A}

Note that h is a uniquely determined monomorphism if it exists. The inclusion relation thus defined for subsets of A is clearly reflexive and transitive. Also x ∈ a iff x ⊆ a and the domain of x is 1, and a is a subset of A iff a ⊆ A and A is an object.

Proposition 2. Let a, b be subsets of A. Then a ⊆ b iff

∀x ∈ A [x ∈ a ⇒ x ∈ b]

(For the proof we assume that the domain of b has elements; however the next axiom makes this restriction unnecessary.)

Proof. If a ⊆ b and 1→^{x} A, then clearly x ∈ a ⇒ x ∈ B.

\xymatrix{ & 1 \ar[dl] \ar@{-->}[dr] \\ • \ar[rr]^{h} \ar[dr]_{a} &  & • \ar[dl]^{b} \\  & A}

Conversely, suppose ∀x ∈ A [x ∈ a ⇒ x ∈ B]. By the axiom of choice there is A →^{g} dom b such that bgb = b. Since b is a monomorphism, bg = dom b (the identity mapping). We define h = ag, and attempt to show a = hb. It suffices to show that \overline{x}a = \overline{x}agb for every element \overline{x} of the domain of a. But given \overline{x}, then x = \overline{x}a is an element of A for which x ∈ a, so by hypothesis x ∈ b, i.e., ∃y [x = yb]. Then

\overline{x}hb = \overline{x}agb = xgb = ybgb = yb = x = \overline{x}a

Since \overline{x} was arbitrary, hb = a because 1 is a generator. This shows a ⊆ b.

Our final group of axioms is the following:

Axiom 6. Each object other than 0 (i.e. other than initial objects) has elements.

Axiom 7. Each element of a sum is a member of one of the injections.

Axiom 8. There is an object with more than one element.

We remark that Axiom 8 is independent of all the remaining axioms, and that, in fact, the full set of axioms with 8 excluded is easily proved consistent, for all these axioms are verified in the finite category

\xymatrix{0 \ar[r] & 1}

(In this case N = 1.) However, the question of independence for Axioms 4,6,7 is still unsettled.

Proposition 3. 0 has no elements.

Proof. If 1→0, then 1 = 0, so that every object has exactly one element, contradicting axiom 8.

Proposition 4. The two injections 1⇉ \begin{matrix}io \\ i_{1} \end{matrix} 2 are different and are the only elements of 2.

Proof. The second assertion is immediate by Axiom 7. Suppose i_{0} = i_{1} and let S be an object with two distinct elements x, y. Then there is t such that

\xymatrix{1 \ar[dr]_{i_{0}} \ar[drr]^{x} \\  & 2 \ar[r]^{t} & S \\ 1 \ar[ur]^{i_{1}} \ar[urr]_{y}}

commutes by the sum axiom, so x = i_{0}t = i_{1}t = y, a contradiction. Thus i_{0} ≠ i_{1}.

It is also easy to establish, by using the axiom of choice, that if A has exactly two elements, then A ≅ 2.

Proposition 5. To any two objects A, B, the two injections

\xymatrix{A \ar[dr]^{i_{A}} \\  & A + B \\ B \ar[ur]_{i_{B}}}

have no members in common.

Proof. Consider A + B→2 induced by the unique maps A→1, B→1. Suppose there are a, b such that ai_{A} = bi_{B} are equal elements of A + B. Then the diagram

\xymatrix{ & A \ar[dr]_{i_{A}} \ar[rr] &  & 1 \ar[dr]^{i_{0}} \\ 1 \ar[ur]^{a} \ar[dr]_{b} &  & A + B \ar[rr] &  & 2 \\  & B \ar[ur]^{i_{B}} \ar[rr] &  & 1 \ar[ur]_{i_{1}}}

is commutative. But the composite maps 1 →^{a} A→1 and 1 →^{b} B →1 must both be the identity, yielding i_{0} = i_{1}, a contradiction.

We now prove five theorems which, together with Theorem 1, are basic to the development of mathematics within our theory.

Theorem 2. Peano’s postulates hold for N.

Proof. That the successor mapping N →^{s} N is well-defined is already implicit. To show that s is injective, note that the predecessor mapping can be defined by primitive recursion; one of the defining equations of the predecessor is that it be right inverse to s. The other defining equation for the predecessor p is that 0p = 0, so that if 0 were a successor, say ns = 0, then n = n(sp) = (ns)p = 0p = 0. But if 0s = 0, then every object has only the identity endomorphism. For let X →^{t} X and x_{0} ∈ X; then there is N →^{x} X such that 0x = x_{0} and sx = xt, hence x_{0}t = 0xt = 0sx = 0x = x_{0}. But x_{0} being arbitrary, we can conclude t = X since 1 is a generator. However, Axiom 8 implies that 2, for example, has non-identity endomorphisms; this contradiction shows that 0 is not the successor of any n ∈ N.

Finally we prove Peano’s induction postulate. Let A→^{a} N be a subset such that 0 ∈ A and

∀n ∈ N [n ∈ a ⇒ ns ∈ a]

The last means that a is included in its own inverse image under s, so there is A→^{t} A such that as = ta.

\xymatrix{A \ar[dddr]_{a} \ar@{-->}[dr] \ar[drrr]^{t (def)} \\  & • \ar[rr] &  & A \ar[dd]^{a} \\  &  & s^{−1}[a] ; “meet” ; diagram \ar[dl] \\  & N \ar[rr]_{s} &  & N}

The first means there is \overline{0} ∈ A such that \overline{0}a = 0. By simple recursion \overline{0}, t determine N →^{x} A such that 0x = \overline{0} and sx = xt. This implies

0(xa) = 0
s(xa) = (xa)s

so that by the uniqueness of mappings defined by simple recursion, xa = N. Thus for any n ∈ N, n = (nx)a, so that n ∈ a.

The following theorem has the consequence that every mapping can be factored into an epimorphism followed by a monomorphism. However, from the viewpoint of general categories, the result is stronger. (It does not hold in the category of commutative rings with unit, for example.)

Theorem 3. For any mapping f, the regular co-image of f is canonically isomorphic to the regular image of f. More precisely, the unique h rendering the following diagram commutative is an isomorphism, where k is the equalizer of p_{0}f, p_{1}f and q is the coequalizer of kp_{0}, kp_{1}, while k^{∗} is the coequalizer of fi_{0}, fi_{1} and q^{∗} is the equalizer of i_{0}k^{∗}, i_{1}k^{∗}.

\xymatrix{R_{f} \ar[r]^{k} & A × A \ar[r]^{p_{0}} \ar[r]_{p_{1}} & A \ar[r]^{f} \ar[d]_{q} & B \ar[r]^{i_{0}} \ar[r]_{i_{1}} & B + B \ar[r]^{k^{∗}} & R_{f}^{∗} \\  &  & I^{∗} \ar@{-->}[r]_{h} & I \ar[u]_{q^{∗}}}

Proof. We first show that hq^{∗} is a monomorphism. This is clear if A = 0, so we assume A has elements. Then by the axiom of choice, q has a left inverse t: tq = I^{∗}. Suppose uhq^{∗} = u′hq^{∗}. Then

⟨ut, u′t⟩p_{0}f = utf = uhq^{∗} = u′hq^{∗} = u′tf = ⟨ut, u′t⟩p_{1}f

Hence, k being the equalizer of p_{0}f, p_{1}f, there is w such that ⟨ut, u′t⟩ = wk. But then, q being a coequalizer,

u = utq = ⟨ut, u′t⟩p_{0}q = wkp_{0}q = wkp_{1}q

= ⟨ut, u′t⟩p_{1}q = u′tq = u′

The above shows hq^{∗} is a monomorphism, from which it follows that h is a monomorphism. A dual argument shows that h is an epimorphism and hence an isomorphism by Remark 3.

The above theorem implies that any reasonable definition of image gives the same result, so we may drop the word “regular”. There is no loss in assuming that I∗ = h = I; we then refer to the equation f = qq∗ as the factorization of f through its image.

For the discussion of the remaining theorems we assume that a fixed labelling of the two maps 1⇉ \begin{matrix}i_{0} \\ i_{1} \end{matrix} 2 has been chosen. It is clear heuristically that the (equivalence classes of) subsets of any given set X are in one-to-one correspondence with the functions X→2. It is one of our goals to prove this. More exactly, we wish to show that every subset of X has a characteristic function X→2 in the sense of

Definition 5. The mapping X →^{φ} 2 is the characteristic function of the subset A→^{a} X iff

∀x ∈ X [x ∈ a ⇔ xφ = i_{1}]

It is easy to see (using equalizers) that every function X → 2 is the characteristic function of some subset. We will refer to those subsets which have characteristic functions as special subsets, until we have shown that every subset is special. This assertion will be made to follow from the construction of a “complement” A′→^{a′} X for every subset A→^{a} X.

Essentially, the complement of a will be constructed as the union of all special subsets which do not intersect a. We first prove a theorem to the effect that such unions exist.

Theorem 4. Given any “indexed family of special subsets of X”

\xymatrix{I \ar[r]^{α} & 2^{X}}

there exists a subset

[figure: ⋃α; a; X]

which is the union of the α_{j}, j ∈ I, in the sense that for any x ∈ X,

x ∈ a ⇔ ∃j ∈ I [⟨x, jα⟩e_{2^{X}} = i_{1}]

where e_{2^{X}} is the evaluation X × 2^{X}→2.

Proof. By exponential adjointness, α is equivalent to a mapping

\xymatrix{X × I \ar[r]^{\overline{α}} & 2}

and the desired property of ⋃_{α} is equivalent to

x ∈ a ⇔ ∃j ∈ I [⟨x, j⟩\overline{α} = i_{1}]

We construct ⋃_{α} as follows:

[figure: _{∑α}; q; k; X × I; p_{X}; \overline{α}; 1; i_{1}; 2; _{⋃α}; a; X]

Here k is the equalizer of \overline{α} with the composite X × I →1 →^{i_{1}} 2, and kp_{X} = qa is the factorization of kp_{X} through its image. Suppose x ∈ a. Then since q is an epimorphism there exists \overline{x} ∈ ∑_{α} such that \overline{x}kp_{X} = x. Define j = \overline{x}kp_{I}. Then

⟨x, j⟩\overline{α} = \overline{x}k\overline{α} = \overline{x}k(X × I→1→^{i_{1}} 2) = i_{1}

since k is an equalizer and since \overline{x}k(X × I→1) = 1. The converse is even easier: if there is j ∈ I such that ⟨x, j⟩\overline{α} = i_{j}, then by the universal mapping property of the equalizer k, ⟨x, j⟩ must come from \overline{x} ∈ ∑_{α}, so that on applying q to \overline{x} one finds that x ∈ a.

Remark 4: Using the above construction of ∑_{α} we can prove a perhaps more familiar form of the axiom of choice, namely, given

\xymatrix{I \ar[r]^{α} & 2^{X}}

if every α_{j} is non-empty (α_{j} ≠ 0), there is I →^{f} X such that jf ∈ α_{j} for each j ∈ I. (Here by α_{j} we mean the subset of X obtained by equalizing with X→1 →^{i_{1}} 2 the map X→2 whose “name” is jα.) We leave the details to the reader, but note that the essential step is the application of the axiom of choice to the composite mapping

[figure: ∑α; X × I; p_{I}; I]

We also leave to the reader the construction of the “product” ∏_{α} which is the subset of (∑_{α})^{I} consisting of all choice functions f as above. Notice that, although in our heuristic model S, ∑_{α} and ∏_{α} are actual (infinite) coproduct and product in the categorical sense, there is no way to guarantee by first order axioms that this will be true in every first order model of our theory. (See also Remark 11.)

Theorem 5. Given any subset A →^{a} X, there is a subset A′ →^{a′} X such that X ≅ A + A′, with a, a′ as the injections. Thus x ∈ a′ iff x ∈ X and x ∉ a, and a has a characteristic function X→2.

We will need for the proof the following

Lemma 1. Given a subset A →^{a} X and an element x ∈ X such that x ∉ a, then there is X →^{φ} 2 such that xφ = i_{1} and aφ ≡ i_{0}; that is, there is a special subset containing x but intersecting a vacuously.

Proof of Lemma 1. Define (_{x}^{a}) by the universal mapping property of sums so that

\xymatrix{A \ar[dr]_{i_{A}} \ar[drr]^{a} \\  & A + 1 \ar[r]^{(_{x}^{a})} & X \\ 1 \ar[ur]^{i_{1}} \ar[urr]_{x}}

and let u be a “quasi-inverse” for (_{x}^{a}) as guaranteed by the axiom of choice. Then define φ to be the composition

\xymatrix{X \ar[r]^{u} & A + 1 \ar[r]^{(A→1)+1} & 1 + 1 = 2}

By axiom 7, (_{x}^{a}) is a monomorphism since a is and since x ∉ a, so we actually have that (_{x}^{a}) u = A + 1. Therefore (setting t_{A} = (A→1) + 1)

xφ = xut_{A} = i_{1}(_{x}^{a})ut_{A} = i_{1}t_{A} = i_{1}
aφ = aut_{A} = i_{A}(_{x}^{a})ut_{A} = i_{A}t_{A} = i_{0}

Proof of Theorem 5. Let j_{0} ∈ 2^{A} be the element corresponding by exponential adjointness to the composition A × 1 →^{p_{1}} 1 →^{i_{0}} 2, and then define a →^{μ} 2^{X} to be the equalizer of 2^{a} with the composition 2^{X} →1 →^{j_{0}} 2^{A}. Thus intuitively μ is the subset of 2^{X} whose members are just the special subsets of X which intersect a vacuously. Define a′ to be the union of μ. Thus

[figure: _{∑μ}; q; k; X × a; p_{X}; \overline{μ}; 1; i_{1}; 2; A′ = ⋃_{μ}; a′; X]

where \overline{μ} corresponds to μ and k is the equalizer of \overline{μ} with the function constantly i_{1}, and where q is an epimorphism while a′ is a monomorphism. There is, of course a mapping f such that the diagram

\xymatrix{A \ar[dr]_{i_{A}} \ar[drr]^{a} \\  & A + A′ \ar[r]^{f} & X \\ A′ \ar[ur]^{i_{A′}} \ar[urr]_{a′}}

commutes. We must show that f is an isomorphism. For this it suffices to show that f is a monomorphism and an epimorphism. That f is a monomorphism follows from axiom 7 and the fact that, by construction, a and a′ have no members in common, since x ∈ a implies that ⟨x, t⟩e_{2^{X}} = i_{0} for every t ∈ μ, whereas x ∈ a′ implies that ∃t ∈ μ [⟨x, t⟩e_{2^{X}} = i_{1}]. On the other hand, to show that f is an epimorphism, it suffices to show that f is surjective, so consider an arbitrary x ∈ X. If x ∉ A then by the lemma there is [φ] ∈ 2^{X} such that xφ = i_{1} while aφ ≡ i_{0}. Since aφ ≡ i_{0}, we actually have [φ] ∈ μ by construction of a→^{μ} 2^{X}. Because ⟨x, [φ]⟩e_{2^{X}} = i_{1}, ⟨x, [φ]⟩ is actually a member of k(X × μ) where k is the equalizer of \overline{μ} with the map constantly i_{1}, so finally applying ∑_{μ} →^{q} A′ to the element of ∑_{μ} which corresponds to ⟨x, [φ]⟩, we find that x ∈ a′. Thus, since we have shown that x comes either from A or A′, f is surjective.

The final “mathematical” theorem we shall prove concerns a more “internal” description of the nature of coequalizers. Actually the theorem only refers to an important special case, but we will remark that the general case can also be handled, leaving details to the reader. We consider a pair

\xymatrix{R \ar[r]^{f_{0}} \ar[r]_{f_{1}} & A}

of mappings, and will sometimes denote by f = ⟨f_{0}, f_{1}⟩ the corresponding single mapping R→A × A, from which f_{0} and f_{1} can be recovered.

Definition 6. We say that f is reflexive iff

∃d [A→^{d} R & df_{0} = A = df_{1}]

symmetric iff

∃t [R→^{t} R & tf_{0} = f_{1} & tf_{1} = f_{0}]

transitive iff

∀h_{0} ∀h_{1} \{X ⇉ \begin{matrix}h_{0} \\ h_{1} \end{matrix} R & h_{0}f_{1} = h_{1}f_{0}

⇒ ∃u [uf_{0} = h_{0}f_{0} & uf_{1} = h_{1}f_{1}]}

It has previously been pointed out (Lawvere 1963a) that the following theorem holds in every “algebraic” category and is in a sense characteristic of such categories. Since S is the basic algebraic category, it is essential that we should be able to prove the theorem from our axioms for S. Notice that although our proof depends on the axiom of choice, and although the validity of the theorem for algebraic categories depends on its validity for S, nevertheless the axiom of choice does not hold in most algebraic categories.

Theorem 6. If R ⇉ \begin{matrix}f_{0} \\ f_{1} \end{matrix} A is such that f = ⟨f_{0}, f_{1}⟩ is reflexive, symmetric, transitive, and a subset of A × A, then f is the equalizer of p_{0}q with p_{1}q, where A →^{q} Q is the coequalizer of f_{0} with f_{1}.

Proof. We actually show that if f is reflexive, symmetric, and transitive, and if a_{0} ∈ A, a_{1} ∈ A, then

a_{0}q = a_{1}q ⇔ ∃r ∈ R [rf_{0} = a_{0} & rf_{1} = a_{1}]

which clearly implies the assertion in the theorem. We accomplish this by constructing a mapping A →^{g} 2^{A} which is intuitively just the classification of elements of A into fequivalence classes. For the construction of g we need two lemmas:

Lemma 2. for any A there is a mapping A →^{{}} 2^{A} such that for any x ∈ A, y ∈ A, y is a member of the subset whose characteristic function has the name {x} iff y = x.

Proof. Let {} be the mapping corresponding by exponential adjointness to the characteristic function of the diagonal subset

\xymatrix{A \ar[r]^{⟨A,A⟩} & A × A}

Lemma 3. Given any mapping R→^{h} A there is a mapping

\xymatrix{2^{R} \ar[r]^{\overline{h}} & 2^{A}}

with the property that given any subset of R with characteristic function ψ, then [ψ]\overline{h} is the name of the characteristic function of the subset a of A having the property that for any x ∈ A,

x ∈ a ⇔ ∃r [rψ = i_{1} & rh = x]

Briefly, \overline{h} is the direct image mapping on subsets determined by the mapping h on the elements.

Proof. Consider the equalizer Ψ of e_{r^{R}} with i_{1}:

\xymatrix{R′ \ar[r]^{Ψ} & R × 2^{R} \ar[rr]^{e_{2^{R}}} \ar[r] & 1 \ar[r]_{i_{1}} & 2}

Thus Ψ is a subset whose members are just the pairs ⟨r, [ψ]⟩ where ψ is the characteristic function of a subset of R of which r is a member. Form the composition of Ψ with

\xymatrix{R × 2^{R} \ar[r]^{h×2^{R}} & A × 2^{R}}

Then the image of this composition is a subset of A × 2^{R} and hence has a characteristic function A × 2^{R} →^{Φ} 2. Let \overline{h} be the mapping 2^{R}→2^{A} corresponding by exponential adjointness to Φ. To show that \overline{h} has the desired property, let R →^{ψ} 2 and let a be the subset of A whose characteristic function φ has the name [ψ]\overline{h}, i.e [φ] = [ψ]\overline{h} and φ is the characteristic function of a. Suppose rψ = i_{1} and rh = x; then we must show that x ∈ a, i.e. that xφ = i_{1}. However, since ⟨r, [ψ]⟩ ∈ Ψ, one has also ⟨r, [ψ]⟩(h × 2^{R}) ∈ Ψ(h × 2^{R}), which is the same as to say rh, [ψ]⟩Φ = i_{1}, which since x = rh, implies by definition of \overline{h} that x is a member of the subset whose characteristic function is [ψ]\overline{h} = [φ]; but the latter subset is a, as required. Conversely, assume x ∈ a. Then xφ = i_{1}, so that ⟨x, [φ]⟩Φ = i_{1} and hence ⟨x, [φ]⟩ ∈ Ψ(h × 2^{R}).

\xymatrix{1 \ar[ddr]_{⟨x,[φ]⟩} \ar@{-->}[dr] \\  & R′ \ar[r]^{Ψ} & R × 2^{R} \ar[dl]^{h×2^{R}} \\  & A × 2^{R}}

Therefore there is r ∈ R ∋ rh = x and ⟨r, [ψ]⟩ ∈ Ψ. But this means rψ = i_{1}.

Remark 5: It is easy to verify that in these lemmas we have actually constructed a covariant functor and a natural transformation {} from the identity functor into this functor. There are actually three different “power-set” functors: the contravariant one f ⇝ 2^{f}, the covariant “direct image” functor h ⇝ \overline{h} just constructed, and a dual covariant functor related to universal quantification in the same way that the direct image functor is related to existential quantification.

We now return to the proof of the theorem. Given the two mappings

\xymatrix{R \ar[r]^{f_{0}} \ar[r]_{f_{1}} & A}

we can by the lemmas construct two mappings A→2^{A} as follows

\xymatrix{ &  & 2^{R} \ar[dr]^{_{\overline{f}_{1}}} \\ A \ar[r]^{\{\}} & 2^{A} \ar[ur]^{2^{f_{0}}} \ar[dr]_{2^{f_{1}}} &  & 2^{A} \\  &  & 2^{R} \ar[ur]_{_{\overline{f}_{0}}}}

We claim that if f = ⟨f_{0}, f_{1}⟩ is symmetric, then the two composites A→2^{A} are actually equal (to a map which we will call g), that if f is symmetric and transitive, then f_{0}g = f_{1}g, and that if f is reflexive, symmetric and transitive, then the induced map Q→2^{A} (where A →^{q} Q is the coequalizer of f_{0} with f_{1}) is actually the image of g (so in particular a subset of 2^{A}). When reflexivity does not hold, the difference between q and the co-image of g is that q keeps separate all elements of A which are not related to any element, whereas g maps all such elements to the empty subset of A.

First we show that symmetry implies \{\}2^{f_{0}} \overline{f}_{1} = \{\}2^{f_{1}} \overline{f}_{0} and hence a unique definition of g. Let a, a′ ∈ A. Then a′ is a member of the subset of A whose characteristic function has the name \{a\}2^{f_{0}} \overline{f}_{1} (briefly a′ϵ_{∼}\{a\}2^{f_{0}} \overline{f}_{1}) iff there is r ∈ R such that rf_{0} = a and rf_{1} = a′. But this condition is clearly symmetrical in f_{0}, f_{1}. (And of course “members” (in the sense of ϵ_{∼}) determine elements of 2^{A}.)

Next we show that f_{0}g = f_{1}g, where g = 2^{f_{0}} \overline{f}_{1} = 2^{f_{1}} \overline{f}_{0}, if symmetry and transitivity hold. Let r ∈ R. Then the desired relation rf_{0}g = rf_{1}g holds iff

∀a′ ∈ A [a′ϵ_{∼}rf_{0}g ⇔ a′ϵ_{∼}rf_{1}g]

So let a′ ∈ A. Then what we must show is that

∃\overline{r} ∈ R [\overline{r}f_{0} = a′ & \overline{r}f_{1} = rf_{0}] ⇔ ∃\overline{\overline{r}} ∈ R [\overline{\overline{r}}f_{0} = a′ & \overline{\overline{r}}f_{1} = rf_{1}]

That the left hand side implies the right hand side follows immediately from transitivity (a′ ≡ rf_{0} & rf_{0} ≡ rf_{1} ⇒ a′ ≡ rf_{1}, where ≡ is defined as the image of f) and the converse follows in the same way after first applying symmetry. Thus f_{0}g = f_{1}g and so there is a unique induced map

\xymatrix{ &  & Q \ar@{-->}[dd] \\ R \ar[r]^{f_{0}} \ar[r]_{f_{1}} & A \ar[ur]^{q} \ar[dr]_{g} \\  &  & 2^{A}}

The third claim made above was that under the additional hypothesis of reflexivity, q is actually the co-image of g. This is essentially just the assertion that a_{0}g = a_{1}g ⇒ a_{0}q = a_{1}q. But a_{0}g = a_{1}g means just that

∀a′ ∈ A [a′ ≡ a_{0} ⇔ a′ ≡ a_{1}]

(where the relation ≡ is just the image of f as above). By reflexivity there is at least one a′ such that a′ ≡ a_{0} (namely a_{0} itself) and by symmetry a_{0} ≡ a′; but since a_{0}g = a_{1}g, it also follows from a′ ≡ a_{0} that a′ ≡ a_{1}, so by transitivity a_{0} ≡ a_{1}. This means ∃r ∈ R [rf_{0} = a_{0} & rf_{1} = a_{1}], and thus a_{0}q = rf_{0}q = rf_{1}q = a_{1}q because f_{0}q = f_{1}q, q being the coequalizer of f_{0} with f_{1}.

Finally we can assert our theorem

a_{0}q = a_{1}g ⇔ a_{0} ≡ a_{1}

The implication a_{0} ≡ a_{1} ⇒ a_{0}q = a_{1}q is trivial (and we just used it), while the converse was proved in the preceding paragraph.

Remark 6: It follows easily now that for an arbitrary pair of mappings

\xymatrix{R \ar[r]^{f_{0}} \ar[r]_{f_{1}} & A}

the equalizer f̃ of p_{0}q with p_{1}q, where q is the coequalizer, is the smallest RST subset of A × A containing the image of f, and that the coequalizer of f̃ is the same as the coequalizer of f. Thus an “internal” construction of an arbitrary coequalizer will be obtained if one knows a way to construct the RST hull of an arbitrary relation. The construction below involves the natural numbers (see Remark 8 in connection with our metatheorem below). Since the symmetric hull is easy to construct we may assume that f is symmetric and reflexive. The reader may verify that the following then describes a construction of the RST hull f̃.

Let 𝒮_{f} →R^{N} be the subset whose members are just the sequences N →^{r} R such that srf_{0} = rf_{1}, s being the successor mapping (that is, form the equalizer of f_{0}^{s} with f_{1}^{N}). Then define f̃ to be the image of the following composite mapping N × N × 𝒮_{f}→A × A:

\xymatrix{N × N × 𝒮_{f} \ar[r]^{diag} \ar[dd]_{epi} & (N × 𝒮_{f}) × (N × 𝒮_{f}) \ar[r] & (N × R^{N}) × (N × R^{N}) \ar[d]|{(N×f_{0}^{N})×(N×f_{1})^{N}} \\  &  & (N × A^{N}) × (N × A^{N}) \ar[d]|{e×e} \\ • \ar[rr]_{f̃} &  & A × A}

(Here e is the evaluation mapping for sequences N → A.) That f̃ is the RST hull of the reflexive and symmetric f then follows from the fact that ⟨a_{0}, a_{1}⟩ ∈ f̃ iff there exists a sequence r in R such that srf_{0} = rf_{1} and there exist n_{0}, n_{1} such that a_{0} = n_{0}x and a_{1} = n_{1}x where x = rf_{0}.

Remark 7: For the development of mathematics in our theory it is also convenient to make use of a “Restricted Separation Schema” the best form of which the author has not yet determined. This theorem schema is to the effect that given any formula involving sets and maps as well as a free variable x ∈ A, if the quantifiers in the formula are suitably restricted (say to maps between sets which result from certain numbers of applications of the operations of Axioms 1-3 to the given sets and maps), then a subset of A exists whose members are precisely the elements of A which satisfy the formula. (Note that A itself could be a product set B^{3} × C, etc.) The Restricted Separation Schema is equivalent to a schema which asserts that there exists a mapping having any given (suitably restricted) rule. This theorem schema is surely strong enough to guarantee the existence of all the constructions commonly encountered in analysis. Without using the theorem schema, one can of course derive particular constructions using equalizers, exponentiation, images, etc, and this can often be illuminating. For example, the ring of Cauchy sequences of rational numbers and the ideal of sequences converging to 0 can be constructed and calculus developed.

The reader should also be able now to construct proofs of Tarski’s fixed point theorem, the Cantor-Schroeder-Bernstein theorem, and Zorn’s lemma.

Finally, we wish to prove a metatheorem which clarifies the extent to which our theory characterizes S. Though our proof is informal it could easily be formalized within a sufficiently strong set theory of the traditional type or within a suitable theory of the category of categories. [For a preliminary description of the latter, see the author’s doctoral dissertation (Lawvere 1963b).]

Let ℂ be any category which satisfies the eight axioms of our theory. (To be more precise, we also assume that for each pair of objects C, C′ in ℂ, the class (C, C′) of maps C→C′ is “small”, i.e. is a “set”.) There is then a canonical functor

\xymatrix{ℂ \ar[r]^{H^{1}} & S}

which assigns to each object C in ℂ the (identity map of the) set (1, C) of all maps 1→C in ℂ.

The functor H^{1} is clearly left exact (i.e. preserves 1, products, and equalizers) and faithful (i.e. if C ⇉C′ are identified by H^{1} then they are equal). Our metatheorem states that under the additional (non-first-order) axiom of completeness, H^{1} is an equivalence of categories, i.e. there is a functor S→ℂ which, up to natural equivalence, is inverse to H^{1}. Thus our axioms serve to separate the structure of S from the structure of all other complete categories, such as those of topological spaces, vector spaces, partially ordered sets, groups, rings, lattices, etc.

Remark 8: For any model ℂ, H^{1} also preserves sums and coequalizers of RST pairs of maps. However it seems unlikely that it is necessary that H^{1} be right exact, since as remarked above, the construction of the RST hull involves N and by Gödel’s theorems the nature of the object N may vary from one model ℂ of any theory to another model. That is, H^{1} need not preserve N. Also H^{1} will be full at 1 in the sense that the induced mapping

\xymatrix{(1, A) \ar[r] & (1, AH^{1})}

must be surjective for each object A in ℂ. However, it is certainly not necessary that H^{1} be full, because there are countable models by the Skolem-Lowenheim theorem, yet (1, N) is always infinite; thus (N, N) can be countable but (NH^{1}, NH^{1}) must be uncountable, so that e.g. the induced map

\xymatrix{(N, N) \ar[r] & (NH^{1}, NH^{1})}

need not be surjective. Of course the countability of (N, N) = (1, N^{N}) could not be demonstrated by maps N→N^{N} in ℂ. For the same reason, H^{1} need not preserve exponentiation.

Actually, we will derive our result (that our axioms together with completeness characterize S) from the following more general metatheorem concerning the category of models for our theory. We will use some of the basic facts about adjoint functors.

Metatheorem. Let ℂ→^{T} ℂ′ be a functor such that:

1. Both ℂ and ℂ′ satisfy axioms 1-8.

2. Both ℂ and ℂ′ have the property that for each object A the lattice of subobjects of A is complete.

3. T has an adjoint Ť.

4. T is full at 1, i.e. for each object A in ℂ the induced mapping

\xymatrix{(1, A)_{ℂ} \ar[r] & (1T, AT)_{ℂ′}}

is surjective.

Then T is an equivalence of categories, i.e. TŤ and ŤT are naturally equivalent to the identity functors of ℂ and ℂ′, respectively.

Remark 9: Completeness of the lattice of subobjects of A in ℂ means that every family A_{α} →^{aα} A, α ∈ F of subobjects of A has an intersection D→A and a union V →A. Here every family is to be understood in an absolute sense, i.e., relative to the universe in which we are discussing model theory; neither F nor the mapping which takes α ⇝ a_{α} need be an object or map in ℂ. We can show of course (Theorems 4 & 5) that in any model ℂ, any family I →^{α} 2^{A} in ℂ has a uniquely determined union and intersection in ℂ. However, as with any first-order set theory, we cannot guarantee that, in a given model ℂ every absolute family of subsets of A is represented by a single mapping in ℂ with codomain 2^{A}. Note that, in particular, lattice-completeness of ℂ implies that to every (absolute) family of elements of A there is a subset of A with precisely those elements as members.

Note that we clearly need to assume that T is full at 1, since for any model ℂ and any object I in ℂ, A ⇝ A^{I} is a functor ℂ→ℂ which has an adjoint; but which is surely not an equivalence if, e.g., I is infinite.

Proof of Metatheorem. Since T has an adjoint it must preserve products and equalizers and in particular 1T = 1. Since T is full at 1, 0T can have no elements, and so 0T = 0 by Axiom 6.

We claim that T is faithful, i.e., that each induced mapping

\xymatrix{(A, B) \ar[r] & (AT, BT)}

is injective. Suppose A ⇉ \begin{matrix}f \\ g \end{matrix} B are such that fT = gT and consider 1 →^{x} A. We must show xf = xg, so consider the equalizer E →1 of xf with xg. We must have E = 1 or E = 0. If E = 0, then ET = 0 is the equalizer of (xf)T with (xg)T which implies (xT)(fT) ≠ (xT)(gT), a contradiction. Hence E = 1 which implies xf = xg and so f = g. Thus T is faithful.

Also, T must preserve sums, because for each A and B in ℂ, the canonical map

\xymatrix{AT + BT \ar[r] & (A + B)T}

is surjective by Axiom 7 and the fact that T is full at 1, and is injective by Axiom 7 and the fact that any functor whose domain satisfies our axiom of choice must preserve monomorphisms.

Now the lattice-completeness of ℂ and ℂ′ together with the fact that T is full at 1 implies that every subset of AT is the value of T at some subset of A, for any object A in ℂ. For

\xymatrix{(1, 2^{A}) \ar[r] & (1, 2^{AT})}

is a homomorphism of complete atomic Boolean algebras which induces an isomorphism

\xymatrix{(1, A) \ar[r]^{≈} & (1, AT)}

on the respective sets of atoms, and hence must be itself an isomorphism. But this implies that T must be full, since arbitrary maps are determined by their graphs, which are subsets.

In general, if a functor T is full and faithful and has an adjoint Ť, then for each A, the canonical map ATŤ→A is an isomorphism. Hence this must hold in our case.

To complete the proof of the metatheorem we need only show that for each I in ℂ′, the canonical map

\xymatrix{I \ar[r]^{φ_{I}} & IŤT}

is injective, for it follows then by the previous remark that φ_{I}, being a subset of a value of T, must actually have its domain I isomorphic to a value of T, which immediately implies that φ_{I} is an isomorphism.

Because ATŤ ≅ A, T is full and hence 1T = 1. Also, Ť, being an adjoint functor, must preserve sums. Since we have already seen that T preserves 1 and sums, it follows that the particular canonical map

\xymatrix{2 \ar[r]^{φ_{2}} & 2ŤT}

is an isomorphism. This, together with the fact that 2 is a cogenerator for ℂ′ (Proposition 1), will imply that every φ_{I} is injective.

For suppose 1⇉ \begin{matrix}x \\ y \end{matrix} I are different. Then there is I →^{t} 2 such that xt ≠ yt. In the commutative diagram

\xymatrix{1 \ar[dr]^{x} \ar[dr]_{y} \\  & I \ar[r]^{φ_{I}} \ar[d]_{t} & IŤT \ar[d]^{tŤT} \\  & 2 \ar[r]_{φ_{2}} & 2ŤT}

φ_{2} is an isomorphism and hence tŤT must separate xφ_{I} from yφ_{I}.

Metacorollary. If ℂ is a complete category which satisfies our axioms then the canonical functor

\xymatrix{ℂ \ar[r]^{H^{1}} & S}

is an equivalence.

Proof. Completeness means that the categorical sum and product of any family of objects exists. However, this can easily be shown to imply lattice completeness. If we define

\xymatrix{S \ar[r]^{Ť} & ℂ}

so that for each I ∈ S, IŤ is the I-fold repeated sum of 1 with itself, then Ť is adjoint to T = H^{1}. By definition of H^{1} = T, it is full at 1.

Remark 10: To give some indication of the extent to which a model of our axioms may fail to be complete, note that the set of all mappings between sets of rank less than ω + ω is a model.

Remark 11: Even countable repeated sums of an object with itself may fail to exist, for the equation

(∑_{N} A, X) ≅ (A, X)^{N}

shows that any non-trivial category in which such sums exist must be uncountable, whereas any first-order theory has countable models. Of course, if such sums do exist in a model for our theory, then

∑_{N} A ≅ N × A

and the latter operation can always be performed.

Remark 12: Of course, it is important to investigate first-order strengthenings of our axiom system in the direction of completeness, although cardinals larger than ℵ_{ω} are usually not needed, e.g., for the development of analysis. The existence of this and many more cardinals would be guaranteed, and hence the model of Remark 10 excluded, if we take the following as an axiom schema

∀A∀B∀B′ [ φ(A, B) & φ(A, B′) ⇒ B ≅ B′ ]

⇓

∀X∃Y [ X < Y & ∀A∀B [ A < Y & φ(A, B) ⇒ B < Y]]

where φ is any formula and X < Y refers to cardinality.

However, it is the author’s feeling that when one wishes to go substantially beyond what can be done in the theory presented here, a much more satisfactory foundation for practical purposes will be provided by a theory of the category of categories.

References.

Eilenberg, Samuel and Saunders Mac Lane (1945), ‘General Theory of Natural Equivalences’, Transactions of the American Mathematical Society 58, 231–94.

Lawvere, F. William (1963a), ‘Functorial Semantics of Algebraic Theories’, Proceedings of the National Academy of Sciences of the U.S.A. 50, 869–872.

Lawvere, F. William (1963b), Functorial Semantics of Algebraic Theories, PhD thesis, Columbia University. Republished in: Reprints in Theory and Applications of Categories, No. 5 (2004) pp 1-121, available on-line at http://tac.mta.ca/tac/reprints/articles/5/tr5abs.html.

This article may be accessed from http://www.tac.mta.ca/tac/reprints or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/tac/reprints/articles/11/tr11.{dvi,ps}

REPRINTS IN THEORY AND APPLICATIONS OF CATEGORIES will disseminate articles from the body of important literature in Category Theory and closely related subjects which have never been published in journal form, or which have been published in journals whose narrow circulation makes access very difficult. Publication in ‘Reprints in Theory and Applications of Categories’ will permit free and full dissemination of such documents over the Internet. Articles appearing have been critically reviewed by the Editorial Board of Theory and Applications of Categories. Only articles of lasting significance are considered for publication. Distribution is via the Internet tools WWW/ftp.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor.

Selection of reprints. After obtaining written permission from any copyright holder, any three TAC Editors may propose a work for TAC Reprints to the Managing Editor. The proposal will be reported to all Editors. The Managing Editor may either accept the proposal or require that the Editors vote on it. Before such a vote, the author, title and original publication data will be circulated to Editors. If a 2/3 majority of those TAC Editors responding within one month agrees, the work will be accepted for TAC Reprints. After a work is accepted, the author or proposer must provide to TAC either a usable TeX source or a PDF document acceptable to the Managing Editor that reproduces a typeset version. Up to five pages of corrections, commentary and forward pointers may be appended by the author. When submitting commentary, authors should read and follow the Format for submission of Theory and Applications of Categories at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@mathstat.uottawa.ca

Lawrence Breen, Paris 13: breen@math.univ-paris13.fr

Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com

Ezra Getzler, Northwestern University: getzler(at)math(dot)northwestern(dot)edu

Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca