ZF style set theory in Knuckledragger I

Zermelo-Fraenkel set theory is a theory of sets.

There are the opaque things called “sets” which have some plausible sounding constructions and properties.

Knuckledragger inherits from being a shallow system on top of SMTLIB being a simply typed higher order logic. While SMT / higher order logic has a built in notion of set as predicates A -> Bool, these don’t always fit the bill of the needs of set theory. They’re too inflexible.

So instead, we make a new sort called ZFSet and start axiomatizing properties about them. I baiscally am following Halmos’ Naive Set Theory https://en.wikipedia.org/wiki/Naive_Set_Theory_(book) chapter by chapter. A very nice little book.

Try this post out yourself at https://colab.research.google.com/github/philzook58/philzook58.github.io/blob/master/pynb/2025-10-13-zf_knuckle1.ipynb . It is pretty useful to see what goals I’m looking at to understand why I’m applying the tactics I am.

! python3 -m pip install git+https://github.com/philzook58/knuckledragger.git@eb4b269e0962b03f7f7d33816f302ad05ebbcc75

import kdrag as kd
import kdrag.smt as smt
ZFSet = smt.DeclareSort("ZFSet")

Classes https://en.wikipedia.org/wiki/Class_(set_theory) of these sets can be represented by the ZFSet -> Bool.

Class = ZFSet >> smt.BoolSort()

We’ll set up all the constant symbols we’ll need

A, B, x, y, z = smt.Consts("A B x y z", ZFSet)
a, b, c, d, p = kd.FreshVars("a b c d p", ZFSet)

P, Q = smt.Consts("P Q", Class)

Set theory is all about the elem element of relationship. Sets in sets in sets in sets.

elem = smt.Function("elem", ZFSet, ZFSet, smt.BoolSort())
elts = kd.define("elts", [A], smt.Lambda([x], elem(x, A)))

Russell’s Paradox

Only some of these are internalizable into ZFSet. Even before we have any axioms of set theory, we already can state and prove russell’s paradox https://en.wikipedia.org/wiki/Russell%27s_paradox

reflects = kd.define("reflects", [P, A], smt.ForAll([x], elem(x, A) == P[x]))
is_set = kd.define("is_set", [P], smt.Exists([A], reflects(P, A)))

# general comprehension is not true. This is Russell's paradox.
@kd.Theorem(smt.Not(smt.ForAll([P], is_set(P))))
def russell(l):
    l.unfold(is_set).unfold(reflects)
    l.assumes(smt.ForAll([P], smt.Exists([A], smt.ForAll([x], elem(x, A) == P[x]))))
    Q = smt.Lambda([x], smt.Not(elem(x, x))) # The class of all sets that do not contain themselves
    l.have(smt.Exists([A], smt.ForAll([x], elem(x, A) == Q[x]))).instan(0, Q).auto()
    A1 = l.obtain(-1)
    l.have(elem(A1, A1) == Q(A1)).instan(-1, A1).auto()
    l.show(smt.BoolVal(False), by=[])

Definition of Subset

le = kd.notation.le.define([A, B], kd.QForAll([x], elem(x, A), elem(x, B)))

Axiom of Extensionality

Sets are extensional. Equality reflects their elem behavior

ext_ax = kd.axiom(
    kd.QForAll([A, B], smt.Eq((A == B), smt.ForAll([x], elem(x, A) == elem(x, B))))
)

Empty Sets

There is an empty set. It has no elements. Because of extensionality, any other set with no elements is the empty set

emp = smt.Const("emp", ZFSet)
elem_emp = kd.axiom(smt.ForAll([x], elem(x, emp) == smt.BoolVal(False)))

@kd.tactics.Theorem(smt.ForAll([A], (A == emp) == smt.Not(smt.Exists([x], elem(x, A)))))
def emp_exists_elem(l):
    _A = l.fix()
    l.split()
    with l.sub() as l1:
        l1.intros()
        l1.intros()
        _x = l1.obtain(-1)
        l1.show(smt.BoolVal(False), by=[ext_ax, elem_emp])
    with l.sub() as l2:
        l2.intros()
        l2.rw(ext_ax)
        _x = l2.fix()
        l2.apply(0)
        l2.exists(_x)
        l2.have(elem(_x, emp) == smt.BoolVal(False), by=[elem_emp(_x)])
        l2.have(elem(_x, _A), by=[])

        l2.auto()


# emp_exists_elem = l.qed()


l = kd.Lemma(smt.ForAll([A], smt.Implies((A != emp), smt.Exists([x], elem(x, A)))))
_A = l.fix()
l.auto(by=[emp_exists_elem(_A)])
l.qed()
not_emp_exists_elem = l.qed()

Picking Elements

Picking an element out of a nonempty set is not a new axiom. It is actually an application of skolemization to the definition of being non empty. https://en.wikipedia.org/wiki/Axiom_of_global_choice

pf1 = kd.prove(
    smt.Exists([x], smt.Implies(a != emp, elem(x, a))), by=[emp_exists_elem(a)]
)
(skolem,), elem_pick0 = kd.tactics.skolem(pf1)
# Note that pick(emp) is undefined. You will not be able to prove anything about it.
pick = kd.define("pick", [a], skolem)

elem_pick = kd.prove(
    smt.Implies(a != emp, elem(pick(a), a)), unfold=1, by=[elem_pick0]
).forall([a])

Unordered Pairs

By fiat, we say there is such a thing as an unordered set. It is a reflection of Or in a sense.

upair = smt.Function("upair", ZFSet, ZFSet, ZFSet)
elem_upair = kd.axiom(
    kd.QForAll([x, y, z], elem(z, upair(x, y)) == smt.Or(z == x, z == y))
)

Some useful properties about upair

l = kd.Lemma(smt.ForAll([a, b], smt.Not(upair(a, b) == emp)))
_a, _b = l.fixes()
l.rw(ext_ax)
l.intros()
l.have(elem(_a, upair(_a, _b)), by=[elem_upair(_a, _b, _a)])
l.have(smt.Not(elem(_a, emp)), by=[elem_emp(_a)])
l.auto()
upair_not_emp = l.qed()

l = kd.Lemma(smt.ForAll([a, b], upair(a, b) == upair(b, a)))
l.fixes()
l.rw(ext_ax)
l.fix()
l.rw(elem_upair)
l.rw(elem_upair)
l.auto()
upair_comm = l.qed()

elem_upair_1 = kd.prove(
    smt.ForAll([a, b], elem(a, upair(a, b)) == smt.BoolVal(True)), by=[elem_upair]
)
elem_upair_2 = kd.prove(
    smt.ForAll([a, b], elem(b, upair(a, b)) == smt.BoolVal(True)), by=[elem_upair]
)


@kd.tactics.Theorem(
    smt.ForAll(
        [a, b, c, d],
        (upair(a, b) == upair(c, d))
        == smt.Or(smt.And(a == c, b == d), smt.And(a == d, b == c)),
    )
)
def upair_inj(l):
    a, b, c, d = l.fixes()
    l.split()
    l.intros()
    l.rw(ext_ax, at=0)
    l.have(elem(a, upair(a, b)), by=elem_upair_1)
    l.have(elem(b, upair(a, b)), by=elem_upair_2)
    l.have(elem(c, upair(c, d)), by=elem_upair_1)
    l.have(elem(d, upair(c, d)), by=elem_upair_2)
    l.auto(by=[elem_upair])
    l.intros()
    l.auto(by=[upair_comm])

pick_upair = kd.prove(
    smt.ForAll([a, b], smt.Or(pick(upair(a, b)) == a, pick(upair(a, b)) == b)),
    by=[elem_pick, elem_upair, elem_emp],
)

Singleton

A derived definition is singleton sets. They are constructed as a unordered pair with itself.

sing = kd.define("sing", [x], upair(x, x))

@kd.tactics.Theorem(smt.ForAll([a, b], elem(a, sing(b)) == (a == b)))
def elem_sing(l):
    a, b = l.fixes()
    l.unfold(sing)
    l.auto(by=[elem_upair])


sing_not_emp = kd.prove(smt.Not(sing(a) == emp), unfold=1, by=[upair_not_emp]).forall(
    [a]
)


@kd.tactics.Theorem(smt.ForAll([a], pick(sing(a)) == a))
def pick_sing(l):
    _a = l.fix()
    l.unfold(sing)
    l.auto(by=[pick_upair])
    # l.rw(ext_ax)
    # _x = l.fix()
    # l.auto(by=[elem_sing, elem_pick, elem_emp])

Axiom of separation

You can filter out the pieces of an existing set. This is kind of a weakened form of general comprehension.

sep = smt.Function("sep", ZFSet, Class, ZFSet)
elem_sep = kd.axiom(
    kd.QForAll([P, A, x], elem(x, sep(A, P)) == smt.And(P[x], elem(x, A)))
)

@kd.Theorem(
    kd.QForAll(
        [a, b, P],
        sep(upair(a, b), P)
        == smt.If(P(a), smt.If(P(b), upair(a, b), sing(a)), smt.If(P(b), sing(b), emp)),
    )
)
def sep_upair(l):
    a, b, P = l.fixes()
    l.rw(ext_ax)
    l.fix()
    l.rw(elem_sep)
    l.cases(P(a))
    l.rw(-1)
    l.cases(P(b))
    l.rw(-1)
    l.simp()
    l.auto(by=[elem_upair])
    l.rw(-1)
    l.simp()
    l.auto(by=[elem_upair, elem_sing])
    l.rw(-1)
    l.cases(P(b))
    l.rw(-1)
    l.auto(by=[elem_upair, elem_sing])
    l.rw(-1)
    l.simp()
    l.auto(by=[elem_emp, elem_upair])

BigUnion Exists

https://en.wikipedia.org/wiki/Union_(set_theory)#Arbitrary_union Big union is a pretty weird operation in my mind and it’s interesting that you axiomatize it.

bigunion = smt.Function("bigunion", ZFSet, ZFSet)
bigunion_ax = kd.axiom(
    kd.QForAll(
        [A, x], smt.Eq(elem(x, bigunion(A)), kd.QExists([B], elem(B, A), elem(x, B)))
    )
)

Binary Union

The more familiar binary union operator

union = kd.define("union", [A, B], bigunion(upair(A, B)))
kd.notation.or_.register(ZFSet, union)

l = kd.Lemma(a | b == b | a)
l.unfold(union)
l.rw(ext_ax)
_x = l.fix()
l.auto(by=[elem_upair, bigunion_ax])
union_comm = l.qed().forall([a, b])

l = kd.Lemma(
    smt.ForAll([x, A, B], elem(x, bigunion(upair(A, B))) == (elem(x, A) | elem(x, B)))
)
_x, _A, _B = l.fixes()
l.rewrite(bigunion_ax)
l.split()
with l.sub() as c1:
    c1.intros()
    _B1 = c1.obtain(0)
    c1.rw(elem_upair, at=0)
    c1.auto()
with l.sub() as c2:
    c2.intros()
    c2.cases(elem(_x, _A))
    c2.exists(_A)
    c2.rw(elem_upair)
    c2.auto()

    c2.exists(_B)
    c2.rw(elem_upair)
    c2.auto()
elem_bigunion_upair = l.qed()


l = kd.Lemma(smt.ForAll([x, A, B], elem(x, A | B) == (elem(x, A) | elem(x, B))))
_x, _A, _B = l.fixes()
l.unfold(union)
l.rw(elem_bigunion_upair)
l.auto()
elem_union = l.qed()


l = kd.Lemma(smt.ForAll([a, b, c], (a | b) | c == a | (b | c)))
_a, _b, _c = l.fixes()
l.rw(ext_ax)
_x = l.fix()
l.rw(elem_union)
l.rw(elem_union)
l.rw(elem_union)
l.rw(elem_union)
l.auto()
union_assoc = l.qed()

l = kd.Lemma(smt.ForAll([a], a | a == a))
l.fixes()
l.rw(ext_ax)
l.fix()
l.rw(elem_union)
l.auto()
union_idem = l.qed()

l = kd.Lemma(smt.ForAll([a, b, c], a <= a | b))
l.fixes()
l.unfold(le)
l.fix()
l.rw(elem_union)
l.auto()
le_union = l.qed()


@kd.tactics.Theorem(smt.ForAll([a, b], sing(a) | upair(a, b) == upair(a, b)))
def sing_union_upair(l):
    a, b = l.fixes()
    l.rw(ext_ax)
    l.fix()
    l.rw(elem_union)
    l.rw(elem_upair)
    l.rw(elem_sing)
    l.auto()

@kd.tactics.Theorem(smt.ForAll([a, b], bigunion(upair(a, b)) == a | b))
def bigunion_upair(l):
    a, b = l.fixes()
    l.rw(ext_ax)
    _ = l.fix()
    l.rw(elem_bigunion_upair)
    l.rw(elem_union)
    l.auto()

Big Intersection

Big intersection, unlike big union, is defined in term of previous constructions.

# Biginter
biginter = kd.define(
    "biginter",
    [a],
    sep(pick(a), smt.Lambda([x], kd.QForAll([b], elem(b, a), elem(x, b)))),
)
# huh. biginter(emp) is undefined since we can't pick from it.
l = kd.Lemma(
    smt.ForAll(
        [A, x],
        smt.Implies(
            A != emp, elem(x, biginter(A)) == kd.QForAll([b], elem(b, A), elem(x, b))
        ),
    )
)
_A, _x = l.fixes()
l.intros()
l.unfold(biginter)
l.rw(elem_sep)
l.simp()
l.split()
l.intros()
l.split()
l.auto()
l.have(elem(pick(_A), _A), by=[elem_pick])
l.auto()

l.intros()
_b = l.fix()
l.intros()
l.have(elem(pick(_A), _A), by=[elem_pick])
l.auto()
elem_biginter = l.qed()

Intersection

Intersection is also not a new axiom. It can be defined using separation.

inter = kd.define("inter", [A, B], sep(A, smt.Lambda([x], elem(x, B))))
kd.notation.and_.register(ZFSet, inter)

l = kd.Lemma(smt.ForAll([x, A, B], elem(x, A & B) == (elem(x, A) & elem(x, B))))
l.fixes()
l.unfold(inter)
l.rw(elem_sep)
l.auto()
elem_inter = l.qed()

l = kd.Lemma(smt.ForAll([A, B], biginter(upair(A, B)) == inter(A, B)))
_A, _B = l.fixes()
l.rw(ext_ax)
l.have(upair(_A, _B) != emp, by=[upair_not_emp(_A, _B)])
_x = l.fix()
l.rw(elem_inter)
l.auto(by=[elem_biginter, elem_upair])
biginter_upair_inter = l.qed()

l = kd.Lemma(smt.ForAll([A, B], A & B == B & A))
l.fixes()
l.rw(ext_ax)
l.fix()
l.rw(elem_inter)
l.rw(elem_inter)
l.auto()
inter_comm = l.qed()

l = kd.Lemma(smt.ForAll([a, b, c], (a & b) & c == a & (b & c)))
l.fixes()
l.rw(ext_ax)
l.fix()
l.rw(elem_inter)
l.rw(elem_inter)
l.rw(elem_inter)
l.rw(elem_inter)
l.auto()
inter_assoc = l.qed()


l = kd.Lemma(smt.ForAll([a], a & a == a))
l.fixes()
l.rw(ext_ax)
l.fix()
l.rw(elem_inter)
l.auto()
inter_idem = l.qed()


l = kd.Lemma(smt.ForAll([a, b, c], a & (b | c) == (a & b) | (a & c)))
l.fixes()
l.rw(ext_ax)
l.fix()
l.rw(elem_inter)
l.rw(elem_union)
l.rw(elem_inter)
l.rw(elem_union)
l.rw(elem_inter)
l.auto()
inter_union_distr = l.qed()

l = kd.Lemma(smt.ForAll([a, b], a & b <= a))
l.fixes()
l.unfold(le)
l.fix()
l.rw(elem_inter)
l.auto()
inter_le = l.qed()


@kd.Theorem(smt.ForAll([a, b, x], (x <= (a & b)) == ((x <= a) & (x <= b))))
def le_inter_2(l):
    a, b, x = l.fixes()
    l.unfold(le)
    l.split()
    l.auto(by=[elem_inter])
    l.auto(by=[elem_inter])


l = kd.Lemma(smt.ForAll([x], x & emp == emp))
l.fixes()
l.rw(ext_ax)
l.fix()
l.rw(elem_inter)
l.rw(elem_emp)
l.auto()
inter_emp = l.qed()


l = kd.Lemma(smt.ForAll([a, b, c], (a | b) & c == (a & c) | (b & c)))
l.fixes()
l.auto(by=[inter_comm, inter_union_distr])
union_inter_distr = l.qed()


@kd.tactics.Theorem(
    smt.ForAll(
        [a, b, c],
        inter(a, upair(b, c))
        == smt.If(
            elem(b, a),
            smt.If(elem(c, a), upair(b, c), sing(b)),
            smt.If(elem(c, a), sing(c), emp),
        ),
    )
)
def inter_upair_2(l):
    a, b, c = l.fixes()
    l.unfold(inter)
    l.rw(ext_ax)
    _x = l.fix()
    l.rw(elem_sep)
    l.simp()
    l.rw(elem_upair)
    l.cases(elem(b, a))
    l.rw(-1)
    l.cases(elem(c, a))

    l.rw(-1)
    l.simp()
    l.rw(elem_upair)
    l.auto()

    l.rw(-1)
    l.simp()
    l.rw(elem_sing)
    l.auto()

    l.rw(-1)
    l.cases(elem(c, a))
    l.rw(-1)
    l.simp()
    l.rw(elem_sing)
    l.auto()

    l.rw(-1)
    l.simp()
    l.auto(by=[elem_emp])


inter_upair_1 = kd.prove(
    smt.ForAll(
        [a, b, c],
        inter(upair(b, c), a)
        == smt.If(
            elem(b, a),
            smt.If(elem(c, a), upair(b, c), sing(b)),
            smt.If(elem(c, a), sing(c), emp),
        ),
    ),
    by=[inter_upair_2, inter_comm],
)

Set Difference

sub = kd.notation.sub.define([A, B], sep(A, smt.Lambda([x], smt.Not(elem(x, B)))))


@kd.Theorem(kd.QForAll([a, b], upair(a, b) - sing(a) == smt.If(a == b, emp, sing(b))))
def upair_sub_sing(l):
    a, b = l.fixes()
    l.unfold(sub)
    l.rw(sep_upair)
    l.simp()
    l.rw(elem_sing)
    l.rw(elem_sing)
    l.simp()
    l.auto()

Ordered Pairs

Set theory has some standard encodings of the concept of pair https://en.wikipedia.org/wiki/Ordered_pair#Defining_the_ordered_pair_using_set_theory . We’re using Kuratowski pairs. It is odd to me that pair is not more primitive than upair, but I was indoctrinated in computer.

pair = kd.define("pair", [a, b], upair(sing(a), upair(a, b)))
is_pair = kd.define("is_pair", [c], smt.Exists([a, b], pair(a, b) == c))
fst = kd.define("fst", [p], pick(biginter(p)))
snd = kd.define(
    "snd",
    [p],
    smt.If(sing(sing(fst(p))) == p, fst(p), pick(bigunion(p) - sing(fst(p)))),
)


@kd.Theorem(smt.ForAll([a, b], is_pair(pair(a, b)) == smt.BoolVal(True)))
def is_pair_pair(l):
    a, b = l.fixes()
    l.unfold(is_pair)
    l.auto()


@kd.tactics.Theorem(
    smt.ForAll([a, b, c, d], (pair(a, b) == pair(c, d)) == smt.And(a == c, b == d))
)
def pair_inj(l):
    a, b, c, d = l.fixes()
    l.unfold(pair)
    l.unfold(sing)
    l.split()
    l.intros()
    l.rw(upair_inj, at=0)
    l.auto(by=[upair_inj])
    l.intros()
    l.auto(by=[upair_comm])


@kd.tactics.Theorem(smt.ForAll([a, b], fst(pair(a, b)) == a))
def fst_pair(l):
    a, b = l.fixes()
    l.unfold(fst)
    l.unfold(pair)
    l.rw(biginter_upair_inter)
    l.rw(inter_upair_2)
    l.rw(elem_sing)
    l.rw(elem_sing)
    l.simp()
    l.cases(b == a)

    # case a == b
    l.rw(-1)
    l.simp()
    l.auto(by=[pick_upair])

    # case a != b
    l.rw(-1)
    l.simp()
    l.auto(by=[pick_sing])


@kd.tactics.Theorem(smt.ForAll([a, b], snd(pair(a, b)) == b))
def snd_pair(l):
    a, b = l.fixes()
    l.unfold(snd)
    l.rw(fst_pair)
    l.cases(sing(sing(a)) == pair(a, b))

    l.rw(-1)
    l.simp()
    l.unfold(sing, at=0)
    l.unfold(pair, at=0)
    l.unfold(sing, at=0)
    l.auto(by=[upair_inj])

    l.rw(-1)
    l.simp()
    l.unfold(pair)
    l.rw(bigunion_upair)
    l.rw(sing_union_upair)
    l.rw(upair_sub_sing)
    l.have((a == b) == smt.BoolVal(False))
    l.unfold(pair, at=0)
    l.unfold(sing, at=0)
    l.auto(by=[upair_inj])
    l.rw(-1)
    l.simp()
    l.rw(pick_sing)
    l.auto()


@kd.tactics.Theorem(
    smt.ForAll([a, b, x], elem(x, pair(a, b)) == smt.Or(x == sing(a), x == upair(a, b)))
)
def elem_pair(l):
    a, b, c = l.fixes()
    l.unfold(pair)
    l.rw(elem_upair)
    l.auto()

Bits and Bobbles

I’m very happy these were going through.

Doing some basic proofs showed some holes in my tactic system which I patched up. I still don’t have a nice way to rewrite under binders.

The new Theorem combinator and chaining of tactics makes things more compact and look nicer. You can see some different looks and styles I’ve been trying out. I haven’t updated all proofs to a consistent style.

Despite being based on z3, sometimes proofs were painfully manual. I could do some things

https://isabelle.in.tum.de/dist/Isabelle2025/doc/logics-ZF.pdf https://lawrencecpaulson.github.io/2022/04/06/ZFC_in_HOL.html https://www.isa-afp.org/entries/ZFC_in_HOL.html

Despite its abstractness, set theory is probably one of the easier pieces of mathematics to formalize, because it is so close to logic itself.

Mizar? https://thmprover.wordpress.com/about/

An (fixed) unsoundness in knuckledragger

I had a skolem rule that could get you a skolem constant. I also had a notion of free variable. I wasn’t making sure the skolems depended on the free variables in the expression. The following proof of False was possible. I added a sweep through in the skolem axiom to find free constants in the expression.

from kdrag.all import *
# Bascially I can't have the ability to skolem and universal var because they enable me to swap exists and forall.
N = kd.FreshVar("N", smt.IntSort())
x = smt.Const("x", smt.IntSort())
pf1 = kd.prove(smt.Exists([x], x > N))
xs, pf2 = kd.tactics.skolem(pf1)
pf3 = pf2.forall([N])(xs[0] + 1)
pf3
kd.prove(smt.BoolVal(False), by=[pf3])