Inspired by some recent revisitations of the Cantor-Bernstein theorem, in particular its formalizations in ZF carried out via the proof assistant AProS by W. Sieg and P. Walsh, we are carrying out the proof of a related graph-theoretical proposition. Our development is assisted by the proof checker tnaNova, and our proof pattern is drawn from Halmos's classic `Naive set theory'. This case-study illustrates the exibility of a proof environment rooted in Set Theory, which can be bent with equal ease toward declarative and procedural styles of proof.
Riding the wave of a revival of interest in the proofs of the Cantor-Bernstein
theorem, in short CBT (cf. [
Stated in streamlined terms, the Cantor-Bernstein theorem claims that whenever ; are injections such that range( ) domain( ) and range( ) domain( ), a one-one correspondence exists between domain( ) and domain( ). Proving this amounts to building, out of the given and , an injection from A = domain( ) onto B = domain( ). Without loss of generality, Halmos [6, pp. 88{89] proceeds under the disjointedness assumption A \ B = ; | K}onig's original proof, which is slightly more informal, does not mention this assumption.
The elegance of Halmos's approach stems from his focusing on bipartite graphs rather than on 1-1 mappings; and we further stress the graph-theoretical nature of his argument by ignoring the orientation of the mappings. Halmos's argument|we contend|could well be referred to the undirected graph whose (typically in nite) sets of vertices and edges are, respectively:
V = A ] B and E = fx; yg : hx ; yi 2 [ & hy ; xi 2= [
The proof-checker tnaNova [
In this new formal essay, again based on tnaNova and related to graph connectivity, our aim is twofold: (1) capture the structural properties of the graph G = (V; E) resulting from generic injections and in the manner explained above; (2) show that any graph enjoying such properties has a perfect matching | namely, it has a set M of edges which is a partition of V .
(3) treat the connected components of an arbitrary graph (actually, of any family E of edges|even an in nite E whose elements are not doubletons, see Fig. 1); for, the sought matching will result from the disjoint union of perfect matchings, one for each connected component of G.
DisconPartn(P ) $Def ; 2= P & 8b 2 P | [ b \ [ ([(P n fbg)) = ; & (; 2 b ! b = f;g) ReachCl(Q; E) $Def ([Q) \ [(E n Q) = ;
CoCo(C; E) $Def f q C \ E | ReachCl(q; E) & q 6= ; g = fCg CoCo(C; E) ! f q C | ReachCl(q; C) g f; ; Cg CoCo(C; C) $ f q C | ReachCl(q; C) g f; ; Cg & C 6= ;
R 2 E ! 9c | CoCo(c ; E) & R 2 c K = f c E | CoCo(c; E) g ! DisconPartn(K) & [ K = E The paper is organized as follows: we o er a quick view of the tnaNova proof-speci cation language through examples related to our case-study in Section 1. Then, after highlighting Halmos's proof of the Cantor-Bernstein theorem in Section 2, we show how his idea can be adapted to the seemingly di erent situation related to bipartite graphs. In the conclusions, we relate the contribution of this paper with ongoing studies on the interplay between sets and graphs in formal reasoning within the respective theories. For the sake of completeness, in Appendix A we outline a di erent proof pattern for the Cantor-Bernstein theorem, closer in spirit to the viewpoint which historically led to its discovery. 1
tnaNova is available as a service at URL http://aetnanova.units.it/, while all of the proof-checking experiments discussed in this paper are available at URL http://aetnanova.units.it/scenarios/BeyondCantorBernstein.
The
tnaNova system: a panoramic tour tnaNova's users organize de nitions, theorem statements, and proof speci cations, in les named scenarios 2, which tnaNova processes in order to establish whether or not they comply with the mathematical standards of rigor built into it. The logical system underlying tnaNova is a variant of the Zermelo-Fraenkel set theory with axioms of foundation and universal choice.
Only two axioms occur in tnaNova explicitly; they are: { s1 6= ; & (8 x 2 s1 | fxg 2 s1) { arb(;) = ; & 8 x | x = ; _ arb(x) 2 x & x \ arb(x) = ; The former, involving the special constant s , acts as in nity axiom; the lat1 ter characterizes the universal choice operator and embodies von Neumann's assumption that 2 is a well-founded relationship. The contents of most familiar axioms of ZF are built into the inferential armory of tnaNova, which handles competently many familiar set constructs: the membership and equality relators 2 and =, the constant ;, the dyadic operators \, n, [, the \elementary set" constructor fS1; : : : ; Sng, the pairing construct hX ; Y i and the conjugated projections associated with it (see the rst three lines of Fig. 6), and a very exible set abstraction construct (e.g., see [9, pp. 42{45]), of the form
f set term : iterators | condition g : tnaNova embodies two kinds of application: when the notation f x is used, f is a set (typically a set of pairs) and f x denotes the value y which f associates with x and, usually, this is the second component of a pair hx ; yi belonging to f , but f x equals ; for any x outside the set domain(f ); when the notation g(x) is used|as in arb( ), range( ), or descs ( )|, g denotes a `global' function: to wit, a proper class of pairs, whose domain consists of all sets.
P(S) =Def fy : y Sg
[S =Def fy : x 2 S ; y 2 xg
Finite(F ) $Def 8 g 2 P(P(F )) n f;g | 9 m | g \ P(m) = fmg Partition(P ) $Def ( 8 b 2 P | nk 2 P | k \ b 6= ;o = fbg )
next(I) =Def I [ fIg nat(I; S) =Def arb f next nat(j; S) : j 2 I | I = fjg \ S g
Even(M ) $Def M = ; _ ChSet(C ; T ) $Def fxg : x 2 C PeMa(M ; E) $Def M E & [E
N =Def fnat(i; s1) : i 2 s1g 9 i 2 M | Even(i) & next next(i) = M = C \ b : b 2 T [M & 8 h 2 M ; k 2 M n fhg | h \ k = ; 2 Sample scenarios can be found at http://aetnanova.units.it/scenarios/.
Three tnaNova-speci ed de nitions have already been shown on the top of Fig. 1; many more are listed in Fig. 2 and Fig. 6; all of these play a role in the `proof-pearl' under development which we are discussing here. Note that recursive speci cations such as the de nition of the function nat(I; S) (`I-th natural number relative to the set S of indices') and the de nition of the property Even(M ) (`M is an even number') make sense thanks to the assumed wellfoundedness of 2.
An example of an tnaNova-speci ed proof is shown in Fig. 3. As one sees, proofs are formed by two-portion lines: the second portion of each line, separated by the sign ) from the rst and at times carrying an identifying label of the form Statxxx, is the assertion being derived; the rst portion is the hint, referencing the basic inference mechanism which enables that derivation in tnaNova. Occasionally an assertion is represented laconically by the keyword AUTO, when no ambiguity or obscurity can ensue from this.
Theorem ch0 : [Every partition has a choice set] Partition(P ) ! ( 9 c | ChSet(c; P ) ): Proof : Suppose not(p0) ) Stat0 : : 9 c | ChSet(c; p0) & Partition(p0) For, suppose that p0 makes a counterexample. In particular, the inequality farb(b)g : b 2 p0 6= farb(b) : b 2 p0g \ b : b 2 p0 must hold, in view of the de nition of ChSet(c; p0). farb(b) : b 2 p0g ,! Stat0 ) : ChSet(farb(b) : b 2 p0g ; p0) Use def(ChSet) ) fxg : x 2 farb(b) : b 2 p0g 6= farb(b) : b 2 p0g \ b : b 2 p0 SIMPLF ) Stat1 : farb(b)g : b 2 p0 6= farb(b) : b 2 p0g \ b : b 2 p0 Therefore, some block b0 of the partition p0 exists which witnesses the said inequality. Since blocks are non-null, arb(b0) 2 b0.
Use def(Partition) ) Stat2 : ( 8 b 2 p0 | nk 2 p0 | k \ b 6= ;o = fbg ) b0 ,! Stat1 ) Stat3 : farb(b0)g 6= ( farb(b) : b 2 p0g \ b0 ) & b0 2 p0 b0 ,! Stat2(Stat2 ) ) Stat4 : nk 2 p0 | k \ b0 6= ;o = fb0g Consequently, arb(b0) 2 farb(b) : b 2 p0g \ b0 holds. This enables simpli cation of the inequality farb(b0)g 6= farb(b) : b 2 p0g \ b0 into farb(b) : b 2 p0g \ b0 6 arb(b0); therefore, an a0 other than arb(b0) belongs to both of b0 and farb(b) : b 2 p0g. Suppose ) arb(b0) 2= ( farb(b) : b 2 p0g \ b0 ) k0 ,! Stat4(Stat4 ) ) Stat5 : arb(b0) 2= farb(b) : b 2 p0g b0 ,! Stat5 ) AUTO (Stat3 )Discharge ) AUTO a0 ,! Stat3(Stat3 ) ) Stat6 : a0 2 farb(b) : b 2 p0g & a0 2 b0 & a0 6= arb(b0) Such an a0 can be rewritten as arb(b1) for some b1 other than b0 in p0, but this contradicts the fact that any two blocks in p0 are disjoint. b1 ,! Stat6(Stat6 ; Stat4) ) Stat7 : b1 2= nk 2 p0 | k \ b0 6= ;o & b1 2 p0 & a0 = arb(b1) o n
k 2 p0 | k \ b1 6= ; b1 ,! Stat2(Stat7 ) ) Stat8 : b1 2 ( ) ,! Stat8(Stat7) ) a0 2 b1 b1 ,! Stat7 ) AUTO (Stat6 )Discharge ) QED
tnaNova, of the controversial Zermelo's principle
tnaNova includes an important construct, named Theory (cf. [
Besides providing theorems of which it holds the proofs, a Theory has the ability to instantiate special variables (whose names are subscripted with the sign), which play the role of output parameters and bear special relationships with the input parameters. Two examples of tnaNova Theory appear in Fig. 4. Theory reachability has two parameters: a property V of sets and a dyadic relation E over sets; its assumption requires that for every set x enjoying the property V(x), the collection of all sets such that E(x; y) holds forms a set (not a proper class).
Theory reachability V(X) ; E(X; Y)
8 x | V(x) ! 9 c; 8 y | E(x; y) & V(y) ! y 2 c =)(descs ) 8 s ; x ; y | s descs (s) &
x 2 descs (s) & V(x) & V(y) & E(x; y) ! y 2 descs (s) 8 y ; x ; z | y 2 descs (fxg) & z 2 descs (fyg) ! z 2 descs (fyg) 8 s ; t | s t & ( 8 x ; y | x 2 t & V(x) & V(y) & E(x; y) ! y 2 t ) ! descs (s) t End reachability Theory connComp( H )
; 6= H =)(th ; cc ) (8 i ; r | th (i; r) = if i = ; then if r 2 H then r else arb(H) else w : j 2 i ; u 2 th(j; r) ; w 2 H | i = j [ fjg & u \ w 6= ; ( 8 r | cc (r) = [ fth(i; r) : i 2 Ng )
8 r | r 2 H ! CoCo(cc (r) ; H) End connComp )
This Theory returns a function, descs , that sends every set s into the sets of its `E-descendants'; that is, descs (s) is the set of all sets y such that a nite sequence x0; : : : ; xn exists satisfying the conditions x0 2 s, y = xn, and E(xi 1; xi) for i = 1; : : : ; n. The three statements appearing below the assumption of reachability in Fig. 4 are theorems, derived once and for all by the proof developer inside this Theory which, from then on, can be applied to any pair V(x), E(x; y) consisting of a property and a dyadic relation.
The other Theory shown in Fig. 4, namely connComp, can be applied to any nonnull set H. For any given element r of H, it returns the stages th (i; r) of an inductive construction of the unique set c = cc (r) such that CoCo(c; H) & r 2 c holds. It can be exploited to ascertain, in a somewhat procedural way, the last two statements of Fig. 1. It should be noted, though, that those claims can be proved in a totally di erent fashion, by resorting to Zorn's lemma (see Fig. 5 and [13, pp. 398{405]) instead of to natural numbers.
x p
T | 8 u 2 x ; v 2 x ; z 2 T | (u
v _ v S | nx 2 [ S | (8 y 2 p | x 2 y)o 2= S = ; & U 2 S u) & (9 y 2 x | z 6 y) (9 m | nx 2 T | x
= ; ! mo = fmg)
The user is referred to [11, Sec. 3] for a crash course on tnaNova, and
to [
Ko}nig-Halmos's proof of the Cantor-Bernstein theorem J. Ko}nig's proof certainly merited Poincare's attention. It brought a new gestalt to CBT proofs which had \remarkable generalizations" in new contexts that could not have been foreseen by either J. Ko}nig or Poincare. J. Ko}nig's son, D. Ko}nig, leveraged on his father's 1906 gestalt, to produce results in set theory, graph theory, and other branches of mathematics. (Hinkis [7, pp. 217{218]) Given injections ; satisfying the constraints stated in the Introduction and echoed by the assumptions of the Theory cbh in Fig. 7, consider the di graph whose sets of vertices and arcs are, respectively, the disjoint union V = A ] B of the domain A of with the domain B of , and
E0 = hw ; vi : w 2 V ; v 2 V | hv ; wi 2 [ .
In connection with this digraph D = (V; E0), consider the ancestry function @ sending each W V into the set @ W of all vertices u such that there is a path (of length > 0) leading from a vertex w 2 W to u in D. It should be clear that this function can be obtained in tnaNova by actualizing the parameters of the Theory reachability shown in Fig. 4 as follows:
Apply(descs : @) reachability V(X) 7! X 2 A [ B ; E(X; Y) 7! hY ; Xi 2
(Since E reverses all pairs forming [ , it seems natural to us to regard the
elements of @fxg as ancestors, instead of as descendants, of x.)
Ordered pair according to Kuratowski hX ; Yi =Def ffXg ; fX ; Ygg
1st of an ordered pair P[
range( ) [ Here is the heuristic idea lying behind this choice of , treated in pedagogical terms. If an element y0 of B does not equal x for any x 2 A, in order to make it an -image under the guidance of , we would like to modify by setting := [fh y0 ; y0ig; such a naive readjustment would create a collision with the preexisting value y0, though, causing to cease being single-valued. It hence seems that the right retouch to be made to is, rather: := nfh y0; y0ig[ fh y0; y0ig. But, then, the previous y1 = y0 will no longer be an -image; hence, in order to x the situation, we are to proceed in analogy with our previous move: inside , we will now replace the pair h y1 ; y1i by h y1 ; y1i, etc. Ultimately, x after x, we will assign a new image to each element xi = yi of A which originally had y0 in its ancestry: initially sent xi to xi = yi+1, but at the end of the replacements its image will turn out to be yi. The sequence of replacements described so far for a single y0 2 B = B n f x : x 2 A g should be developed likewise for all others; consequently, at the end of the overall processing, the original edges hy ; yi with B \ @ fyg 6= ; will turn out to be reversed, and the corresponding edges h y ; yi withdrawn, precisely in the manner described in the de nition of .
In a formal check that the said meets our desiderata, the key steps are: ;
Next we want to get rid of the assumption|inherent in what precedes|that A \ B = ;, so as to prove the Cantor-Bernstein theorem in its full extent, to wit: 0 1{1(F ) & 1{1(G) & 1 0 1{1(h) & 1 @ range(F ) domain(G) & A ! 9 h @ domain(h) = domain(F ) & A : range(G) domain(F ) range(h) = domain(G) Under the new less constraining hypothesis, we put A? = domain(F ), B = domain(G), and A = x [ fA? [ Bg : x 2 A? ; thus,
E =
hx [ fA? [ Bg ; xi : x 2 A? turns out to be an injection with range(E) = A? and domain(E) = A disjoint from B. Then we take = F E = hx [ fA? [ Bg ; F xi : x 2 A? and = E^ G = hy ; (G y) [ fA? [ Bgi : y 2 B , so that an injection with domain( ) = A, range( ) = B can be singled out on the grounds of what precedes. The sought h is just: h = E^ = hx ; (x [ fA? [ Bg)i :x 2 A? .
An tnaNova scenario developed from the bare rudiments of set theory and containing the above-outlined proof of the Cantor-Bernstein theorem is available at URL http://aetnanova.units.it/scenarios/BeyondCantorBernstein/. This scenario contains 13 de nitions and 48 theorems, organized in 5 Theorys. The overall number of proof lines is 680, there are only four proofs exceeding the lenght of 24 lines, and processing the entire scenario takes less than 5 seconds.
The said scenario could be developed rather quickly (namely, in about three weeks), because most of the needed preparatory lemmas had been developed long before: in particular, we could take advantage of the availability of the reachability Theory shown in the upper part of Fig. 4 (cf. [13, pp. 378{386]); roughly, only one third of the proofs was new. The situation with the extension that will be discussed next is di erent; we have not yet formalized all details, but devoted much time in nding the best usable de nitions (e.g., see the de nition of CoCo( ; ) in Fig. 1 and the ones of ChSet( ; ) and PeMa( ; ) in Fig. 2), as well as in properly formulating a graph-theoretical counterpart of the Cantor-Bernstein theorem. We feel that we are now at the end of the design phase. 3
Halmos's proof pattern adapted to special graphs As announced in item (1) of the Introduction, we want to capture the structural properties of the graph induced (in the manner explained there) by a pair ; of domain-disjoint injections such that range( ) domain( ) and range( ) domain( ). Fig. 8 shows the outcome of this elicitation task, formalized as an tnaNova's Theory.
When the tnaNova's Theory graphCBH shown in Fig. 9 gets applied, the set of edges of a graph induced by injections ; is provided as parameter E: we can focus on this set alone, taking it for granted that the set V of vertices equals [E. The perfect matching constructed inside this Theory is returned via pm . The assumptions to which E is subject match the conclusions of the previous Theory bij bip. Besides requiring that no vertex has more than two incident edges, those assumptions yield that the connected components of E are vertex-disjoint paths of three kinds: a) cycles involving an even number of edges|each nite component is in fact required to have a choice set ch; b) in nite simple paths endowed with one endpoint; c) in nite simple paths devoid of endpoints.
It should be intuitively clear that paths of kind b) have exactly one perfect matching, whereas paths of kinds a) and c) have two; this indicates the rationale End bij bip for imposing, in the above speci cation of pm , that pm = arb fq
cc | PeMa( q ; cc )g holds: should we only require pm 2 fq cc |PeMa( q ; cc )g, we might be putting in pm too much. One way of constructing each set fq cc | PeMa( q ; cc )g, with cc connected component of E, is by considering the sum sets [ n th(i; r) n [f th(j; r) : j 2 ig : i 2 N | Even(i) o associated with the elements r of cc. When cc is of kind either a) or c), all such sum sets (of which only two di er) are perfect matchings; as regards a component cc of kind b), the sole r 2 cc to be taken into account is the one that includes the singleton k 2 cc | k n [ cc n fkg 6= ; .
In Section 2 we gave clues on how, inside the Theory cbh outlined in Fig. 7, one can construct and prove the pertaining facts (e.g., its injectivity) in a stand-alone fashion. Here below we discuss a slicker implementation of the internals of cbh, which will come into e ect once the Theorys bij bip and graphCBH of Fig. 8 and Fig. 9 will be available.
Under the assumptions of cbh, which are identical to the ones of bij bip,
we can apply the latter Theory to and , and so get acbh = domain( )
along with an ecbh complying with the statements that appear in the lower
part of Fig. 8; in their turn, those statements enable application of the Theory
graphCBH to E = ecbh, which then provides a perfect matching pm for the
graph endowed with vertices [ecbh and edges ecbh. To obtain the desired
oneone correspondence, it now su ces to put
= hx ; yi : e 2 pm ; x 2 e \ acbh ; y 2 e n acbh [
:
| a[
Those many experiments are intended to contribute collectively to a unitary study on the foundations of discrete mathematics; therefore each of them is meant to have a bearing on others, and is designed in such terms that it can reuse achievements of previous e orts and can easily be integrated with the rest.
This explains why, even though only graphs and digraphs enter the proof of
the Cantor-Bernstein theorem, we chose to de ne the connected components of
an arbitrary set E|not obligatorily one consisting of doubletons|, seen as the
set of edges of a hypergraph. By so doing, we can more easily merge the proof
scenario discussed in this paper with the one of [
Also, the collection f c E | ReachCl(c; E) g of those sets of (hyper)edges that are closed under reachability forms, one readily sees, a Boolean algebra: in fact, it is closed under intersection and symmetric di erence and E is one of its members. Elsewhere, in proving Stone's results, we had to bring into play Zorn's lemma; accordingly, in this paper we found it convenient to opt for a declarative de nition of connected components, albeit a characterization of connected components relying either upon paths or|which amounts, roughly, to the same|upon the Theory connComp seen in Fig. 4 would have su ced for the limited goals addressed above.
Discussions with Francesco Cancian were fruitful for the matters of this paper.
Cardinalities and the Cantor-Bernstein theorem When the discovery of the Cantor-Bernstein theorem took place (late 19th century), it contributed to clarifying the then emerging notions of equipotence and cardinality.
Equipotence is the equivalence relationship that holds between two sets whose respective elements can be put in one-one correspondence. Denote by the relation between sets:
A
B $Def an exists such that 1{1( ) and
domain( ) = A , range( ) B ; then we can phrase the Cantor-Bernstein theorem as follows: k When A
B and B
Cardinality |as seen from a contemporary viewpoint|is the function that sends every set S to a canonical representative, #S, of the equipotence class to which S belongs. Hence, we can also thus state the Cantor-Bernstein theorem: k When A
B and B
A both hold, #A = #B holds as well.
It has today become customary to regard cardinals|namely, the representatives of equipotence classes|as forming a strict subclass of the class of von Neumann's ordinal numbers. In their turn, ordinals are special sets internally well-ordered by membership; they enable one to impose a well-ordering to a set S whatsoever by somehow `enumerating' the elements of S. Speci cally, under the assumption that membership is a well-founded relation over sets, ordinals can be de ned a la Raphael M. Robinson as follows:
Ord(O) $Def 8 x 2 O ; y 2 O n fxg | x 2 y _ y 2 x & O [O ; then, after formulating the recursive de nition of the enumeration process as enum(X; S) =Def if S fenum(y; S) : y 2 Xg then S
else arb(S n fenum(y; S) : y 2 Xg) ; one proves that 9 o | Ord(o) & S = fenum(y; S) : y 2 og &
8 u 2 o ; v 2 o n fug | enum(u; S) 6= enum(v; S) holds for every S .
Through Skolemization|which in tnaNova acts as a built-in Theory|, this claim leads to the de nition of a global function, enumord, such that 8 s | Ord enumord(s) & s = enum(y; s) : y 2 enumord(s) & 8 u 2 enumord(s) ; v 2 enumord(s) n fug | enum(u; s) 6= enum(v; s) : #S =Def arb o 2 next enumord(S) | Card(C) $Def Ord(C) &
8 o 2 C | :9 f | Svm(f ) & domain(f ) = o & range(f ) = C ; that is to say, a cardinal number is an ordinal number C such that no function f exists mapping an ordinal o smaller than C onto C.
Along the path discussed in [13, Section 5.3], one reaches two key theorems, 1{1(F ) & Card domain(F ) ! domain(F ) = #range(F ) 1{1(F ) & Card domain(F ) & Ord range(F ) ! domain(F ) range(F ) ; which leads straightforwardly to the Cantor-Bernstein theorem, in a way that di ers substantially from the pattern discussed earlier (see Sections 2 and 3). and whence