Re: [isabelle] A set is not its own member




Dear Victor,

There is a solution, based on Russell's paradox, that doesn't require the axiom of foundation. Let Y be the set of elements of Z that are not elements of themselves; i.e.

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

I claim that Y is not in Z; otherwise, we would have Y in Y if and only if Y not in Y, a contradiction.

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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.