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

	\hspace{-1.5em}

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

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

	&

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

		\\

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

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

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

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 sorting of variables 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.

As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae immediately below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.

Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, e.g.\

\todo{}