We report on a proof-checked version of Stone's result on the representability of Boolean algebras via the clopen sets of a totally disconnected compact Hausdor↵ space. Our experiment is based on a proof verifier based on set theory, whose usability can in its turn benefit from fully formalized proofs of representation theorems akin to the one discussed in this note.
Introduction
This paper reports on a formally verified proof of Stone’s celebrated results
[
A website reporting on our experiment is at http://www2.units.it/eomodeo/ StoneReprScenario.html. In its final form, the script-file supporting it and leading from first principles to the topological version of Stone’s result, comprises 42 definitions and proves 210 theorems altogether, organized in 19 Theory s, including the background Theory Set theory. Its processing takes about 25 seconds. ? Work partially supported by the INdAM/GNCS 2013 project “Specifica e verifica di algoritmi tramite strumenti basati sulla teoria degli insiemi” and by the Academy of Finland under grant 250345 (CoECGR) 1
Boolean algebras and rings A ring is said to be Boolean when every one of its elements is self-inverse w.r.t. addition and idempotent w.r.t. multiplication:
X + X = 0 ,
X · X = X .
The former of these laws makes it superfluous to postulate the commutativity of addition (for, it implies it); the latter implies the commutativity of multiplication. When endowed with multiplicative identity, 1, a Boolean ring is called a Boolean algebra. (To avoid trivialities, we will require that 06=1).
An aspect of the richness of Boolean rings is that the relation
X 6 Y $ Def X · Y = X is a partial order, in which every pair X, Y of elements has greatest common lower bound X u Y = X · Y and least common upper bound X t Y = X · Y + X +Y . In this ordering 0 acts as the minimum and—when present—1 acts as the maximum. Historically, Boolean algebras were first studied as lattices endowed with peculiar properties (namely, distributivity and complementedness).4 The salient operations, from this viewpoint, were u, t, ; the algebraic kinship with the rings of numbers remained unnoticed for quite a while (cf.[9, p. 208]).
From the ring-based point of view—the one which will prevail in these pages— the complementation operation turns out to be: X =Def 1 + X.
X 2 B ! {X, Y } ✓ B ! {X, Y } ✓ B !
X 2 B ! {X, Y } ✓ B ! {U, V, X, Y } ✓ B
X 2 B & X = X & 1B = 0B & 0B = 1B
X + X = 1B & Y · X + Y · X = Y & (Y · X) · (Y · X) = 0B
X + Y = X · Y + X · Y
X 6= X & (X 2 /{ 0B, 1B} ! X 2 B \ { 0B, 1B})
(X · Y = 1B ! X = 1B & Y = 1B)
! U · X + V · Y = (U · X + V · Y ) · X · Y
4 From the lattice-based point of view, the simplest available characterization of the
structure ‘Boolean algebra’ is the one proposed by Herbert Robbins, ca. 1933 (cfr.
[
X t Y = Y t X, X t (Y t Z) = (X t Y ) t Z, X t Y t X t Y = X. 2
Fields of sets Starting with a non-void set S, let us construct the following families of sets:5 – P(S) =Def { x : x ✓ S } , the family of all subsets of S; – F(S) =Def { x ✓ S | |x| 2 N } , the family of all finite subsets of S; – B(S) =Def F(S) [ { S \ x : x 2 F(S) } , the family formed by those subsets
of S each of which is either finite or has a finite complement (relative to S).
If S is finite, P(S) = F(S) = B(S) holds; otherwise, we get three families.
To get Boolean rings out of these, it suces to define:
X · Y =Def X \ Y (intersection),
X + Y =Def (X [ Y ) \ (X \ Y ) (symmetric di↵erence ).
One readily sees that P(S) and B(S) thus become Boolean algebras, whose additive identity, 0, and multiplicative identity, 1, are ; and S; as for F(S), it lacks 1 when S is infinite.
By generalizing the case of P(S) and B(S), one calls field of sets any family B which – is closed under the operations of intersection and symmetric di↵erence; – has S B among its members, viz., owns a maximum w.r.t. set inclusion; – di↵ers from {;} .
This clearly is an instance of a Boolean algebra. How general? A renowned
theorem by Marshall H. Stone [
Every Boolean algebra is isomorphic to a field of sets.
This field is not always of the form P(S) (this holds only for particular Boolean algebras, among which the ones whose underlying domain is finite6): in fact it is trivial that the field B(N), whose cardinality equals the one of N, cannot be isomorphic to P(S) for any S.7 3
Stone spaces We define a base of a topological space to be a pair (X , ) such that: (i) X 6= ; ; (ii) ✓ P(X ); (iii) enjoys, w.r.t. dyadic intersection, \ , and to monadic union, S, the following closure properties: 5 We designate by |X| the cardinality of a set X and by N the set {0, 1, 2, . . . } of all natural numbers (which is, in its turn, a cardinal number—the first infinite one). 6 More generally, the Boolean algebras which are isomorphic to P(S) for some S are the ones which are completely distributive; [2, pp. 221–222] credits this result to
Alfred Tarski. 7 Indeed, |P(S)| 2 N (i.e., |P(S)| is smaller than the cardinal number N) when |S| 2 N; whereas |P(S)| exceeds N—because |P(S)| exceeds |S|—when S is infinite. 1) S 2) (A 2 = X , & B 2 ) ! (A \ B) ✓
S{ c 2
| c ✓ (A \ B) }.
The topological space generated by such a base is, by definition, the pair (X , ⌧ ) where ⌧ = { S a : a ✓
} .
A topological space hence is a pair (X , ⌧ ) such that: (i) X 6= ; ; (ii) ⌧ ✓ P(X ); (iii) ⌧ enjoys, w.r.t. dyadic intersection, \ , and to monadic union, S, the following closure properties: – X 2 ⌧ , – A, B 2 ⌧ ! (A \ B) ✓ – A 2 P(⌧ ) ! S A 2 ⌧ ,
S{ c 2 ⌧ | c ✓ (A \ B) }, whence it plainly follows that A, B 2 ⌧ ! A \ B 2 ⌧ and, more generally, that A 2 F(⌧ ) ! T A 2 ⌧ , under the proviso that the intersection T ; equals X .
The open and the closed sets of such a space are, respectively, the members of ⌧ and their complements X \ A (with A 2 ⌧ ). A subset of X which is open and closed is called a clopen set: examples are ; and X . It is apparent that clopen sets form a field of sets.
A topological space is said to be a Hausdorff space if: for every pair of distinct members p, q 2 X , there exist
disjoint open sets P, Q ✓ X such that p 2 P , q 2 Q;8 compact if: every family of open sets whose union is X includes a finite sub
family whose union is X .
One calls Stone space any topological space which, in addition to enjoying the two properties just stated, also – owns a base—namely a ✓ ⌧ such that every open set is the union of a subfamily of —entirely formed by clopen sets.
By relying on these concepts, one enhances the claim of Stone’s theorem as
follows (cf. [
Every Boolean algebra is isomorphic to a field of sets consisting of the clopen sets of a Stone space.
In sight of the proof of this theorem, it is worthwhile to recall another way of stating the compactness property, dual to the one proposed above:
A topological space (X , ⌧ ) is compact if and only if every (non-void) family C of closed sets whose intersection T C is void has some finite subfamily whose intersection is void : F ✓ C , |F | 2 N \ {0}, T F = ; . 8 This definition implies that in a Hausdor↵ space every singleton subset of X is closed. 4
Boolean ideals and their maximal enlargements The study of an abstract algebraic structure forcibly leads one to investigate the associated homomorphisms. In the Boolean case at hand, to move resolutely in the direction that best suits our purposes, we will just consider those homomorphisms which translate the operations of a Boolean algebra (the homomorphism’s domain) into the set-operations \ , 4 of intersection and symmetric di↵erence. The images of such a homomorphism will hence form a field of sets; particularly worth of consideration, among the homomorphisms of interest, are the ones whose values form the special field 2 = ; , {;} , \ , 4, {;} , ; .
Let us refer by B = (B, ·, +, 1B, 0B) to a Boolean algebra which, tacitly, will act as domain of the homomorphisms that will enter into play. A homomorphism of B into 2 is fully characterized by either one of the two subsets of the underlying domain B which are counter-images, respectively, of 0 = ; and of 1 = {;} . Not all subsets of B can play the role of counter-images of the minimum via a Boolean homomorphism; let us hence figure out which conditions a set must meet in order to qualify for such a role. In investigations of this nature, algebraists tend to focus on the counter-images of the minimum, the so-called ideals, or ‘kernels’; logicians, on the opposite, tend to focus on the counter-images of the maximum, the so-called filters, or ‘shells’. We will conform to the algebraic habit; moreover, since we must concentrate mainly on homomorphisms into 2, we will tribute special attention to ideals which are maximal w.r.t. to set inclusion.
Definition 1. An ideal is a subset of the underlying domain B which is closed with respect to addition, as well as to multiplication of its elements by elements of B, and which is not one of the (exceedingly trivial) sets ; , {0B}, B.
Three theorems about ideals play a crucial role in the proof of Stone’s results: a) Every element x of B which is neither 1B nor 0B belongs to at least one ideal: the least such ideal, named a principal ideal, is simply formed by the multiples of x. It hence follows, save in the case when B = {0B, 1B}, that there is at least one ideal. b) To each ideal I and each x 6= 1B not belonging to I, there corresponds an ideal J ◆ I one of whose elements is x: this is {a · x + y : a 2 B , y 2 I}. c) Every ideal I is included in an ideal which is maximal w.r.t. ✓ .
Checking the first two of these is very plain; the third can be proved by means of Zorn’s lemma, after observing that every chain of ideals is closed w.r.t. union. 5
1st Stone’s representation theorem Let us recall first the algebraic version of Stone’s theorem: Theorem 1 (Stone’s algebraic representation). Every Boolean algebra
B = (B, ·, +, 1B, 0B) is isomorphic to a field H of sets whose underlying domain is included in P(H), where H is the set of all homomorphisms from B into 2.
Proof. Associate with each x 2 B the set x of those homomorphisms in H which e send x to {;} ; thus, clearly, 0fB = ; and 1fB = H. Moreover xg· y = xe \ ye holds: in fact, when h is a homomorphism, h(x · y) = h(x) \ h(y) equals {;} if and only if h(x) = h(y) = {;} , i.e. i↵ h 2 xe \ y. By an analogous argument, e h(x + y) = h(x) 4 h(y) and x]+ y = xe 4 ye. Take H to be the image-set of the function x 7! x.
e
In order to see the injectivity of this function, consider the di↵erence e0 = x0 + x0 · x1 between two elements x0, x1 2 B such that x0 · x1 6= x0 (whence e0 6= 0B). We will show that there is an h 2 H sending e0 to 1B; accordingly, since 1B = h(e0) = h(x0 + x0 · x1) = h(x0) 4 h(x0) \ h(x1) , we will have h(x0) = {;} , h(x1) = ; , and therefore h 2 xe0 \ xe1 as desired. We readily get the sought h if B = {0B, 1B}; otherwise we pick a y0 2 B \ { 0B, 1B}, choosing y0 = e0 if e0 6= 1B. This y0 belongs to a principal ideal and hence to a maximal ideal M , and it is plain that the opposite h = 1 M of the characteristic function of M , manifestly a homomorphism from B to 2, does to our case. a
Call set-representation of the algebra B the field of sets just built. We will see next that this H generates a very peculiar topology on H. 6
2nd Stone’s representation theorem We are now ready for the topological version of Stone’s theorem: Theorem 2 (Stone’s topological representation). The field of sets by which we have represented a Boolean algebra B is the base—as well as the family of all clopen sets—of a topology on the set H of all homomorphisms from B into 2. Once endowed with such a topology, H turns out to be a Stone space.
Proof. To see that H (constructed as in the preceding proof) is the base of a topology on H, we can directly check that H ✓ P(H) and S H = H 6= ; hold, and that T F belongs to H for every finite non-void subset F of H. Indeed, H is the image-set of an injective function x 7! xe from B into P(H), where B is at least doubleton; hence, readily, H 6= ; , H ✓ P(H), and S H ✓ H hold. The last inclusion is in fact an equality, because H, which is 1fB, belongs to H. Then we get that H is closed under intersection through the remark, made above, that xe \ ye = xg· y.
Knowing, at this point, that H qualifies as the base for a topology on H, let us notice that all sets in H are clopen in the topology ⌧ generated by it: in fact, since H \ xe = H 4 xe = 1fB 4 xe = 1^B+ x, the complement of a set in the base belongs to the base in its turn. This remark readily gives us that (H, ⌧ ) is a Hausdor↵ space. In fact, when f, g 2 H di↵er, there is an x 2 B such that f (x) = 1 $ g(x) 6= 1; thus, since H \ xe = xe, we can find sets u, v 2 ⌧ such that f 2 u, g 2 v, and u \ v = ; , by also insisting that {u, v} = {xe, xe}.
It remains to be shown that the space is compact, which will also yield that every clopen set of ⌧ belongs to H.9 One easily sees that the closed sets in ⌧ are: H and all intersections of non-void subsets of {xe : x 2 B} ; compactness will hence readily follow if we manage to show that whenever ; 6 = O ✓ H and T O = ; hold, there is an F ✓ O such that |F | 2 N \ {0} and T F = ; . Equivalently, assuming that ; 6 = O ✓ H and that T F =6 ; holds for every finite non-void subset F of O, we will show that T O 6= ; .
Notice that the subset
n B0 =Def x : F ✓ O | |F | 2
o
N \ {0} & xe = \ F [ { 1B} of B meets the conditions: 1) x · y 2 B 0 for all x, y 2 B 0 , 2) 0B 2 /B 0 6✓ { 1B}, implying that { a · x : a 2 B , x 2 B 0 } is an ideal of B. By enlarging this into a maximal ideal, we get the kernel of a homomorphism h sending all complements of el’ts of B0 to ; , hence sending all elements of B0 to {;} . Thus, h 2 T O. a 7
Formalization of Stone’s representation theorems in Ref This section o↵ers glimpses of our formal development of Stone’s result on the representability of Boolean algebras via the clopen sets of a totally disconnected, compact Hausdor↵ space. In carrying out this task, we relied on a proof checker: Ref. Our experiment culminated in a rather elaborate series of mathematical claims, shown not in this section, but in the appendix.
Organization and rationale of our automated proof assistant are extensively
discussed in [
Brief presentation of the proof-checking framework Ref is a proof assistant for mathematics based on a variant of Zemelo-Fraenkel set theory, which is “hardwired” in Ref’s proof-checking abilities. From the user Ref receives script files, called scenarios, consisting of successive definitions, theorems, and auxiliary commands, which it either certifies as constituting a valid sequence or rejects as defective. In the case of rejection, the verifier attempts to pinpoint the troublesome locations within a scenario, so that errors can be 9 To derive from compactness that S O 2 H holds when O ✓ H and S O is closed, we argue as follows. Assuming, w.l.o.g., that ; 6 = O, since ; = (S O) \ (H \ S O) = (S O) \ T{H \ u : u 2 O} is the intersection of a family of closed sets, we can pick an F such that ; 6 = F ✓ O , |F | 2 N, and (S O) \ T{H \ u : u 2 F } = ; . Thus S O = T{H \ u : u 2 F } 2 H, because H is closed relative to complementation and to finite intersection. located and repaired. Step timings are produced even for correct proofs, to help the user in spotting places where appropriate modifications could speed up proof processing.
The bulk of the text normally submitted to the verifier consists of theorems and proofs. Some theorems (and their proofs) are enclosed within so-called Theorys, whose external conclusions are justified by these internal theorems. This lets scenarios be subdivided into modules, which increases the readability and supports proof reuse.
Many theorems are not enclosed within a user-defined Theory; when this happens, they belong on their own right to the underlying “big” Theory identified by the name Set theory.
Of all relationships treated within Set theory, the most fundamental is membership, 2 , which is supposed to be well founded in the sense that no infinite sequence x0, x1, x2, . . . of sets can satisfy xi+1 2 xi for every i. The well foundedness of 2 is witnessed by the built-in arbitrary selection operator, arb, meeting the conditions arb(x) 2 x and arb(x) \ x = ; for every set x other than the null set ; (about which the equality arb(; ) = ; is assumed).
At their simplest definitions are merely abbreviations which concentrate attention on interesting constructs by assigning them names which shorten their syntactic form (an example of this kind is the definition of finitude that we will soon meet). Beyond this simple level, Ref o↵ers a primitive scheme of 2 -recursive definition legitimatized by the well foundedness of 2 and illustrated, e.g., by the following specification:
Def : [Join singletons] filum(X) =Def {X} [ arb filum(y) : y 2 X | X = {y} (This collects together into filum(X) all elements of the finitely many singletons “spreading”—in a quite definite sense—from {X}.)
This example also shows the availability, in the formal language of Ref, of perspicuous set-formers such as filum(y) : y 2 X | X = {y} . Just in order to see a few other set-formers at work, consider the following shorthand definitions:
S Y =Def { z : x 2 Y , z 2 x} , edges(V, E) =Def {x, y} : x 2 V, y 2 V | x 6= y \ E ,
Connected(E) $ Def {b : b ✓ E | S b \ S(E \ b) = ;} ✓ {; , E} .
A very small Ref scenario, consisting of one definition (involving yet another set-former) and two theorems with their proofs, is shown in Fig. 2. As one sees there, each inference step in a Ref proof has two components, separated by the ‘) ’ sign: on the right of which a logical statement (sometimes hidden behind one of the keywords Auto, Qed) appears; while, on the left, there is a justification of the statement, namely an indication of which inference method enables its derivation from the preceding part of the proof.
Last but not least, Ref supports proof reuse through a costruct named Theory, essentially a second-order form of Skolemization. Fig. 3 shows the interface of a specific Theory, named finite image, which has two input parameters: s0, a
Def P: [Family of all subsets of a given set] PS =Def {x : x ✓ S} Thm pow0: [No set equals its own powerset] (X ◆ Y $ Y 2 PX) & X 6= PX. Proof:
Suppose not(x0, y0) ) Auto Use def(Px0) ) Auto Suppose ) x0 = Px0 ELEM ) Stat0 : x0 2 /{ y : y ✓ x0} hx0i,! Stat0 ) false; Discharge ) Auto EQUAL ) Stat1 : x0 ◆ y0 6= y0 2 { y : y ✓ x0} Suppose ) Stat2 : y0 2 { y : y ✓ x0} hy1i,! Stat2(Stat1?) ) false; Discharge ) Stat3 : y0 2 /{ y : y ✓ x0} hy0i,! Stat3(Stat1?) ) false; Discharge ) Qed Thm pow1: [Monotonicity of powerset] S ◆ X ! PX [ {; , X} ✓ PS. Proof:
Suppose not(s0, x0) ) Auto Set monot ) {x : x ✓ x0} ✓ {x : x ✓ s0} Use def(P) ) Stat1 : ; 2 /{ x : x ✓ s0} _ x0 2 /{ x : x ✓ s0} h; , x0i,! Stat1 ) false; Discharge ) Qed Thm pow2: [Powerset of null set and of singletons] P; = {;} &
P {X} = {; , {X}} . Proof: Suppose not(x0) ) Auto Suppose ) P; 6 = {;} h; , ; i,! T pow1 ) Stat0 : P; 6✓ {;} hy0i,! Stat0(Stat0?) ) Stat1 : y0 2 P; & y0 2 /{;} h; , y0i,! T pow0(Stat1?) ) false; Discharge ) h {x0} , {x0} i,! T pow1 ) Stat2 : P {x0} 6✓ {; , {x0}} hy1i,! Stat2 ) Stat3 : y1 2 P {x0} & y1 2 /{; , {x0}} h {x0} , y1i,! T pow0(Stat3?) ) false; Discharge ) finite set, and g, a global function. Inside finite image, from the assumed finiteness of s0 the user has derived that { g(x) : x 2 s0 } is a finite set; moreover, (s)he has defined the output parameter f⇥ so as to insure that f⇥ be an ✓ -minimal subset of s0 such that f⇥ and s0 are sent by g to the same image.
Theory finite image (s0 , g(X))
Finite(s0) ) f⇥
Finite { g(x) : x 2 s0 } f⇥ ✓ s0 & h 8 t ✓ f⇥ | g(t) = g(s0) $ t = f⇥ i
End finite image 7.2
Excerpts from our proof scenario of Stone’s theorems As a warm-up exercise, we developed with the assistance of Ref the Theory pord displayed in Fig. 4, showing that every partially ordered set is isomorphic to a family of sets partially ordered by inclusion. The assumptions of pord state that Le must be a partial ordering of dd. By sending each element x of dd to the set consisting of those elements of dd which are smaller than or equal to x, we get an order monomorphism between (dd, Le) and (P(dd), ✓ ): whose name ‘poIso⇥ ’, as indicated by the subscript ⇥ , is specified—along with its definition—inside the Theory.
Theory pord dd, Le(U, V) h8 x, y | {x, y} ✓ dd ! Le(x, y) & Le(y, x) $ x = y i h8 x, y, z | {x, y, z} ✓ dd ! Le(x, y) & Le(y, z) ! Le(x, z)i ) (poIso⇥ ) poIso⇥ = {[x, {v 2 dd | Le(v, x)}] : x 2 dd} h8 x | x 2 dd ! Le(x, x) & poIso⇥ x = {v 2 dd | Le(v, x)} i h8 x, y | {x, y} ✓ dd ! Le(x, y) $ poIso⇥ x ✓ poIso⇥ y i 1–1(poIso⇥ ) & domain(poIso⇥ ) = dd
End pord Our next step consisted in developing a theory of Boolean rings: Theory booleanRing(bb, ·, ÷) bb 6= ; h8 x, y | {x, y} ✓ bb ! x · y 2 bbi h8 x, y | {x, y} ✓ bb ! x ÷ y 2 bbi h8 x, y, z | {x, y, z} ✓ bb ! x · (y · z) = (x · y) · zi h8 x, y, z | {x, y, z} ✓ bb ! x ÷ (y ÷ z) = (x ÷ y) ÷ zi h8 x, y, z | {x, y, z} ✓ bb ! (x ÷ y) · z = z · y ÷ z · xi h8 x, y | {x, y} ✓ bb ! x ÷ x = y ÷ yi h8 x, y | {x, y} ✓ bb ! x ÷ (y ÷ x) = yi h8 x | x 2 bb ! x · x = xi ) (zz⇥ ) zz⇥ = arb(bb) ÷ arb(bb) h8 x | (x 2 bb ! x ÷ x = zz⇥ & x ÷ zz⇥ = x & zz⇥ ÷ x = x) & zz⇥ 2 bbi h8 x, y | x, y 2 bb ! x ÷ y = y ÷ xi h8 x, y | x, y 2 bb ! x · y = y · xi h8 x | x 2 bb ! zz⇥ · x = zz⇥ i h8 u, v | {u, v} ✓ bb & u · v = u & v · u = v ! u = vi End booleanRing
Here zz⇥ designates the additive identity. Notice, among the internally derived claims, the commutativity laws.
Due to its entirely algebraic character, this Theory could have been developed somewhat more easily with an autonomous theorem prover oriented to the treatment of equality: as announced in [6, Sec. 3], we plan to implement interfaces between Ref and outer automated proof assistants.
Our next Theory, presupposing the definition of symmetric di↵erence, shows that rings of sets match the assumptions of the Theory booleanRing: ) Theory protoBoolean(dd) ; 6 = Sdd h8 x, y | {x, y} ✓ dd ! x \ y 2 ddi h8 x, y | {x, y} ✓ dd ! x 4 y 2 ddi dd 6= ; h8 x 2 dd, y 2 dd, z 2 dd | x \ (y \ z) = (x \ y) \ zi h8 x 2 dd, y 2 dd, z 2 dd | x 4 (y 4 z) = (x 4 y) 4 zi h8 x 2 dd, y 2 dd, z 2 dd | (x 4 y) \ z = z \ y 4 z \ xi h8 x 2 dd, y 2 dd | x 4 x = y 4 yi h8 x 2 dd, y 2 dd | x 4 (y 4 x) = yi h8 x 2 dd | x \ x = xi
End protoBoolean Two claims, proved inside the background Theory, namely Set theory, and presupposing the definition of P, show that the family of all subsets, and the one of all finite and cofinite subsets, of a non-void set constitute instances of protoBoolean:
Another Theory, akin to the preceding one, introduces a slightly more specific algebraic variety than the one treated by protoBoolean:
Theory archeoBoolean(dd) ; 6 = Sdd h8 x, y, z | {x, y} ✓ dd & z ✓ x [ y ! z 2 ddi ) h8 x, y | {x, y} ✓ dd ! x \ y 2 ddi h8 x, y | {x, y} ✓ dd ! x 4 y 2 ddi dd 6= ;
End archeoBoolean
After switching back to the background Set theory level, one proves that there are fields of sets which are instances of protoBoolean but are not instances of archeoBoolean. Indeed, the collection of all finite and cofinite subsets of an infinite set is not closed with respect to inclusion.
Thm . ¬Finite(W) & D = {s ✓
W | Finite(s) _ Finite(W\s)} !
W 2 D & h9 z ✓ W | z 2 / Di.
Surprisingly enough, it is unnecessary to resort to a theory of cardinals of any sophistication in order to get the result just cited: the distinction between finite sets and sets which are not finite more than suces for that purpose, where the following definition applies:
Def : [Finitude] Finite(F) $ Def h8 g 2 P(PF)\ {;} , 9 m | g \ Pm = {m} i
Last but not least, we developed the Theory booleanAlgebra whose interface is shown in the Appendix.
Conclusions and future work Proof-verification can highly benefit from representation theorems of the kind illustrated by Stone’s results on Boolean algebras. On the human side, such results disclose new insights by shedding light on a discipline from unusual angles; on the technological side, they enable the transfer of proof methods from one realm of mathematics to another.
Examples of this can be found in various recent proofs concerning connected
claw-free graphs:10 thanks to a convenient choice on how to represent those
graphs, Milaniˇc and Tomescu [
This motivated us in undertaking the formal development, with Ref, of proofs
of various representation theorems (see also [
A The main theory in our scenario on Boolean algebras Theory booleanAlgebra(B,·,÷,1B) h8 x | ⇣x 2 B ! (x)⇥ 2 B & ⇣(x)⇥ ⌘⇥ = x⌘ & 1B ⇥ = 0⇥ & 0⇥ ⇥ = 1Bi h8 x,y | {x,y} ✓ B ! (x)⇥ ÷ x = 1B & y · x ÷ y · (x)⇥ = y & y · x · y · (x)⇥ = 0⇥ i h8 x,y | {x,y} ✓ B ! (x ÷ y)⇥ = x · y ÷ (x)⇥ · (y)⇥ i h8 x | x 2 B ! (x)⇥ 6= x & x 2/{ 0⇥ ,1B} ! (x)⇥ 2 B \{0⇥ ,1B} i h8 u,v | {u,v} ✓ B & u · v = 1B ! u = 1B & v = 1Bi h8 u,v,x,y | {u,v,x,y} ✓ B ! u · (x)⇥ ÷ v · (y)⇥ = u · (x)⇥ ÷ v · (y)⇥ · (x · y)⇥ i h8 i | Ideal⇥ (i) $ {x ÷ y : x 2 i,y 2 i} ✓ i & {x · y : x 2 B ,y 2 i} ✓ i & i ✓ B\{1B} & i 6✓ {0⇥ }i h8 i,x,y | Ideal⇥ (i) & {x,y} ✓ i ! x ÷ y 2 ii h8 i | Ideal⇥ (i) ! 0⇥ 2 i & x 2 i & y 2 B ! x · y,y · x 2 i & (x)⇥ 2/ i & 1B 2/ ii h8 i | Ideal⇥ (i) ! h9 m | i ✓ m & h8 j | Ideal⇥ (j) & m ✓ j $ j = miii h8 b | b ✓ B\{0⇥ } & {x · y : x 2 b,y 2 b} ✓ b & b 6✓ {1B} ! Ideal⇥ {a · (x)⇥ : a 2 B ,x 2 b} h8 x | x 2 B \{0⇥ ,1B} ! Ideal⇥ ({a · x : a 2 B} ) & x 2 { a · x : a 2 B} i h8 h | BooHom⇥ (h) $ Svm(h) & domain(h) = B & h 1B = Srange(h) & h 1B 6= h 0⇥ & h8 x 2 B ,y 2 B | h (x · y) = h x \ h y & h (x ÷ y) = h x 4 h yii
H⇥ = {h ✓ B ⇥ 2 | BooHom⇥ (h)} h8 h | h 2 H ⇥ ! h 0⇥ = ; & h 1B = 1i h8 h | h 2 H ⇥ & {x, y} ✓ B & h (x ÷ x · y) = 1 & h y = ; ! h x = 1i h8 i, x | Ideal⇥ (i) & x 2 B & (x)⇥ 2/ i ! h9 j | Ideal⇥ (j) & i [ {x} ✓ jii h8 x, m | x 2/ m & x 2 B & h8 j | Ideal⇥ (j) & m ✓ j $ j = mi ! (x)⇥ 2 mi h8 m | h8 j | Ideal⇥ (j) & m ✓ j $ j = mi ! {[x, if x 2 m then ; else 1 fi] : x 2 B} 2 H ⇥ i B ✓ {0⇥ , 1B} ! {[0⇥ , ; ] , [1B, 1]} 2 H ⇥ h8 x 2 B \ {0⇥ } | {h 2 H ⇥ | h x = 1} 6= ; i & H⇥ 6= ; ' ⇥ = {[b, {h 2 H ⇥ | h b = 1}] : b 2 B} h8 x 2 B | ' ⇥ x = {h 2 H ⇥ | h x = 1} i h8 x, y | {x, y} ✓ B ! ' ⇥ (x · y) = ' ⇥ x \ ' ⇥ y & ' ⇥ (x ÷ y) = ' ⇥ x 4 ' ⇥ yi h8 x, y | {x, y} ✓ B & x · y 6= x ! ' ⇥ x 6= ' ⇥ yi H⇥ = Srange(' ⇥ ) & ' ⇥ 0⇥ = ; & ' ⇥ 1B 6= ' ⇥ 0⇥ & ' ⇥ 1B = H⇥ h8 x 2 B | ' ⇥ (x)⇥ = H⇥ \' ⇥ xi 1–1(' ⇥ ) & domain(' ⇥ ) = B BooHom⇥ (' ⇥ ) range(' ⇥ ) ✓ {x : x ✓ H⇥ } & ; 2 range(' ⇥ ) & H⇥ 2 range(' ⇥ ) h8 u 2 range(' ⇥ ) | H⇥ \u 2 range(' ⇥ )i h8 f, g | {f, g} ✓ H⇥ & f 6= g ! h9 u 2 range(' ⇥ ), v 2 range(' ⇥ ) | f 2 u & g 2 v & u \ v = ; ii h8 f ✓ range(' ⇥ ) | f 6= ; & Finite(f) ! T f 2 range(' ⇥ )i h8 k ✓ range(' ⇥ ) | k 6= ; & T k = ; ! h9 f ✓ k | f 6= ; & Finite(f) ! T f = ; ii End booleanAlgebra