Subject: 2 bug fixes

From: categories <[email-masked]>
Date: Sat, 16 Mar 1996 23:08:32 -0400 (AST)

Date: Sat, 16 Mar 1996 18:43:26 -0800
From: Vaughan Pratt <[email-masked]>

The following repairs two problems I found with my ordinal-based
axiomatization of Set: missing axiom of infinity (no NNO), and an
inconsistent definition of product.

1.  Add "There exists x such that 1+x=x."  (Set *forbids* FinSet.)

(By equality in my axiomatization I always mean identity, not just
iso.)

[A reminder that i/j = min k[i < j*(k+1)], and  i%j = i - j*(i/j)
(ordinal division and ordinal remainder, used in the following).
Exercises.  (i) j*(i/j) <= i.  (ii)  i%j < j. ]

2.  Replace the definition of product by the following.

Given an ordinal i, the i-product p = p_i of a family <n_j>,j<i of
ordinals is defined up to Choice by recursion on i to be the least
ordinal p_i satisfying the following.

The 0-product p_0 is 1.

For all j<i, the j-product p_j of the family <n_m>,m<i is defined by
recursion along with, for all k<=j, an *auxiliary* projection
f_{jk} : p_j -> p_k, namely \n.n%p_k.  (So f_{jj} is the identity.)

For successor ordinals i = k+1, the definition of p_i is completed by
requiring that it have in addition a *main* projection
g_k : p_{k+1} -> n_k, namely \n.n/p_k (a monotone function).

For limit ordinals, the definition of p_i is completed, up to Choice,
by requiring it to be *a* categorical limit of the diagram whose
objects are, for j<i, the j-products p_j of <n_m>, 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 p_j are the auxiliary projections f_{ij} : p_i -> p_j
defined at this level.

The counit of i-product at family <n_j>, j<i, has for its j-th map,
j<i, the composite g_j f_{i,j+1} : p_i -> p_{j+1} -> n_j.  These are
the *standard* projections of ordinal product.

The unit of I-product at n (the diagonal d_n: n->n^I) 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
product adapted to infinite ordinals.

Compare the explicit definition \n.n%p_k, a monotone function, at
successor products to the underdetermined categorical definition at
limit products.  The latter defines ordinal product only "up to
Choice," bringing in Choice as a "randomizer".

That a limit of this (small) diagram exists is immediate by the
completeness of Set.  Once one such limit has been found in this
version of Set, all ordinals of the same cardinality become equally
eligible, and the first paragraph of the definition 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.

Barring further bugs, this definition is an underdetermined alternative
to those of Birkhoff 1942 and Hausdorff, 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.

Vaughan Pratt

PS.  I learned after giving the obvious (for Set) ordinal version of
the axiom of infinity above, that Peter Freyd had shown it was
equivalent to NNO not just for Set but for *any* topos.  Now *that's*
what I call an interesting property of toposes.  A lightweight
collection of such nice facts in one place might put hard-to-please
types like me in a more receptive frame of mind for the massive body of
theory that topos theory seems dependent on.  Halmos fits "all" the
basic material about naive set theory in his 100-page book.  Is it fair
to say that the corresponding material treated in topos theory requires
considerably more space?  And if not, when can we expect the topos
counterpart to Halmos?