Set Difference

Some theorems about set difference.

These theorems, as usually stated, are based on an Algebra of sets (Wikipedia). However, we will use Boolean algebra as their basis here. (I'm given to understand that these two theories are subtlely different, but I've concluded that the difference, if there is one, is too subtle to matter for our purposes; all the axioms and properties we care about are shared by the two, and it is only a matter of adjusting the nomenclature.)

Requires Boolean algebra.

Definition of set difference.

axiom (#diff)          diff(A, B) = and(A, not(B))

A theorem about set difference: difference distributes over union.

theorem (#diff-union-distrib)
    or(diff(A, C), diff(B, C)) = diff(or(A, B), C)
proof
    or(diff(A, C), diff(B, C)) = or(diff(A, C), diff(B, C))
    or(diff(A, C), diff(B, C)) = or(diff(A, C), and(B, not(C)))
    or(diff(A, C), diff(B, C)) = or(and(A, not(C)), and(B, not(C)))
    or(diff(A, C), diff(B, C)) = or(and(A, not(C)), and(not(C), B))
    or(diff(A, C), diff(B, C)) = or(and(not(C), A), and(not(C), B))
    or(diff(A, C), diff(B, C)) = and(not(C), or(A, B))
    or(diff(A, C), diff(B, C)) = and(or(A, B), not(C))
    or(diff(A, C), diff(B, C)) = diff(or(A, B), C)
qed

Another theorem about set difference: the difference of A and B is the same as the difference of A and the intersection of A and B.

theorem (#diff-of-inter-is-diff)
    diff(A, B) = diff(A, and(A, B))
proof
    diff(A, B) = diff(A, B)
    diff(A, B) = and(A, not(B))
    diff(A, B) = or(and(A, not(B)), 0)
    diff(A, B) = or(0, and(A, not(B)))
    diff(A, B) = or(and(A, not(A)), and(A, not(B)))
    diff(A, B) = and(A, or(not(A), not(B)))
    diff(A, B) = and(A, not(and(A, B)))
    diff(A, B) = diff(A, and(A, B))
qed

Both of these theorems were adapted from this presentation by Mustafa Jarrar.