Email Gateway (Aug 18 2022 at 16:45): Email Gateway (Aug 18 2022 at 16:45):From: Victor Porton <porton@narod.ru>
In ZF.thy the foundation axiom is:
foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"
Why there are no simplified version?
foundation: "A=0 | (\<exists>x\<in>A. x Int A=0)"
Isn't the latter more convenient in use?
So my question: Why there are no second version of foundation in Isabelle/ZF?
\--
Victor Porton - http://portonvictor.org
Last updated: Apr 16 2024 at 20:15 UTC