Subject: Definition of "definable in"

From: categories <[email-masked]>
Date: Wed, 20 Mar 1996 11:40:06 -0400 (AST)

Date: Tue, 19 Mar 1996 19:57:06 -0800
From: Vaughan Pratt <[email-masked]>

After giving more thought to my question about Set vs. Ab I decided
that it was hopeless to try to resolve as a theorem, and that the
only way out was to resolve it with a definition.

Definition.  A category C is *definable in* a closed category D when it
embeds fully (as a category) in every self-dual closed category
embedding D (as a closed category).

This definition settles by fiat the question of whether *finite* sets
can be defined from finite groups, since FinAb is self-dual, as I
mentioned previously.  Extending this to Ab is a matter of checking
that Set does not embed in Ab\op x Ab, which would surprise me
greatly.

If Set actually does embed in Ab, as some have been telling me
privately, this does not contradict my definition, it merely answers my
original question in the other direction.  To convince me that Set
embeds in Ab it will suffice for you to give me representatives of 2
and 3 whose homobjects between them are the representatives of 4, 8, 9,
and 27.

If you have a more productive notion of "definable in", meaning one
that lets you define categories not possible with the above, there is a
possibility that some trace of Set has leaked into your definition.
If, after convincing yourself that all traces of Set have been
eliminated, it is *still* more productive, then this would be a notion
of "definable in" well worth discussing.

Vaughan Pratt

---

From: categories <[email-masked]>
Date: Thu, 21 Mar 1996 13:33:38 -0400 (AST)

Date: 21 Mar 96 15:59:04 +0100
From: Reinhard Brger, Prof. Pumpl n <[email-masked]>

Since the set of maps from a non-empty set to the empty set is empty
and since Ab x Ab\op has no empty hom-sets, there is no full
embedding from Set to Ab x Ab\op. Does that answer your question?

                                    Reinhard Boerger

---

From: categories <[email-masked]>
Date: Thu, 21 Mar 1996 23:14:17 -0400 (AST)

Date: Thu, 21 Mar 1996 13:08:38 -0800
From: Vaughan Pratt <[email-masked]>

Not if I understand you, for two reasons.  First, you said the word
"hom-set" which isn't allowed in Ab---you have to say homgroup (or
homab).  There being no empty group, if Set embeds in Ab then the empty
set must embed as a nonempty group.  Emptiness in the sense definable
via the forgetful functor U:Ab->Set is not a predicate known to be in
Ab.  Emptiness needs to be defined in terms of the Abelian group
representing the empty set.

You have to analyze any proposed embedding by treating both the objects
and the homobjects between them as Abelian groups.

The second problem is my fault.  I noticed yesterday that my definition
(repeated below, near the end) is too weak.  As a simple
counterexample, groups are well known to be definable in Set, but Grp
certainly does not fully embed as a category in the closed self-dual
category Set + Set\op (= Chu(Set,0)), which embeds Set as a closed
category (that is, the embedding respects tensor products, not
necessarily cartesian products).  The objects are just sets and
antisets, clearly nowhere to store Grp.

I was basing my definition on two theorems of mine.

1. Every category of relational structures, and hence every full
subcategory thereof definable by any wacky language you want, far
wilder and less computable than first order logic, fully embeds in
Chu(Set,2^k) where k is the total arity of the structure.

To determine total arity k of a multisorted multirelation structure,
form the disjoint union of all the carriers, add one unary predicate
per carrier as a marker, and then form the "natural join" of all the
relations.  The embedding works for total arities up to any ordinal;
for a proof look near the end of

	http://boole.stanford.edu/gamut.ps.gz

2.  Every small concrete category embeds in Chu(Set,K) for some set K.

Proof: Take K to be the disjoint union of the carriers of the objects,
and proceed as in

	http://boole.stanford.edu/embed.ps.gz

On the strength of these two theorems I speculated that any method of
defining a category that confined its language to that of V would embed
in Chu(V,k) for a suitable object of k.

What does "confine language" mean?  Terrible things!  It might even
entail giving up conventional equality in favor of weighted limits when
V is not cartesian closed, as with Ab.  Some of you might enjoy a world
where equality didn't exist, not in the sense you have to settle for in
Set where you have to convince skeptical students that equality doesn't
exist, but in the more pragmatic sense that no one else in that world
uses it either, because it really doesn't exist!

What I forget to allow for in my definition was the variability of k.
Larger k lets you define more.  k functions as a simple but effective
and pure notion of signature.  Pure in the sense that the 256 colors on
your monitor are the clean signature of pixel depth, purified of the
grubby representational issues implied by talking instead of the 8
pixel planes as though each plane were a real thing.  This
representation is clearly meaningless for people whose computers have 6
pixel planes coding 729 colors in ternary.

I had foolishly thought that the essence of the Chu construction could
be purified to a statement about duality, but had clean forgotten to
allow for the possibility that a definitional method might cunningly
think to use language to express the definition!

Just how little language can be present in a self-dual category
embedding Set can be can be seen from the example above of Chu(Set,0),
a self-dual category consisting *only* of sets and antisets (aka CABA's
if you ignore concreteness issues).  The sets are realized as the
inconsistent Chu spaces (A,0), the antisets as the empty Chu spaces
(0,A), with (0,0) as the one set that is also an antiset.  (Obviously
this doesn't work for what Dusko Pavlovic calls "little Chu," no
repeated rows and columns.) Chu(Set,0) understood skeletally consists
of just the "dynamic integers," thinking of (0,A) as minus (A,0).  The
only subcategories of this sparse category have as their objects some
sets and some antisets.  This does not even embed Set\op x Set =
Chu(Set,1), which also is too small for anything much, e.g. no posets,
which enter at Chu(Set,2).

I see nothing for it for now but to be upfront about putting Chu in the
definition.

Old definition.  A category C is *definable in* a closed category V
when it embeds fully (as a category) in every self-dual closed category
embedding V (as a closed category).

New definition 1.  A category C is *definable in* a closed category V
when it embeds fully in the category Chu(V,k) for some k in ob(V).

This definition steers between the Scylla of arbitrarily large
self-dual categories and the Charibdis of self-dual categories barely
bigger than V.  It is also a tad shorter.

But there is *still* a problem.  In Set it is not hard to define
Chu(Set,*) as a colimit of Chu(Set,K1) < Chu(Set,K2) < ...  For example
the category of hypergraphs described in

	@Article(
DW80,	Author="D{\"o}rfler, W. and Waller, D.A.",
	Title="A category-theoretical approach to hypergraphs",
	Journal="Archives of Mathematics", Volume=34, Number=2,
	Pages="185-192", Year=1980)

does not to my knowledge embed in any Chu(Set,K) for any fixed K.
(This is an open question, I imagine mainly because no one has looked
hard at it.)  But any *small* subcategory of it does, by the general
result above that *every* small concrete category embeds in Chu(Set,K)
for some K.

This too is easily fixed.  There is a *nonclosed* category
Chu(Set,Set).  The definition looks no different from the usual
definition of Chu, except that in all small interactions (no proper
class of participants), all Chu spaces involved are taken to be over
the colimit of all their K's.  The only failure of this category to be
closed is its lack of tensor unit 1 and its dual _|_ (I've switched to
Girard's notation because these days it makes a lot more sense to me).
The rest of linear logic is fine; furthermore the absence of 1 and _|_
removes the odd-ball property 1@1 |- 1 that Lafont and Streicher
noticed.

With that and MIX gone, about all LL should need now is induction, and
Chu(Set,Set) should then be a complete model of LL without
multiplicative units.

If there is any justice, all this should generalize to Chu(V,V) by
arranging to embed the k's of any interaction of V-enriched Chu spaces
in the appropriate colimit of them in V before letting them interact.

This leads to the even shorter:

New definition 2.  A category C is *definable in* a closed category V
when it embeds fully in the category Chu(V,V).

In view of Dusko Pavlovic's paper on the couniversality of Chu, about
the only improvement likely for this definition (barring further bugs,
sigh) is to replace the explicit Chu construction by its abstract
properties.  The effect will be the same either way, though the
definition is presumably not going to get any shorter that way!

One residual question is how to do enriched category theory from
scratch in V.  Max, help!

Vaughan Pratt