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

\section{An arithmetic for the polynomial hierarchy}

%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$.

Our base language is defined by the set of functions (and constants) symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|\}$ and the set of predicate symbols

 $\{\leq, \safe, \normal \}$.

We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$.

We will also use as shorthand notations:

$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$

We call \textit{atomic formulas} formulas of the form $(s\leq t)$ or $(s=t)$.

 As we are in classical logic, we will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of subformula of the form $\neg \neg A$.

Now, let us describe the axioms we are considering.The $\basic$ axioms are as follows:

\[

\begin{array}{l}

\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   )\\

\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^\normal \safe(u)

\end{array}

\]

\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}

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.

\begin{definition}

[Quantifier hierarchy]

$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded.

We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.

We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.

\end{definition}

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

\begin{definition}\label{def:polynomialinduction}

[Polynomial induction]

The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms,

\[

A(0)

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

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

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

\]

for each formula $A(x)$.

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

%We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.

\end{definition}

\begin{definition}\label{def:ariththeory}

Define the theory $\arith^i$ consisting of the following axioms:

\begin{itemize}

	\item $\basic$;

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

\end{itemize}

and an inference rule, called $\rais$, for closed formulas $\exists y^\normal . A$:

\[

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

\]

\end{definition}

\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{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)$.

\subsection{Graphs of some basic functions}

Todo: $+1$,

\subsection{Encoding sequences in the arithmetic}

\todo{}

\anupam{Assume we have a $\Sigma^\safe_1$ predicate $\beta(i,x,y)$, expressing that the $i$th element of the sequence $x$ is $y$, such that $\arith^1 \proves \forall i^\normal , x^\safe . \exists ! y^\safe . \beta (i,x,y)$.}

\subsection{A sequent calculus presentation}

\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}\label{fig:sequentcalculus}

\end{figure}

 We denote sequence as $\Gamma \seqar \Delta$ where $\Gamma$, $\Delta$ are multi sets of formulas. The sequent calculus rules are displayed on Fig. \ref{fig:sequentcalculus},  where $p$ is atomic, $i \in \{ 1,2 \}$, $t$ is a term and the eigenvariable $a$ does not occur free in $\Gamma$ or $\Delta$.

We consider \emph{systems} of `nonlogical' rules extending this sequent calculus, which we write as follows,

 \[

 \begin{array}{cc}

    \vlinf{(R)}{}{ \Gamma , \Sigma' \seqar \Delta' , \Pi  }{ \{\Gamma , \Sigma_i \seqar \Delta_i , \Pi \}_{i \in I} }

\end{array}

\]

 where, in each rule $(R)$, $I$ is a finite possibly empty set (indicating the number of premises) and we assume the following conditions and terminology:

 \begin{enumerate}

 \item In $(R)$ the formulas of $\Sigma', \Delta'$  are called \textit{principal}, those of $\Sigma_i, \Delta_i$ are called \textit{active}, and those of

$ \Gamma,  \Pi$ are called \textit{context formulas}.

\item Each rule $(R)$ comes with a list $a_1$, \dots, $a_k$ of eigenvariables such that each $a_j$ appears in exactly one $\Sigma_i, \Delta_i$ (so in some active formulas of exactly one premise)  and does not appear in  $\Sigma', \Delta'$ or $ \Gamma,  \Pi$.

    \item A system $\mathcal{S}$ of rules must be closed under substitutions of free variables by terms (where these substitutions do not contain the eigenvariables $a_j$ in their domain or codomain).

   \end{enumerate}

%The distinction between modal and nonmodal formulae in $(R)$ induces condition 1

 Conditions 2 and 3 are standard requirements for nonlogical rules, independently of the logical setting, cf.\ \cite{Beckmann11}. Condition 2 reflects the intuitive idea that, in our nonlogical rules, we often need a notion of \textit{bound} variables in the active formulas (typically for induction rules), for which we rely on eigenvariables. Condition 3 is needed for our proof system to admit elimination of cuts on quantified formulas.

%\begin{definition}

%[Polynomial induction]

%The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms,

%\[

%A(0)

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

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

%\cimp  \forall x^{\normal} . A(x)

%\]

%for each formula $A(x)$.

%

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

%

%We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.

%\end{definition}

As an example any axiom can be represented by such a nonlogical rule $(R)$, with no premise ($I=\emptyset$), $\Delta'$ equal to the axiom and $\Gamma=\Sigma'=\Pi$. For instance the axiom $\pind$ of Def. \ref{def:polynomialinduction}.

Actually  $\pind$ is equivalent to the following rule:

\begin{equation}

\label{eqn:ind-rule}

\small

\vliinf{\pind}{}{ \normal(t) , \Gamma , A(0) \seqar A(t), \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{0} a) , \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{1} a) , \Delta  }

\end{equation}

where $I=2$ and  in all cases, $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent of the $\pind$ rule.

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

 \[

 \begin{array}{cc}

    \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \exists  y^\normal .  A }{  \normal(t_1), \dots, \normal(t_k) \seqar \exists  y^\safe .  A}

\end{array}

\]

%\patrick{In fact, I think we rather need the following nonlogical rule, which implies the previous one but is I guess more general:

%\[

% \begin{array}{cc}

%    \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \normal(t) }{  \normal(t_1), \dots, \normal(t_k) \seqar \safe(t)}

%\end{array}

%\]

%}

The $\basic$ axioms are equivalent to the following nonlogical rules, that we will also designate by $\basic$:

\[

\small

\begin{array}{l}

\begin{array}{cccc}

\vlinf{}{}{\seqar \safe (0)}{}&

\vlinf{}{}{\safe(t) \seqar \safe(\succ{} t)}{}&

\vlinf{}{}{ \safe (t)   \seqar 0 \neq \succ{} t}{} &

\vlinf{}{}{\safe (s) , \safe (t)  , \succ{} s = \succ{} t\seqar s = t }{}\\

\end{array}

\\

\vlinf{}{}{\safe (t) \seqar t = 0 \cor \exists y^\safe . t = \succ{} y  }{}

\qquad

\vlinf{}{}{\safe(s), \safe(t) \seqar \safe(s+t) }{}\\

\vlinf{}{}{\normal (s), \safe(t) \seqar \safe(s \times t)  }{}

\qquad

\vlinf{}{}{\normal (s), \normal(t) \seqar \safe(s \smsh t)  }{}\\

\vlinf{}{}{\normal(t) \seqar \safe(t)  }{}

\end{array}

\]

 The sequent calculus for $\arith^i$ is that of Fig. \ref{fig:sequentcalculus} extended with the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.

 \begin{lemma}

 For any term $t$, its free variables can be split in two sets $\vec{x}$ and $\vec{y}$ such  that the sequent $\normal(\vec x), \safe(\vec y) \seqar \safe(t)$ is provable.

 \end{lemma}

\subsection{Free-cut free normal form of proofs}

\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}

Since our nonlogical rules may have many principal formulae on which cuts may be anchored, we need a slightly more general notion of principality.

    \begin{definition}\label{def:anchoredcut}

  We define the notions of \textit{hereditarily principal formula} and \textit{anchored cut} in a $\system$-proof, for a system $\system$, by mutual induction as follows:

  \begin{itemize}

  \item A formula $A$ in a sequent $\Gamma \seqar \Delta$ is \textit{hereditarily principal} for a rule instance (S) if either (i) the sequent is in the conclusion of (S) and $A$ is principal in it, or

(ii)  the sequent is in the conclusion of an anchored cut, the direct ancestor of $A$ in the corresponding premise is hereditarily principal for the rule instance (S), and the rule (S) is nonlogical.

  \item A cut-step is an \textit{anchored cut} if the two occurrences of its cut-formula $A$ in each premise are hereditarily principal for nonlogical steps, or one is hereditarily principal for a nonlogical step and the other one is principal for a logical step.

  \end{itemize}

     A cut which is not anchored will also be called a \textit{free-cut}.

  \end{definition}

  As a consequence of this definition, an anchored cut on a formula $A$ has the following properties:

  \begin{itemize}

  \item At least one of the two premises of the cut has above it a sub-branch of the proof which starts (top-down) with a nonlogical step (R) with $A$ as one of its principal formulas, and then a sequence of anchored cuts in which $A$ is part of the context.

  \item The other premise is either of the same form or is a logical step with principal formula $A$.

  \end{itemize}

   Now we have (see \cite{Takeuti87}):

   \begin{theorem}

   [Free-cut elimination]\label{thm:freecutelimination}

   \label{thm:free-cut-elim}

    Given a system  $\mathcal{S}$, any  $\mathcal{S}$-proof $\pi$ can be transformed into a $\system$-proof $\pi'$ with same end sequent and without any free-cut.

   \end{theorem}

   Now we want to deduce from that theorem a normal form property for proofs of certain formulas. But before that let us define some particular classes of sequents and proofs.

   Say that a sequent $\Gamma \seqar \Delta$ is \textit{well-typed} if for any free variable $x$ occurring in $\Gamma$ or $\Delta$, there exists a formula $\safe(x)$ or $\normal(x)$ in $\Gamma$. A proof is well-typed if its sequence are.

   \begin{lemma}\label{lem:welltyped}

   If a well-typed sequent $\Gamma \seqar \Delta$ is provable, then there exists $\vec u$  such that

 the sequent $\normal(\vec u), \Gamma \seqar \Delta$ admits a well-typed proof.

   \end{lemma}

   \patrick{It seems to me the statement had to be modified so as to prove the lemma. Maybe I misunderstand something.}

   \begin{proof}[Proof sketch]

   First by Thm \ref{thm:freecutelimination} we know that $\Gamma \seqar \Delta$ admits a proof $\pi$ without any free-cut. Let us then prove that $\pi$ can be transformed in a proof $\pi'$ of conclusion of the form  $\normal(\vec u), \Gamma \seqar \Delta$ and such that, for any sequent, if it is well-typed then its premises are well-typed.

   Observe first that by definition of $\arith^i$ and the absence of free cut, all quantifiers occurring in a formula of the proof are of one of the forms

   $\forall^{\safe}$,   $\exists^{\safe}$,  $\forall^{\normal}$,   $\exists^{\normal}$, and for the last two ones they are sharply bounded.

  Then, one can check that for all rules but the quantifier rules and the cut rule, if the conclusion is well-typed, then so are the two premises.  For the remaining rules, $\forall-r$ and $\exists-l$ are unproblematic, because of the observation above. Let us now examine the case of $\exists-r$, with a $\safe$ label, and the other rules can be treated in the same way. In the premise we get a formula $\safe(t) \cand A(t)$. Then what we do is that, if  $\vec u$ denote the free variables of $t$, we add to the context of all sequents of the proof $\normal(\vec u)$. We obtain in this way a valid proof new proof,  and the premises of the rule have become well-typed.

       \end{proof}

     \patrick{As mentioned after Def 14, I don't think that we can prove that the proofs we consider are equivalent to integer positive proofs, by arguing that negative occurrences $\neg \safe(t)$ could be replaced by 'false', by using the lemma above. Indeed even if for all its free variables we have $\safe(\vec x)$, $\normal(\vec u)$ on the l.h.s. of the sequent, it is not clear to me why that would prove $\safe(t)$. My proposition is thus to restrict 'by definition' of $\arith^i$ to integer positive formulas.}

 \begin{theorem}

   Assume the $\arith^i$ sequent calculus proves a closed formula $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$. Then there exists a proof $\pi$ of the sequent

   $\normal(\vec u), \safe(\vec x) \seqar \exists y^\safe . A(\vec u ; \vec x , y)$ satisfying:

   \begin{enumerate}

    \item $\pi$  only contains  $\Sigma^\safe_{i}$ formulas,

    \item $\pi$ is a well-typed and integer-positive proof.

   \end{enumerate}

   \end{theorem}