Interior Algebra

Interior algebra (Wikipedia) corresponds to both the rules of general topology, and the modal logic S4, which I think is pretty neat. So it would be nice to formalize it in Eqthy.

Alas, as it is usually stated, it is not purely equational. One of its axioms is a subset relationship rather than an equality relationship:

interior(x) ⊆ x

However, that can be overcome by observing that we can rewrite this relation in terms of set difference and the empty set:

interior(x) ∖ x = ∅

So, as long as we have set difference, we can state the axioms, and maybe even some simple results in interior algebra! (We could state the Kuratowski closure axioms (Wikipedia) too, to similar effect: they also define the fundamental topological closure operation.)

Requires Set Difference (which itself is based on Boolean algebra).

axiom (#interior-closed)   diff(interior(X), X) = 0
axiom (#interior-idem)     interior(interior(X)) = interior(X)
axiom (#interior-distrib)  interior(and(X, Y)) = and(interior(X), interior(Y))
axiom (#interior-total)    interior(1) = 1

We can define the closure operator in terms of the interior operator.

axiom (#clos)              clos(X) = not(interior(not(X)))

This is the dual of the interior. Duals of the above axioms all hold. We can prove them as theorems.

But first, here is a trivial and rather uninteresting proof about the interior operator.

theorem
    interior(and(X, and(Y, Z))) = and(interior(X), and(interior(Y), interior(Z)))
proof
    interior(and(X, and(Y, Z))) = interior(and(X, and(Y, Z)))
    interior(and(X, and(Y, Z))) = and(interior(X), interior(and(Y, Z)))
    interior(and(X, and(Y, Z))) = and(interior(X), and(interior(Y), interior(Z)))
qed

Right, so, onto the closure operator.

theorem (#closure-total)
    clos(0) = 0
proof
    clos(X) = clos(X)
    clos(X) = not(interior(not(X)))
    clos(0) = not(interior(not(0)))   [by substitution of 0 into X]
    clos(0) = not(interior(1))
    clos(0) = not(1)
    clos(0) = 0
qed