kdrag.theories.logic.zf

ZF style set theory

• https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory

• Naive Set Theory by Paul Halmos

• https://www.isa-afp.org/entries/ZFC_in_HOL.html

There are multiple specific ways to go about roughly the same thing.

Some versions, such as in Suppes’ text have a predicate is_set to distinguish sets from classes. This is not done here.

Functions

FinSet(*xs)	A helper for sets of the form {x1, x2, ..., xn}
slemma(thm[, by])
test()

kdrag.theories.logic.zf.FinSet(*xs)

A helper for sets of the form {x1, x2, …, xn}

kdrag.theories.logic.zf.slemma(thm, by=[], **kwargs)

kdrag.theories.logic.zf.test()

>>> True
True