FOM: basic concepts; structuralism

[Vaughan R. Pratt]

(Sorry about both the length and argumentative tone of this.  -vp)

	If I'm not mistaken, Vaughan's remarks are informed by a
	category-theoretic perspective, wherein "set" is interpreted as
	"object in a topos",

Good heavens no, you'd have directed graphs and simplicial sets being
sets.  The category of directed graphs (aka binary relations) with the
evident homomorphisms (don't lose any edges and don't tear connected
edges apart) forms a topos.  So does that of simplicial sets and the
more generous notion of homomorphism (than the evident one) that
includes the degenerate maps.  Lots of toposes arise in nature that are
not at all equivalent to the category of sets.

If it clears the air at all, my remarks are informed by the perspective
that a set is an ordinal.  This makes membership transitive, which
could bother some but suits me just fine.  In any event membership
plays no role at all in my axiomatization of sets, though it has a
simple definition in terms of the primitives I use in the
axiomatization, namely a suitable adaptation of ordinal arithmetic.

	I have never really understood the way category theorists seem
	to view the rest of mathematics

Eighteen months ago, when I was just starting to grapple with what I
personally considered to be a set, I asked the categories mailing list
(which btw has been very active since the late 1980's) the question
attached at the end of this message.  Briefly, I asked why it seemed
harder to get from composition to membership than the other direction,
and what to do about it.  For some reason this stirred up a real
hornet's nest, I think more than any other single message ever posted
to this list.  I kept about 70 messages from this correspondence that
collectively demonstrated a wide range of opinions held by category
theorists on the nature of sets and membership, some very strongly
held.

Shortly after posting this message I decided that a set was an
ordinal.  Not too surprisingly in retrospect, this found little support
from the list.  The biggest objection (which may well bother some of
you too) was that this builds Choice explicitly into every set so that
you can't get away from it even when you aren't using it.  People
weren't used to Choice being moved up to the front of the list of
axioms in this way and wanted, very naturally, to be able to say that
certain theorems definitely did not depend on Choice.

My feeling about this is that those like me who accept Choice from the
get-go and have no interest in keeping score as to which theorems
depend on it should be allowed to put Choice anywhere they like in
their Theory of Everything.  If putting it at the very front, as
implied by the definition of a set as an ordinal, yields a nicer
axiomatization of sets than ZF, then we Choice Philistines should have
no qualms about putting it there.  Choice zealots who like keeping
score are free to stick with their system.

	I know that some topos theorists such as Peter Freyd have
	sometimes asserted that category theory or topos theory is or
	can be turned into a good foundational theory for all of
	mathematics or at least a good portion of it.  I have never
	understood how this can be.  It seems wildly exaggerated.
	Could somebody please try to explain it clearly?

For one comprehensive story see Goldblatt's book on Topoi (out of
print?).  For a (to some extent) competing viewpoint see Johnstone's
book on Topos Theory (definitely out of print).

I'm not a category theorist (no category theorist would dream in their
worst nightmare of taking Choice as their first axiom) though I take an
active interest in the field.  In my only partially informed view, the
basis for category theory's claim to being foundational in the first
instance is that it replaces a nonconstructively nontransitive theory
of membership by a constructively transitive theory of morphism,
meaning one in which morphisms not only compose but more fundamentally
*exist*, unlike instances x\in y of the membership relation.  In place
of the *axioms* of extensionality, separation, union, and power set are
the *entities* of functor, natural transformation, and adjunction.
Their development from a set theoretic standpoint, as done in most
category theory texts, takes inordinately long.  When treated coming in
the other direction from a 2-category perspective however, they can be
axiomatized relatively succinctly, closer to the brevity if not the
exact style of ZF.  Oddly, no category theory text does this or even
hints at the possibility.

What I find appealing about ZF, besides its succinctness, is that it is
a typeless theory: there is just one big universe of sets.  The very
term "category" tells you that CT is the opposite: it depends for its
very existence on dividing up the mathematical universe into
categories.

I find this easily the most distressing part of category theory.  I see
it as confusing two entirely orthogonal concepts, the notion of
structure of an object as encoded in the behavior of composition of
morphisms *at that object*, and the notion of <category in which that
object resides>.

A good categorical foundations should be like ZF, having a single
universal category of objects as a generalization of the notion of set
to structured objects.  Being typeless does not mean there are no
subcategories, any more than ZF being typeless does not mean there are
no subclasses of the class of all sets; indeed the category of sets
would itself form a full subcategory of this universal category, namely
its discrete objects.

Defining and axiomatizing such a universe, including proving a
stronger-than-normal completeness property of the axiomatization in
which syntax and semantics are perfectly reconciled not only for the
theorems but the proofs, is currently a central interest of mine.

	The question right now is, how can category theory be used to
	explain real analysis?

Category theorists might not let me get away with saying this, but I
think real analysis is better treated within the elementary (first
order) theory of reals than with category theory.  (But see below.)

But why is real analysis your litmus test of the worth of a
foundation?  What if we substitute homological algebra for real
analysis?  This is where transformational accounts (in terms of
homomorphisms between objects) seem to work better than elementary
accounts (in terms of relationships between individuals in a single
object such as the set of reals).  Category theory is the more natural
setting/framework for some areas, set theory (I claim) for others.

	In particular, it's natural to ask how completeness of the
	reals would be defined in the absence of the concept of an
	arbitrary bounded set of reals.

Ok, so here's where I step in and contradict myself about real
analysis.  As far as completeness is concerned, category theory, or
duality theory if you prefer, offers a much neater solution to defining
completeness than does set theory.  I'll take inner product spaces as
the specific example since I know the relevant reference, but I would
expect something like this to work in some other situations too,
hopefully including the reals themselves.

In JSL 49:2,401-404, Rob Goldblatt shows that metric completeness is
not first-order definable.  In fact he shows that all
infinite-dimensional sub(inner-product-space)s of separable Hilbert
space H, none of which are metrically closed except H itself, are
elementarily equivalent to H.

This notwithstanding, a necessary and sufficient condition for an
inner-product space to be metrically complete is that its lattice of
orthoclosed subspaces be orthomodular.  Orthomodularity is first-order
definable in the language of lattices, in fact equationally definable.
Thus by describing Hilbert spaces in this dual framework, the desired
property can be expressed simply and cleanly.

Another such situation is transitive closure, well known not to be
first-order definable.  But if you take as your universe not that of
individuals structured by a binary relation, but binary relations
structured by union, composition, and left and right residuation, then
transitive closure becomes definable equationally---in fact the whole
setup can be completely axiomatized with fourteen equations, see my
1990 JELIA paper showing how to do this,
http://boole.stanford.edu/pub/jelia.ps.gz.

This system incidentally solves the old problem of finitely
axiomatizing the equational theory of regular expressions: just add the
residuals a->b meaning "had a then b" and "b<-a" as "b if only a", with
ab meaning "a then b", and you conservatively extend a
nonfinitely-based equational theory to a finitely based one.
Furthermore this extension kills off all the finite nonstandard models
that plagued the former (which allows in particular a four element
model {0<1<a<a*} in which aa=a yet a* is not a, crazy).

	The structuralist creed is that each subject exists in its own
	internal world or framework and is understandable only from
	that narrow viewpoint.  Thus structuralism tends to isolate
	subjects and cut off all of their connections with the rest of
	human knowledge.

Well, yes and no.  No in that this is what functors in general and
adjunctions (constructive Galois connections) in particular are for: to
make all the necessary connections between categories.  On the other
hand, yes in that this is what I was complaining about above as my
biggest gripe about category theory.  My position is the fragmentation
of the universe of transformational mathematics into categories is an
unfortunate but entirely unnecessary artifact of category theory
arising as an historical accident from the way the subject has
evolved.

My complaint goes beyond mere making of connections, I want to connect
all the categories in the world into one single category, with the
seams invisible.  This is the level of seamlessness that ZF achieves.
So I can agree with you provided the connections you are asking for are
seamless connections, but you didn't seem to be going that far.

	It's the opposite of the foundational approach, which regards
	the unity of human knowledge as paramount.

Oh, come on, now you're getting carried away.  I didn't know the
foundational approach did that, but if it does it is as confused as
19th century physics was about light.  The unity of human knowledge has
the same status as the old view of light as *only* a coherent wave.
There is as much room for disunity in human knowledge as there is for
photons in the theory of light.  I can't even begin to imagine human
knowledge keeping pace with human progress without a lot of disunity.


	But they will have a very hard time explaining how results in
	sheaf theory, general topology, model theory, etc should be or
	could be of interest to the general scientific/philosophical
	public.

I disagree for all three examples.  Let me treat each in turn.

Sheaf theory is just continuous presheaf theory.  Presheaf categories
provide perhaps the most important instance of toposes, and are much
more fundamental, insightful, *and simple* than noncategorists
realize.  I think this is due in large part to most category theorists
being constitutionally incapable of explaining what they do in terms
that the rest of the world can easily relate to.

Point-set topology is to universal mathematics as group theory is to
universal algebra: it instantiates the general concept with specific
axioms that limit its scope to a particular application, namely
infinite limits.  The closure of classical open sets under arbitrary
union and finite intersection serves to limit the applications of
topology to the treatment of infinite limits and pairwise comparisons
(and the T1 condition eliminates the latter), just as the group axioms
limit algebra to the treatment of composable permutations and their
inverses.  Without those restrictions (union, intersection, classical),
point-set topology *is* universal mathematics, or at least universal
transformational mathematics.

First-order model theory is the flip side of what I was saying about
metric completeness and transitive closure.  If you find yourself
struggling with arcane ultraproducts, simply dualize and you'll have a
much easier time of it with quantifiers, relations, and Boolean
connectives, the theory of which furthermore is finitely
axiomatizable.  Your point about the model theory side of that duality
is therefore well taken.

But if you pass to the more general notion of model as simply an
featureless entity that may or may not satisfy an equally featureless
sentence, model theory and proof theory surprisingly become equally
beautiful dual subjects that you could easily entertain a technically
literate audience with, thanks to the miracle of Galois connections.
With nothing more than an arbitrary binary relation of satisfiability
between a class of models and a class of sentences, one shows that both
deductive closure and model closure (e.g. HSP closure in the case of
equational theories) are necessarily well defined.  Furthermore the
evident notions of model-of and theory-of, as the polarities of the
Galois connection induced by the satisfiability relation, both map
unions to intersections, as intuition would suggest, but not
intersections to unions.  This is a lovely little subject that creates
a nice structural framework into which one can plug a number of
well-known instances, including equational logic, universal Horn logic,
and first-order logic, with all the above features then taking specific
forms, e.g. various complete axiom systems on the proof side and
HSP/ISP/ultraproduct closure on the model side.

Model theory at this more abstract level, unlike its more arcane
instances such as first-order model theory, is simple, pretty,
powerful, and eminently presentable to a broadly-based technical
audience.

Vaughan Pratt



==Message posted to the categories mailing list last year==

Date: Mon, 11 Mar 1996 10:15:45 -0400 (AST)
From: categories <cat-dist at mta.ca>
To: categories <categories at mta.ca>
Subject: Set membership <-> function composition 

Date: Sun, 10 Mar 1996 17:23:14 -0800
From: Vaughan Pratt <pratt at cs.Stanford.EDU>


I don't know quite how much sense this question makes, but let me ask
it anyway.

Set membership and function composition can be defined in terms of each
other.  However getting from the former to the latter seems to be
*much* easier than going back, which would appear to entail first
picking out the transitive closure of membership in Set and then
recovering membership itself from it (see e.g. Goldblatt's Topoi 12.4),
a messy process.

What significance does this asymmetry have for you?  Does it mean that
Set itself is somehow to blame by having been improperly formulated?
Or does it mean that membership is an intrinsically obscure notion
because of the messiness of the process?  Or is transitivity itself
merely an unnatural preoccupation of set theorists that has no place in
proper mathematics?  In that case is membership better regarded as just
an undefined notion in Set?  Should one forget altogether about
membership *and* Set and just work in one's favorite topos, e.g. the
effective topos?

Or should we just define set membership as done by ZF instead of trying
(pretending?) to extract it from function composition?  This need not
entail abandoning any part of category theory.  All it would do is make
set membership the elementary concept we all (well, surely almost all)
intuit it to be, instead of one that depends on a tour de force.

Pointers to relevant literature much appreciated.

Vaughan Pratt