T.Forster at dpmms.cam.ac.uk T.Forster at dpmms.cam.ac.uk
Sun Sep 18 16:37:12 EDT 2011

I think what is going on is this: the nonexistence of the Russell class
(and the non existence of \{x: (\forall y)(\neg(x \in y \wedge y \in x)\}
etc etc is a theorem of first-order logic, indeed constructive first order
logic. One of my students was good enough to write out a constructive proof
of the double Russell'' case just mentioned - which Thierry Libert and i
appended to the end of our recent NDJFL article. The nonexistence of the
class of grounded sets is not a theorem of first-order logic, but needs
some (pretty basic) set theoretic axioms, specifically what Allen Hazen
calls subscission'' - the existence of x \setminus \{y\}\$. If we think of
grounded sets inductively (so that a set is grounded iff it belongs to
every set that contains all its own subsets, then (if my memory serves me
right) a universe that contains precisely one thing, and that thing is
self-membered, believes there is a collection of all grounded sets.

The observation from my textbook that Daniel is kind enough to quote was
really intended as a *paedogogical* comment (advice to students) rather
than a philosophical one, but i suppose i can stand by it.

Thomas

On Sep 18 2011, Daniel Mehkeri wrote:

>Harry Deutsch offers:
>
> > AyEzAx(F(xz) <--> x=y). Therefore,
> >
> > -EwAx(F(xw) <--> Au([F(xu) --> Ey(F(yu) & -Ez{F(zu) & F(zy)])]).
>
>
> > Anyone care to comment on whether it's intuitionistically valid as it
> > stands?  (I presume one can hedge by inserting a few "surely"'s,
> > formalized as not-not, to make it so, via Goedel's translation.)
> > Nik Weaver?
>
>I don't think it is what you want anyway. The classical foundation axiom
>is not constructively valid. Yes it is true we can make it valid by
>contraposition: no inhabited set intersects all of its members. However
>(and this is the sort of thing Nik Weaver keeps reminding us about) this
>is weaker than set induction over all first-order formulas.
>
>I'd say set induction is the intended meaning of well-foundedness.
>Thomas Forster seems to agree: "The only context in which this
>definition [well-foundedness] makes sense at all is [set] induction, and
>the only way to understand the definition or to reconstruct it is to
>remember that it is cooked up precisely to justify induction." (_Logic,
>Induction and Sets_)
>
>CZF just postulates set induction as a schema. I don't know if there is
>a single first-order formula that is equivalent to it over some basic
>assumptions. I don't know how the "set of all well-founded sets" paradox
>would work.
>
>Daniel Mehkeri
>_______________________________________________
>FOM mailing list
>FOM at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/fom
>