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

Namely, in addition to usual axioms, our $\basic$ includes the following:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}

\begin{enumerate}[(a)]

	\item $\forall u^\normal. \safe(u) $

	\item $\safe (0) $

	\item $\forall x^\safe . \safe (\succ{} x) $

	\item $\forall u^\safe .\safe(\hlf{u})$

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

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

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

	\item $\forall u^\normal .\safe(|x|)$

\end{enumerate}

%\[

%\begin{array}{l}

%\forall u^\normal. \safe(u) \\

%\safe (0) \\

%\forall x^\safe . \safe (\succ{} x) \\

%\forall u^\safe .\safe(\hlf{u})

%\end{array}

%\qquad

%\begin{array}{l}

%\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)\\

%\forall u^\normal .\safe(|x|)

%\end{array}

%\]

Notice in particular that we have $\normal \subseteq \safe$.

%

\begin{enumerate}[(1)]

	\item $\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) $

	\item $\forall x^{\safe}. x \neq \succ{} x$

	\item $\forall x^{\safe}.0 \leq x$

	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) $

	\item $\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)$

	\item $\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)$

	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)$

	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)$

	\item $|0|=0$

	\item $\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) $

	\item $|\succ{}0|=\succ{} 0$

	\item $\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)$

	\item $\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)$

	\item $\forall y^{\normal}.    0 \smsh y=\succ{} 0$

	\item $\forall x^{\normal}.    (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))$

	\item $\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x$

	\item $\forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)$

	\item $\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))$

	\item $\forall x^{\safe}, y^{\safe}.      x\leq x+y$

	\item $\forall x^{\safe}, y^{\safe}.    (  ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand  \succ{}(\succ{0}x) \neq \succ{0}y))$

	\item $\forall x^{\safe}, y^{\safe}.     x+y=y+x$

	\item $\forall x^{\safe}.       x+0=x$

	\item $\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)$

	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)$

	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)$

	\item $\forall x^{\safe}       0\cdot x =0$

	\item $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$

	\item $\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x$

	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)$

	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))$

	\item $\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))$

	\item $\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))$

\end{enumerate}

%$$

%%\begin{equation}

%\begin{array}{l}

%\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) \\

%\forall x^{\safe}. x \neq \succ{} x\\

%\forall x^{\safe}.0 \leq x\\

%\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\

%\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\

%\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\

%\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\

%\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\

%|0|=0\\

%\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\

%|\succ{}0|=\succ{} 0\\

%\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)\\

%\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)\\

%\forall y^{\normal}.    0 \smsh y=\succ{} 0\\

%\forall x^{\normal}.    (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))\\

%\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x\\

%\forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)\\

%\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\

%\forall x^{\safe}, y^{\safe}.      x\leq x+y\\

%\forall x^{\safe}, y^{\safe}.    (  ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand  \succ{}(\succ{0}x) \neq \succ{0}y))\\

%\forall x^{\safe}, y^{\safe}.     x+y=y+x\\

%\forall x^{\safe}.       x+0=x\\

%\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)\\

%\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)\\

%\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)\\

%\forall x^{\safe}       0\cdot x =0\\

%\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x\\

%%\text{\anupam{check above normal/safe! Pretty sure should be other way around.}}\\

%\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\

%\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\

%\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\

%\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))\\

%\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))

%\end{array}

%%\end{equation}

%$$

%

In addition to these axioms, our theories will contain forms of induction, defined below.

We will introduce in fact a hierarchy of theories calibrated by the complexity of induction formulae, so we now introduce the appropriate quantifier hierarchy.

\begin{definition}

	[Quantifier hierarchy]

	$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.

	We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.

	We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.

\end{definition}

Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.

The criterion is purely to give an appropriate definition of the hierarchy above.

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{\Xi}$, when $A \in \Xi$.

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

We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall  \vec x^{\safe}, \exists! y^{\safe}. A_f (\vec u , \vec x , y)$, such that $\Nat \models A_f (\vec u , \vec x , f(\vec u , \vec x))$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.

We sometimes explicitly delimit variables as such when it is helpful, writing $A_f (\vec u ; \vec x , y)$.

$$

\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. 

\left( 

\begin{array}{rl}

&\exists z^{\safe}.x=\succ{0}z \cand y=y_0 \\

\cor&  \exists z^{\safe}.x=\succ{1}z \cand y=y_1

\right)

%$$\begin{array}{ll}

%\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\

%                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\

%                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\

%\end{array}

%$$