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

 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} in Appendix~\ref{sect:app-sequent-calculus}.

%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$.

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

 For instance the axiom $\pind$ of Def. \ref{def:polynomialinduction} is represented by the following rule:

\section{Sequent calculus formalisation of $\arith^i$}

\label{sect:app-sequent-calculus}

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