‘Reverse Mathematics’ Illuminates Why Hard Problems Are Hard
In reverse mathematics, researchers replace axioms, the foundations of mathematical systems, with the theorems they want to prove.
Son of Alan for Quanta Magazine
Introduction
When it comes to hard problems, computer scientists seem to be stuck. Consider, for example, the notorious problem of finding the shortest round-trip route that passes through every city on a map exactly once. All known methods for solving this “traveling salesperson problem” are painfully slow on maps with many cities, and researchers suspect there’s no way to do better. But nobody knows how to prove it.
For over 50 years, researchers in the field of computational complexity theory have sought to turn intuitive statements like “the traveling salesperson problem is hard” into ironclad mathematical theorems, without much success. Increasingly, they’re also seeking rigorous answers to a related and more nebulous question: Why haven’t their proofs succeeded?
This work, which treats the process of mathematical proof as an object of mathematical analysis, is part of a famously intimidating field called metamathematics. Metamathematicians often scrutinize the basic assumptions, or axioms, that serve as the starting points for all proofs. They change the axioms they start with, then explore how the changes affect which theorems they can prove. When researchers use metamathematics to study complexity theory, they try to map out what different sets of axioms can and can’t prove about computational difficulty. Doing so, they hope, will help them understand why they’ve come up short in their efforts to prove that problems are hard.
In a paper published last year, three researchers took a new approach to this challenge. They inverted the formula that mathematicians have used for millennia: Instead of starting with a standard set of axioms and proving a theorem, they swapped in a theorem for one of the axioms and then proved that axiom. They used this approach, called reverse mathematics, to prove that many distinct theorems in complexity theory are actually exactly equivalent.
“I was surprised that they were able to get this much done,” said Marco Carmosino, a complexity theorist at IBM. “People are going to look at this and they’re going to say, ‘This is what got me into metamathematics.’”
Pigeon Proofs
The story of the reverse-mathematics paper began in the summer of 2022, when Lijie Chen, a complexity theorist now at the University of California, Berkeley, was wrapping up his doctorate. He found himself with a lot of extra time on his hands and decided to devote a few months to reading up on metamathematics.
“Because I was graduating, I didn’t have much research to do,” Chen said. “I was figuring I should learn something new.”
As he read, Chen began thinking about a branch of complexity theory called communication complexity, which studies the information two or more people must exchange to accomplish certain tasks. One of the simplest problems in communication complexity, called the “equality problem,” is like a collaborative game. Two players start with separate strings of 0s and 1s (or bits). Their goal is to use as little communication as possible to determine whether their strings are the same. The simplest strategy is for one player to just send their full string for the other to check. Is there any way to do better?
Complexity theorists proved decades ago that the answer is no. To solve the equality problem, the players need to send, at a minimum, a number of bits equal to the number in the full string. Theorists say that this string length is a “lower bound” on the amount of communication needed.
Chen wasn’t focused on the equality problem’s lower bound itself — he was interested in how researchers had proved it. All known proofs depend on a simple theorem called the pigeonhole principle, which states that if you put some number of pigeons into a smaller number of holes, at least one hole must end up holding more than one bird. That may sound self-evident, but it can be a surprisingly powerful tool in complexity theory and beyond.
Chen had hit upon a tantalizing hint that the link between the equality problem and the pigeonhole principle might also go the other way. It’s easy to use the pigeonhole principle to prove the equality problem’s lower bound. Could you instead use the lower bound to prove the pigeonhole principle?
Uncanny Equality
Chen discussed his idea with Jiatu Li, at the time an undergraduate at Tsinghua University with whom Chen had recently collaborated on another paper. To make the connection rigorous, they would have to choose a set of axioms to work with. Metamathematics researchers prefer to use axioms that are more restricted than the typical ones. These weaker axioms make it easier to pin down the precise relationships between different theorems. Chen and Li decided to work with a popular set of axioms called PV1. PV1 is strong enough to prove some important theorems about computational complexity on its own. Add a specific version of the pigeonhole principle as an extra axiom, and you can also prove the equality problem’s lower bound. In December 2022, Li and Chen formally showed that, as Chen had suspected, the proof also works with the two theorems interchanged.
Igor Oliveira helped helped prove that many different theorems are actually equivalent.
Richard Cunningham
The fact that you can prove the equality problem’s lower bound from the pigeonhole principle or vice versa implies that within the logical framework of PV1, the two theorems are exactly equivalent. When Li and Chen discussed the result with Igor Oliveira, a complexity theorist at the University of Warwick, the trio realized that their reverse-mathematics method might also work for theorems in other far-flung areas of complexity theory. Over the following months, they systematically proved equivalences for many other theorems.
“At the beginning, we only had two equivalent things,” Chen said. “But now we have a big web of stuff.”
The team’s most striking connection related the same version of the pigeonhole principle to one of the first theorems that students encounter in introductory complexity theory courses. This “classic banger of a theorem,” as Carmosino described it, sets a lower bound on the amount of time required for a type of theoretical computer called a single-tape Turing machine to determine whether a string of 0s and 1s is a palindrome (that is, whether it reads the same forward and backward). Li, Chen and Oliveira used reverse mathematics to prove that within PV1, this palindrome lower-bound theorem is equivalent to the pigeonhole principle.
“If you told me this, I wouldn’t believe it,” Chen said. “It sounds very ridiculous.”
The equivalence between the palindrome lower bound and the pigeonhole principle is surprising because the two theorems are so superficially different. The pigeonhole principle doesn’t inherently have anything to do with computation: It’s a simple statement about counting. The palindrome lower bound, on the other hand, is a statement about a specific model of computation. The new result implies that such seemingly narrow theorems are more general than they appear.
“It suggests that these complexity lower bounds we want to understand are much more fundamental,” Oliveira said.
Uncharted Territory
This new web of equivalences has also helped illuminate the limits of PV1. Researchers already had reason to believe that the pigeonhole principle can’t be proved from the axioms of PV1 alone, so Li, Chen and Oliveira’s results imply that their other equivalent theorems are also likely unprovable in PV1.
“I think it’s beautiful,” said Ján Pich, a complexity theorist at Oxford University who proved a big result about the power of PV1 in 2014. But he cautioned that the reverse mathematics approach may be most useful for revealing new connections between theorems that researchers have already proved. “It doesn’t tell us much, as far as we can say, about the complexity of statements which we do not know how to prove.”
Understanding this uncharted territory remains a distant goal for metamathematics researchers. But that hasn’t tempered Li’s enthusiasm for the subject. He started graduate school at the Massachusetts Institute of Technology in 2023, and he recently wrote a 140-page guide to metamathematics for complexity theorists. It’s one example of a broader trend: After decades of relative obscurity, metamathematics is increasingly attracting attention from a wider community of researchers who bring new perspectives to the field.
“People are tired of being stuck,” Carmosino said. “It’s time to just step back and work out the foundation.”
