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, ${\exp(x)}$ 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

${\dots}$ 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:

${\dots}$ 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.

## Real Theory

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:

$\displaystyle \forall x \ \exists y \ x^{2}+1 =y^{2}.$

This is a true sentence. Note the theory can define order: ${x \le y}$ is defined as:

$\displaystyle \exists z \ x + z^{2} = y.$

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 ${\mathsf{P=NP}}$ 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 ${\mathsf{P=NP}}$.

Tarski’s original proof used quantifier elimination, and yielded a bound of the form ${2^{^{.^{.^{.^{n}}}}}}$ 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.

## HSI

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:

$\displaystyle (x+y)^{2} = x^{2} + 2xy + y^{2}.$

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:

$\displaystyle \begin{array}{rcl} x+y &=& y+x \\ (x+y)+z &=& x +(y+z) \\ x \cdot 1 &=& x \\ x \cdot y &=& y \cdot x \\ (x \cdot y) \cdot z &=& x \cdot (y \cdot z) \\ x \cdot (y+z) &=& x \cdot y + x \cdot z \\ 1^{x} &=& = 1 \\ x^{1} &=& x \\ x^{y+z} &=& x^{y} \cdot x^{z} \\ (x \cdot y)^{z} &=& x^{z} \cdot x^{y} \\ (x^{y)})^{z} &=& x^{(y \cdot z)}. \end{array}$

Let’s call these HSI: for high school identities—what else? It is known that determining whether ${s=t}$ is an identity is decidable, where ${s,t}$ 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:

$\displaystyle \begin{array}{rcl} &&((1+x)^y + (1+x+x^2)^y)^x\cdot ((1+x^3)^x + (1+x^2+x^4)^x)^y\\ &=&((1+x)^x + (1+x+x^2)^x)^y\cdot ((1+x^3)^y + (1+x^2+x^4)^y)^x. \end{array}$

The intuitive reason this is true is that

$\displaystyle 1 + x^2 + x^4 = (1 - x + x^2)(1 + x + x^2),$

so we can factor out ${(1 - x + x^2)^{xy}}$, 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 ${f,g}$ are linearly ordered by the relation ${f = o(g)}$ modulo ${f = \Theta(g)}$. 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.

## Open Problems

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?

1. July 10, 2014 10:06 am

See Peirce on Logical Involution

2. July 10, 2014 11:57 am

Excellent reasoning
Dyiaram

July 10, 2014 1:22 pm

Good stuff!

Question about a special case of the real theory of arithmetic. Can someone tell me what’s known about the computational complexity of deciding existence of real roots to a given system of multivariate polynomials, say with integer coefficients?

(There are two cases, where the exponents are written in binary or where they’re written in unary and so considered to be <= poly(n). I guess the latter is reasonable.
Also, I'm aware that with real coefficients, the problem is NP-complete in the Blum-Shub-Smale model. But I'm interested in the old-fashioned model.)

July 10, 2014 1:30 pm

Something else to go in your open problems list for this post: the existential theory of the reals lies somewhere between NP and PSPACE (and has many natural complete problems). Can this gap be narrowed?

5. July 10, 2014 4:28 pm

I’m not sure what you have in mind with the open problem on boolean functions — for example, just how tightly you want to maintain the analogy with real arithmetic — but it does remind me of some issues having to do with the difference between implicational rules of inference and equational rules of inference. Equational inference preserves the information of the initial formula and is therefore reversible while implicational inference is allowed to lose information as the inference proceeds.

• July 10, 2014 9:50 pm

Here’s a possibly related story —

July 31, 2014 2:00 am

Sorry to be commenting too late.

Truth of identities was shown to be decidable by Macintyre

[A. Macintyre. Model Theory and Arithmetic, volume 890 of
Lecture Notes in Mathematics, chapter The laws of exponentiation, pages 185-197. Springer Berlin Heidelberg, 1981]

and before that by Richardson for the univariate case

[D. Richardson. Solution of the identity problem for int egral exponential functions. Zeitschrift fr mathematische Logik und Grundlagen der Mathematik, 15:333–340, 1969].

Some people claim that the decision procedure computes, based on the form of the equation, an upper bound and then does brute force search up to it.

Also, there is a recursive extension HSI* of the axioms of HSI that was shown by Wilkie to be complete. [the same article of Wilkie that gives the counterexample to HSI]

Recently I surveyed and used some results around HSI for questions of contructive cardinality of sets. [ http://dx.doi.org/10.1145/2603088.2603115 ]