> 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 ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
