Linear Logic complements Classical Logic
Vaughan Pratt∗
Dept. of Computer Science
Stanford University
Stanford, CA 94305-2140
pratt@cs.stanford.edu
January 9, 2005

Abstract
Classical logic enforces the separation of individuals and predicates,
linear logic draws them together via interaction; these are not right-orwrong alternatives but dual or complementary logics. Linear logic is an
incomplete realization of this duality. While its completion is not essential for the development and maintenance of logic, it is crucial for its
application. We outline the “four-square” program for completing theconnection, whose corners are set, function, number, and arithmetic, anddefine ordinal Set, a bicomplete equational topos, meaning its canonicalisomorphisms are identities, including associativity of product.

1

A Postcard from the Edge
∗ This work was supported by ONR under grant number N00014-92-J-1974

1

Hi, boss. Just took over source’s shift. Did
you hear about the line and the dot? What
does she see in him? He’s an impractical bore,
goes on forever. I know when to start and stop.
I’m on the day shift these days, boss, my two
vertices do the night shift. When they’re sleeping they look real small, but when they’re on
the job and I’m asleep it’s the other way round,they’re the long ones. Some call it duality, I
call it common sense. No one does their best
working round the clock.
Yawn, target’s turn. Remember me, boss.
Please? Your faithful • •Boss3210 Go Street
Stop Junction

Edges and vertices is a right-sized math metaphor for the stop-and-go of life.
Why be just an edge when you could be a whole line?1 Because breaks makelife interesting. They give maintenance a turn, which is good. And they give
your opponent a turn, which is bad but that’s the breaks in an interesting life.
Category theory and set theory don’t get on too well, but what can you
expect when an irresistible force meets an immovable object? Common sense
suggests that they make up. The trick is for each to recognize the virtues of theother, and not try to do everything on their own.
In life’s stop-and-go traffic, sets are the brakes and categories the accelerator.
You can’t get smooth motion out of just sets, that’s what the edges of a category
give you: postulated smooth motion that permits breaks but does not requirethem. Sets can’t offer this, any smooth motion created purely out of sets musthave breaks everywhere. So dense are Set’s breaks in smooth motion that one
cannot even make sense of them, or so the undecidability in ZF of the continuum
hypothesis seems to be telling us.
But surely you can stop in a category, namely at an object? Yes, but that’s
because ob(C) is a set (not necessarily a small one). This is inevitable: we don’tknow how to broaden our world view by moving away from the set conceptionof ob(C), and it seems very plausible to me that there is no such way. All weknow is how to narrow our view, for example by weakening the cartesian closed
category Set as the target of our external homfunctor to the closed category
Ab of abelian groups. You can define an abelian group in Set, but you can’t
define a set in Ab.
This paper outlines preliminary ideas for a program of mathematical fitness.
The two essential ingredients are dual interaction and the category Set.
Dual interaction has the form of an edge in a graph. The source and target
are the duals, the edge is the interaction. At that level of abstraction duality
1 http://forum.swarthmore.edu/pow/solu3.html

2and interaction are themselves duals, as witnessed by the interchange of vertices and edges when dualizing a linear order [Pra92]. Furthermore duality andinteraction interact fruitfully as witnessed for concurrency theory by [GP93]
and mathematics by [Pra95], both applications of the Chu construction, themathematical quintessence of dual interaction. Dual interaction rests on itself.
The category Set is where categories and sets must get along. We shall givea new axiomatization of Set that stresses duality and simplicity throughout.
The objects of Set are the ordinals, the morphisms are functions between theunderlying sets of the ordinals.
There are three identifiable levels of duality in this version of Set. Level 0
contains just (whimsically named) position and momentum. Level 1 has twodualities, the two values stop and go of momentum, and the two values vertex
and edge (or city and highway) of position. Level 2 has four dualities, being
the four edges of a square whose corners in order are number, set, function, andarithmetic. These seven dualities may be laid out as follows.

Position•••

Momentum
Stop
Go
NumberSet
Arithmetic

Function

There is one further duality that did not seem to fit in here, inside andoutside. On the outside, numbers are stopped, sets are on the go. But theinside of a number, as an ordinal, seems all rigged up for travel, whereas a set isdiscrete inside, no highways at all. This is typical of duality: the elements of any
collection (at least those constructed implicitly or explicitly by the contravariant
power set functor) behave dually to the collection itself.
Without going into details, let us just point out that the duality of number
and set is put to a variety of uses. A good example is the following.
From a set-theoretic perspective, one simplification achieved by this implementation of Set is in the computation of the membership relation ∈ on theobjects of Set, specifying for all pairs A, B of objects whether or not A ∈ B.
Goldblatt [Gol83, 12.4] gives Osius’ method of computing membership from theepsilon trees of Set, concisely explained in six pages. In our Set the computation reduces to the equation ∈ = <. The epsilon trees of this Set makemembership and ordinal comparison one and the same relation on the objects.
It might appear that we have thrown the baby out with the bathwater:
membership couldn’t possibly be that simple. But in fact our Set is equivalent,in the categorical sense, to all other categories claiming to be Set, and there
is no evident reason for preferring the versions of Set requiring six pages ofcomputation to our version. In fact quite the opposite, there are good reasonsfor preferring ours, for example the following.
3

From a category perspective, one prominent simplification is to the natural
isomorphisms associated with the cartesian closed structure, such as associativity of product. In our Set these are identities. This has three advantages. First,
we can do true equational logic, writing A × (B × C) = (A × B) × C instead ofclumsy A × (B × C) ∼= (A × B) × C, without dishonestly misrepresenting thesituation as some do. Second, no additional information need be supplied as towhich isomorphisms are intended. Third, there are no awkward coherence conditions that need be checked, since identities compose to identities, immediately
guaranteeing that “all diagrams commute.”

2

Dual Interaction

The essence of classical first order logic is duality, that of linear logic, interaction.
The interaction should be an edge connecting the two vertices of the duality,
but the interaction of linear logic does not stretch quite far enough on eitherside to reach the duality of classical logic.
The duality of classical logic is the simple categorical duality of opposites:
Set and Setop . Duality acts to classify the entities of the language into individuals and predicates, holding them at a respectful distance. Setop is well-known
to be equivalent to the category CABA of complete atomic Boolean algebras,
the essence of propositional or zeroth order logic (though one can quibble about
where to put the infinite propositions). The objects of Set supply first orderlogic with its universes; here there is no analogous quibble, a first-order universeis exactly a set.
Whereas duality in classical logic serves to separate the two kinds of entity
into two classes, interaction in linear logic (LL) draws them together by permitting them to interact. Its two fundamental operations are perp, A⊥ , and tensor:
binary tensor A ⊗ B and zeroary tensor or unit 1.
Perp acknowledges the connectedness of duality by permitting travel froman object A to its dual A⊥ . This contradicts classical logic’s philosophy ofmaintaining the distinction about as completely as one could imagine!
But perp gives only a quantum tunnelling kind of connectedness. Applying
it again just takes you back to where you started, A⊥⊥ = A, giving no hintof whether there is an “in between” over which perp jumped. Tensor gives amore creative form of connection by producing an object A ⊗ B blending boththe separate concepts of A and B and their knowledge about those concepts,
in a way that not only preserves knowledge but draws all possible inferencesfrom it relevant to the pooled set of concepts. This is achieved for the concepts
by forming the product space of concept pairs, and for the knowledge by thefamiliar process of logical deduction.
A simple example of tensor product is given by the product of two 2-chains{a < b}, {a0 < b0 } in Pos, a square. The “concepts” are the two vertices in4each poset, which multiply to form four vertices. The four sides of the square
are deduced by holding a vertex of one poset fixed while varying the other, theuniversally understood way of observing one half of an interacting pair with theminimum of interference from the other. (Pos being cartesian closed, that is,
its tensor being ordinary categorical product, this method guarantees no interference from the stationary object, but this fails when e.g. there are constants
and the stationary point is one of them. But this is just “bleeding over” ofextra information from the supposedly stationary argument, not destruction ofknowledge about the argument being observed; we can overlearn that way but
not underlearn.)
But now consider the diagonal, from (a, a0 ) to (b, b0 ). Here we are varying
both objects. Going around either side of the square lets us deduce by transitivity that (a, a0 ) < (b, b0 ). This deduction was made by the tensor product, which
is a very simple yet remarkably effective deduction engine!
The blending process tends to average the knowledge-to-concept balance of
its operands, which can range from coherent (knowing a lot about a little) todiscrete (knowing little about a lot), see [Pra95] for more detailed numericalaspects of this measure. Perp negates this balance; thus if A is off-center (theorigin) in one direction, A⊥ will be just as off-balance in the other. A ⊗ A⊥
then produces a larger but more balanced object.
Depending on “which way round” one looks at the arguments and the result,..........
interaction might also appear as par A ................ B, the De Morgan dual (A⊥ ⊗ B ⊥ )⊥ of..........
tensor, or as the internal homfunctor or linear implication, A−◦B = A⊥ ................ B =(A ⊗ B⊥ )⊥ .
The asymmetry of linear implication gives it the character of an experimenter
B observing a subject A. We may interpret B−◦C as C enlightened by observing
B, and A−◦(B−◦C) as C’s further enlightenment by A. Thus if specialist A
informs C that Socrates is a man while generalist B declares all men to bemortal, C can in principle draw the famous conclusion. Commutative linear logic
presumes C to be capable of factoring out all dependencies on the order in which
the information is presented, which it asserts with the identity B−◦(A−◦C) =A−◦(B−◦C).
But this viewpoint suggests that it might be more natural to view C as
observing A and B in combination, in a form which allows C to see both at thesame time, each seen as clearly as in A−◦C and B−◦C, with C able to combine
information from both. This is what tensor accomplishes, via A−◦(B−◦C) =(A ⊗ B)−◦C. This identity shifts the responsibility for doing logic from C totensor: on the left C must make the inference herself, on the right she needmerely look it up in A ⊗ B, which has precomputed the inference. A ⊗ B is the
canonical observer of its constituents, as expressed by the unit A−◦(B−◦A ⊗ B)of the adjunction making B−◦− right adjoint to − ⊗ B. This is a theorem ofHilbert-style LL.
The counterpart theorem to the unit is the counit A ⊗ (A−◦B)−◦B, the5evaluation map telling us how to apply a “function” f : A → B to an argumentx ∈ A to yield f (x) ∈ B. This looks very interesting. But when we move it
around a little using just the simple rules we’ve already presented, evaluation
reduces to the triviality A ⊗ B ⊥ −◦A ⊗ B⊥ . Running this derivation backwards,
we conclude that the rules themselves must somehow incorporate the meaningof evaluation, since the triviality surely cannot. This is very surprising given
the simplicity of these rules, which do not appear on the surface to embed theessence of evaluation.
The interactive nature of tensor should be contrasted with linear logic’s sum,A ⊕ B, their noninteracting parallel play. Its observation by C, (A ⊕ B)−◦C, isequivalent to (A−◦C)&(B−◦C), the separate observation of A by C with theseparate observation of B by C, which we can restate in terms of plus itself as((A−◦C)⊥ ⊕ (B−◦C)⊥ )⊥ by dualizing everything. With is simply the De Morgan
dual of plus with respect to ⊥ , like tensor and par.
This much of linear logic has no specific orientation relative to classical logic;“concept” and “knowledge” could be interchanged without compromising anyof the language and associated logic seen so far.
A first step towards connecting linear logic to classical logic is made withtwo dual unary operations, !A and ?A. These act as projections, projecting the
LL universe in the general direction respectively of the Set and Setop worldsof classical logic.
They may be represented graphically as terminating the interaction “at eachend” by equipping it with vertices. This gives the vague notion of “in between” created by tensor a specific direction as well as a tension (“making tensor
tenser”) that stretches out the LL universe towards the poles defined by classical logic. This tension is a weak reflection of classical logic’s rigid separation ofindividuals and predicates.
What LL does not do however is to move the endpoints out as far as thepoles themselves.
Now if you saw an amorphous blob start to orient itself parallel to the line
between two points, and to stretch itself out along the line towards them, what
would you predict would or should happen? If it gets near the poles but stops,
is this ok?
If it turned out there were other equally good poles at the place the blob
stopped, this would make sense. If it turned out that the blob would break if
stretched that far, or if contact with the poles would injure the blob, stopping
early also makes sense.
But if there are no better poles to aim for, and stretching out all the way
only improves the blob’s constitution, I’d recommend that it go for it, wouldn’tyou? This is what I shall try to argue here for the LL blob reaching out for theclassical poles: go all the way, tie yourself to the poles.
As an object of study LL may well be better off detached from everything
6and free to wave around or be waved around by its investigators. But whether
to tie anything down in a lab is very simple. What you stand on or put books
on should be tied down, what you need to pick up and wave around to study
better should not.
My personal interest in LL is not at all as an object of study but as aframework. The more tightly secured it is, the less effort need be invested onincestuous study of the lab’s foundations and the more time one has to get somereal work done. The study of foundations is not real work for most of us, it ismerely construction and maintenance incidental to real work.
For specialists in foundations it is of course a legitimate object of study andbeing a fulltime maintenance worker is a perfectly respectable occupation. But
maintenance is best done in downtime, which users want minimized. During
uptime, linear logic needs to be properly secured.
The problem of putting LL to work then becomes, where should the endpoints
of interaction be secured?
Given that LL axiomatizes !A as projection onto a cartesian closed category, there are a few canonical choices that come to mind: Set, more generally
presheaves SetC (e.g. RGrph, reflexive graphs), more generally still toposes,
and then beyond toposes, Pos (posets) or Cat (categories).
I favor Set for four reasons: audience, simplicity, generality, and number.
Audience. More people understand sets than any of the alternatives. This
could be for any of the remaining reasons, all of which strongly recommend Set
as a useful and usable category.
Simplicity. Mac Lane and Moerdijk’s “First introduction to topos theory”[MM92] is over 600 pages. Halmos’ “Naive Set Theory,” as an essentially complete first introduction to set theory, is in contrast a mere 100 pages.
Generality. Set appears to reach as far to the “left” or discrete end of
the Stone Gamut as any topos, thereby equipping LL with the largest possible
universe [Pra95].
One might suppose that these arguments would apply a fortiori to the moregeneral category Pos, or the yet more general one of Cat. However it is atheorem that enlarging Set to Pos2 Chu(−, −) dual adds nothing to what is
obtained when the Chu construction is used to extend Set out to Setop to create
the Stone Gamut. Furthermore Set confers the additional benefits of a topos,
unlike either Pos or Cat, which though cartesian closed are not toposes.
Number. Our lives are founded on reading, writing, and arithmetic (andother things but those are less painful to learn). No viable replacement forarithmetic has been proposed for commerce in millennia, and none is on thevisible horizon either.
But if our lives are founded so fundamentally on numbers, and if mathe2 Conjecture: Further enlarging to Cat yields 2-Cat and so on up.

7matics is to continue as the important servant it has been to date, it would be
incredibly shortsighted of mathematics to move away from its present arithmetic
foundation when it has no replacement for it!
Although toposes offer a notion of number, namely an element of the natural
numbers object, Set can be understood in a way that make sets and numbers
the same thing. Instead of the set of numbers as an object and a number as
an element of an object, one can think of the set of numbers as just anothernumber, ω. Logicians split over this, some going for the separation created by
the topos viewpoint, others for the identification created by the set theoretic
viewpoint.
I favor identification for the same reason I favor tying down !A and ?A. For
objects of study, more degrees of freedom are better. For foundations and tools,
fewer. Identifying sets and numbers, and making the natural numbers object
just another number, creates a simple, powerful, very useful, and widely usedstructure, the ordinals.
We identify sets and numbers by defining a number to be an ordinal, understood as the set of ordinals less than it, and by having no other sets thanordinals. Hence there will be exactly one set of each finite cardinality, but
uncountably many countable sets.
This may seem draconian to say the least! How are we to understand thedifference between the evidently different sets {1} and {2}, for example?
Well, in the category of ordinals, there are two entities perfectly capableof representing these sets, namely the characteristic functions of these two setsfrom the (sufficiently large in this case) ordinal 3 = {0, 1, 2} to 2 = {0, 1}. This is
how Pascal represents sets. If one is expecting sets with larger natural numbers,
Pascal’s implementation is reluctant to take as the domain of the characteristic
function the natural numbers, but only the most applied mathematicians needhave such qualms.
To perform set operations on a pair of such sets, simply compose the appropriate Boolean gate: an OR-gate for union, AND for intersection, etc., with thepair of functions.
If one needs sets with more complex structure, such as the set of all realω
valued functions, one passes to larger ordinals still, in this case 22 , and forms anappropriate subset of it, as a particular function, along with whatever operations
are required.
There really is no generality of representability lost by working in a categoryof sets consisting of just the ordinals, and all functions between their underlyingsets.
One last remark: Set only contains sets. It contains the set of reals forexample. However it does not contain the field of reals. For one thing thefield of reals does not transform as a set, but as a field. Set does not caterfor this notion. Standardly one implements algebraic structure with relational8

structure, sets of tuples over the carrier, and topological structure as sets ofopen sets. The Chu construction and its applications, not treated here but
which may be found elsewhere [Bar79, LS91, Pra93], is, we have argued [Pra95],
a workable universal framework for much if not most of concrete mathematics.
This is the machinery that should be used in conjunction with this Set to create“the rest of mathematics,” as the chain of categories Chu(Set, K) where K is
an arbitrary set, an ordinal in our version of Set.
Thus far I have only claimed that giving up global membership is not a
great sacrifice. I will now consider the other side and argue the benefits of aparticular extreme approach to local membership, the identification of number
and set. I have already mentioned the benefit of fewer degrees of freedom. I
will now describe how rich and beautiful such a world can be.

3

Two Kinds of Negative Number

There are not one but two kinds of negative number. One gets up and creates,
the other sits back and annihilates. These represent respectively dynamic andstatic ways of extrapolating backwards from the two natural but orthogonal
directions of the natural numbers.
The annihilating kind are the usual negative integers, which annihilate byinteraction with the positive integers according to the familiar law x+(−x) = 0,
yielding zero, whose dynamic interpretation is the empty set.
The creating kind are the objects of Setop , which create by interaction withthe positive integers via the Chu construction [Bar79] to create the Stone gamut[Pra95]. Although Setop is perhaps most familiar as the concrete category
CABA of complete atomic Boolean algebras, in this context CABA’s are as wellor better understood as sets that transform by antifunctions defined as binary
relations whose converse is a function.
When Kronecker shared the attribution for the integers between God andus, he did so for the annihilating kind. Had Ramanujan known of the creating
kind, one could imagine his rebutting Kronecker by instead apportioning thenatural numbers to Vishnu the preserver, the annihilating negatives to Shiva
the destroyer, and the creating negatives to the western God of creation.
The two systems arise because numbers, being practical, lead a stop-and-go
life. Edges are more practical than lines and dots. Numbers are harder to see
when they’re on the go, which is why we first notice them when they’re at rest.
At rest, numbers become rigid, both individually and as a group. We callrigid numbers ordinals, small by default, and their totality a large ordinal or wellordered proper class, one for which every nonempty subclass has a least member.
Rigidity of the whole lets us identify every number according to its position in
the whole, independently of any question of cardinality such as finiteness.

9With numbers at rest so neatly lined up, it takes little imagination to extrapolate their order backwards to create the negative integers.
On the go, numbers lose their rigidity and become flexible sets. The totalityof sets forms a large category Set, a proper class, whose morphisms the functions
are the possible trajectories of the objects of Set. Functions are the hallmark
of complete flexibility, permitting every element of a set to go where it will
independently of every other. Note the future tense: functions look forward.
With numbers on the go, it takes little imagination to extrapolate theirmotion backwards to create the creatively negative integers, which I will call theantisets to avoid confusing them with the standard negative integers, forming thecategory Setop . Where the imagination was needed was to see that numbers canmove at all. This idea does take some getting used to, but although unfamiliar it
is not at all deep mathematically, and with some practice you can get perfectly
comfortable with it.
I have already written about the Stone gamut [Pra95], to which the reader
should refer. My thesis, supported by several theorems in that paper, is that theStone gamut as the dual interaction of sets and antisets creates the better partof concrete mathematics, while at the same time revealing more of its common
structure than is apparent from the relational structure viewpoint. For theinteraction, the logic of that common structure is linear logic, and its algebra iscategory theory. For the duality at the endpoints of the interaction, the logic isclassical logic, and its algebra is set theory.

4

Stop-and-go Numbers

To summarize, we want a homogeneous universe to keep our foundations as
simple as possible. We shall achieve this by identifying the notions of set andnumber, relying heavily on ordinal arithmetic. Our number-sets must be rigid
at rest, cold so to speak, but maximally flexible on the go, warmed up. These
two objectives are combined very simply in the one model by taking numbers
at rest to be ordinals, but transforming as though they were sets by taking asmorphisms all functions, not just those respecting the order. This is not justa gimmick, it has profound mathematical implications, including the alreadymentioned trivial solution to the awkward coherence problem.
The class of sets has traditionally been defined by the axiom system of
Zermelo and Fränkel with Choice, ZFC. (There is no practical advantage tomerely dropping Choice, and the consequences of replacing it with an alternative
are confined to the stratosphere of set theory.)
ZFC proceeds by first laying the ground rules for the behavior of sets, andthen priming the universe with a transitive well-ordered set, to be interpreted
as a set of ordinals. The rules then unroll the rest of the universe, including therest of the ordinal hierarchy, itself a large ordinal. (A large ordinal is a transitive10

proper class every nonempty subclass of which has a least element. A class istransitive when every member is also a (necessarily improper) subclass.)
Without attempting to be self-contained, I will give a complete description(up to the randomness introduced by Choice) of the bicomplete topos Set defined as having for its objects just the ordinals. “Bicomplete topos” is jargon fora category with certain additional structure. Rather than say in advance whatthat structure needs to be, I will simply describe all of that structure in thecase of Set and then label the parts afterwards. It will be a lot more concretethat way, and also most of the parts will be very familiar, except perhaps forthe coequalizers, the part of Set people tend to exercise least even though it is
all there, probably because its operation is the most obscure.
Our dual view of objects as numbers when at rest and sets when on the go
is reflected in our organization of Set.
At rest, objects are understood as ordinals, and their algebra is that ofordinal arithmetic, extended a useful amount, if not all the way, to infinite ordinals. Ordinal arithmetic is characteristically different from cardinal arithmetic;
Birkhoff [Bir42] makes the distinction clear with a beautiful unification of both
systems as one domain of posets with two copies of the arithmetic operations,cardinal and ordinal.
Our system of arithmetic is much smaller than Birkhoff’s: our posets arelinear and well-founded, that is, well-ordered. Moreover order isomorphism isidentity: we admit just the one well-ordered set of each order type. And ouroperations are also more restrictive: we have only Birkhoff’s ordinal operations,
not the cardinal ones (though these can be defined from the ordinal ones, so
this is not a real limitation).
At least almost the same: one difference is that Birkhoff’s exponential preserves only linearity and not well-foundedness. Another is that we admit infinitary sums and products, stoically accepting that they are underdefined forthe sake of at least having the operations, complete with “Choice noise.” And
we upgrade the traditional concept of arithmetic with equalizers and coequalizers. This ensures that Set is bicomplete, without which we could not claim
equivalence to other versions of Set.
On the go, objects turn into sets, and their algebra becomes that of a category equipped with all limits and colimits, as well as cartesian closed structure,
and also topos structure, including the ability to perform induction over thenatural numbers.
Yet these are not separate structures, but merely different views of the samething, in a way that will become apparent.

11

5

Set via ordinals

We take Set to be the ordinals together with all functions between their underlying sets. There is an evident binary relation of membership well-ordering
the objects, and wherever i ≤ j, Set(i, j) contains the inclusion function as a
distinguished morphism, generalizing the identity functions in Set(i, i).
We remind the reader of three operations on ordinals, monus i − j, quotient
i/j, and remainder i%j (borrowing the C programming language notation),defined as follows.
i − j < k iff i < j + ki/j < k iff i < j · k
i%j = i − j · (i/j)
Exercises. (i) j · (i/j) ≤ i. (ii) i%j < j.
We now describe the arithmetic of Set, namely products, subobjects, sums,
equalizers, coequalizers, and exponentials.
Q
Product. Given an ordinal i, the i-product pi = j<i nj of a family hnj i
of i ordinals is defined up to Choice by induction on i to be the least ordinalsatisfying the following.
The 0-product p0 is 1.
For all j < i, the j-product pj of the family hnm i, m < i is defined byrecursion along with, for all k ≤ j, an auxiliary projection fjk : pj → pk ,namely λn.n%pk . (So fjj is the identity.)
For successor ordinals i = k +1, the definition of pi is completed by requiringthat it have in addition a main projection gk : pk+1 → nk , namely λn.n/pk (amonotone function).
For limit ordinals, the definition of pi is completed, up to Choice, by requiring
it to be a categorical limit of the diagram whose objects are, for j < i, thej-products pj of hnm i, m < j, and whose maps are the recursively defined
auxiliary projections between those objects. The projections of this limit to
the recursively defined j-products pj are the auxiliary projections fij : pi → pj
defined at this level.
The counit of i-product at family hnj i, j < i, has for its j-th map, j < i,the composite gj ◦ fi,j+1 : pi → pj+1 → nj . These are the standard projectionsof ordinal product.
The unit of i-product at n (the diagonal dn : n → ni ) is the K combinator,
λm.(m, m, m, ...), sending m to the constant i-tuple of m’s.
i-Products act just like counters with i digits; this is lexicographic productadapted to infinite ordinals.
Compare the key ingredient λn.n%pk , a monotone function, of the explicit
definition of successor products to the underdetermined categorical definition12

of limit products. The latter defines ordinal product only “up to Choice,” Godplaying with dice.
That a limit of this (small) diagram exists is immediate by the completenessof Set. Once one such limit has been found in this version of Set, all ordinalsof the same cardinality become equally eligible, and the first paragraph of thedefinition then selects the least ordinal from among these. By definition this is a
cardinal, and so our definition makes all limit products cardinals, a nice feature.
But even though we know exactly which cardinal, the product is only defined
up to an automorphism. The well-ordering of that cardinal is thus completely
uncorrelated with the projections.
This definition is an underdetermined alternative to those of Birkhoff [Bir42]
and Hausdorff [Hau14], who gave fully specified notions of ordinal or lexicographic product. Birkhoff’s definition did not always produce ordinals, though
it did preserve linearity. Hausdorff’s definition did not even send ordinals to
linear orders. The above preserves ordinals, inevitably at the cost of nondeterminism at each limit ordinal.
Subobjects Given f : i → 2, the associated subobject is the least j such that
there exists a monotone injection g : j → i such that f g = d1e◦!j . Claim: sucha g : j → i exists and is unique, and is the pullback of d1e : 1 → 2 (the element
1 of set 2 = {0, 1} along f .
Sum. Given an
hnj ij<i of i ordinals, let s0 = {k <S ordinal i and a family
0nj | ∃j < i} (i.e.
P j<i nj ) and let f : s · i → 2 satisfy f (a, j) = a<nj . Define
the i-sum s = j<i nj to be the subobject of s0 · i associated to f .
The counit j : j · i → j of sum at j is λk.k%j. For the unit, define
gj : nj → s0 as gj (a) = (a, j). This factors through s ⊆ s0 as fj : nj → s. The
unit η at hnj i is then the family hfj ij<i .
Equalizers. The equalizer of f : i → j and g : i → j is the subobject ofi corresponding to the predicate “f (x) =i g(x)” (the subscript i denoting “oni”). Theorem: this exists and is unique.
Coequalizers. The coequalizer object k of f : i → j and g : i → j is thesubobject of j whose characteristic function p : j → 2 is the predicate “is theleast representative in its block.” The coequalizer h : j → k maps each elementof j to the least representative of its block. Theorem: h exists and is unique.
Exponentials. The exponential ij is defined as the product of j copies ofi (inheriting the infinite product problem when j is infinite). The unit of thedefining adjunction (−j right adjoint to j · −, not − · j) has for its morphisms
linear functions an + b where a is the sum of ((ji)k for 0 ≤ k < j and b is thesum of ki(ji)k for 0 ≤ k < j. The counit (evaluation map) i : j · (ij ) → i at i isthe function λn.((n/j)/in%j )%i. Evaluation first projects out the function partof n as n/j and the argument part as n%j, and then evaluates by “shifting”
and “masking” to pick out “digit” n%j in radix i. Claim: i is the evaluation
map.

13

Isbell’s argument at the end of [Mac71, VII.1] shows that we can’t always
make the natural isomorphisms λ, ρ, α identities, even in a cartesian closed category like Skel(Set). In the present context Isbell’s argument yields more, namelythat any construction we use to further reduce Set from the ordinals to a skeletal
category must weaken these identities to isos.
What saves the day for ordinals is that when x, y, z are countably infinite, x·yand (x · y) · z become different infinite ordinals. Isbell’s argument gives insight
into why set theorists find ordinals work better than cardinals: as cardinals,
countable x · y and (x · y) · z have to be the same countable cardinal, ordinals
create useful elbow room.
The above construction is unabashedly committed to Choice, assuming itfrom the outset. If Choice “is” false, the product of some family of ordinals is
likely to be a cardinal that cannot be well-ordered. It will therefore be missing
from this version of Set, putting at risk the completeness of Set.
Offsetting this is that the units and counits are specified in complete and concise detail, facilitated by the nonmonotone ordinal functions monus, quotient,and remainder. Furthermore associativity of binary sum and binary productare strict, an unusual feature that legitimizes writing = instead of ∼=. Moreoverthe construction is sufficiently specific as to make clear that the replacement of∼= by = in 1 + ω ∼= ω, i + j ∼= j + i, and i · j ∼= j · i is not merely bad form but
simply false. For the former the specified isomorphism, while an automorphismof ω, is of course not 1ω . And for the latter two equality is false even at theobject level, witness 1 + ω 6= ω + 1 and ω · 2 6= 2 · ω.

References[Bar79] M. Barr. ∗-Autonomous categories, volume 752 of Lecture Notes inMathematics. Springer-Verlag, 1979.
[Bir42] G. Birkhoff. Generalized arithmetic. Duke Mathematical Journal, 9(2),June 1942.
[Gol83] Robert Goldblatt. Topoi: The Categorial Analysis of Logic. Studies
in Logic and the Foundations of Mathematics Vol 98. North-Holland,
revised edition, 1983.
[GP93] V. Gupta and V.R. Pratt. Gates accept concurrent behavior. In Proc.
34th Ann. IEEE Symp. on Foundations of Comp. Sci., pages 62–71,
November 1993.
[Hal60] P.R. Halmos. Naive Set Theory. Van Nostrand, Princeton, N.J., 1960.
[Hau14] F. Hausdorff. Grundzüge der Mengenlehre. Leipzig, 1914.

14

[LS91]

Y. Lafont and T. Streicher. Games semantics for linear logic. In Proc.
6th Annual IEEE Symp. on Logic in Computer Science, pages 43–49,
Amsterdam, July 1991.

[Mac71] S. Mac Lane. Categories for the Working Mathematician. SpringerVerlag, 1971.
[MM92] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First
Introduction to Topos Theory. Springer-Verlag, 1992.
[Pra92] V.R. Pratt. The duality of time and information. In Proc. of CONCUR’92, volume 630 of Lecture Notes in Computer Science, pages 237–
253, Stonybrook, New York, August 1992. Springer-Verlag.
[Pra93] V.R. Pratt. The second calculus of binary relations. In Proceedingsof MFCS’93, volume 711 of Lecture Notes in Computer Science, pages
142–155, Gdańsk, Poland, 1993. Springer-Verlag.
[Pra95] V.R. Pratt. The Stone gamut: A coordinatization of mathematics. In
Logic in Computer Science, pages 444–454. IEEE Computer Society,
June 1995.

15