# On Undecidability and Millipedes_with Art by A.T. Fomenko

December 2012

"No problem can be solved from the same level of consciousness that created it." -Albert Einstein

"At least, you have to leave Bombay." -Bangere Purnaprajna at a colloquium.

One important discovery of twentieth-century mathematics was first published in the 1931 volume of Monatshefte für Mathematik und Physik.  In a paper titled On Formally Undecidable Propositions in Principia Mathematica and Related Systems I, mathematician and logician Kurt Gödel (1906-1978) wrote:
Theorem VI. For every ω-consistent recursive class κ of FORMULAS there are recursive CLASS SIGNS r, such that neither v Gen r nor Neg(v Gen r) belongs to Flg(κ) (where v is the FREE VARIABLE of r).  [1]
Thus the world first read about the existence of undecidable mathematical propositions according to Gödel.  Kurt Gödel went on to refine his statement of undecidability, suggesting two so-called incompleteness theorems.

An undecidable statement, in the mathematical or theoretic sense, is a statement that is neither provable nor refutable in a particular deductive system.  This definition is related to Kurt Gödel’s incompleteness theorems which essentially indicate the impossibility of defining a complete system of mathematical rules that is also consistent.   For mathematicians, one commonly debated implication of Gödel's theorems is that the basis of mathematics can never be entirely rigorous, so there will always be some uncertainties.  For computer scientists, another profession impacted by Gödel, this translates to all of the truths of mathematics not being computable by a machine; computability theory can prove that there are decision problems for which no mechanical process can provide an answer on any input.  As for me, an investigator of creativity, I am prompted to conjecture that Gödel’s theorems points to the very good news that mathematics is inherently creative and her relative uncertainties are key to unleashing human intuition, ingenuity, and combinatorial skills.  An example: Sometimes an axiom will come up and mark the entryway to a new mathematical world, at other times an axiom will be removed.

To temper any exuberance, one must point out that the idea of axioms is relatively new.  Just as music theory is often superimposed onto a long-ago written symphony for the academic purpose of harmonic analysis, axioms have only recently been superimposed onto various areas of mathematics by theorists.   It was a founder of mathematical logic, Giuseppe Peano (1858-1932), who axiomatized the natural numbers, obviously long after counting numbers had been in use.  Also, while philosophers and logicians consider that mathematics cannot be both complete and consistent, workaday mathematicians point out Gödel merely showed that there are unprovable theorems "out there" and the implication that the whole of mathematics is not consistent does not follow from this.  For instance, the consistency of Peano arithmetic cannot be proved using the axioms of the theory itself, but it can be proved in other, larger theories. This fosters hope among Gödelian optimists.  Once mathematicians find out that an idea cannot be proven in a given system, they usually discard it, but the idea may well reappear as an axiom in another theoretical system.  There is no agreement in mathematics against this.

As a rule, mathematicians engage in mathematics for fun.   Mathematicians enjoy entertaining clever insights. Telling other people about what they have been thinking via a proof tends to be a separate activity and not a source of inspiration per say.  Thus there is a bit of casualness in the mathematician’s relationship with logic, though what lurks beneath the casualness merits mention.  A summary of why most mathematicians may not be too concerned with mathematics’ logic, except perhaps for a few topics in Real Variables or Algebra qualifier courses might have been revealed to me after hours, in a darkening university hallway:  “Since the Zermelo-Fraenkel set-theory axiom walled off Russell’s paradox, no other problem has shown up,” I was puckishly reminded.  As I confirmed for myself the next morning, the 1901 Russell paradox regards set theory and predates Gödel’s first mathematical publication.

Above: Simplicial spaces, cellular spaces, crystal and liquid by Professor of Mathematics Anatoly Timofeevich Fomenko (Moscow State University); India ink and pencil on paper, 43 x 61.5 cm,  No. 190 (1976).  A mathematician runs beneath a mutating cell complex and an evolving crystal, seen landing to his right.  The classification of crystal structures is a branch of group theory.

One would be remiss not to mention at this point that Russell’s efforts were in keeping with those of famous mathematician and contemporary David Hilbert. Hilbert’s own impetus in the direction of mathematical formalism led him to co-write with Wilhelm Ackermann the treatise Principles of Mathematical Logic, a ground breaking book published in 1928.  To his credit, Hilbert was a supporter of the much reviled George Cantor (1845-1918) and of Cantor's theory of infinite sets, which so many philosophers, mathematicians, and Christian theologians of the day saw as trespassing on spirituality.   Hilbert's 1888 basis theorem is said to have been likewise received with a "This is not mathematics.  This is theology" editorial verdict from Mathematishe Annalen—of which Hilbert later became the Chief Editor (1902-1939).  It is usually recognized that Hilbert’s undertaking to rebuild the foundations of mathematics and his defense of George Cantor paved the way for one significant achievement of mathematical logic in the second half of the twentieth century: the Classification of the Finite Simple Groups (CFSG) project.  In 1983, Daniel Gorenstein announced that the classification of the finite simple groups was complete.  However, given that the proof behind this colossal scheme is spread over 500 articles, many of which are lengthy and obtuse enough to test the endurance of the best among mathematicians, the veracity of Gorenstein’s pronouncement was difficult to ascertain.  Mathematicians usually get in trouble when working with impossibly long and complex proofs and tend to avoid them.  As one in the know would expect, mathematicians remained aloof of the media spotlights and skeptical as to the completeness and correctness of the gigantic work;  the result being that the announcement of the project's completion went unheralded.  A good thing, it turned out, since the project had ground to cover still.  Gaps were found in the proof for decades thereafter.   The project eventually came to an end with the publication of the 2004 proof on quasithin groups by Michael Aschbacher (1944- ).

Becoming a leading force in the CFSG in the 70s, Aschbacher distinguished three stages for any new group: discovery, existence, and uniqueness.  He pointed out that there are more hypothesis than there are facts.   “I understand a sporadic group to be discovered when a sufficient amount of self-consistent information about the group is available …" Aschbacher wrote in 1980. [2] “Notice that under this definition the group can be discovered before it is shown to exist […] Of course the group is said to exist when there is a proof that there exists some finite simple group satisfying P.”  In mathematics the relationship between hypothesis and evidence must be logical.  (This idea is further discussed below.)  Within the classification of the finite simple groups project, Aschbacher's proof replaced an 800 pages proof by Geoff Mason which was found to be incomplete and was never published.  It is now accepted that the classification of the finite simple groups is complete and that all gaps in proof have been addressed.  Gaps, that is.  Errors are harder to detect.  Along that vein, it is worth keeping in mind that a second version of the proof of the quasithin case by Michael Aschbacher and Steve Smith runs 1200 pages.   A second generation proof in eleven volumes of the classification theorem for finite simple groups, which omits the ‘even’ quasithin case and sporadic simple groups, is underway. The project, led by Daniel Gorenstein (now deceased), Richard Lyons, and Ronald Solomon, is published by the American Mathematical Society.  Six volumes have appeared so far.

Returning now to Russell’s paradox,  in his 1929 doctoral thesis, Gödel proved the completeness theorem which was first stated by Hilbert and Ackermann in Principles of Mathematical Logic thus:  “Every valid logical expression is provable. Equivalently, every logical expression is either satisfiable or refutable.”  From then since, for a statement to be a logical mathematical statement, one has to determine that it cannot take both a true and a false value.  A statement should be either true or it should be false.  If not, it is not a logical mathematical statement.  Thus my statement about the Barber of Seville shaving all men and only those men who do not shave themselves is not a mathematical statement.   The combined works of Ernst Zermelo (1871-1953) and Abraham Fraenkel (1891-1965) next offered other means of getting around Russell’s paradox by relaxing mathematical logic somewhat and shifting from an axiom schema of comprehension to an axiom schema of specification (implied by the axiom schema of replacement and the axiom of the empty set).   This meant that solely a logically definable subclass of a set is a set.  The relationship between hypothesis and facts must be logical.  Thus my Barber of Seville is not a set.  It is rather what Zermelo-Fraenkel refers to as a proper class—which in ZF set theory terms means:  It is definitely not a set.   This new focus on the axiom schema of specification marked the beginning of axiomatic set theory.   Gödel next demonstrated that Zermelo and Fraenkel’s way of going about mathematical logic was not a bad idea by publishing his Consistency Proof for the Generalized Continuum Hypothesis in 1939 and The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory in 1940.    (In 1963, Paul Cohen—a formalist—proved that the Continuum Hypothesis is independed from the axioms of set theory.) One should stress that mathematicians need only to be convinced that a statement cannot be both true and false in order to consider it—i.e., it is not necessary to prove that the statement cannot be both true and false in order to consider it.   In fact, Gödel had circa 1931 asserted that there are mathematical statements that cannot be proven within a logical system, thus there will always be some uncertainties.  Should one consider the Goldbach conjecture (1742), the distinction is easily grasped:  It is not known whether the Goldbach conjecture is provable, but it is very clear that there is no option aside from it being a yes or a no.  The Goldbach conjecture is good and sound mathematics.
In the words of my mathematician friend as we reflected on logic and its impact for workaday mathematicians on a cool and rainy October evening: “Everything was fine after that.”

Sort of.  Obsessing over logical certainty can be maddening as history would tell. Cantor did go mad, Gödel starved himself to death, Russell’s son and grand-daughter became schizophrenic.  Lucy Russell ended her life by fire.  Meek looking Friedrich Ludwig Gottlob Frege (1848-1925)  who firmly believed and dedicated his life to proving (unsuccessfully) that the whole of mathematics was reducible to logic, is reported to have morphed into a “foaming anti-Semite.” (See [3] and also the graphic novel Logicomix: An Epic Search for Truth by mathematicians A.Doxiadis and C.H. Papadimitriou, with illustrations by A. Papadatos and A.Di Donna.)  It may be reassuring to know that among mathematicians, logicians who exclusively concern themselves with the foundation of mathematics are a somewhat separate species.  While mathematicians often begin with creative ideas, and allow themselves to be further led by intuition and even aesthetics, logicians work differently.  In the 20th century, composer Arnold Schoenberg (1874-1951) wrote music strictly based on 12 tone row matrices and spearheaded a certain formalism in musical composition that reverberated throughout the century.  Likewise, 20th century logician Gerhard Gentzen (1909 -1945) worked from the rules to the theorem.  Getzen's 1936 proof of Peano's axioms using combinatorial methods marked the beginning of ordinal proof theory. The logician’s remains a somewhat unusual way to go about doing mathematics, just as a 12 tone row matrice remains an unusual begining for a piece.  Still, medals and prizes are awarded to mathematicians who can take a look at a number of examples and find a (consistent) theorem that explains them all.  At the end of the day, regardless of the method that has been employed, there is one thing we have all come to agree on.  It is that mathematics is inherently filled with creative potential.

As is apparent from the above investigation, undecidability permeates the deep, fundational logic layer of mathematics.  And, although—or since—most mathematicians do not concern themselves with undecidability in their everyday work,

Left: Deformation of the Riemann Surface of an Algebraic Function by Professor of Mathematics Anatoly Timofeevich Fomenko (Moscow State University); India ink and pencil on paper, 44 x 62 cm,  No. 229 (1983).  Set in four-dimentional Euclidian space.

undecidable problems are not uncommon.  In fact, undecidable problems are ubiquitous in mathematics, as Chaim Goodman-Strauss (University of Arkansas) states in [4], a paper he submitted to the Notices in 2009 and that prompted my current writing.   This ubiquity confounds formal decidability.  We might remember from Gödel’s thesis that every valid logical expression is provable.  No proof exists from standard set theory arguments that amounts to “I can’t decide it."  Yet it is the case that unruly undecidable problems tend to surround us and this, I believe, is due to our creative tendencies.

Research mathematicians delight in constructing mathematical objects with certain properties to fit conjectures in an attempt to prove them, and then to pluck or poke at these constructions to see how they fare.  This may not lead to a Fields medal, but it is a lot of fun.  What is less so, often impractical—and in some cases as it turns out, impossible—is for mathematicians to go back to the generating axioms of their discipline and check that the whole system, including their new theorem is consistent .  There are computer programs that allegedly could now do this for humans, but one wonders if the practice of thus checking proofs should be institutionalized or even frequent.  Many find the idea of discarding new mathematical thoughts on such basis to be worrysome. Should proofs be verified by means of a mechanical device, therein arise systemic opportunities to limit the otherwise exuberant process of mathematical creativity.  And should proofs be generated by brute computing force, the question comes up whether this is truly mathematics.   Luckily, algorithms may never be deemed intelligent enough to act as overseers of creative environments.  Algorithms cannot substitute the traditions that encourage new mathematics to be born.   If you study at WUSTL, you might have heard the story of the Princeton mathematics professor that referred to graduate theses as millipedes.  The task of the thesis committee was then to pull on its legs and observe if the millipede could crawl.   It should not be too surprising that what is left crawling could well be new, seminal, and mutating—and a fine mathematical idea, too.

Related to the topic of automated and interactive theorem proving, I found two comments at a recent WUSTL colloquium presentation by Michael Warren (IAS, Princeton) on homotopy theory and univalence [5] to be fascinating. As the lively talk broached type theory (see  P. Martin-Löf [6], [6a]) and a homotopical interpretation thereof (see Vladimir Voevodsky [7] and Martin Hoffman-Thomas Streicher [8]), proof theory (see the Mathematical Components project with Jeremy Avigad, which has been working towards a verification of the Feit-Thompson theorem [9]), and theorem proving with Coq and Agda (see a tale of the Kepler Conjecture and the Flyspeck project in [10]), Professor Ari Stern mentioned that it is a human that eventually checks the theorem that is running the system. While agreeing, the speaker added that the programs are often not that transparent: “You still have to have some faith that it [a program] is correct,” Warren said. I promptly jotted down another component of human creativity and mathematics in my lecture notes: faith.
An update: Michael Warren just emailed that the verification of the Feit-Thompson Theorem project headed by Georges Gonthier (Microsoft Research & INRIA) is completed.  See http://www.msr-inria.inria.fr/Projects/math-components/feit-thompson for details on the six year effort.  To give an idea of the scope of the work, Warren sent a link to the final graph (it is very large, so be sure to scroll down and zoom out) which describes the connections between the various Coq files making up "an axiom-free formalization of the proof of the Odd Order theorem,"  see http://ssr.msr-inria.inria.fr/~jenkins/current/index.html»

Some logicians (mathematical) have a sense that, given undecidability and incompleteness is built in the system, mathematics itself establishes limits as to mathematical knowledge.  In practice, mathematicians tend to disagree, though they appreciate the theoretical point when it comes to knowledge about mathematics.  An optimist myself, I trust there is always more for a human being to discover, ponder and convey, and I can back up my intuition by pointing out that there is no proof that this is not true.  Mathematical knowledge as a display of the propensity of the human mind to engage in creative inquiry is likely endless.   But, as is the case for any artist, it is the mathematician who ultimately imposes and should go on imposing constraints on the creative process, on creative practices, and on the realm of enquiries relative to the discipline.   Meanwhile, inherent to the system that is mathematics, we can all agree to notice the creative potential of relative uncertainty.  Uncertainty—undecidability in common terms—is ubiquitous in our natural environments and necessary to motivate human creative processes.  Given some uncertainty and paradoxes, while we are fallible, we will organically strive to be consistent.   Mathematical creativity helps in this attempt all the while the creative potential intrinsic to mathematics also plays a role.   Thus mathematicians and mathematics remain mutually engaged and spiraling onward to the tune of an ever creative duet.

I thank Anatoly Timofeevich Fomenko for letting me reproduce his magnificent art work which adds in the direct, worldless way of the fine arts a rich and meaninful layer to this news note.  More of his "mathematical pictures" can be found in the book by A.T.Fomenko, Mathematical Impressions, published by the American Mathematical Society in 1990.

— Math news, stories, videos, and interviews by Marie Taris, http://www.math.wustl.edu/marietaris/math.html»
(v1, 10/20/2009; v2, posted 11/28/2012)

Enjoyed this story? See also November 2012 News story  Portraits in C with Wegert_Wickerhauser_Weiss»

[1] Über formal unentscheidbare Sätze der Principia Mathematica und verwandte Systeme I, Kurt Gödel, with page-facing English translation, in Solomon Feferman, et al. (eds.), Kurt Gödel, Collected Works, vol. I., Oxford, New York, 1986.
[2] The Finite Simple Groups and Their Classification, Michael Aschbacher (1980) pp. 6-7.
[3] New York Times, Book Reviews, Algorithm and Blues, Jim Holt, September 27, 2009.
[4] Can't Decide? Undecide!, Chaim Goodman-Strauss, Notices of the AMS (March 2010). Link to the paper: www.ams.org/notices/201003/rtx100300343p.pdf.
[5] Homotopy type theory and Voevodsky's univalent foundations, with Á. Pelayo, M. Warren (October 2012). Link to the paper: arXiv:1210.5658.
[6] An intuitionistic theory of types, Per Martin-Löf, Twenty-fi ve years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol. 36, Oxford Univ. Press, New York, 1998, pp. 127-172; originally a 1971 preprint from the Department of Mathematics at the University of Stockholm.
[6a] Intuitionistic Type Theory, notes  of a series of lectures given in Padua in June 1980, by Giovanni Sambin with introduction by Per Martin-Löf, Bibliopolis (1984).  Download the document: here.
[7] The Simplicial Model of Univalent Foundations, Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky (November 2012). Link to the paper: arXiv:1211.2851.
[8] The groupoid interpretation of type theory, Martin Hofmann and Thomas Streicher, Twenty-five years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol. 36, Oxford Univ. Press, New York, 1998, pp. 83–111.
[9]Type inference in mathematics, Jeremy Avigad (May 10, 2012). Link to the paper: arXiv:1111.5885.
[10]A revision of the proof of the Kepler conjecture, Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller (February, 2009). Link to the paper: arXiv:0902.0350v1.