🚀 go-pugleaf

In article <4134@seti.UUCP> ziane@nuri.inria.fr (ziane mikal -) writes:
>In article <1992Aug25.120515.15090@husc3.harvard.edu> zeleny@husc9.harvard.edu (Michael Zeleny) writes:
>>Greetings,
>[...]
>>Je suis pr\^et \`a partir pour Paris jusqu'a 17 septembre; par
>>cons\'equent, il me sera impossible de tenir mes propos provocants.
>>Veuillez envoyer vos messages concernant mes defauts personnels \`a ma
>>adresse not\'ee ci-dessous.
>[...]
>
>I cannot resist. Correcting MZ is such a pleasure.
>It's "mon adresse" and not "ma adresse".
>I confess however that the rest of his French looks better
>than my English.
>
>BTW, Mishka, si tu passes par l'inria, viens donc me faire
>une petite visite au batiment 9 ou appelle moi a paname.
>Je suis dans l'annuaire.
>
>
>Since this can hardly justify a posting by itself here is something 
>more interesting I hope.
>
>Russel's paradoxical set is the set of normal sets, i.e. sets which
>don't belong to themselves.
>However, the set of all sets, let's call it S, is often considered 
>paradoxical because of the following, with P(S) the powerset of S:
>
>P(S) is included into S, then Card(P(S)) <= Card (S)
>which contradicts a theorem saying that
>Card(P(S)) > Card(S)
>
>However, looking back to the proof for Card(P(S)) > Card(S)
>it appears that the proof uses a set might quite be paradoxical !
>The idea is to consider a function from S onto P(S).
>If you take the identity the dubious set is indeed Russel's set !
>
>Thus you might as well reject the proof rather than the concept
>of set of all sets. However if you define sets with ZF it seems
>that you must accept the proof. The separation "axiom" which is
>in facta theorem of ZF,  implies that the above dubious set be
>a proper set. (Am I wrong ?)

The usual terminology is "proper class".

>
>The question is now, whether or not alternative axiomatizations
>have been proposed that are consistent with the existence of the
>set of all sets ?

	There are a number of such axiomatizations.  The nicest is
Jensen's version NFU of Quine's set theory NF ("New Foundations").  NF
itself is not recommended, because it is not known to be consistent,
and it also has the curious feature of disproving the Axiom of Choice.
Jensen's system is known to be consistent, and can be extended with
the Axiom of Choice and as many axioms of strong infinity as one might
desire (loosely speaking).

	NFU is a first order theory with equality and membership.  Its
axioms are as follows:

	(Ext)  If x and y have the same elements, then either x = y or
both x and y have no elements

	The axiom (Ext) allows many individuals (objects with no
elements); one of these should be identified as the empty set and the
others as bare individuals (non-sets).  If we do not allow individuals
other than the empty set, we get full NF.

	(Comp)  If P is a formula which is "stratified" (defined
below) then there is an object y such that for all x, x is an element
of y iff P (of course, P says something about x).  y can be referred
to as {x|P}, and is unique by (Ext) if it has any elements; otherwise,
we let {x|P} be the individual we have singled out as the empty set
((Comp) proves the existence of at least one object with no elements).

	A formula is said to be "stratified" if it is possible to
assign types to the variables occurring in it in such a way that it
makes sense in the simple theory of types.  To be precise, a formula
is stratified if we can assign an integer to each variable (called the
type of the variable) in such a way that in each subformula "x = y"
the two variables are assigned the same type, while in each subformula
"x E y" the type of y is one greater than the type of x.  The formula
"not(x E x)" is unstratified (what single type can be assigned to x?),
so {x| not(xEx)} (the Russell class) is not provided by (Comp); but
{x| x = x}, the universe, _is_ provided.  Notice that the objects of
NFU do not have types; the typing scheme is only used to see what
instances of set comprehension are acceptable.

	Jensen proved this theory consistent.  It should be extended
at least with the Axioms of Infinity and Choice for practical
purposes.  Cardinal and ordinal numbers are defined as in naive set
theory.  The paradox of Cantor is avoided because the Cantor theorem
|A| < |P[A]| of naive set theory takes the form |USC[A]| < |A| in this
theory (where |USC[A]| is the set of one-element subsets of A.  The
special case |USC[V]| < |V| (V is the universe) establishes that the
unrestricted singleton map x |-> {x} cannot exist (its definition is
usntratified).  Thus, there are "fewer" singletons than objects,
although there is a "proper class" bijection between them.  Sets A
such that the restriction of the singleton map to A exists are called
"strongly Cantorian" and satisfy the naive version of the Cantor
theorem; in suitable extensions of NFU, the "class" of hereditarily
strongly Cantorian sets looks rather like the "small" sets of the
usual set theory.  The Burali-Forti paradox is avoided because the
result of nive set theory that the set of ordinals less than an
ordinal a has order type a under the natural order is proven by
induction on an unstratified condition and is false in NFU; the set of
all ordinals exists, and has an order type under the natural order,
but this order type (which is an ordinal) is less than the largest
ordinals.  Numbers are finite cardinals, and NFU + Infinity
supports nth order arithmetic for every n, thus all of classical
mathematics except the higher reaches of set theory, which can be
provided by adjoining further axioms of infinity.  All of this is
"safe"; it can be modelled in ZFC, in fact.  Jensen's paper is in
Synthese, volume 19.  Rosser's book "Logic for Mathematicians"
develops foundations of mathematics in NF (not NFU); his treatment of
the pair will not work in NFU, but it can be proven in NFU + Infinity
+ Choice that there is an ordered pair with the same type as its
projections, which is all that is needed to use the rest of Rosser's
development.  His section on the Axiom of Choice is valid for NFU,
since Choice is consistent with NFU; his Axiom of Counting is known to
be consistent with NFU (and strengthens it). (All of this will make
sense if you read Rosser).


>
>Also, I don't know anything yet about categories. I have heard
>though that the category of all the categories is not a pb.
>Does category theory have similar paradoxes though ?

The category of all categories is a proper class in the usual
treatment in ZFC, and this is all that it needs to be.  In NFU, it is
a set.

>
>Do the problems with the set of all sets prevent the possibility
>to properly define an Abstract Data Type "set" ? Set of anything
>of course.

What do you mean by "set of anything"?  For any type, we can define
"set of things of that type" as an ADT; we can define a polymorphic
type "set of 'a", where 'a is a parameter supplied in context (when
needed).  If sets can be defined in sufficiently strong ways, then the
paradoxes would preclude a universal type "set of _anything_", but
type discipline does that already. 

>
>Finaly, for computer scientists, is it problematic to have a
>universal type. I think of hierarchies in Object Oriented
>languages, where you have a root like Object or Class.

Types are usually disjoint.

>
>Mikal Ziane.


-- 
The opinions expressed		|     --Sincerely,
above are not the "official"	|     M. Randall Holmes
opinions of any person		|     Math. Dept., Boise State Univ.
or institution.			|     holmes@opal.idbsu.edu