Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)

Use base theory + sharply bounded quantifiers.

\anupam{Perhaps use prefix quantifier instead of sharply bounded (a la Ignatovic?), since plays nicer with sharply bounded lemma?}

\begin{definition}

[Quantifier hierarchy]

We define:

\begin{itemize}

	\item $\Sigma^\safe_0 = \Pi^\safe_0 $ = sharply bounded formulae. 

	\item (Increase with predicative quantifiers)

\end{itemize}	

\end{definition}

\begin{definition}

Define the theory $\arith^i$ as $\basic + \cpind{\Sigma^\safe_i }$	

\end{definition}

\begin{lemma}

[Sharply bounded lemma]

Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.

Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.

\end{lemma}

\begin{proof}

	We give the $\forall$ case, the $\exists$ case being dual.

	The characteristic function $f(v , \vec u ; \vec x)$ is defined by predicative recursion on $v$ as:

	\[

	\begin{array}{rcl}

	f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\

	f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (\succ i v, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) )

	\end{array}

	\]

\end{proof}

Notice that $\prefix$ suffices to encode usual sharply bounded inequalities,

since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$.