The main goal of this reading group is to understand how close the human has come to the point where his machines can do mathematics for him. Some mathematicians, such the Fields medalists Paul Cohen, Tim Gowers, Maxim Kontsevich, and Vladimir Voedodsky have all at some point predicted that computers will be able to out-reason mathematicians in the 21st century. But is that really plausible?
To make any sound judgment on this question, we need to better understand
What is (and what should be regarded as) mathematical progress?
What is (and what should be regarded as) mathematical proof? Do we always need formal proofs to do mathematics? (c.f. theorems vs porisms )
What is the role of human intuition in mathematical reasoning and in mathematical proofs? Where do new ideas in mathematics come from?
What is the role of natural language in mathematics and how different is it from the mathematical languages in which the proofs are written? What are the limits of our mathematical languages compared to our natural language where we reason about mathematics at a meta level? And could these limits be problematic for the computers to do mathematics equally or even better than humans?
What is the machine mathematics? What are automated theorem provers (ATPs) and interactive theorem provers (ITPS) and what are their differences? Can the advances in AI, ML, and neuroscience bridge the gap between ATP+ITP and the human mind when it comes to doing (creating/discovering) interesting new mathematics?
Will we have two mathematics in future: the machine mathematics, and the human mathematics? And how do we, humans, react to such a situation? Will we simply accept the proofs generated by computers which conceivably could not be understood by any human being at all? Will such proofs have the same status as human generated proofs
These are pressing questions and we need to ransack various philosophies and foundations of mathematics that have been thought before us; they give us radically different insights to the questions above and presents us with cast territories of philosophical though. In the first session of our reading group, I will give an introductory talk charting out a basic map of these territories, and establishing some reading resources that get us going.
To put some of the discussions above in context, here is the point of view of the geometrician Bill Thurston regarding the activity of mathematicians:
The product of mathematics is clarity and understanding. Not theorems, by themselves. Is there, for example any real reason that even such famous results as Fermat’s Last Theorem, or the Poincaré conjecture, really matter? Their real importance is not in their specific statements, but their role in challenging our understanding, presenting challenges that led to mathematical developments that increased our understanding.
I think of mathematics as having a large component of psychology, because of its strong dependence on human minds. Dehumanized mathematics would be more like computer code, which is very different. Mathematical ideas, even simple ideas, are often hard to transplant from mind to mind. Mathematical ideas, even simple ideas, are often hard to transplant from mind to mind. There are many ideas in mathematics that may be hard to get, but are easy once you get them. Because of this, mathematical understanding does not expand in a monotone direction.
And he continues
Our understanding frequently deteriorates as well. There are several obvious mechanisms of decay. The experts in a subject retire and die, or simply move on to other subjects and forget. Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction
conceptual -> concrete and symbolicis much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding. And mathematical conventions and taken-for-granted knowledge change, so older texts may become hard to understand.
Here is a common sense and self-evident proposal:
What mathematicians think and do should be important for the philosophy of mathematics.
Now, if you are not familiar with the current state of affairs in the philosophy of mathematics in academia, you are for a hard surprise that the proposal above could not be further from the reality of the most of academic activities in philosophy of mathematics. Not in this reading group. We do not want to confine ourselves with the narrow interests of the academic philosophy of mathematics. Here we tend to think of mathematics as a rich network of ideas and their formal embodiements, therefore we will be concerned with the history and development of ideas, concepts, and structures in various branches of mathematics rather than reducing the content of our philosophical interest either to set theory or arithmetic. Therefore, a basic knowledge of mathematics is necessary as a background for the philosophy of mathematics. To get started, perhaps the best introduction is Saunders MacLane’s Mathematics Form and Function.
In particular, we shall try to ask questions such as
When do we call a kind of knowledge mathematical? How does mathematical knowledge grow? What is mathematical progress? What makes some mathematical ideas (or theories) better than others? What is mathematical explanation? etc
I believe in epistemological anarchism, that is, if needed, we have to be receptive to ideas from the most disparate and apparently far-flung domains, even at the price of losing the comfort of our nests. Therefore, in this reading group we will remain open to all ideas and philosophies as long as they are helpful to our goals and hopes discussed in above. May this group be a place for deep learning (and deep unlearning/ unindoctorination) as well as unashamedly free speculations. We will review the main tenets of the following philosophies and foundations of mathematics:
(2) Introduction to formal logic and formal proofs: From Aristotle’s Prior Analytics to Frege’s Begriffsschrift]: slides
(1) Introduction to Logicism an Frege’s Begriffsschrift, slides, video recording
(0) The initial meeting: Introduction to Kant’s philosophy of mathematics, slides, video recording
(-1) The Roots of Constructivism and Intuitionism in Mathematics - Part II This talk introduced various aspects of intuitionism and its vast differences from the classicial foundation of mathematics (ZFC set theory built on top of the classicial logic). Topics discussed included Brouwer’s writings, BHK interpretation, the principle of excluded middle, the axiom of choice, the continuum, the role of real numbers in classicial and intuionistic mathematics, and the creating mind’s perception of time.
(-2) The Roots of Constructivism and Intuitionism in Mathematics - Part I This talk mostly centered around the role of foundations, and an informal discussion of various foundations of mathematics
Historically what has underlied the growth of our cognitive capacity for generating and understanding new mathematical concepts is basically the recognition of our increasing tolerance for thinking the insane.
In below, I list some of the references which I personally found interesting, intriguing, and edifying. Occasionally, we will discuss some of them, but we do not limit ourselves to them.
Also, there are a lot of interesting articles on logic, philosophy and foundations of mathematics by John Bell. John was my former mentor. John is a master in tracing back mathematical ideas to their origins in a very rare and particular way which I call “demummification” of mathematical ideas. He has also had a very interesting life which you can read here: Perpetual Motion: The Making of a Mathematical Logician.
Regarding mathematical proofs we shall discuss the following these: (i) Proofs are abstract mathematical objects (inductively-defined data structures such as plain lists, boxed lists, or trees) which are constructed according to the axioms and rules of inference of the logical system. (ii) Proof is not manipulation of meaningless syntactic symbols, as the manipulists, or strict formalists, would have it. The knowledge of truth is gained though proof.
We shall argue against the first thesis and discuss our reasons for favouring the second thesis. Our guiding arguments are essentially those of Corcoran’s:
First, belief can be an obstacle to finding a proof because one of the marks of proof is its ability to resolve doubt. Second, we usually don’t try to prove propositions we don’t believe or at least suspect to be true. Third, the attempt to find proof often leads to doubts we otherwise never would have had. If you have a treasured belief you would hate to be without, do not try to prove it.
However, the second thesis is far from perfect: it does not have the formal force of the first thesis which led to the creation of wonderful mathematical fields such as proof theory and constructive type theory. Also, how does the claim that
the knowledge of truth is gained though proof holds against the Zero-Knowledge Proofs (ZKPs) whereby the proof convinces the verifier to any high degree of certinty (strictly below 100%)
Some stuff on proofs
Visual proofs and the role of visual reasoning in mathematics
We will get familiar with the following philosophies and foundations of mathematics.
The following papers give a good introduction to the structuralist thinking within simple kinds of structures.
Paul Benacerraf. What numbers could not be. Philosophical Review, 74:47–73, 1965
A categorical formulation of the structuralist thesis is in
Steve Awodey. “Structure in mathematics and logic: A categorical perspective“. Philosophia Mathematica, 4(3):209–237, 1996
and a follow-up:
Steve Awodey. “An Answer to Hellman’s Question: Does Category Theory Provide a Framework for Mathematical Structuralism“, Philosophia Mathematica, 2004
Feferman, S. “Categorical Foundations and Foundations of Category Theory”, 1977.
Good introductions to category theory are:
On the relationship between the structuralist thesis and the univalent foundation:
On the relationship between category theory and the set theoretic foundation:
Intuitionistic and constructive mathematics and type theory
Logic is philosophy’s essence [...] It is the science whereby we are enabled to test reasons.
Prior Analytics, Aristotle, 350 B.C.E : the first time in history when Logic is scientifically investigated and it is about deductive reasoning, known as syllogism. The Prior Analytics is part of what later Peripatetics called the Organon.
A very good place to learn the basics of modern logic is van Fraassen’s Formal Semantics and Logic. For other standard references have a look at the big books of logic. Also, for extra resources, see here.
Logic, semantics, metamathematics, Papers from 1923 to 1938, by Alfred Tarski, translated by J. H. Woodger, second edition edited and introduced by John Corcoran, Hackett Publishing Company, Indianapolis 1983
Syntax vs semantics The distinction between syntax and semantics is one of the fundamental distinctions in the modern logic. We have to understand the origins of this distinction better. Some have traced it back to Frege. Also see this article by Szabó
The conception and perception of the universal objects in category theory (c.f. Husserl’s ideas on the universal objects)
We shall not cease from exploration And at the end of all our exploring Will be to arrive where we started And know the place for the first time
There is a lot to be said about the mathematical notations and symbols: for millenia they have been cognitive technologies enabling us to think previously unthinkable thoughts. For instance, take Khwarizmi’s solution of the problem of solving the quadratic polynomial equation:
If some one says: “You divide ten into two parts: multiply the one by itself; it will be equal to the other taken eighty-one times.” Computation: You say, ten less a thing, multiplied by itself, is a hundred plus a square less twenty things, and this is equal to eighty-one things. Separate the twenty things from a hundred and a square, and add them to eighty-one. It will then be a hundred plus a square, which is equal to a hundred and one roots. Halve the roots; the moiety is fifty and a half. Multiply this by itself, it is two thousand five hundred and fifty and a quarter. Subtract from this one hundred; the remainder is two thousand four hundred and fifty and a quarter. Extract the root from this; it is forty-nine and a half. Subtract this from the moiety of the roots, which is fifty and a half. There remains one, and this is one of the two parts.
And all these words and their meaning are compressed in in modern mathematical notation.