Email Gateway (Aug 18 2022 at 16:44): Email Gateway (Aug 18 2022 at 16:44):From: Victor Porton <porton@narod.ru>
First, I don't understand what square brackets here means:
definition
foundation_ax :: "(i=>o) => o" where
"foundation_ax(M) ==
∀x[M]. (∃y[M]. y∈x) --> (∃y[M]. y∈x & ~(∃z[M]. z∈x & z ∈ y))"
Please clarify.
Second, could you help to prove "not({t}: t)"?
\--
Victor Porton - http://portonvictor.org
Email Gateway (Aug 18 2022 at 16:44):From: Lawrence Paulson <lp15@cam.ac.uk>
The material that you quote is from the development of the constructible universe, and is highly technical. For more information, see the following paper:
The relative consistency of the axiom of choice — mechanized using Isabelle/ZF
The foundation axiom itself is simply called foundation and is defined in ZF.thy. I suggest that you find a contradiction from {t} : t on paper first and then reconstruct it formally.
Larry Paulson
Last updated: Apr 25 2024 at 20:15 UTC