git @ Cat's Eye Technologies Eqthy / master eg / interior-algebra.eqthy.md
master

Tree @master (Download .tar.gz)

interior-algebra.eqthy.md @master — view rendered · raw · history · blame 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
Interior Algebra
================

<!--
SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
For more information, please refer to <https://unlicense.org/>
SPDX-License-Identifier: Unlicense
-->

[Interior algebra (Wikipedia)](https://en.wikipedia.org/wiki/Interior_algebra)
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)](https://en.wikipedia.org/wiki/Kuratowski_closure_axioms)
too, to similar effect: they also define the fundamental topological closure operation.)

Requires [Set Difference](set-difference.eqthy.md)
(which itself is based on [Boolean algebra](boolean-algebra.md)).

    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