Bounding the existential variables after the elimination of a bounded universal quantifier

Yuri Matiyasevich

In 1961 Martin Davis, Hilary Putnam and Julia Robinson published selebrated paper [1] where they described a method for transforming a formula of the form

∀y_{≤b}∃z_{1} … z_{m}[P (a_{1}, …, a_{n}, y, z_{1}, …, z_{m}) = 0],  (1)

where P is a polynomial with integer coefficients, into an equivalent formula of the form

∃x_{1} … x_{l}[E_{L}(a_{1}, …, a_{n}, b, c, x_{1}, …, x_{l}) = E_{R}(a_{1}, …, a_{n}, b, c, x_{1}, …, x_{l})], (2)

where E_{L} and E_{R} are so called exponential polynomials, i.e., some expressions constructed using the conventional rules from particular natural numbers and variables a_{1}, …, a_{n} and x_{1}, …, x_{l} by addition, multiplication and exponentiation.

In 1970 the author [3] improved this result by showing that exponentiation is not necessary in (2), i.e., that one can find a formula which is equivalent to (1) and which has the form

∃x_{1} … x_{l}[Q(a_{1}, …, a_{n}, b, c, x_{1}, …, x_{l}) = 0],  (3)

where Q is a polynomial with integer coefficients.

This result evidently has a counterpart for formulas with bounded existential quantifiers: a formula of the form

∀y_{≤b}∃z_{1}_{≤c} … z_{m}_{≤c}[P (a_{1}, …, a_{n}, y, z_{1}, …, z_{m}) = 0]  (4)

can be transformed into an equivalent formula of the form

∃x_{1}_{≤X(a_{1},...,a_{n},b,c)} … x_{l}_{≤X(a_{1},...,a_{n},b,c)}[Q(a_{1}, …, a_{n}, b, c, x_{1}, …, x_{l}) = 0]. (5)

The original technique for eliminating the single universal quantifier was modified by several authors (see [4, 2]). An essentially different technique was introduced in [5]. The technique presented in [6] for Diophantine simulation of partial recursive functions can be also viewed as a method for eliminating a bounded universal quantifier because such a quantifier can be easily modelled by primitive recursion. Yet another method for eliminating bounded universal quantifiers was recently proposed by the author in [7].

However, all these techniques suffer from the same shortcoming: being applied to a formula (4) with bounded existential quantifiers they produce an equivalent formula (5) in which the bound X actually depends on the parameters a_{1}, …, a_{n}. In 1992 Zofia Adamovicz asked the question whether this is inevitable or not. It turned out that the abovementioned shortcoming can be overcome.

Theorem For every formula of the form (4) one can effectively find an equivalent formula of the form

∃x_{1}_{≤X(b,c)} … x_{l}_{≤X(b,c)}[Q(a_{1}, …, a_{n}, b, c, x_{1}, …, x_{l}) = 0],  (6)

where Q is a polynomial with integer coefficients.

References

[1] Davis M., Putnam H., Robinson J. The decision problem for exponential Diophantine equations. Annals of Mathematics, Second Series, 74(3):425– 436, 1961.

[2] Hirose K., Shigeaki I. A proof of negative answer to Hilbert’s 10th Problem. Proceedings of the Japan Academy, 49(1):10–12,1973.

[3] Matiyasevich Yu. V. Diofantovost perechislimykh mnozhestv. Dokl. AN SSSR, 191(2):278–282, 1970. Translated in: Soviet Math. Doklady, 11(2):354-358, 1970.

[4] Matiyasevich Yu. V. Diofantovy mnozhestva. Uspekhi Mat. Nauk, 27:5(167), 185–222, 1972. Translated in: Russian Mathematical Surveys, 27(5):124–164, 1972.

[5] Matiyasevich Yu.V. Desyataya Problema Gilberta. Moscow, Fizmatlit, 1993. English translation: Hilbert’s tenth problem. MIT Press, 1993.

[6] Matiysevich Yu. A direct method for simulating partial recursive functions by Diophantine equations. Annals Pure Appl. Logic, 67, 325–348, 1994.

[7] Matiyasevich Yu.V. A new Technique for Obtaining Diophantine Representations via Elimination of bounded universal Quantifiers. Zap. nauchn. seminar. Leningr. otd. Mat. in-ta RAN, 220, 83–92, 1995.