Email Gateway (Aug 18 2022 at 13:11): Email Gateway (Aug 18 2022 at 13:11):From: Victor Porton <porton@narod.ru>
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.)
Email Gateway (Aug 18 2022 at 13:11):From: Lawrence Paulson <lp15@cam.ac.uk>
The theorem that you request is already present and is called
mem_not_refl. Similar proofs can be found in the file ZF/upair.thy.
Larry Paulson
Email Gateway (Aug 18 2022 at 13:12):From: Jeremy Avigad <avigad@cmu.edu>
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:
Last updated: May 03 2024 at 12:27 UTC