[YG Conlang Archives] > [jboske group] > messages [Date Index] [Thread Index] >
On Tue, Jan 14, 2003 at 12:33:07PM -0500, John Cowan wrote:
> Jordan DeLong scripsit:
> > > That's Cantor's paradox: the set of all sets must contain its power set
> > > as a member, which is impossible. The whole point of Quine abstraction
> > > is that it's eliminable *without* reifying over sets.
> >
> > I dunno what 'eliminable' means.
>
> You can rewrite all talk of Quine abstraction in terms of pure quantified
> logic without introducing any sets that are the values of variables.
> So the pseudo-set x^ = {x | x is even} is just Ax: x is even.
Well, it's a little more complicated than that. Rewriting to "All
x such that x is even" has problems with russell sets, etc.
Ok so now I know what you meant by eliminable (apparently this is
from 'eliminate', but it's not in my dictionary).
However, sets *are* possible values of variables in Quine[1]... So
I still don't know what you mean.
[1] Wee, something I can actually proove (using '<' as
containment again):
|- (x)(x = x) (theorem 182)
|- V < V (theorem 210)
|- V = x^(x = x) (definition of V)
|- V < x^(x = x) (subst of equivalents)
|- Ey(V < y . (x)(x < y -> x = x)) (def of abstraction)
|- Ex(x = V)
(theorem numbers from 'mathematical logic').
I hope I didn't skip a step.... Those "natural deduction" styles
of doing proofs are a lot easier to avoid skipping things in...
--
Jordan DeLong - fracture@hidden.email
lu zo'o loi censa bakni cu terzba le zaltapla poi xagrai li'u
sei la mark. tuen. cusku
Attachment:
binAlWtrdQBoc.bin
Description: application/ygp-stripped