
%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}




