*To*: Victor Porton <porton at narod.ru>*Subject*: Re: [isabelle] A set is not its own member*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 17 Mar 2009 09:12:06 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1237243740.24805.4.camel@victor>*References*: <1237243740.24805.4.camel@victor>

Larry Paulson On 16 Mar 2009, at 22:49, 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 beprovedthat 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 ownmember inIsabelle/ZF.

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

- Previous by Date: Re: [isabelle] Meta_impE and other tactics
- Next by Date: Re: [isabelle] Meta_impE and other tactics
- Previous by Thread: [isabelle] A set is not its own member
- Next by Thread: Re: [isabelle] A set is not its own member
- 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