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

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

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