High School Theorems
Taking a conjecture about identities to college
Alex Wilkie is a Fellow of the Royal Society, and holds the Fielden Chair in Mathematics at the University of Manchester. Ken knew him at Oxford in 1981—1982 and again from 1986. In 1993 Wilkie won the Karp Prize of the Association of Symbolic Logic, equally with Ehud Hrushovski. This is named not after Dick Karp but rather Carol Karp, a mathematical logician in whose memory the prize was endowed.
Today I wish to talk about logical theories, motivated by some questions from Bill Gasarch and others.
The questions I have been considering really revolve around the role of the exponential function, and its interactions with our tamer friends, plus and times. And subtraction. It is subtraction that causes some hitches, because over the reals, is always a positive number. The sum and product of positive numbers are positive, but subtraction makes positivity go away. Subtraction and exponentiation also cause immediate issues in computational complexity, and the meeting point of complexity and logic is what has my attention.
The Karp Prize citation for Wilkie says it is
for proving the model completeness of the field of real numbers with the exponential function.
Model completeness is a step toward quantifier elimination and decidability—it implies that every first-order formula in the theory is equivalent to an existential one, and conversely. The Karp Prize itself has an interesting stipulation. It is awarded every five years:
for a connected body of research, most of which has been completed in the time since the previous prize was awarded.
Nothing like the lifetime retro span of a Nobel Prize or Turing Award or the 14-year horizon of the Gödel Prize, which until recently was 7 years. Once a Karp Prize is awarded, everybody basically starts again with a clean slate. This was no hurdle for Wilkie, even though the famous theorem of his that this post is covering in detail dates to 1980.
A Question By E-mail
The other day, our friend and fellow blogger Bill Gasarch asked us a natural question. He asked me for the best upper bound on the theory of real arithmetic. It’s one of those things that I happened to know, and I was happy to help him get a quick reference. Sometimes people can beat Google, ha.
The answer is that the upper bound is double exponential time. This is pretty large, but it is not terrible. I have used a special case of this result that shows that solving existential sentences—essentially solving equations—is in single exponential time. This was in a paper with Markakis Vangelis that showed that Nash Games can be done in exponential time, even multi-party games.
The theory of the reals allows the operations of addition and multiplication of reals. It is a first order theory with equality, and so we can write sentences like:
This is a true sentence. Note the theory can define order: is defined as:
The axioms of the theory are all the basic properties of addition and multiplication, along with that fact that any odd degree polynomial has a root and that every positive number has a square root.
A famous theorem of the logician Alfred Tarski is:
Theorem: The theory of the reals is decidable.
Actually Tarski proved much more: he showed that any real closed field has a decidable and complete theory. A real closed field is a natural generalization of the reals. This beautiful theorem is in stark contrast to the situation of the theory of arithmetic, which by the Incompleteness Theorem of Kurt Gödel cannot be decidable. (Well it can be decidable, if it is inconsistent.) Tarski’s result is in the 1951 book: Decision Method for Elementary Algebra and Geometry.
Bounds On Decidability
But since our interest is in feasible computation, the question is lurking about. So the theory of reals cannot be too easy to solve, since it must at least be as least as hard as SAT. There are several ways to see this, some use a standard reduction, some use a direct encoding. So the real theory cannot be too easy unless .
Tarski’s original proof used quantifier elimination, and yielded a bound of the form on the running time. Many years later, Michael Ben-Or, Dexter Kozen, and John Reif proved that the theory of real closed fields is decidable in exponential space, and therefore in doubly exponential time.
Tarski raised a very interesting problem that I did not know, but found as I was writing this. Consider identities that you might find in a high school class on algebra. You might be asked to prove:
No doubt you can do this by simply expanding the left-hand side. Tarski said, let’s consider the following list of “obvious” rules for plus, times, and exponentiation:
Let’s call these HSI: for high school identities—what else? It is known that determining whether is an identity is decidable, where are terms that use plus, multiplication, and exponentiation. Tarski’s asked:
Are there identities involving only addition, multiplication, and exponentiation, that are true for all positive integers, but that cannot be proved using only HSI?
Another way to say this is: Can we use just the facts we learned in high school to prove any identity? The proof might be long and tricky to find, but does it always exist? A positive answer would have been cool—even in high school we had all the tools needed to resolve identities.
Alas, the answer is no. The HSI rules are not complete. In 1980, Wilkie found an example of a true identity that is beyond the ability of the HSI rules:
The intuitive reason this is true is that
so we can factor out , but the presence of subtraction makes this operation escape the parts of HSI dealing with exponentiation. The usual trick of representing subtraction by an existential quantifier and an addition does not work here.
See this paper by Stanley Burris and Karen Yeats for a nice survey of the area. It includes the use of Godfrey Hardy’s theorem that exp-log functions are linearly ordered by the relation modulo . It emphasizes the hunt for the smallest algebra in which HSI are true but Wilkie’s identity is not. Since then, further identities escaping proof by HSI have been discovered, and also researchers have found families of identifies that always can be proved by HSI.
Complexity Of Identities
A natural question is, what is the complexity of determining if such identities are true? Is there a fast way to test them? One idea that comes to mind is to try the identities on multiple random values. Of course this works for identities without exponentiation.
The key to understand this would be to show that an expression over plus, times, and exponentiation is not zero too often without being identically zero. If this was true, with an effective bound, then a random testing idea would work.
I am not aware of this result.
We wonder if there might be a similar theory for boolean circuits for example. Are there rules of the above kind that suffice to prove all boolean identities? This needs to be carefully defined. If there are obvious rules, could there be examples like the Wilkie example of a true identity that is unprovable using just these rules? Perhaps we can show that or even get lower bounds in this way for restricted rule sets.
What do you think?