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

	\label{thm:soundness}

We also define length-bounded inequality as:

\[

\begin{array}{rcl}

\leqfn (0 ; x ,y) & \dfn & \cimp (; \bit (0;x), \bit (0;y) ) \\

\leqfn (\succ i l ; x,y) & \dfn & \orfn ( ; <(\bit (\succ i l ; x) , \bit(\succ i l ; y) ) , \andfn (; \equivfn (\bit (\succ i l ; x) , \bit(\succ i l ; y)) , \leqfn (l;x,y ) ) )

\end{array}

\]

	\charfn{}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\

	\charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\

	\charfn{}{\neg A} (l, \vec u ; \vec x) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\

	\charfn{}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \cor (; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x) ) \\

	\charfn{}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \cand(; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x) ) \\

	\charfn{}{\exists x^\safe . A(x)} (l, \vec u ;\vec x) & \dfn & \begin{cases}

	1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x) = 1 \\

	\charfn{}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn & 

\anupam{sharply bounded case obtained by sharply bounded lemma}

\begin{proposition}

	If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A$ is true.

	\anupam{check statement, need proof-theoretic version?}

\end{proposition}

In order to prove Thm.~\ref{thm:soundness} we need the following lemma:

\begin{lemma}

	[Proof interpretation]

	\label{lem:proof-interp}

	For any $\arith^i$ proof of a $\Sigma^\safe_i$ sequent $\Gamma \seqar \Delta$, there is a $\mubci{i-1}$ function $f$ such that, for any $l, \vec u , \vec x  , w$, we have:

	\[

	\wit{\vec u ; \vec x}{ \wedge \Gamma } (l, \vec u ; \vec x , w) 

	\quad \leq \quad

	\wit{\vec u ; \vec x}{\vee \Delta} (l, \vec u ; \vec x , f(l, \vec u ; \vec x , w))

	\]

	\anupam{maybe want $f(\vec u \mode l ; \vec x \mode l , w)$}

\end{lemma}

\begin{proof}

	We assume the proof, say $\pi$, is in integer positive free-cut free form, by the results from the previous section.

	This means that the predicate $\charfn{\vec u ; \vec x}{A}$ is defined for each formula $A(\vec u ; \vec x)$ occurring in a proof, so the theorem is well-stated.

	We define the function $f$ inductively, by considering the various final rules of $\pi$.

	\paragraph*{Negation}

	Can assume only on atomic formulae, so no effect.	

	\paragraph*{Quantifiers}

	\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}

	\paragraph*{Contraction}

	Left contraction simply duplicates an argument, whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula.

	\paragraph*{Induction}

	Corresponds to safe recursion on notation.

\end{proof}

We are now ready to prove the soundness theorem.

\begin{proof}

	[Proof of Thm.~\ref{thm:soundness} from Lemma~\ref{lem:proof-interp}]

	(watch out for dependence on $l$, try do without)

	Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\normal . A(\vec u ; x)$. Then by raising, inversion, free-variable normal forms, we have a proof of,

	\[

	\normal (\vec u ) \seqar \exists x^\normal . A(\vec u , x ;)

	\]

	whence, by Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f$ such that:

	\[

	\vec u \mode l = \vec a \mode l

	\quad \implies \quad

	\wit{\vec u ; }{A} ( l , \vec u , f(l, \vec u;) ) =1

	\]

	Now it suffices to choose an $l$ bigger that both all the $\vec u$ and $f(\vec u)$, which is a polynomial in $\vec u$ by the polymax bounding lemma.

\end{proof}