Since the beginning of the 20^{th} century, logicians and philosophers have been preoccupied with providing mathematics with a firm logical base. The aim of the foundational project was not only to improve rigorousness of an already rigorous discipline but to shed some light on the very object of mathematics – to determine what it is *about*.

Due to sudden developments in formal logic in the beginning of the 20^{th} century, mathematicians such as B. Russell, G. Frege and D. Hilbert among others counted on logical concepts to provide such base. Arithmetic and geometry were thought to stem from simple logic, and the goal was to simply formalize it once and for all. However, the task turned out to be more complicated than expected.

In his nominal foundations program Hilbert proposed the hypothesis that all of mathematics could be axiomatized in such a way that all its true statements of the day, as well as those of the future, would be mere logical conclusions of these basic postulates. The project was put to end by the famous Gödel’s first incompleteness theorem, stating that in each sufficiently strong formal system there are true statements that are not derivable as logical conclusions of that system.

Many, however, continued their quest for a foundational theory and one particular set theory, called ZFC (for Zermelo-Fraenkel set theory with the Axiom of Choice), became a widely accepted candidate. It turned out that all of mathematics could be expressed in ZFC. Gödel’s theorem still applied, however since true and non-provable sentences are not objects of everyday mathematical research, they could be simply ignored for the most part – although stripping the theory of its grand philosophical pretensions.

Thus, although differently than originally intended, mathematics *was* in a sense explained in purely logical terms.

But with the great developments of late 20^{th} century mathematics, some scientist began to doubt ZFC’s status as a theory of logic, as well as its adequateness to the mathematical practice of the day. Each theory is based on some fundamental concepts that it can not define. In case of most set theories, the basic primitive is that of *belonging: *each object in the universe described by the theory belongs to some collection of objects called a set. In the mid-sixties, an American mathematician W. Lawvere put this very concept to doubt.

According to Lawvere, there is nothing essentially logical about the notion of belonging. His proposal was to use the more universal notion of a function instead. Moreover, Lawvere noticed that the structure of a set, as it is described by ZFC, can be described in more intuitive and more fundamental terms by means of category theory.

Category theory can be regarded as the most abstract mathematics possible. Perhaps due to its abstract nature, it turned out that its concepts suffise to describe all that can be described in ZFC without the controversially logical primitive of belonging.

But that is not all – Lawvere’s theory gave a little extra. It turns out that the mathematical structures that are in a way equivalent to those described by ZFC – called *toposes* – can themselves be easily described in geometric terms.

In fact, there is nothing surprising in the fact that a theory is related to some other theory. In logic this happens all the time, because once one has a theory, one has to provide a case when this theory is true – otherwise one has possibly built a theory that is good for nothing.

But what is striking in the case of Lawvere’s topos theory is that not only the non-logical notions such as variables of one order or another are represented geometrically, but also the logical operations, such as ‘and’, ‘or’, ‘not’, etc. The fact that even logical operators can be expressed as a kind of geometry, led Lawvere to conclude that “in a sense logic is a special case of geometry”.

Although at first sight a statement like this might seem like a new slogan with no implications, the fact that most mathematics can be thought of as logic which in turn is a kind of geometry, changes the whole picture of what mathematics is about.

A Russian philosopher of science A. Rodin notes that this picture has been present all along, since Euclid’s *Elements*. The main divergence from 20^{th} century logical-axiomatic approach is that in geometry, one mostly *constructs* things. That is, we are not at all concerned with determining what kind of figure *exists*, in geometry we only care if we can construct it.

Such view of mathematics corresponds better to both its everyday practice – including beyond geometry – and the way contemporary mathematicians see what is fundamental in the discipline itself. One of the greatest foundational projects of our time is to build a wholly constructive mathematics based on the connection between logic and topology. In 2013 a group of mathematicians released a book called *Homotopy Type Theory: Univalent Foundations of Mathematics*, providing a huge step forwards.

Although the project is not finished yet, one can see the pressing need for a newly formulated, coherent picture of mathematics and mathematical work.

**Article: **arXiv:1408.3591v2 [math.HO] 19 Oct 2014, source link.