Re: [Hol-info] Can I define a ZF FOL constant using only FOL symbols?

[Josef U. <jos...@gm...>]

> can you give me the FOL formula for (0 \<in> 0), and how your derived it?"

This is explained in
http://en.wikipedia.org/wiki/Extension_by_definitions#Definition_of_function_symbols
.

The empty set is obtained by proving

?!y: !u : ~(u \in y)

so, to match their notation, \phi is then "!u : ~(u \in y) " and f is then 0.

Then you asked to expand the empty set in an atomic formula \psi: "0 \in 0" .

So just follow their instructions: [...] choose an occurrence of f in \psi,
and let \xi be obtained from \psi be replacing that occurrence by a
new variable z. Then since f occurs in \xi one less time than in \psi, the
formula \xi* has already been defined, and we let \psi^* be "!z:
\phi(z) => \xi^*"

In your case, this is (after two expansions for each 0):

!z1: (!u1 : ~(u1 \in z1)) => (!z: (!u : ~(u \in z)) => (z \in z1))

or in a simplified form:

!z: (!u : ~(u \in z)) => (z \in z)

The conservativity claim is then that T' |- \psi <=> \psi^* .

Josef