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

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

   [Free-cut elimination]

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