*To*: Victor Porton <porton at narod.ru>*Subject*: Re: [isabelle] A set is not its own member*From*: Jeremy Avigad <avigad at cmu.edu>*Date*: Tue, 17 Mar 2009 09:05:40 -0400*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1237243740.24805.4.camel@victor>*References*: <1237243740.24805.4.camel@victor>*User-agent*: Thunderbird 2.0.0.19 (Windows/20081209)

Dear Victor,

Y = { X in Z | X not in X }

Jeremy Victor Porton wrote:

A problem about Isabelle/ZF: I have a set Z and need to construct a set which is not a member of Z. I heard that with the axiom of foundation (see ZF.thy) it can be proved that any set is not member of itself. (This solves the above stated problem.) Could anyone guid me how I can prove that a set is not its own member in Isabelle/ZF. (I am an Isabelle novice but developing a theory which will revolutionarize further development of formal proof assistants based on ZF. Please help me to accomplish this task.)

**References**:**[isabelle] A set is not its own member***From:*Victor Porton

- Previous by Date: Re: [isabelle] Displaying some element of a list of facts
- Next by Date: [isabelle] More complete theory?
- Previous by Thread: Re: [isabelle] A set is not its own member
- Next by Thread: [isabelle] Overview article on OS verification
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list