In principle...
On existence, construction, and intuition
Philosophy calls scepticism the Biblical tale of Doubting Thomas: I must see it to believe it! And “seeing” for Thomas and the sceptics means to present something in the concrete.
This article is not a Biblical tale however, but one about the foundations of mathematics or, more generally, on ways of thinking about science and mathematics. Does a number one can never write exist? Can we construct an argument using an object which we proved exists, but know nothing else about it? Or perhaps we must also be a Doubting Thomas — any existence must be a concrete one, we must write it to see it?
The opposition between the two viewpoints was an important motivation for the development of proof assistants and the mathematical study of programming languages. The connection between them — induction.
Formally, my dear Hilbert!
In both theoretical and practical research, the essential is sought after. The analytic method — whose etymology traces it precisely to decomposition in ever smaller parts — is a precious tool in any researcher’s kit. The ancients were already thinking about atoms, that which can no longer be cut, a-tomos. The Greeks have pondered atoms in abstract ways: Zeno and Democritus speak about atomic time periods, while in the Indian philosophy, in multiple creation tales, atoms appear as building blocks of the Universe, thus giving them a material meaning.
Jumping forward to the nineteenth century, mathematics starts to raise questions about its own atoms. Researchers such as David Hilbert, Gottlob Frege, Bertrand Russell, and their peers attempt either an analytic search or a generative one. In other words, they ask what are we left with after extracting the essential from any theorem and definition or what should the fundamental starting objects be if we try to obtain all of mathematics?
The historical context was adequate, as around the same time, the Russian-born German mathematician Georg Cantor (1845-1918) had recently published the foundational papers of set theory. He established and regulated the existence of sets, those mathematical objects which many considered to be elementary, precisely because of their almost total lack of internal structure. To be able to obtain anything in mathematics, one clearly must start with objects that are as general as possible. Around the same time, mathematical logic added something to the mix, through the works of Gottlob Frege and Bertrand Russell: Foundations of Arithmetic (1884) and Principia Mathematica (1910-1913 for the first edition) respectively. They show that there is an almost mandatory connection between sets of numbers and mathematical logic.
Such evidence amounts to saying that since mathematical proofs use logic and any mathematical object is, essentially, a set itself or an element of a set, it follows that logic and set theory are the foundations of mathematics. Put differently, any theorem can be reduced to one about sets, expressed using logic; conversely, starting with specific sets and using carefully picked logical methods one can obtain any theorem.
This confident program was called logicism and the Principia Mathematica, along with the Foundations of Arithmetic tried to add more arguments towards reducing mathematics to logic and set theory.
The trust in such abstract foundations can be found in the research of David Hilbert (1862-1943) as well. He proposes a program called formalism and expressed by some critics as Mathematics is just a game of meaningless marks on paper, following certain rules. Through formalism, Hilbert proposes that mathematics should start with objects and tools that are so abstract, that the results one proves using them remain valid regardless of the concrete interpretation of said objects. To understand this, think about the arguments that are studied in high school, such as:
All A are B.
x is A,
therefore, x is B.
Nowhere have we mentioned what A, B or x were, so the argument is as general as it can possibly be. This means that it is true even if, say, A is a fruit, B is a human trait and x is a colour, provided one can establish such truth to begin with. The form we use to express it is fundamental, not its realization.
Hilbert’s approach was related to axiomatization, following the program he presented at a mathematical congress in 1900, which contained 23 problems that mathematicians had to solve as soon as possible. Among them, some about the search for foundations in the form of axioms: principles and statements that are accepted as true, abstract forms on which further results should rely.
Intuitively, my dear Brouwer!
History records Hilbert reading a proof of a theorem which contained a statement that some mathematical object exists, but the object never appears in the concrete. That is, the proof relied on an object whose existence was established, but the author could not and need not construct. Hilbert is said to have exclaimed, as a Doubting Thomas: This is not mathematics, this is theology! Subsequently, as more such proofs have reached his eyes, he sighed with resignation: I must admit that even theology has its merits…[1]
The Dutch Luitzen E. J. Brouwer (1881-1966) was not so easily convinced. More deeply rooted in philosophy than Hilbert, but with remarkable results in mathematical analysis and topology, Brouwer had a daring idea: one should never accept in mathematics any existence which could not be constructed, even in principle. Any mathematical statement containing an argument of the form there exists x such that… must either be followed by a concrete method of obtaining said x (concluded either with a concrete realization, such as x = 5, or a procedure one could finish), or otherwise completely abandoned.
This is the birth of the main opposing beliefs for logicism and formalism. They are called intuitionism, which contains the belief that humans possess an abstract sense — intuition, which allows one to “see” and finalize abstract constructions — and constructivism, which imposes concrete constructions.
What does it mean to construct something in principle and why is it so important that we titled the article with it? Requiring concrete constructions for any mathematical object means banishing infinity from all of mathematics. The sequence of natural numbers, 0, 1, 2, 3,…, becomes forbidden, as one could never concretely construct it entirely. But we can do it in principle. Here is where Brouwer’s and his peers’ subtlety comes into play, allowing applications in computer science decades later. If a construction is expressed in the form of an algorithm or a procedure, then it can be finalized in principle, since at every step the following one is prescribed. In the case of natural numbers, the procedure is called the successor: we are allowed to step further to the next natural number by adding one. Clearly such a procedure never finishes concretely, but it is accepted by Brouwer because it can be completed in principle.
In this context, the connection with mathematical induction is manifest and through it, that with proof assistants, as well as a good part of modern computer science. In the linked article above, we detail such aspects.
Incomplete, my dear Gödel!
The mathematical and philosophical systems presented showed their limitations and were even refuted, each in their own way. It took only a couple of decades and the genius of the Austrian Kurt Gödel (1906-1978), considered by some the most important logician since Aristotle. The theorems he proved were the subject of a significant body of research and popular science articles, since they rigorously prove a fundamental flaw, which some attributed to mathematics, while others, to human reasoning. Gödel proved that we must make a choice:
either we construct a system based on axioms which can be used to prove any theorem, but that system will contain contradictions — namely some theorems could simultaneously and correctly be proved to be true and false;
or, if we don’t want any contradictions, we must accept the existence of results which can never be proved. This is not due to their immense difficulty, but to an extreme peculiarity of mathematics: one can prove that some results cannot be proved!
In technical terms, one must choose between contradiction and incompleteness.
Gödel’s theorems showed that a search for foundations is impossible since it certainly ends bad: either in contradictory statements, or with unreachable results.
What about intuitionism? The blow to it was not as hard, but the program of the intuitionists is one particularly difficult to begin with. More than a century later, mathematicians still struggle to recast in intuitionistic form parts of mathematical analysis that are known since the 1700s. Therefore, Brouwer’s program is much more than a reform — it is an actual rewriting of all mathematics.
Whether such a conclusion is equivalent to Doubting Thomas’ version of mathematics remains to be seen. What is clear is that Hilbert’s form of theology has led us so far. Its dogma seems to have been It exists, that suffices. Is Brouwer’s intuitionism realizable? In principle…
The thumbnail image is from Caravaggio’s painting, “The Incredulity of Saint Thomas” (1601-1602)
[1] The story is almost folklore, but it is duly recorded in the biography written by Constance Reid, titled Hilbert and published in 1996.