One more conjecture about provability without axiom of choice

I addition to this conjecture I formulate one more similar conjecture: Conjecture $latex a\setminus^{\ast} b = a\#b$ for arbitrary filters $latex a$ and $latex b$ on a powerset cannot be proved in ZF (without axiom of choice). Notation (where $latex \mathfrak{F}$ is the set of filters on a powerset ordered reverse to set-theoretic inclusion): $latex […]

Generalization in ZF

I wrote short article “Generalization in ZF” accompanied with Isabelle/ZF sources. This is a draft and alpha. I await your comments on both the article and Isabelle sources. I’m sure my Isabelle sources may be substantially improved (and I plan to work over this). Comments are welcome. After hearing your comments and improving the files, […]