🚀 go-pugleaf

In article <26922@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <1992Nov21.230530.117800@Cookie.secapl.com> Frank Adams writes:
>]In article <26788@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>]>I propose for discussion the
>]>
>]>  Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
>]>
>]>where "Exist! x" means "there exists a unique x such that".
>]
>]Actually, no.  Unless I am much mistaken, this kind of definition is
>]eliminable.  If we have a definition X := E, we can rewrite a wff of
>]the form P(X) as (All X.((Ex! X.X=E) => X=E) => P(X)).
>
>I'm not sure what you mean.  If you mean that the definition plus the
>axiom is eliminable, then of course you are right.

(I am leaving out the discussion of exactly how to eliminate the definition;
it suffices that we agree it is eliminable.)

In my previous article, I quoted:
>  And by adding some of the well-known machinery
>from recursion theory to prove Exist!... you could also talk about a lot
>of self-containing sets.  Wouldn't this theory be much more powerful
>than ZF?

Perhaps I misunderstood; I though David was asserting that his definitions
and axiom thereof would make a theory much more powerful than ZF.  If they
are eliminable, they don't.

So I must have misinterpreted "the well-known machinery from recursion
theory".  I think I know recursion theory fairly well, and I don't know just
what is being referred to here.  Thus I have to ask David to explicate just
exactly what machinery he wishes to import.