🚀 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

In article <1992Sep4.172833.20527@guinness.idbsu.edu>, holmes@opal.idbsu.edu (Randall Holmes) writes:

> >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".

I think he just means "... implies that the above set be an honest-to-goodness
set, where we're assuming the universe to be a set". So no, he's not wrong.

> >
> >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).

Hmm. One could alternatively argue that NFU is not recommended because it is
known to have a model within ZFC, so it's not likely to tell us anything we
didn't know already...
Seriously, ZF isn't known to be consistent either, just believed to be so
because we've been playing with it for ages and not found any holes. (As I'm
quite sure you're perfectly well aware!) Why shouldn't we play with NF for
a while and see if it falls over? If it doesn't -- well, perhaps we'll start
to trust NF the way we presently trust ZF, and perhaps it will give some new
insights.
I don't mean to malign NFU or anything; I just take exception to the idea that
a set theory that's not provably weaker than ZF can't be worth studying!

     Actually, there are now several interesting type-free,
consistent, non-trivial set theories.  Gilmore's NaDSet (Journal
of Symbolic Logic 1986) is joined by the "map theory" by ??
(someone from Germany, sorry I've forgotten the name) in the
latest issue of Theoretical Computer Science, and a set theory
by Fairouz Kamareddine in Volume 1 Issue 1 of the new Journal of
Logic, Language and Information.

     Interestingly, the TCS writer and Kamareddine seem not to
have known about each other's work or Gilmore's, though they
refer to Aczel's papers on non-well-founded set theory, which in
turn refer to Gilmore's earlier work.

     All three papers refer to (and, basically, refute) Scott's
1975 paper "Combinators and Classes", which bemoaned the lack of
type-free set theories and implied that set theory was not a
suitable basis for theoretical computer science.  Any of the
three set theories looks like it would work OK as a basis.  (I
prefer Gilmore's for sentimental reasons and because it's simpler.)

     I wouldn't consider NF and its extensions to be really
"type-free" because they sneak type theory ideas in the back
door with the stratification condition.

--Jamie.
  jamie@cs.sfu.ca
"Every \item command in item_list must have an optional argument." LaTeX pg.168

In a previous article, ziane@nuri.inria.fr (ziane mikal -) says:

              (much else deleted)
>
>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 ?
>
>
>Mikal Ziane.
>

	The category of categories is an open problem.  Set theoretic
approaches to it are not promising.  I have a tiny note in _JSL_ _57_
(pp.555-6) showing in effect that if you define categories set
theoretically in a set theory which includes a set of all sets, then
you can get an actual category of all categories but it will have
such terrible properties as to be useless.  (That does not mean that 
set theoretic considerations can not bear on the question, but 
straightforward set theory will not solve it.)

	The category of categories can be approached categorically too.
The classic source is by Lawvere, "The category of categories as
a foundation for mathematics" in _Proc. of the La Jolla conference on
Categorical Algebra", Springer-Verlag 1966 (pp.1-20).  More recently 
there is my own "Axiomatizing a category of categories" in _JSL__56_
(pp.1243-60).  Both briefly discuss what would be needed for "a
category of ALL categories".

	On a categorical approach a "category of ALL categories"
would presumably use Benabou's approach via fibrations (see Benabou 
"Fibered categories and the foundations of naive category theory" 
_JSL__50_ pp.10-37).  It would require a kind of universal fibration.  
It would require a universe of categories and functions, one of whose 
functors was a fibration such that:

	Every category in that universe is a fiber of that fibration

	Every functor in that universe appears as the functor
		between fibers induced by some arrow of the base
		of the fibration.

That second condition seems to me to want an elegant statement, and I
don't have one for it.

	It seems very unlikely that such a "category of all
categories" will give anything like a Russell's paradox--in part
because we never say EXACTLY WHAT any category is MADE OF.  Such
talk is nonsense on a categorical account.  So we can not define
a paradoxical category by giving an impossible requirement on the
categories and functors it should be MADE OF, the way we do for
elements of the Russell set.

	Such a fibration might lead to some kind of cardinality
paradox.  I am inclined to doubt it.  But I will speculate no more
here.  The problem remains open--even as to its exact statment.

Colin McLarty

	 

In article <4134@seti.UUCP>
ziane@nuri.inria.fr (ziane mikal -) writes:
 
>The question is now, whether or not alternative axiomatizations
>have been proposed that are consistent with the existence of the
>set of all sets ?
 
In the 1920's Paul Finsler proposed a system of set theory in which
a set of all sets is allowed. His system is not formal (in Hilbert's
sense); the discussion of his system within the mathematical community
was rather emotional and not free from personal animosities. In
his system, Finsler showed incompleteness before Goedel.
As far as I know, a serious and in depth study of his Finsler's set
theory has yet to be done.
 
Ivo Duentsch
Rechenzentrum
Universitaet Osnabrueck
duentsch@dosuni1.rz.uni-osnabrueck.de

In article <1685C6F56.DUENTSCH@dosuni1.rz.uni-osnabrueck.de> 
DUENTSCH@dosuni1.rz.uni-osnabrueck.de writes:

   >Finsler showed incompleteness before Goedel.

  Not really. Finsler is represented in "From Frege to Godel". See
his paper there, and its introduction.