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 \}$. We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$.

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}

\]

%\patrick{For $\forall \vec x^\normal . \exists  y^\safe .  A$ closed ?} 

\end{definition}

\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 it admits a well-typed proof.

   \end{lemma}

   \begin{proof}

   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 same conclusion and such that, for any sequent, if it is well-typed then its premises are well-typed.

   \patrick{to be finished}

     \end{proof}

     \patrick{ TODO: define integer-positive sequents and proofs.}

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