The Four-Color Theorem of Map-Making Proved by Construction

Show more

1. Introduction and a Brief Literature Review

Easy to express but difficult to prove, the “four-color map theorem” is a proposition plainly put by Francis Guthrie in 1852. It seemed to be an almost trivial problem for map-making, and though evidently true, it turned out to be more interesting and complex than it seemed on first look [1] - [7] . In its simplest form, the theorem says that “no more than four colors are required to color the regions” of any planar map “so that no two adjacent regions have the same color” ( [6] , p. 1383). The theorem presupposes that corners, consisting of points shared by three or more colored spaces do not qualify as “adjacent” borders or edges. Logically, this is a necessary presupposition so long as any given “corner” shared by two or more colored spaces consists of a single dimensionless point. This is the same as saying that any adjacent border between two distinct regions of the map must have a length greater than zero.

However, proof of the four-color theorem turned out to be more difficult than seemed likely at first blush [1] [6] [7] and even now it ranks higher in complexity than many others including, for instance, Riemann’s Hypothesis [2] [3] . It is not known whether it is possible to meaningfully define a “highest complexity order of well-known mathematical problems” ( [2] , p. 10) or how high in the mix the four-color theorem might rank with respect to such a theoretical limit if one could be defined, but we do know historically that the first satisfactory proof of the four-color theorem was not achieved until 1976, 124 years after it was clearly stated. Also, the first satisfactory proof relied heavily on the brute force of modern computing to examine the multitudinous adjacent pieces of map coloring puzzles that were constructed by combinatory algorithms on a planar surface [1] .

Over the last several decades, it has become increasingly feasible to assess the validity of cumbersome formalized mathematical proofs by taking advantage of the speed, power, and accuracy of modern computing. However, the advantages of automated auditing of formalized proofs, such as the proofs of the four-color theorem, presents special difficulties to human auditors. Efforts along that line have led to a rephrasing of the long- standing question of “artificial intelligence”. Govindarajalulu, Bringsjord, and Taylor put that question like this: “Is it possible to apply computational power to generate entirely new proofs not previously discovered by humans?” ( [8] , p. 2077). Of course, it almost goes without saying that proofs, or audits of proofs, dependent on the brute force of modern computing are probably going to be difficult for slower and more fallible human auditors who are hard-pressed to access, remember, or otherwise carry out very large numbers of computations in whole lifetimes not to mention in reasonable segments of our ordinary wakeful experience [9] [10] . If humans have difficulty checking the computations of a super-computer or a network of such computers, how will it be possible for them to check the computer audit of a proof of one or many difficult formalized proofs dependent on the speed, power, and accuracy of the technology? For that reason, as argued long ago by the Earl of Ockham, by Galileo, and also by C. S. Peirce [11] [12] , simpler theories and simpler proofs are much to be preferred.

Although the four-color theorem is believed to be true, and its complex computer- assisted proofs are believed to be valid, certain conjectures related to that theorem remain unproved and simpler proofs of the four-color theorem itself are still being sought. In 2012 Cooper, Rowland, and Zeilberger took some steps toward what they described as a “language theoretic proof” involving the parsing of binary trees. They argued that within their simple grammar the proposition “that every pair of trees has a common parse word is equivalent to the statement that every planar graph is four-co- lorable” and they also supposed that the results they achieved “are a step toward a language theoretic proof of the four color theorem” ( [4] , p. 414). Yet they do not claim to have completed such a proof though it seems that if such a proof can be completed, it may be simpler than the existing computer-assisted proofs.

In the meantime, according to the Web of Science Core Collection, Gonthier’s 2008 computer-assisted proof of the four-color theorem has been cited at least 75 times at the time of this writing (June 14, 2016). Also, continuing interest in proofs of the four- color theorem is shown in the non-linear increase in citations of Gonthier’s proof as shown in Figure 1. More than half (57.33%) of the citing articles referring to that eight- year-old proof (43 of the 75) have appeared in the most recent three and a half years.

Therefore, in light of all the foregoing, a simple constructive proof of the four-color theorem might be of interest. In building the following proof, as in my mathematical proofs about biosemiotic entropy [13] [14] , I follow Peirce. He summed up his method by saying: “I never introduce a distinction without having deduced the necessity for it” ( [15] , p. 340). In applying such a method of “exact logic”, he claimed in 1867 to have proved that “... all mathematical reasoning is diagrammatic and that all necessary rea-

Figure 1. Number of citations appearing in sources both included and not included in the Web of Science Core Collection of Gonthier’s “Formal Proof-The Four Color Theorem” in Notices of the American Mathematical Society, 55(11), 1382-1393.

soning is mathematical reasoning, no matter how simple it may be. By diagrammatic reasoning, I mean reasoning which constructs a diagram according to a precept expressed in general terms, performs experiments upon this diagram, notes their results, assures itself that similar experiments performed upon any diagram constructed according to the same precept would have the same results, and expresses this in general terms. This was a discovery of no little importance, showing, as it does, that all knowledge without exception [including mathematical knowledge] comes from observation” ( [16] , pp. 47-48). Peirce argued that mathematical thinking in consisting of experimentation carried out on diagrams is itself a form of material (empirical) observation. Yet he refused to believe that “mathematics depends in any way upon logic” because he contended “all formal logic is merely mathematics applied to logic” ( [17] , p. volume 4, paragraph 228).

In the case of map-making, it is the role of every index in a well-formed map to separate any colored space contained within its scope from all other spaces. To accomplish that function, every indexical boundary in any well-formed planar map must be binary in two critical respects: for one, it forms a boundary completely separating (1) its contained space from (2) all other spaces on the map, and, for another, if during the construction of the map, the completed boundary is cut by a new index so as to form a new and distinct space on the map, the index in question can only possess at most two ends: (1) the beginning end and (2) the final end of the cut that joins its own beginning or some other edge of an existing boundary to fully enclose the new bounded space on the map. It is necessary that the two ends of the new space meet up with each other by being connected through the completed boundary enclosing the new space. If these binary aspects of every index that might be used to create a new space on a colored map are kept in mind, that peculiar binary nature will assist the reader in understanding the rigor and completeness of the following proof.

2. A Simple Indexical Proof of the Four-Color Theorem by Construction

To begin, we can color any bounded surface in 1 color as in Figure 2. Next, we can cut the existing map into two completely bounded and separated pieces with an index that

Figure 2. Any planar surface can be colored completely in just one color.

Figure 3. An emergent island anywhere on the map requires a second color.

(a) (b)

Figure 4. An emergent island contained in an existing colored space does not require any new color.

Figure 5. An emergent island overlapping two existing colors requires a third color.

Figure 6. An emergent island within any of the existing colored spaces does not require any new color.

Figure 7. An emergent island overlapping three existing colors requires a fourth color.

4^{th} color would be needed, but with just 4 colors all of the adjacent bounded parts of the whole surface could be colored and would be differentiated in all possible cases constructed in the manner described irrespective of the shapes of the adjoining spaces filling the entire map.

Figure 8. The problem of an island emerging so that it overlaps at least 4 existing colored spaces as found in the map of the United States at the Four Corners Monument.

Figure 9. An emergent island covering all four existing colors that, at first look, might seem to require a fight color.

5

Figure 11. However, given that no more than three adjacent colors can exist at any point (corner) shared by three or any number of adjacent spaces having such an un-extended corner point (one of 0 dimensionality), exactly four colors are sufficient to color any planar surface whatsoever as suggested in the following figure.

Figure 12. Four colors are sufficient to color any emergent island covering any point shared by 3 or more adjacent already colored spaces.

Further, given that it is not possible to construct any additional spaces in any portion of any planar map by any method other than the ones already examined, the proof is complete. To fault the proof it would be necessary for any would-be critic to show by any method of construction how it is possible to make an indexical cut of any bounded portion of a map in a manner that divides an existing space so as to produce a nexus of 2 adjacent corners on the perimeter of that new island that mark the intersection of more than 3 spaces with boundaries adjacent to the new island. But, that cannot be done, because we have already examined all of the possible ways of dividing any colored space on any map into an old space and a new one. We have also examined the corner problem in a manner showing that any number of corners joined at any single point on the map, or at any number of points on the perimeter of any given piece of the map, old or new, can always be resolved as already shown by the foregoing construction. Also, the simple proof presented here suggests that a “language theoretic proof” along the lines of [4] can probably be completed.

3. Conclusion

By induction from the foregoing constructions, it follows that any map, including the infinitely complex sorts constructed in the complex number plane as differentiated into the fractal patterns of the Mandelbrot set, sampled in Figure 13, can also be colored so that all of its bounded spaces are differentiated by no more than 4 colors.

Figure 13. A bit of the Mandelbrot Set in the complex number plane. Reprinted under the GNU Free Documentation License, Version 1.2 retrieved at https://commons.wikimedia.org/wiki/File:Mandel_zoom_14_satellite_julia_island.jpg on May 7, 2016.

Competing Interests

The author declares that he has no competing interests.

References

[1] Appel, K. and Haken, W. (1977) Every Planar Map Is Four Colorable. Part I: Discharging. Illinois Journal of Mathematics, 21, 429-490.

[2] Burgin, M., Calude, C.S. and Calude, E. (2011) Inductive Complexity Measures for Mathematical Problems. Centre for Discrete Mathematics and Theoretical Computer Science.

[3] Calude, C.S. and Calude, E. (2010) The Complexity of the Four Colour Theorem. LMS Journal of Computation and Mathematics, 13, 414-425.

https://doi.org/10.1112/S1461157009000461

[4] Cooper, B., Rowland, E. and Zeilberger, D. (2012) Toward a Language Theoretic Proof of the Four Color Theorem. Advances in Applied Mathematics, 48, 414-431.

https://doi.org/10.1016/j.aam.2011.11.002

[5] Dvorák, Z., Kawarabayashi, K. and Král, D. (2016) Packing Six T-Joins in Plane Graphs. Journal of Combinatorial Theory, Series B, 116, 287-305.

https://doi.org/10.1016/j.jctb.2015.09.002

[6] Gonthier, G. (2008) Formal Proof—The Four Color Theorem. Notices of the American Mathematical Society, 55, 1382-1393.

[7] Wilson, R. (2002) Four Colors Suffice. How the Map Problem Was Solved. Princeton Science Library, Princeton University Press, Princeton.

[8] Govindarajalulu, N.S., Bringsjord, S. and Taylor, J. (2015) Proof Verification and Proof Discovery for Relativity. Synthese, 192, 2077-2094.

https://doi.org/10.1007/s11229-014-0424-3

[9] Adams, M. (2016) Proof Auditing Formalised Mathematics—Researcher Publication. Journal of Formalized Mathematics, 9, 3-32.

[10] Edwards, C. (2016) Automating Proofs. Communications of the ACM, 59, 13-15.

https://doi.org/10.1145/2892710

[11] Peirce, C.S. (1885) On the Algebra of Logic: A Contribution to the Philosophy of Notation. American Journal of Mathematics, 7, 180-202.

https://doi.org/10.2307/2369451

[12] Peirce, C.S. (1897) The Logic of Relatives. The Monist, 7, 161-217.

https://doi.org/10.5840/monist18977231

[13] Oller, J.W. (2010) The Antithesis of Entropy: Biosemiotic Communication from Genetics to Human Language with Special Emphasis on the Immune Systems. Entropy, 12, 631-705.

https://doi.org/10.3390/e12040631

[14] Oller, J.W. (2014) Biosemiotic Entropy: Concluding the Series. Entropy, 16, 4060-4087.

https://doi.org/10.3390/e16074060

[15] Peirce, C.S. (1982) The Logic Notebook. In: Fisch, M., Kloesel, C.J.W., Moore, E.C., Roberts, D.D., Ziegler, L.A. and Atkinson, N.P., Eds., Writings of Charles S. Peirce: A Chronological Edition, Indiana University Press, Indianapolis.

[16] Peirce, C.S. (1976) The New Elements of Mathematics by C. S. Peirce. Mouton, Hague.

[17] Peirce, C.S. (1931) The Collected Papers of C. S. Peirce, 1-8. Belknap Press of Harvard University, Cambridge.