%LaTeX
\documentstyle{article}
\date{}
\title{Bounding the existential variables after the elimination of a
bounded universal quantifier}
\author{Yuri Matiyasevich}
\begin{document}
\maketitle
In 1961 Martin Davis, Hilary Putnam and Julia Robinson published
selebrated paper \cite{DavisPR61} where they described a method for
transforming a formula of the form
\begin{equation}
\forall y_{\le b} \exists z_1 \dots z_m
[P(a_1,\dots,a_n,y,z_1,\dots,z_m)=0], \label{p}
\end{equation}
where $P$ is a polynomial with integer coefficients, into an equivalent
formula of the form
\begin{equation}
\exists x_1 \dots x_l
[E_{\mbox{\rm \scriptsize L}}(a_1,\dots,a_n,b,c,x_1,\dots,x_l)=
E_{\mbox{\rm \scriptsize R}}(a_1,\dots,a_n,b,c,x_1,\dots,x_l)],
\label{ee} \end{equation}
where $E_{\mbox{\rm \scriptsize L}}$ and $E_{\mbox{\rm \scriptsize R}}$
are so called {\em exponential polynomials}, i.e., some expressions
constructed using the conventional rules from particular natural
numbers and variables $a_1,\dots,a_n$ and $x_1,\dots,x_l$ by addition,
multiplication and exponentiation.
In 1970 the author \cite{Matiyasevich70D} improved this result by
showing that exponentiation is not necessary in (\ref{ee}), i.e., that
one can find a formula which is equivalent to (\ref{p}) and which has
the form
\begin{equation}
\exists x_1 \dots x_l
[Q(a_1,\dots,a_n,b,c,x_1,\dots,x_l)=0], \label{q}
\end{equation}
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
\begin{equation}
\forall y_{\le b} \exists {z_1}_{\le c} \dots {z_m}_{\le c}
[P(a_1,\dots,a_n,y,z_1,\dots,z_m)=0] \label{bp}
\end{equation}
can be transformed into an equivalent formula of the form
\begin{equation}
\exists {x_1}_{\le X(a_1,\dots,a_n,b,c)} \dots
{x_l}_{\le X(a_1,\dots,a_n,b,c)}
[Q(a_1,\dots,a_n,b,c,x_1,\dots,x_l)=0]. \label{bq}
\end{equation}
The original technique for eliminating the single universal quantifier
was modified by several authors (see
\cite{Matiyasevich72U,HiroseI73}). An essentially different technique
was introduced in \cite{Matiyasevich93H}. The technique presented in
\cite{Matiyasevich94A} 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 \cite{Matiyasevich95}.
However, all these techniques suffer from the same
shortcoming: being applied to a formula (\ref{bp}) with bounded
existential quantifiers they produce an equivalent formula (\ref{bq})
in which the bound $X$ actually depends on the parameters
$a_1,\dots,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.
\
{\bf Theorem} {\em For every formula of the form {\rm (\ref{bp})}
one can effectively find an equivalent formula of the form}
\begin{equation}
\exists {x_1}_{\le X(b,c)} \dots {x_l}_{\le X(b,c)}
[Q(a_1,\dots,a_n,b,c,x_1,\dots,x_l)=0], \label{qb}
\end{equation}
{\em where $Q$ is a polynomial with integer coefficients}.
\begin{thebibliography}{9}
\bibitem{DavisPR61}
Davis M., Putnam H., Robinson J.
The decision problem for exponential {Diophantine} equations.
{\em Annals of Mathematics, Second Series}, 74(3):425--436, 1961.
\bibitem{HiroseI73}
{Hirose K., Shigeaki I.}
A proof of negative answer to {Hilbert's} 10th {Problem}.
\newblock {\em Proceedings of the Japan Academy}, 49(1):10--12,1973.
\bibitem{Matiyasevich70D}
Matiyasevich Yu. V.
Diofantovost perechislimykh mnozhestv.
{\em Dokl. AN SSSR}, 191(2):278--282, 1970.
Translated in: {\em Soviet Math. Doklady}, 11(2):354-358,
1970.
\bibitem{Matiyasevich72U}
Matiyasevich Yu. V.
Diofantovy mnozhestva.
{\em Uspekhi Mat. Nauk},
27:5(167), {185--222}, 1972.
\newblock
Translated in:
{\em Russian Mathematical Surveys}, 27(5):124--164, 1972.
\bibitem{Matiyasevich93H}
Matiyasevich Yu.V.
{\em Desyataya Problema Gilberta.}
Moscow, Fizmatlit, 1993.
English translation:
Hilbert's tenth problem. MIT Press, 1993.
\bibitem{Matiyasevich94A}
Matiysevich Yu.
A direct method for simulating partial recursive functions by {Diophantine}
equations.
{\em Annals Pure Appl. Logic},
67, 325--348, 1994.
\bibitem{Matiyasevich95}
Matiyasevich Yu.V.
A new Technique for Obtaining Diophantine
Representations via Elimination of bounded universal Quantifiers.
{\em Zap. nauchn. seminar. Leningr. otd. Mat. in-ta RAN},
220, 83--92, 1995.
\end{thebibliography}
\end{document}