%LaTeX2e
%\documentclass{article}
\documentstyle[12pt]{article}
\date{}

\title{Elimination of
       bounded universal quantifiers standing in front of a quantifier-free
arithmetical formula}

\author{Yuri Matiyasevich}

\begin{document}

\maketitle

 Raphael M. Robinson proved in 1956 in \cite{RRobinson56} the following
theorem:

\begin{quote}\em
For every polynomial $P(a_1,\dots,a_n,y)$ with
integer coefficients one can effectively find another polynomial
$Q(a_1,\dots,a_n,b)$ also with
integer coefficients such that formula
\begin{equation}
\forall {y}_{\le b}
[P(a_1,\dots,a_n,y)=0]               \label{Pabyeq0}
\end{equation}
is equivalent to formula
\begin{equation}
        Q(a_1,\dots,a_n,b)=0.      \label{Qabeq0}
\end{equation}
\end{quote}
In other words, bounded universals quantifiers can be eliminated if they
stand in front of a polynomial equality.

The proof of R. M. Robinson heavily depends on the special form of
formula (\ref{Pabyeq0}) and cannot be immediately extended to formulas of
other kinds, say, of the form
\begin{equation}
\forall {y}_{\le b}
[P(a_1,\dots,a_n,y)\ne 0].               \label{Pabyneq0}
\end{equation}

Clearly, inequality in (\ref{Pabyneq0}) can be transformed into an
equality at the cost of introduction of an additional existential
quantifier: formula (\ref{Pabyneq0}) is equivalent to formula
\begin{equation}
\forall {y}_{\le b} \exists z
[P^2(a_1,\dots,a_n,y)=z+1].               \label{Pabyeqz}
\end{equation}

A method for elimination of a bounded universal quantifier
standing in front of a purely existential arithmetical formula
was given in 1961 by Martin Davis, Hilary Putnam and Julia Robinson in their
selebrated paper \cite{DavisPR61}. Namely, 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{Pabyzeq0}
\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 \small L}}(a_1,\dots,a_n,b,x_1,\dots,x_l)=
       E_{\mbox{\rm \small R}}(a_1,\dots,a_n,b,x_1,\dots,x_l)],
                                                      \label{EEabxeq0}
\end{equation}
where $E_{\mbox{\rm \small L}}$ and $E_{\mbox{\rm \small 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$, $b$ and $x_1,\dots,x_l$, by
addition, multiplication and exponentiation.

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 proposed by the
author in \cite{Matiyasevich95}.

   In 1970 the author \cite{Matiyasevich70D} improved the above
mentioned result of Davis-Putnam-Robinson by
showing that exponentiation is not necessary in (\ref{EEabxeq0}), i.e., that
one can find a formula which is equivalent to (\ref{Pabyzeq0}) and which has
the form
\begin{equation}
        \exists x_1 \dots x_l
            [Q(a_1,\dots,a_n,b,x_1,\dots,x_l)=0],       \label{Qabxeq0}
\end{equation}
where $Q$ is a polynomial with integer coefficients.

Applying this technique to formula (\ref{Pabyeqz}), we would obtain
for (\ref{Pabyneq0}) an equivalent formula of the form (\ref{Qabxeq0}).
Unfortunately, the latter formula is not quantifier-free like formula
(\ref{Qabeq0}) was.

The goal of the present work is to obtain a kind of extention of the
above cited result of R.~M.~Robinson to formulas of the form
(\ref{Pabyneq0}) and, more generally, to arbitrary universal arithmetical
formulas. The interest in getting equivalent quantifier-free formulas is due
to some applications in model theory.

In general case we cannot hope to obtain as simple quantifier-free
formula as~(\ref{Qabeq0}). The cost of elimination of a bounded universal
quantifier will be the use of extra functions. Namely, besides
exponentiation as in (\ref{Qabxeq0})
we need \emph{integer division}, i.e.\ the function
$\lfloor { a\over b}\rfloor$.
On the other hand, we can reduced exponentiation to \mbox{one-argument}
function $2^s$.

\begin{quote}
  {\bf Theorem} {\em Let $\phi(a_1,\dots,a_n,y_1,\dots,y_k)$ a
quantifier-free arithmetical formula, i.e., a Boolean combination
of polynomial equalities.
Then formula
\begin{equation}
\forall {y_1}_{\le b_1}\dots {y_k}_{\le b_k}
\phi(a_1,\dots,a_n,y_1,\dots,y_k)
\end{equation}
is equivalent to some
formula of the form
\begin{equation}
        Q(a_1,\dots,a_n,b_1,\dots,b_k)=0,      \label{qyk}
\end{equation}
where $Q$ is an
expression constructed by conventional rules from particular
natural numbers and variables $a_1,\dots,a_n$, $b_1,\dots,b_k$ by
addition, subtraction, multiplication, integer division and exponentiation
with base $2$;
such a $Q$ can be effectively constructed for given $\phi$.
}
\end{quote}

The proof is based on technique of elimination of bounded universal
quantifiers introduced by the author in \cite[Section 6.3]{Matiyasevich93H}.

\

The present work was supported by grant 96-01-01612 from Russian Fund for
Basic Research.

\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:
{\em Hilbert's tenth problem} MIT Press, Cambridge,1993.
French translation: {\em Le dixi{\`e}me probl{\`e}me de Hilbert.
Son ind{\'e}cidabilit{\'e}}. Masson, Paris, Milan, Barcelone, 1995.

\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. Peterbug. otd. Mat. in-ta RAN},
220, 83--92, 1995.


\bibitem{RRobinson56}
R.~M.~Robinson.
Arithmetical representation of recursively enumerable sets.
\newblock {\em Journal of Symbolic Logic}, 21(2):162--186, 1956.

\end{thebibliography}

 \end{document}




