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?