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

\section{Proof of completeness}

\todo{Make statement above proper, with all bounds and moduli. I cut the proof to the appendix, maybe add sketch if space.}

From this lemma we can readily prove the soundness result:

	\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

		\wit{\vec u ; }{A} ( l , \vec u , f(\vec u \mode l;) ) =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}

\input{appendix-soundness}

\input{appendix-completeness}

\section{Proof of soundness}

For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec w')$, with $\vec w'$ in place of $\vec f( \cdots )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.

\begin{proof}

	Since the proof is in typed variable normal form we have that each line of the proof is of the same form, i.e.\ $\normal (\vec u), \safe (\vec x) , \Gamma \seqar \Delta$ over free variables $\vec u ; \vec x$.

	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*{Logical rules}

	Pairing, depairing. Need length-boundedness.

	If we have a left conjunction step:

	\[

	\vlinf{\lefrul{\cand}}{}{ \normal (\vec u ), \safe (\vec x) , A\cand B , \Gamma \seqar \Delta }{ \normal (\vec u ), \safe (\vec x) , A, B , \Gamma \seqar \Delta}

	\]

	By inductive hypothesis we have functions $\vec f (\vec u ; \vec x , w_A , w_B , \vec w)$ such that,

	\[

	\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , w_A , w_B , \vec w)

	\quad \implies \quad

	\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f ( (\vec u ; \vec x) \mode l , (w_A , w_B , \vec w) \mode p(l) ))

	\]

	for some polynomial $p$.

	%

	We define $\vec f^\pi (\vec u ; \vec x , w , \vec w) \dfn \vec f (\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $p^\pi = O(p)$.

	Right disjunction step:

	\[

	\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }

	\]

	$\vec f^\pi_\Delta$ remains the same as that of premiss.

	Let $f_A, f_B$ be the functions corresponding to $A$ and $B$ in the premiss, so that:

	\[

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

	\quad \implies \quad

	\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , f_C ( (\vec u ; \vec x) \mode l , \vec w \mode p(l) ))		

	\]

	for $C = A,B$ and for some $p$, such that $f_A , f_B$ are bounded by $q(l)$ (again by IH).

	We define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.

	\paragraph*{Quantifiers}

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

	Sharply bounded quantifiers are generalised versions of logical rules.

	\[

	\vlinf{|\forall|}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar  \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar  \Delta, A(u)  }

	\]

	By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that:

	\[

	\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )

	\quad \implies \quad

	\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )

	\]

	with $|f|\leq q(|l|)$.

	By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....

	We set $f^\pi_{\forall u^\normal \leq t . A} (\vec u ; \vec x , \vec w) \dfn F(q(|l|), t(\vec u;), \vec u ; \vec x , 0, \vec w  )$.

	Right existential:

	\[

	\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t)}

	\]

	Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form.

	\paragraph*{Contraction}

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

	\[

	\vlinf{\cntr}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A }{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A , A}

	\]

	$\vec f^\pi_\Delta$ remains the same as that of premiss. Let $f_0 ,f_1$ correspond to the two copies of $A$ in the premiss.

	We define:

	\[

	f^\pi_A ( \vec u ; \vec x , \vec w  )

	\quad \dfn \quad

	\cond (; \wit{\vec u ; \vec x}{A} ( l , \vec u ; \vec x , f_0(\vec u ; \vec x , \vec w) ) , f_1(\vec u ; \vec x , \vec w) , f_0(\vec u ; \vec x , \vec w)  )

	\]

	\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }

	\paragraph*{Induction}

	Corresponds to safe recursion on notation.

	Suppose final step is (wlog):

	\[

	\vlinf{\pind}{}{ \normal (\vec u), \safe (\vec x) , \Gamma, A(0) \seqar A(t(\vec u ;)) , \Delta}{ \left\{\normal (u) , \normal (\vec u) , \safe (\vec x) , \Gamma,  A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }

	\]

	\anupam{need to say in normal form part that can assume induction of this form}

	For simplicity we will assume $\Delta $ is empty, which we can always do by Prop.~\todo{DO THIS!}

	Now, by the inductive hypothesis, we have functions $h_i$ such that:

	\[

	\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x ,  \vec w)

	\quad \implies \quad

	\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x ,  h_i ((u , \vec u) \mode l ; \vec x \mode l , \vec w) )

	\]

	First let us define $ f$ as follows:

	\[

	\begin{array}{rcl}

	f (0 , \vec u ; \vec x, \vec w,  w ) & \dfn &  w\\

	f( \succ i u , \vec u ; \vec x , \vec w, w) & \dfn & 

	h_i (u , \vec u ; \vec x , \vec w , f(u , \vec u ; \vec x , \vec w , w ))

	\end{array}

	\]

	where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$.

	\anupam{Wait, should $\normal (t)$ have a witness? Also there is a problem like Patrick said for formulae like: $\forall x^\safe . \exists y^\safe. (\normal (z) \cor \cnot \normal (z))$, where $z$ is $y$ or otherwise.}

	Now we let $f^\pi (\vec u ; \vec x , \vec w) \dfn f(t(\vec u ; ) , \vec u ; \vec x , \vec w)$.

	\paragraph*{Cut}

	If it is a cut on an induction formula, which is safe, then it just corresponds to a safe composition since everything is substituted into a safe position.

	Otherwise it is a `raisecut':

	\[

	\vliinf{\rais\cut}{}{\normal (\vec u ) , \normal (\vec v) , \safe (\vec x) ,\Gamma \seqar \Delta }{ \normal (\vec u) \seqar \exists x^\safe  . A(x) }{ \normal (u)  , \normal (\vec v) , \safe (\vec x) , A(u), \Gamma \seqar \Delta }

	\]

	In this case we have functions $f(\vec u ; )$ and $\vec g (u, \vec v ; \vec x , w , \vec w )$, in which case we construct $\vec f^\pi$ as:

	\[

	\vec f^\pi ( \vec u , \vec v ; \vec x , \vec w )

	\quad \dfn \quad

	\vec g ( \beta (1 ; f(\vec u ;) ) , \vec v ; \vec x , \beta(0;f(\vec u ;)) , \vec w )

	\]

	\end{proof}

\todo{Present typed variable free-cut free form.}

\anupam{I cut-and-pasted the rest of this section into appendices to save space. Move things back gradually.}

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