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

 We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively. We refer to these as \emph{safe} quantifiers.

 We also write $\exists x^\normal \leq |t| . A$ for $\exists x^\normal . ( x \leq |t| \cand A )$ and $\forall x^\normal \leq |t|. A $ for $\forall x^\normal. (x \leq |t| \cimp A )$. We refer to these as \emph{sharply bounded} quantifiers, as in bounded arithmetic.

For instance, we include the following axioms:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}

\[

\begin{array}{l}

\forall u^\normal. \safe(u) \\

\safe (0) \\

\forall x^\safe . \safe (\succ{} x) \\

\forall x^\safe . 0 \neq \succ{} (x) \\

\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\

\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )  

\end{array}

\qquad

\begin{array}{l}

\forall x^\safe, y^\safe . \safe(x+y)\\

\forall u^\normal, x^\safe . \safe(u\times x) \\

\forall u^\normal , v^\normal . \safe (u \smsh v)\\

\forall u^\safe .\safe(\hlf{u})\\

\forall u^\normal .\safe(|x|)

\end{array}

\]

Notice that we have $\normal \subseteq \safe$.

A full list of our $\basic$ axioms can be found in Appendix \ref{appendix:arithmetic}.

%\begin{definition}

%	[Basic theory]

%	The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.

%	\end{definition}

%Notation: if $\vec t=t_0,\dots, t_k$, we will denote as $\safe(\vec t)$ the sequence of formulas $\safe(t_0),\dots, \safe(t_k)$. Similarly for $\normal(\vec t)$.

%\begin{definition}

%[Derived functions and notations]

%We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.

%We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively.

%

%Need $bit$, $\beta$ , $\pair{}{}{}$.

%\end{definition}

%

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

%

%Use base theory + sharply bounded quantifiers.

$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.

Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.

The criterion is purely to give an appropriate definition of the hierarchy above.

%\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}

\begin{definition}

\label{def:polynomialinduction}

The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms, for each formula $A(x)$:

\left(

\cand (\forall x^{\normal} . ( A(x) \cimp A(\succ{0} x) ) )

\cand  (\forall x^{\normal} . ( A(x) \cimp A(\succ{1} x) ) ) 

\right)

For a class $\Xi$ of formulae, $\cax{\Xi}{\pind}$ denotes the set of $\pind$ axioms where $A(x) \in \Xi$. 

Define the theory $\arith^i$ consisting of the $\basic$ axioms, $\cpind{\Sigma^\safe_i } $,

%\begin{itemize}

%	\item $\basic$;

%	\item $\cpind{\Sigma^\safe_i } $:

%\end{itemize}

and a particular inference rule, called $\rais$, for closed formulas $\forall x. \exists y. A$:

 \dfrac{\proves \forall \vec x^\normal . \exists  y^\safe .  A }{ \proves \forall \vec x^\normal .\exists y^\normal . A}

We will write $\arith^i \proves A$ if $A$ is a logical consequence of the axioms of $\arith^i$, in the usual way.

%\patrick{I think in the definition of  $\arith^i$ we should impose that the formulas considered are \textit{integer positive}, that is to say that the only negative occurrences of atoms $\safe(t)$, $\normal(t)$ are those occurring in $\forall^{\safe}$ and $\forall^{\normal}$.  Indeed I don't think this can be just proved to be a consequence of a kind of 'normal form' of proofs, as we had discussed (see sect 4.4)}

%

%\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}

\begin{remark}

Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$, and indeed we believe there is a way to present these results in such a framework.

However, the proof theory of first-order modal logics, in particular free-cut elimination results used for witnessing, is not sufficiently developed to carry out such an exposition.	

	\end{remark}

We say that a function $f$ is \emph{represented} by a formula $A_f$ if we can prove a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.

Let us give a few examples for basic functions representable in $\arith^1$:

\begin{figure}

	\[

	\small

	\begin{array}{l}

	\begin{array}{cccc}

	%\vlinf{\lefrul{\bot}}{}{p, \lnot{p} \seqar }{}

	%& \vlinf{\id}{}{p \seqar p}{}

	%& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}

	%& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}

	\vlinf{id}{}{\Gamma, p \seqar p, \Delta }{}

	& \vliinf{cut}{}{\Gamma \seqar \Delta }{ \Gamma \seqar \Delta, A }{\Gamma, A \seqar \Delta}

	&&

	\\

	\noalign{\bigskip}

	%\noalign{\bigskip}

	\vliinf{\lefrul{\cor}}{}{\Gamma, A \cor B \seqar \Delta}{\Gamma , A \seqar \Delta}{\Gamma, B \seqar \Delta}

	&

	\vlinf{\lefrul{\cand}}{}{\Gamma, A\cand B \seqar \Delta}{\Gamma, A , B \seqar \Delta}

	&

	%\vlinf{\lefrul{\laand}}{}{\Gamma, A\laand B \seqar \Delta}{\Gamma, B \seqar \Delta}

	%\quad

	\vlinf{\rigrul{\cor}}{}{\Gamma \seqar \Delta, A \cor B}{\Gamma \seqar \Delta, A, B}

	&

	%\vlinf{\rigrul{\laor}}{}{\Gamma \seqar \Delta, A\laor B}{\Gamma \seqar \Delta, B}

	%\quad

	\vliinf{\rigrul{\cand}}{}{\Gamma \seqar \Delta, A \cand B }{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, B}

	\\

	\noalign{\bigskip}

	\vlinf{\lefrul{\neg}}{}{\Gamma, \neg A \seqar \Delta}{\Gamma \seqar A, \Delta}

	&

	\vlinf{\lefrul{\neg}}{}{\Gamma, \seqar \neg A, \Delta}{\Gamma, A \seqar  \Delta}

	&

	&

	%\vliinf{\lefrul{\cimp}}{}{\Gamma, A \cimp B \seqar \Delta}{\Gamma \seqar A, \Delta}{\Gamma, B \seqar \Delta}

	%&

	%

	%\vlinf{\rigrul{\cimp}}{}{\Gamma \seqar \Delta, A \cimp B}{\Gamma, A \seqar \Delta,  B}

	\\

	\noalign{\bigskip}

	%\text{Structural:} & & & \\

	%\noalign{\bigskip}

	%\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}

	%&

	\vlinf{\lefrul{\cntr}}{}{\Gamma, A \seqar \Delta}{\Gamma, A, A \seqar \Delta}

	%&

	%\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}

	&

	\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, A, A}

	&

	&

	\\

	\noalign{\bigskip}

	\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}

	&

	\vlinf{\lefrul{\forall}}{}{\Gamma, \forall x. A(x) \seqar \Delta}{\Gamma, A(t) \seqar \Delta}

	&

	\vlinf{\rigrul{\exists}}{}{\Gamma \seqar \Delta, \exists x . A(x)}{ \Gamma \seqar \Delta, A(t)}

	&

	\vlinf{\rigrul{\forall}}{}{\Gamma \seqar \Delta, \forall x . A(x)}{ \Gamma \seqar \Delta, A(a) } \\

	%\noalign{\bigskip}

	% \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&

	\end{array}

	\end{array}

	\]

	\caption{Sequent calculus rules, where $p$ is atomic, $i \in \{ 1,2 \}$, $t$ is a term and the eigenvariable $a$ does not occur free in $\Gamma$ or $\Delta$.}\label{fig:sequentcalculus}

\end{figure}

In order to carry out witness extraction for proofs of $\arith^i$, it will be useful to work with a \emph{sequent calculus} representation of proofs.

Such systems exhibit strong normal forms, notably `free-cut free' proofs, and so are widely used for the `witness function method' for extracting programs from proofs.

We introduce the required technical material here only briefly, due to space constraints.

A \emph{sequent} is an expression $\Gamma \seqar \Delta$ where $\Gamma$ and $\Delta$ are multisets of formulas. 

The inference rules of the sequent calculus $\LK$ are displayed in Fig.~\ref{fig:sequentcalculus}.

Of course, we have the following:

\begin{proposition}

	$A$ is a first-order theorem if and only if there is an $\LK$ proof of $\seqar A$.

\end{proposition}

We extend this purely logical calculus with certain non-logical rules and initial sequents corresponding to our theories $\arith^i$.

where $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent.

%

Similarly the $\rais$ inference rule of Dfn.~\ref{def:ariththeory} is represented by the nonlogical rule,

%

and the $\basic$ axioms are represented by designated initial sequents.

For instance here are some initial sequents corresponding to some of the $\basic$ axioms:

The sequent system for $\arith^i$ extends $\LK$ by the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.

 Naturally, by completeness, we have that $\arith^i \proves A$ if and only if there is a sequent proof of $\seqar A$.

 In fact, by \emph{free-cut elimination} results \cite{Takeuti87,Cook:2010:LFP:1734064} we may actually say something much stronger.

 Let us say that a sorting $(\vec u ; \vec x)$ of the variables $\vec u , \vec x$ is \emph{compatible} with a formula $A$ if each variable of $\vec x$ occurs hereditarily safe with respect to the $\bc$-typing of terms, i.e.\ never under $\smsh, |\cdot|$ and to the right of $\times$.

	If $\arith^i\proves  A$ then there is a $\arith^i$ sequent proof $\pi$ of $A$ such that each line has the form:

	\[

	\normal(\vec u), \safe (\vec x), \Gamma \seqar \Delta

	\]

	where $\Gamma \seqar \Delta$ contains only $\Sigma^\safe_i$ formulae for which the sorting $(\vec u ;\vec x)$ is compatible.

\end{theorem}

Strictly speaking, we must alter some of the sequent rules a little to arrive at this normal form. For instance the $\pind$ rule would have $\normal(\vec u)$ in its lower sequent rather than $\normal (t(\vec u))$. The latter is a consequence of the former already in $\basic$.

The proof of this result also relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible typing on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.