Curry Howard Lambek Stone Tarski Scott Grothendieck Voevodsky Löf Brouwer Heyting Kolmogorov Correspondence

A first question that might have crossed your mind while reading this is, what is up with the absurdly long title? There are two reasons:

1. This correspondence spans multiple fields. The work of many a great mind from a variety of port of calls have cumulatively unearthed this picture. This is one of the reasons the list is so huge, but even after listing a dozen of that names, I am still doing grave injustice to people involved like Tait, Lawvere, Kleene, de Bruijn, Priestley, Makkai and a whole lot of others who have made massive contributions in furthering our understanding of various aspects of this correspondence
2. This is still an emerging picture being worked out in many fields with a lot of details to be thoroughly worked out to get to a clarified idea of what is up. This will enable new research and existent work getting connected with the ideas here and more names being added to this list. This could lead to the work of even those who might have passed away retrospectively enriching our idea about this picture. This is motivation for us to actively engage with these ideas and figure out the relationships playing out here.

So now, you might be wondering, what is this all about? To give a brief summary, there’s a deep set of correspondence happening across some domains proximate to computation that is pointing at a unified picture. I choose to concentrate on computation, logic, type theory, topology, and category theory in this article, but towards the end, I will reveal more details on what other fields are involved. As a result of the cumulative work of some brilliant minds, an amazing picture is unfolding that shines light on an underlying harmony between different aspects of computation. But I find that there isn't many resources online that talks about this big picture without delving deep into the formalisms. I hope to help a curious person to work their way into the thick of this amazing ideas without the heavy apparatus of formalisms standing in their way. But let me say upfront that, the hard lifting is necessary if one is to make advances in understanding these ideas deeper. I can only offer superficial pointers on what is happening. This guide is no substitute for hours of dedicated work in gaining intuition by working through the formalisms involved yourself. And such work comes with the prescient benefit of making some advances on these ideas yourself! So let’s get started uncovering the story playing out here.

The idea of computers is deeply interconnected with the history of mathematics. The constructivism trend emerging in the early 19th century had as one of its central tenets that the existential proof of mathematical objects one claims should supply ways for constructing them to be of valid existence. This trend sort of intensified with Brouwer’s ideas. Figure out Poincaré’s role here. These ideas would lead on to what we see today. But classical proofs also are present in this story as their computational content has also been under investigation. Point to some resources like that Charles Stewart dissertation as learning resource for this.

TODO: Decide if I should start by explaining what a formalism, logic, logical theory, quantification, predicate logic, propositional logic etc. is for someone who might be totally new entrant to this. There is a high chance that most of the readers might not have the sufficient logical background to understand what is going on.

There are many places to start telling this story, but a renowned starting point is the starting of the 20th century where Hilbert began his programme for finitistic foundations of mathematics. This lead to a flurry of activities among which many significant mathematical results. Gödel incompleteness result, Lambda Calculus, Combinatory Logic, Schönfinkel and other such resources to read about what happened. I need to mention the works like Logicomix and Engines of Logic here. Now once you have familiarized yourself with these, what has since unfolded from this point is an astounding number of results surrounding constructive mathematics and computation. Constructive mathematics is ... use this as a starting point to connect with Troelstra’s history of constructivism.

There are two histories: Logicomix and Engines of Logic which are worth reading here. Both of these start the story from Llull/Leibniz and proceed on to show how the idea of computation in an analytic thread unravelled before us. But in my researches and especially because this connects with logic and topology in general, another strand of Leibniz’s work on modal logic, calculus, and topology needs to be explored and in this direction, we can see the ideas connecting with that of Kant and the empiricists and how that lead to influence Hilbert and Brouwer in building their philosophies of mathematics. I am yet to chance upon a book that tells this history, but for the interim, this paper by Troelstra is a really good catalogue of the constructivist strand and their cumulative work.

In search of foundations

By the end of the 19th century, a lot of results were getting accumulated. TODO: Cantor's work on set theory and Kronecker? find out the results that were getting accumualted. There was this ambience around that the mathematical results need to be unified and cast on strong foundations. Three school stood influential in this period: Frege, Russell, and Whiteheads Logicism, Brouwer’s Intuitionism, Hilbert’s Formalism.

Shortly before Hilbert, there was algebraization of logic in the British school, shortly before that the advent of strong currents of algebraic thinking, and before that formalization of logic by the medieval schoolmen, development of Aristotle’s logic in the Arab golden age, Greek schools of logic, Aristotle’s development of formal logic, and the philosophical debates in various Greek schools. These events that happened in the Western tradition of logic need to be understood to some degree to get a feel for how logic developed over the epochs to reach the form under which these are studied. But I intend to focus on the period when we started focussing on concepts closer to Computation and this is identified to be the period beginning at the end of 20th century. Dedekind was working on Zahlentheorie. In this paper one sees the definition of Dedekind cut, a recursive mode of thought, and what else? I need to look into this work and may be Kummer’s in a bit more detail. TODO: Link to each of the articles on Pre-socratic / Socratic debates, Aristotle’s development of logic, Greek logic schools, Arab golden age, formalization, medieval period, advent of algebra, British school logic. TODO: May be show the countries in which these movement took root? Formalism - Intuitionism, Nominalism - Realism, Rationalism - Empiricism May be create a triad out of this and locate the people you have studied in this? Most of the ideas mentioned here had the harmonious work of history and cooperation of various milieus partaking in this activity giving us some of the most astounding instruments and results of mathematics.

The accumulated work presented a possibility to cast the results so far in a universal symbolic language. There were three people: Frege, Peano, and Russell who were interested in such a logicistic process

TODO: Research about Bolzano and Brentano’s position

For Hilbert, we have access to the infinite, only through finite means. And reflecting this philosophy, he wanted to prove the consistency of mathematics in finitistic methods.

Hilbert gives 23 problems. There is a very interesting 24th problem, which is rather unnoticed when talking about it, which connects up with intuitoinistic logic. Now, after the 23 problems, Hilbert returned to the foundational issues a few years after the publishing of Principia Mathematica. While he praised the effort of Russell and Whitehead in the beginning, he chose to go in a different route. For him, the Kantian influence of mathematics as distinct from logic was a central influence. He considered there to be some extralogical content such as numbers which precedes logic. So this idea of formalization combined with the idea of proving consistency of mathematics by finitary means were the two central ideas driving his program. TODO: Verify after reading other papers if this is an adequate framing of his program

Hilbert’s address in 1900. Already here we can see the consistency proofs making an appearance as the ?th problem. From here Hilbert went on to give a shape to his program. TODO: What was his motivation factor behind giving shape to the program? The idea was to secure the foundations of mathematics in the ambient context of many antinomies getting unearthed.

A pivotal moment was when Hilbert asked for the consistency proof of all theories(?) in mathematics and this lead to investigations in the theory of numbers as most branches of mathematics had deep connections with the theory of numbers. One of the most important idea here was the theory of natural numbers as theorems proved in this framework would have reverberations all across mathematics. TODO: Research if everything can be reduced to arithmetic

TODO: Give a brief introduction to the idea of logical form. And how this makes the concept of an algorithm possible. Put this near the models of computation section and may be briefly outline how Lambda Calculus is such a rewriting calculus where the logical form is preserved? That is the functional mapping between entities?

Background to the Hilbert program

Kronecker vs. Cantor. Traditional mathematics. May be mention the idea of Salve Veritate -> Identity of Indiscernibles -> Sense and Reference idea Venus is the evening star / Venus is the morning star President example from StackOverflow Cantor opened up a whole playing field opening up ideas like set theory, idea of cardinals, ordinals, hierarchy of infinities, new kinds of real numbers like transcendental numbers which can't be captured by any closed algebraic equation. This means that you can’t write an expression for these numbers using +, -, *, /, or the powers. Probably this is a good point to introduce Diagonalization? And this didn’t come easy, it attracted some intense controversies echoes of which continues to this day. And the idea of the constructive interpretation Hamkins’ poster of counting ordinals. Controversies: Cantor vs. Frege Poincaré vs. Cantor Frege vs. Hilbert Cantor vs. Kronecker Hilbert vs. Brouwer TODO: Brief overview of Cardinals vs. Ordinals. The use of them in real analysis and limit point. TODO: Link the work being done by J. D. Hamkins. May be his talk?u TODO: Add details on Continuum Hypothesis, ZF + C TODO: Add details on Church-Turing Thesis, Gandy’s Principles of Mechanism TODO: Transfinite recursion TODO: Mention books that dig into the history of infinity such as: Understanding the Infinite: Shaughan Levine The Logic of Infinity: Barnaby Sheppard Finite vs. infinite content. Kant’s conceptualization and his view on antinomies.

There is a popular opinion that Gödel’s incompleteness theorems brought Hilbert program to a halt, but this is highly contested among professional historians and mathematicians. Hilbert’s opinions changing over the course of time and his nuanced philosophy is also significant factors in arriving at a conclusion on this.

A really good book to learn about this is Logicomix. This book tells the story of this period with Bertrand Russell as the main protagonist. The comic is well written by giving equal space to most of the characters involved and is an engrossing read about the psychological struggle of working on ambitious projects. If you want to dive a bit deeper and get a taste for some of the mathematics involved Martin Davis (who contributed to the solution of Hilbert’s 10th problem from those he proposed) is another great read in this direction. It tells the story starting with Leibniz’s vision of Characteristica Universalis / Calculus Ratiocinator carrying it to modernity. TODO: Give a bit more detail on the table of contents here.

Finitary mathematics

There are certain techniques and results like the continuum hypothesis, diagonalization, the halting problem which are the landmark ideas in the map of mathematics powering computation theory which are worth understanding. I can only hope to give brief summaries of these ideas here. But they are well worth investigating deeper to get a feel for the landscape. These techniques were used in ingenious fashion by the people involved to reveal some striking observations on the nature of computation. Diagonalization, Cantor would resuscitate the medieval idea of different levels of infinities discussed in theology and would work on formalizing these in mathematics. Cantor’s work had definitive theological undertones to it and was even called theology by his rival Kronecker. Sketch in a very brief way the hierarchy of numbers and reveal how N, squares, Q have same cardinality but not R. Show how R is defined in various ways. This could be a later todo. Now show how diagonalization was used here. The connection between diagonalization and Russell’s paradox by making use of the classical vs. constructive framework might be a nice thing to add. TODO: Understand how Kauffman studies the Liar’s paradox using the fixed point operator and makes use of Lawvere’s proof here. In a sufficiently powerful system such as one that is capable of expressing arithmetic, you get a complementary trade off between consistencey and completeness. Its a two choices, pick one situation. Mind you, there are other systems like the Presburger arithmetic, which is complete. It is only in systems which can be arithmetized so as to have a ceratain kind of self-referentiality that this phenomena occurs. Cantor was overtly theological in his investigations and was attempting to understand the nature of God with his excursions in the infinitary paradise. TODO: Think if I need to add that book by Amir Aczel here. Transfinite numbers. These are the numbers that come after the numbers are listed. So he essentially created an infinite number of numbers after infinity. After you establish something as existing after infinity, then you get a sort of meta-recursion of the ideas you have established with numbers after, w comes w. So if at some level you sort of assume as having the finite numbers having reached a conclusion, you can use that as the starting point and make a subset out of those and reach one level further. This sort of always unboundedly going further was a hallmark of the kind of paradoxes that were getting unearthed. Such silly/deep ideas had deeper implications for the kind of things we want to to do with computers seen at large. Diagonal argument, where you can get out a new set from the already established set. Now what happens when you imagine the set of everything? You land in a conundrum. The set of everything already contains everything and you can't add any more to it. A key step of such a set that contains everything is made by attempting to create a negative predicate and creating a set of everything that doesn't contain themselves, you arrive at a paradox. It leads to a paradox where something has to not belong to itself in order to belong to itself. This sort of ideas result in a contradcition where a predicate is both true and false at the same time. There are many ways to resolve this paradox such as settle for accepting that a statement can both be true and false at the same time, avoid the use of universal set by careful axiomatization, and construct a meta theory of types to indicate that no such self-referential construction of types is possible. This last one is of significant import for the ideas that unfolded in the aftermath of these foundational crises.

All this would eventually come pointing at the discourses in ancient times such as that between Heraclitus and Parmenides. A small sampling of this history can be seen here. But the important points regarding this is how the Eleatic paradoxes of One vs. Many would be resolved by Plato and Aristotle by eliminating the actual infinity from scientific usage. If you see parallels between the finitistic views and this idea of eliminating the talk about complete infinity, you would be seeing the echoes from that times until modernity where the philosophers have taken a specific position in this eons long debate on the foundations of philosophical inquiry.

Models of Computation

TODO: Link the image of the Diophantine problem of Hilbert.

The Decision Problem

Now that we have seen what a model of computation is and how it helps formalize the notion of an algorithm, let us get to the central question that drove these ideas. The so called Enstcheidungsproblem. Decision problem also known as Entscheidungsproblem was a central locus of attention for the mathematicians who were involved in this. It was proven in the negative by both Church and Alan Turing independently. Alonzo Church proved this before Turing, which made him do a dissertation under him where he sort of tries to “escape out of Gödel’s incompleteness by constructing a tower of ordinals”.

Crisis in the foundations

TODO: What motivated Hilbert to propose the program? How was he trying to secure the foundations using finitary mathematics.

Formalism and Intuitionism

TODO: How is Hilbertism different from these? Garlandus article on Göttingen.

Arithmetization of Syntax

Show the idea of a machine printing from Raymond. Give links to the work of Gödel as a thread or in Github which makes it easy to consume for a new entrant.

The Halting Problem and Undecidability

Provide resource to understand the work of Alan Turing. Undecidability is this sort of conundrum where you as an entity cannot make up a decision on whether you do one thing or another. This is the kind of thing that is present when we have a computer try to determine if an algorithm halts or not. Even if you have a formal system, which is what Hilbert’s program implied, you still get into trouble and Turing made an ingenious use of diagonalization to show that even if you try to arrange the proofs in size order, there’s a way to apply the same techniques used by Cantor to show that you cannot enumerate the list of proofs. So in effect, there’s no way to determine mechanistically if there exists a proof. This opens up a creative space for devising proofs. The same conclusion was arrived on by Post. Related ideas to undecidability are verifiability, satisfiability (in the semantic notion) as developed by Skolem and Löwenheim, this finds a dual representation in the proof theoretical tradition in the results found by Herbrand/(Bernays/Gödel(?)) as provability and (in)consistency. TODO: Provability, Satisfiability, Verifiability, Consistency, Completeness, Soundness, Independence, Finiteness, Decidability, Tautology, Contingency, Contradictory, P vs. NP, Categoricity(?). Create a concept map of what implies what and how the relationship changes as settings change. Show how P vs. NP is connected with these ideas. An undecidable problem was mentioned by Dehn in the 1900s (TODO:make precise) where you cannot determine conclusively the word problem. TODO: Briefly describe this problem and may be mention the multiple model aspect of Whitehead’s problem. I am actively trying to investigate these ideas at the moment and I will definitely add more details in here on the details involved if I can abstract them to a level accessible from the scope of this essay. I think it is a richly woven tapestry worth examining in detail! Now given a time frame, we can determine if a program halts or not. What Turing essentially proved is that given a problem before hand, there is no way to know if it would halt or not.

Meet the constructivists

List the intuitionists of the period. TODO: Give a brief sketch of how these people’s views differed TODO: Find out how close the realizability interpretation of Kleene is to the BHK interpretation.

Boon in the bane

This search for what exactly is formalizable would result in the theory of algorithms from multiple ends. Here are the list of models of computations that were put up in this period: TODO: Insert Models of Computation image Then there are further directions the work from here was carried out by people such as Kolmogorov with his complexity measure and Gregory Chaitin with his algorithmic complexity theory. TODO: Investigate what other strands have been spun off from here in the direction of theory side A and theory side B. The benefit of studying these ideas are three-fold:

1. They give you a technical toolkit to work with
2. They give you fluency to explore the edifice that has been constructed. Understanding about these ideas give you a frame of reference from which you can say, this one is like that but with a twist.
3. Imbibing the details about the variety of ideas present here, one gets a sense of direction to navigate the jungle of formalism and develop a keen intuition on where to direct one’s efforts so as to make the most out of the time they are investing in this.

These constitute a standard toolkit for the working logician. Along with providing practical benefits in solving certain problems, they also provide tractability in the form of metaphors to talk about the problem and to map them on to these abstractions, so that a logician can find out where they fit/misfit to detect the shape fo the problem they are tackling. Now that we have seen the history in a brief detail, let us just summarize the kind of conflicts between opinions that existed among the famous figures. I will only outline very briefly the skirmishes among the schools here and relegate a detail discussion to another essay. But the central figures to note here are: Kronecker (Finitism), Cantor (?), Frege (Logicism), Poincaré (?), Hilbert (Hilbertism?), Who is a good candidate for formalism(?), Brouwer (Intuitionism) There are other ideas at this time like that of Skolem (recursive mode of thought), Formalism (Curry/Schönfinkel) active at the time