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

\section{Proof of Thm.~\ref{thm:deduction}, Sect.~\ref{sect:preliminaries}}

\label{sect:app-preliminaries}

%Equality axioms:

%\[

% \begin{array}{rl}

%\refl & \forall x . x = x \\

%\symm & \forall x, y. (x = y \limp y = x )\\

%\trans & \forall x , y , z . ( x = y \limp y = z \limp x = z ) \\

%\subst_f & \forall \vec x , \vec y . (\vec x = \vec y \limp f(\vec x) = f(\vec y) ) \\

%\subst_P & \forall \vec x , \vec y. (\vec x = \vec y \limp P(\vec x) \limp P(\vec y)  )

% \end{array}

% \]

%\begin{theorem}[Theorem \ref{thm:deduction}]

%tt

%\end{theorem}

% \begin{proof}[Proof of Thm.~\ref{thm:deduction}]

Suppose $\theory \cup \{ A \}$ proves $B$ and let $\pi$ be a $\theory$-derivation with end-sequent $\seqar B$ and leaves $\seqar A$, i.e.:

\[

\vltreeder{\pi}{ \seqar B }{ \seqar A }{\vldots}{\seqar A}

\]

Then construct the following $\theory$-proof of $!A \limp B$,

\[

\vlderivation{

\vlin{\rigrul{\limp}}{}{\seqar !A \limp B}{

\vltr{!A, \pi }{ !A \seqar B }{

\vlin{\lefrul{!}}{}{!A \seqar A}{

\vlin{\id}{}{A\seqar A}{\vlhy{}}

}

}{ \vlhy{\vldots} }{

\vlin{\lefrul{!}}{}{!A \seqar A}{

\vlin{\id}{}{A\seqar A}{\vlhy{}}

}

}

}

}

\]

where $!A, \pi$ is obtained by appending $!A$ to the antecedent of each sequent in $\pi$, inserting left-contraction steps when necessary. Free variable conditions are satisfied since $A$ is closed (and so also $!A$) and side-conditions are satisfied since $!A$ is a $!$-formula.

For the other direction simply extend any $\theory$-proof of $!A \limp B$ as follows:

\[

\vlderivation{

\vliin{\cut}{}{ \seqar B }{

\vlin{\rigrul{!}}{}{\seqar !A }{\vlhy{\seqar A}}

}{

\vliq{ \inv{{\limp}} }{}{ !A \seqar B }{ \vlhy{\seqar !A \limp B }}

}

}

\]

% \end{proof}