Index: appendix-sequent-calculus.tex
===================================================================
--- appendix-sequent-calculus.tex	(revision 221)
+++ appendix-sequent-calculus.tex	(revision 222)
@@ -73,4 +73,64 @@
 	\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}
\ No newline at end of file
+	\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}
\ No newline at end of file
