[FOM] About Paradox Theory

[T.Forster at dpmms.cam.ac.uk]

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)])]).
>
>about which Vaughan Pratt asks:
>
> > 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
>