# What is some current research going on in foundations about?

What is some current research going on in the foundations of mathematics about?

Are the foundations of mathematics still a research area, or is everything solved? When I think about foundations I'm thinking of reducing everything to ZFC set theory + first order logic. Is this still contemporary?

• Given that many mathematicians do not know the answer to this question, perhaps this is not out of scope? – Andrej Bauer Nov 14 '16 at 19:55
• Well, it would make sense to turn this question into a wiki, as there can't be "the most correct answer". – Andrej Bauer Nov 14 '16 at 20:43
• I am voting to reopen because I believe that this is not quite the same as (say) the question, "What is current research in algebra about?" Many mathematicians have a rather dismissive attitude towards foundations, as people who work in foundations can attest. This question gives researchers in foundations an opportunity to explain that there is interesting work being done. Everybody takes it for granted that there is so much interesting algebra research that it cannot be summarized succinctly, but for foundations, there is doubt in many minds that there are any interesting questions left. – Timothy Chow Nov 15 '16 at 3:00
• – Monroe Eskew Dec 12 '16 at 20:43

It is quite difficult to answer this question comprehensively. It's a bit like asking "so what's been going on in analysis lately?" It is probably best if logicians who work in various areas each answer what is going on in their area. I will speak about logic in computer science. I am very curious to see what logicians from other areas have to say about their branches of logic.

A hundred years ago logic was driven by philosophical and foundational questions about mathematics. The development of first-order logic and ZFC was one important branch of logic, but others were model theory and computability theory. In fact, computability theory led directly to the invention of modern computers. Ever since logic has had a very fruitful relationship with computer science.

One could argue that applications of logic in computer science are not about foundations of mathematics, but such an opinion can hardly be defended. Of course, many applications of logic in computer science are just that, applications, but not all of them. Some are directly related to foundations of mathematics (see below), while others are about understanding what computation is about (Turing got us on the right track, but there's a lot more that can be said about computation apart from "it's all equivalent to Turing machines"). I hope you can agree that computation is a foundational concept in mathematics, equal to such concepts as (mathematical) structure and deductive method.

We live in an era of logic engineering: we are learning how to apply methods of logic in situations that were not envisioned 100 years ago. Consequently, we need to devise new kinds of logic that are well-suited for new problems at hand. To give just one example: real-world computer systems often work concurrently with each other in an environment which acts in a stochastic fashion. Computer scientists have learned that Turing machines, first-order logic and set theory are not a very good way of describing or analyzing such systems (the computers are of course no more powerful than Turing machines and can be simulated by them, but that's hardly a helpful way to look at things). Instead they devise new kinds of logic which are well suited for their problems. Often we design logics that have good computational properties, so that machines can use them.

Another aspect of logic in computer science, which is closer to a mathematician's heart, is computer-supported formalization of mathematics. Humans are not able to produce complete formal proofs of mathematical theorems. Instead we adhere to what is best described as "informal rigour". Computers however, are very good at checking all the details of a mathematical proof. Modern tools, such as various proof assistants (Coq, HOL, Agda, Lean), are improving at a fast rate, and many believe they will soon become useful tools for the working mathematician. Be that as it may, the efforts to actually do mathematics formally are driving research in how this can be feasibly done. While some proof assistants do use first-order logic and set theory (e.g. Mizar), most use type theory. This is probably not just a fashion. It is a response to the fact that first-order logic and set theory suffice for formalization of mathematics in principle, but not so much in practice. Logicians have been telling us that in principle all mathematics can be formalized. And now that we're actually doing it, we're learning new things about logic. This to my mind is one of the most interesting contermporary developments in foundations of mathematics.

• What do you mean with "One could argue that applications of logic in computer science are not about foundations of mathematics, but such an opinion can hardly be defended."? – rere Nov 14 '16 at 20:31
• Ok, let me argue that a bit. – Andrej Bauer Nov 14 '16 at 20:33
• Nice answer. I'd be interested in references on the last two sentences of the fourth paragraph. – Paul Larson Dec 2 '16 at 2:50
• @PaulLarson: Have a look at what people are doing at the Logic in computer science (LICS), Computer science logic (CSL), Principles of programming langauges (POPL) and Types for Proofs and Programs (TYPES) conferences. – Andrej Bauer Dec 2 '16 at 9:20

When I think about foundations I'm thinking of reducing everything to ZFC set theory + first order logic. Is this still contemporary?

The only sense in which this is contemporary is that nowadays, people are actually constructing formal proofs using computerized proof assistants, as mentioned in Andrej Bauer's answer. As Andrej mentioned, Mizar is based on set theory and first-order logic, but most proof assistants use type theory. One system not mentioned by Andrej is homotopy type theory as pioneered by Voevodsky and others. Some highly nontrivial mathematical theorems have been fully formalized, such as the Feit–Thompson theorem and the Kepler conjecture.

Another active area of research in foundations is reverse mathematics, which is concerned with examining exactly which axioms are needed for various portions of mathematics. It has long been recognized that ZFC is far stronger than necessary for formalizing most of mathematics, and so there is interest in figuring out which axioms are really needed. The standard introduction to reverse mathematics is Simpson's book, Subsystems of Second-Order Arithmetic. However, there is a lot of research into axiomatic systems not treated in Simpson's book. There are weaker systems, such as bounded arithmetic, which have close connections to computational complexity theory. In the other direction, Harvey Friedman has a long-term research program to construct natural-looking elementary combinatorial statements that cannot be proved except by assuming (the consistency of) large cardinal axioms.

Although Gödel's results tell us that we cannot expect a general decision procedure for theoremhood, there continues to be research into the decidability of various finite fragments of mathematics. As mentioned by Harvey Friedman, all three-quantifier sentences of first-order set theory are decided in a weak fragment of ZF. It is also an open problem whether Hilbert's Tenth Problem is decidable over $\mathbb Q$.

By the way, it is perhaps worth mentioning that some people equate "foundations" with "logic and set theory." I personally don't agree with this equation. There is a lot of interesting technical work in logic and set theory that I would not describe as being concerned with the foundations of mathematics as such. If you're interested in current research topics in logic, this MO question provides some information.

• Is reverse mathematics still active? I always get the feeling that Simpson's book more or less finished the subject off. – Andrej Bauer Dec 14 '16 at 7:46
• @AndrejBauer : Yes, reverse mathematics is very active. MathSciNet lists almost a hundred papers with "reverse mathematics" in the title that have been published since Simpson's book. There are so many new results that there is now a "Reverse Mathematics Zoo" to help people keep track of them. rmzoo.math.uconn.edu Simpson's book didn't finish the subject; it started it. – Timothy Chow Dec 14 '16 at 18:46
• Excellent. Glad to hear it. – Andrej Bauer Dec 14 '16 at 20:54

The foundations of mathematics has undergone an astounding series of revolutions in the 20th century, which continues into the 21st. Many of the most spectacular discoveries have been in set theory, although revolutionary developments have occurred in other branches as well.

Here is a brief list of some of these developments.

1938. Godel's definition of the constructible sets L.

1963. Cohen's prof that the continuum hypothesis is independent of ZFC, provided ZFC is consistent.

1963 (and later). The discovery of the metamathematical properties of measurable cardinals.

1966–67. Silver and Solovay's discovery of $0^\#$.

1970 (and later). Determinacy and large cardinals properties. http://plato.stanford.edu/entries/large-cardinals-determinacy, section 3

1972. Jensen's discovery of combinatorial principles which hold in L.

1977. Paris and Harrington produce a combinatorial problem independent of Peano arithmetic.

1998. Friedman produces a combinatorial problem independent of ZFC (in fact having large cardinal strength). http://scirate.com/arxiv/math/9811187

A more extensive compilation would require an entire book. To mention one more area, many logicians agree that ZFC needs to be extended with new axioms; see this or this for example. In 2011 I wrote a paper which gives some new axioms that are sufficiently conservative and well-justified that it is arguable that they can be adopted at this point.

• It would be great if you could hint at what set theorists consider to be current research. Maybe expanding on the last sentence would do it. What are these new axioms about, for instance? Just more large cardinals? – Andrej Bauer Dec 14 '16 at 7:47
• This is a good example of how set theorists see foundations of mathematics. – Matt F. Dec 14 '16 at 14:21
• @AndrejBauer : Roughly speaking, Dowd takes a "minimalist" approach and uses reflection-type arguments to justify "small" large cardinals, and he is favorably disposed towards V=L. Woodin is more interested in determinacy principles, notably projective determinacy. – Timothy Chow Dec 15 '16 at 1:18
• @TimothyChow: The question of whether 0# exists can be "temporarily ignored" in arguments in favor of existence of cardinals which do not imply it. The method permits adding axions which might be more likely to be accepted, by minimalists or maximalists, even though the latter might consider the arguments academic. – Martin Dowd Dec 15 '16 at 2:11
• I am a bit amazed that after having discovered billions and billions of set-theoretic models, there are still set theorists in search of the One True Model to Rule Them All. Or am I mistaken about the motivation here? For instance, reading @MartinDowd's last comment, it certainly looks like he's in search of truth (although it looks like a social truth, since he talks about people accepting axioms). – Andrej Bauer Dec 15 '16 at 7:11

I list some relevant developments, or/and give references, in the section on "related results" (see esp. sections 4.4. and 4.5.) in my SEP entry on incompleteness theorems:

https://plato.stanford.edu/entries/goedel-incompleteness/#UndRes

and in the section 3 of my paper on Hilbert's Program: