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

It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:

\begin{proposition}

	[Length induction]

	The axiom schema of formulae,

\begin{equation}

\label{eqn:lind}

	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)

\end{equation}

	for formulae $A \in \Sigma^\safe_i$

	is equivalent to $\cpind{\Sigma^\safe_i}$.

\end{proposition}

\begin{proof}

	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.

	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.

\end{proof}

Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.

We will freely use this in place of polynomial induction whenever it is convenient.

\newcommand{\lind}{\mathit{LIND}}

\newcommand{\clind}[1]{#1\text{-}\lind}

We now define \emph{length-bounded $\beta$ function} $\beta(i,l;x,b)$ as:

\[

\forall j \leq l . \bigvee\limits_{b=0,1} ( \beta\bit (i,j;x,b) \cand \bit (j;y,b) )

\]

\end{definition}

Our aim is to construct sequences formed from old sequences and new elements.

Namely we want the following result, which says that, given a number $x$ and a sequence $y$, there is another sequence $z$ formed from prepending $x$ to $y$:

\begin{proposition}

	[In $\arith$]

	$$

	\forall x^\safe, y^\safe. \exists z^\safe . \forall i^\normal\leq k, j^\normal\leq l . 

	\left(

	\begin{array}{rl}

	& \bigwedge\limits_{b=0,1} (\bit(j;x,b) \cimp \beta (0,j;z,b) ) \\

	\cand & i>0 \cimp \bigwedge\limits_{b=0,1} (\beta(i-1, j;y,b) \cimp \beta(i,j;z,b) )

	\end{array}

	\right)

	$$

\end{proposition}

To prove this we will need two lemmata.

The first says we can construct a sequence whose $0$th element is $x$ and every other element is $0$.

\begin{lemma}

[In $\arith$]

$\forall l . \exists z . (\beta (0,|l| ; z , x) \cand \forall i \leq |k| . \beta(i,|l|;z,0) )$.	

\end{lemma}

\begin{proof}

	Length induction on $l$.

\end{proof}

The second says we can prepend $0$ to any sequence:

\begin{lemma}

	[In $\arith$]

	$\forall x . \exists z . ( \beta(0,|l|;z,0) \cand \forall i\in (0,|k|] . \exists y . (\beta (i, |l| ; z,y) \cand \beta(i-1,|l|;x,y) )   )$

\end{lemma}

\begin{proof}

	Length induction on $l$.

\end{proof}