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

\forall x^\safe, y^\safe . \safe(x+y)\\

\forall u^\normal, x^\safe . \safe(u\times x) \\

\forall u^\normal , v^\normal . \safe (u \smsh v)\\

\end{array}

\]

\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}

	\item $\basic$;

	\item $\cpind{\Sigma^\safe_i } $:

\end{itemize}

\[

 \dfrac{\forall \vec x^\normal . \exists  y^\safe .  A }{ \forall \vec x^\normal .\exists y^\normal . A}

\]

\end{definition}

\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}

%& \vlinf{\id}{}{p \seqar p}{}

%& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}

%& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}

& \vliinf{cut}{}{\Gamma \seqar \Delta }{ \Gamma \seqar \Delta, A }{\Gamma, A \seqar \Delta}

&&

\\

%\text{Structural:} & & & \\

%\noalign{\bigskip}

\vlinf{\lefrul{\cntr}}{}{\Gamma, A \seqar \Delta}{\Gamma, A, A \seqar \Delta}

&

&

\\

\noalign{\bigskip}

\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}

\vlinf{}{}{\normal (s), \safe(t) \seqar \safe(s \times t)  }{}

\qquad

\vlinf{}{}{\normal (s), \normal(t) \seqar \safe(s \smsh t)  }{}\\

\end{array}

\]