🚀 go-pugleaf

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".  What if you
>altered ZF to contain this axiom (and introduction of definitions)?  In
>the first place, you could immediately prove the existence of all sets
>that are already there.  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?

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

(This rewrite is a bit complicated, since it covers the case where X is not
uniquely defined.  The essential form is (All X.X=E => P(X)), which can be
used if Ex! X.X=E has been proved.)

Please try again.