[FOM] Axiomatizing functions with finite domains

[Vaughan Pratt]

Harvey's discussion of axiomatizing finite arithmetic prompts the question
of how categorically (i.e. precisely) can one axiomatize finite sets, and
more generally, functions with finite domains but codomains of arbitrary
cardinality.  The following describes an elementary (i.e. first-order)
finite axiomatization of set theory having the interesting property that in
every model of the axioms, the functions f:X->Y are exactly those understood
naively, provided only that X is finite.  In particular if X is nonempty
and Y is uncountable, then the model is guaranteed to have uncountably many
functions from X to Y.  Moreover it will have exactly the correct ones if X
is finite, no matter how big Y is.  If X has n elements and Y has k elements
where k is any cardinal, then the model, *viewed externally*, will contain
exactly k^n functions from X to Y, seemingly counter to Löwenheim-Skolem.

This is quite different from topos theory, which does not aim to model
sets with this precision, and indeed has little in common with the present
theory other than that both are finitely axiomatized elementary theories,
and the categories FinSet of finite sets and Set of all sets are models
of both theories.  Almost any other interesting model of either theory
is unlikely to be a model of the other; in particular directed graphs,
with or without the requirement that they be finite, form a topos but not
a model of our axioms.

The individuals of the universe are sets and functions.  Our axioms are in
no way pathological, admitting for example Gödel's constructible universe L.
On the other hand they are surprisingly weak given what they accomplish.

There is no axiom of infinity, and indeed one model of the axioms, in
fact the smallest model, consists of one set of each finite cardinality.
This least model of the axioms is unique up to isomorphism, and contains
exactly the correct functions between all pairs of sets in the model.
(That is, every homset of FinSet is present and correct as understood
in naive set theory, having cardinality n^m where m,n are the respective
cardinalities of the domain and codomain.)

As an interesting corollary, the same axioms can be used to axiomatize
complete atomic Boolean algebras and their homomorphisms with the same
precision.  In this case however it is the homomorphisms f:A->B such that
Boolean algebra B is finite, in the sense of having only finitely many
(complete) ultrafilters, that are all present and correct.  Here A might
well have uncountably many ultrafilters in some model, but again the model is
guaranteed to produce the uncountably many homomorphisms from A to B that must
exist for such an A when B is any but the one-point Boolean algebra.  Since
completeness is not normally associated with first-order axiomatizations,
finite or otherwise, and uncountability would seem impossible to maintain in
this way because of Löwenheim-Skolem, this corollary might seem an impossible
goal for first-order logic.  It should therefore be surprising at first
that this ostensibly deep notion has an almost trivial axiomatization!

The Löwenheim-Skolem theorems show the impossibility of an elementary
categorical characterization of any abstract infinite universe.  Moreover
they show the impossibility of extending the above axiomatization of sets to
cater equally reliably for functions with infinite domains, since the model
would be obliged to contain uncountably many functions from X to 2 when X is
countable, by LS an impossibility for any elementary axiomatization of sets
and functions that admits arbitrarily large finite sets.  But if we accept
the inevitability of such LS monsters, and agree to ignore those regions
of the model encountering problematic cardinals in problematic places,
namely infinite sets as domains of functions, then we have a chance of
doing an end run around LS.  In this way we characterize the manageable
bits of our desired universe "on the nose", i.e. up to isomorphism, which
is as close as any abstract characterization can hope to come.

A case in point is the rationals structured not as a field but just as a
linear order.  The rationals are of course dense, and there is no least
or greatest rational, and these two elementary properties together with
the axioms for a linear order *and the externally imposed requirement that
the model be countable* exactly pin down the order type of the rationals.
That is, the notion of dense linear order with neither endpoint is
aleph-null-categorical.

The sort of categoricity we are shooting for here is not categoricity in
power of the whole model but rather of its individuals: instead of picking
out those models having a certain cardinality, we accept *every* model,
but pick out just those functions whose domains have a certain cardinality,
in this case finite.  Functions with infinite domains were sent to torment
logicians, and while no axiom of our system requires such functions to
misbehave, neither can we control them.

In particular we take no responsibility in our model for the correct
behavior of subsets of infinite sets defined in terms of their characteristic
functions.  (Unlike topos theory, whose axioms are designed to pair up the
subobjects of an object with its characteristic functions, the sets of our
theory have no other notion of subset than that of characteristic function.)
Subsets of finite sets so defined are however all present and correct.

We now list all but two of the axioms.  The individuals are of two sorts,
sets X,Y,... and functions f:X->Y.  The axioms simply say that the universe
is a category with initial and final objects and binary sums.

(i) The functions compose associatively where possible (f:X->Y and g:Y->Z
compose as gf:X->Z), and every set X has an identity function 1_X such that
for all f:X->Y, f 1_X = f = 1_Y f.

(That is, sets and their functions form the objects of a category; indeed
this is often the first example students encounter of a category.)

(ii) There is an empty (initial) set 0 and a singleton (final) set 1 such
that for every set X there is exactly one function from 0 to X and one from
X to 1.

(There is no restriction on how many singletons there may be; 1 is merely
the name of an arbitrarily chosen singleton.  An inadvertent side effect
of Axiom (v) will be to rule out multiple copies of 0.)

(iii) Sets X,Y sum to a set X+Y together with functions i:X->X+Y, j:X->X+Y
(the *inclusions*) in such a way that for any functions f:X->Z, g:Y->Z,
there exists exactly one function h:X+Y->Z such that hi=f, hj=g.

(This the coproduct condition; we shall prove below with the help of axiom
(iv) that this must be realized as juxtaposition or disjoint union of sets.
With the signature used in ZFC, X+Y is typically obtained as Xx{0} U Yx{1}.)

The axioms up to this point are extremely mild: in fact they are far from
being specific to sets and functions, holding of most kinds of objects of
mathematical interest, even those whose objects purportedly aren't built from
sets, such as locales (Isbell's famous 1972 "Atomless parts of space" paper).

We define an object X to be *connected* when every function f:X->Y+Z factors
through exactly one of Y or Z.  For topological spaces and continuous
functions, this defines the standard notion of connectedness: since Y+Z
creates no link between Y and Z, they are completely separated whence a
connected space cannot be continuously mapped to regions in both Y and Z.
We now bring in the penultimate axiom.

(iv) 1 is connected.

This is still extremely mild: how could a singleton fail to be connected?
In the category of topological spaces 1 is the one-point space, which
certainly is connected.  We only have one axiom left, with which we must rule
out not only topological spaces but many other kinds of objects for which 1
is connected, and at the same time exactly capture those functions that have
finite domains, in the process ruling out all trace of structure from sets
that might inhibit some function.  This must be a very powerful axiom indeed!

(v) Every set except 0 is of the form X+1.

This axiom does for sets a little of what Peano Arithmetic does for numbers.
It says that one can pick an element out of a nonempty set in such a way that
adding it back in reconstructs the set.  The adding-back part is where the
disconnectedness comes in: it says that we were able to pick out a point and
then demonstrate that this point was disconnected from the rest of the object.
(However this is more than one infers from the corresponding behavior of
the numerical successor operation in Peano Arithmetic.  This among other
things demonstrates the greater expressive of functions over mere inclusions.)

(The axiom also implies that there is only one empty set, since 0, like 1,
names a specific set.  A slightly different phrasing, e.g. "except initial
sets," would have avoided this implication, but what the heck.  Who on
this mailing list objects to limiting the number of copies of the empty
set to one?  No such proscription applies to 1: although the constant 1
certainly names a particular singleton, no axiom disallows isomorphic copies
of 1.  There could be just one singleton, or a bijection {}:S->O between the
class S of all sets and the subclass O of singleton sets that maps X to {X}
if needed for some application.)

But now one can start to see where finite sets enter the picture.  Any finite
set can be inductively picked apart element by element until it is empty,
showing the whole set to be disconnected.

And we know both by common-sense and Löwenheim-Skolem that picking infinite
sets apart element by element is a lost cause, not to be embarked on at
risk of losing your sanity.  This is the logician's torment, which we
sidestep by not worrying in this theory about whether infinite sets are
totally disconnected.

Now we have said dramatically little that is specific to sets here, really
only this last nit-picking axiom (1 being the nit).  Notably absent is any
sort of induction or other minimality principle, which turns out not to
be needed *in the axioms* for the main theorem.  We will need to reason
inductively about *models* of these axioms, but that reasoning is external.

Yet sets and functions have now been fully axiomatized to the promised
precision: every function f:X->Y from a finite set to an arbitrary set,
naively understood, must be present in the model, and no spurious ones.
Furthermore *all* functions in the model, regardless of the cardinality of
their domain, must compose in the usual manner of set-theoretic functions.
And, up to isomorphism, every finite set must be present; the axioms do not
rule out such infinite sets as N, Q, and R, but do not require them either.

We identify the functions x:1->X with the elements x of X, there being no
other candidate for the notion of element in this framework.  Application of
a function f:X->Y to an element x:1->X is defined by composition: f(x) =
fx:1->Y, an element of Y.

Proposition 1.  Functions compose standardly.

Proof.  Given an element x:1->X and functions f:X->Y, g:Y->Z, we must show
that (gf)(x) = g(f(x)).  Translating application to composition, this goal
becomes (gf)x = g(fx).  But this is simply associativity.  QED

Proposition 2.  The set X+Y is the disjoint union of the sets X and Y.

Proof.  By Axioms (iii) and (iv), every element z:1->X+Y of X+Y arises as
either an element z = ix where x:1->X is an element of X, or z = jy where
y:1->Y is an element of Y, but never both.  Furthermore every element of
X or Y is made an element of X+Y by composing the corresponding inclusion
i or j with that element.  This establishes the desired bijection between
the elements of X and Y taken separately and the elements of the single
set X+Y.  QED

Lemma 3.  0 has no elements.

(This is less trivial than it sounds, in fact it is false for any class of
algebras with a constant in its signature, e.g. groups or vector spaces,
where the initial algebra has one element.  On the other hand it does not
depend on Axiom (v), and so must hold for any model of (i)-(iv) including
topological spaces.  Groups and vector spaces satisfy (i)-(iii) but not (iv).)

Proof.  Let z:1->0 be an element of 0.  Then by Axiom (iii) there exist
maps iz:1->0+0 and jz:1->0+0 where i,j:0->0+0 are the two inclusions.
But by Axiom (ii), i = j, whence iz = jz.  Hence this map from 1 to 0+0
factors through both copies of 0 in 0+0, whereas Axiom (iv) requires that
it factor through only one of them.  Hence no such z is possible.

Theorem 4.  In any model of these axioms for which X is a finite set with n
elements, the functions from X to any set Y are precisely those understood
by naive set theory, namely the n-tuples over Y.

Proof:  We proceed by induction on n.

Basis case: 0.  By Lemma 3 this case caters for X = 0.  Axiom (v) forces
any set other than 0 to have at least one element, whence the empty set 0
is the only case catered for here.  Axiom (ii) promises a unique function
f:0->Y, which we may identify with the unique 0-tuple on Y.

Inductive step: n+1.  Suppose X has n+1 elements.  By Lemma 3, X cannot
be 0 and therefore by Axiom (v) must have the form Z+1.  If !:1->1 is the
unique function on 1 and j:1->Z+1 the second inclusion, j!:1->Z+1 must be
the element of X that factors through 1, whence by Axiom (iv) the remaining
n elements of X must factor through Z, showing that Z has n elements.

By the induction hypothesis, the functions t:Z->Y correspond to the n-tuples
over Y.  By Axiom (iii) the functions s:Z+1->Y are the pairs (t,y) where t is
an n-tuple over Y and y is an element of Y.  But this exactly captures all
and only the (n+1)-tuples over Y, which we may identify with the functions
from X to Y, with the particular elements of X in this role determined by
the respective inclusions from Z and 1 to X.  QED

Note.  We have not shown the result for all functions, only those with finite
domains, because induction is not an axiom of our universe.  Induction does
however hold externally (naively if you will) for those sets X with finitely
many elements.  If it did not, there would have to exist some set X of the
form 0+1+...+1, say with 17 elements, and a set Y, for which the theorem
was false.  We could then step our way manually through the cases Y^0, Y^1,
..., up to Y^17 checking each of them by hand to see where the model of
the axioms had gone astray, at which point we would have refuted not the
induction principle itself but merely the reasoning in an instance of the
inductive step for a specific n.  The only role being played by induction here
is to rule out the possibility of a counterexample to our understanding of
"function on a finite domain."  Finiteness and induction go hand in hand as
purely external considerations; neither enter into the axiomatization itself.

All this might seem like little if no improvement over ZF set theory.
But what if our task had been instead to axiomatize complete atomic Boolean
algebras with the same precision?  Löwenheim-Skolem is just as much a
problem there.  But if one simply dualizes the whole of the above, that
is, reverses all arrows, interchanges 0 and 1, replaces sum by product,
and views complete Boolean algebras as "consisting of" their (complete)
ultrafilters, one obtains an elementary axiomatization of complete atomic
Boolean algebras having the intriguing property that in every model,
the complete Boolean homomorphisms (those preserving arbitrary sups
and infs) f:B->C are exactly the right ones when C is a finite complete
atomic Boolean algebra.  Arriving at this result via the conventional set
theoretic definition of complete atomic Boolean algebra, based on the ZFC
axiomatization of sets and the conventional approach to defining complete
lattices and their homomorphisms, would be *way* more work, not to mention
likely to fall afoul of Löwenheim-Skolem at some point.

As a side remark, Axiom (v) can be slightly strengthened as follows.

(v)'  Given an element x:1->X, there exists a set Y such that Y+1 is the
set X with the associated inclusion j:1->X being x.

This removes the indeterminacy of which element is picked out of a nonzero
set by permitting the picked-out element to be specified in advance.  In this
way every element can be demonstrated to be disconnected from the rest of
the set.  This is a more satisfyingly global notion of disconnectedness.

However it does not establish completely arbitrary partionability of X as Y+Z
in all naively conceivable ways.  The following is a noble attempt at this.

(v)" Every predicate p:X->1+1 has the form !_Y + !_Z : Y+Z -> 1+1 where
!_Y:Y->1 and !_Z:Z->1 are the unique maps from Y,Z respectively to 1.

The meaning of this is that if you have a rule p for painting the elements
of X two different colors, then you can split X up as two color coordinated
sets Y+Z.  Here the full functoriality of + is being pressed into service.
+ adds not only sets but functions, the idea being that f:W->X and g:Y->Z
sum to f+g:W+Y->X+Z via the definition (f+g)(w) = f(w), (f+g)(y) = g(y)
for w,y in W,Y respectively.  (In this respect Axiom (iii) as stated above
is an incomplete characterization of the functor +, dealing only with
its object part.)

But however well-intentioned this attempt, it suffers from our inability to
pin down in the model exactly which f:X->1+1 exist for infinite X.  If the
model provides only countably many such f, as LS promises can happen when X
is countably infinite, then (v)" can only deliver countably many partitions
of X into two disjoint blocks when naively there should be uncountably many.

Open problem.  Do finite (in some appropriate sense) Abelian groups and their
group homomorphisms admit an analogous elementary on-the-nose axiomatization?
On the principles that toposes and abelian categories are essentially the
same notion modulo whether 0 and 1 are identified (false for toposes, true
for abelian categories), and that Set and Ab are the respective prototypical
members of these two classes, one would assume there would be a similar
axiomatization to the above.  I confess to having spent a number of hours
on this yes-no problem, so far without success.  A complicating factor here
is that the generator of Ab is the group Z of integers, an infinite group.
Thus perhaps what needs to be axiomatized as the counterpart of the finite
sets are something like the finite sums of Z, without however overaxiomatizing
things to the point of excluding Ab as a model.

Vaughan Pratt