Révision 230 CSL17/appendix-arithmetic.tex
| appendix-arithmetic.tex (revision 230) | ||
|---|---|---|
| 1 |
\section{An arithmetic for the polynomial hierarchy}\label{appendix:arithmetic}
|
|
| 1 |
\section{Appendix: remaining axioms of $\basic$}\label{appendix:arithmetic}
|
|
| 2 | 2 |
|
| 3 | 3 |
We give here the list of remaining axioms of $\basic$, which are directly inspired by the $\basic$ theory of Buss's bounded arithmetic \cite{Buss86book}:
|
| 4 | 4 |
%$\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
|
| ... | ... | |
| 7 | 7 |
$$ |
| 8 | 8 |
%\begin{equation}
|
| 9 | 9 |
\begin{array}{l}
|
| 10 |
\forall x^{\safe}, y^{\safe}. (y\leq x) \cimp (y \leq \succ{} x) \\
|
|
| 10 |
\forall x^{\safe}, y^{\safe}. (y\leq x\cimp y \leq \succ{} x) \\
|
|
| 11 | 11 |
\forall x^{\safe}. x \neq \succ{} x\\
|
| 12 | 12 |
\forall x^{\safe}.0 \leq x\\
|
| 13 |
\forall x^{\safe}, y^{\safe}.(x\leq y \cand x \neq y) \leftrightarrow \succ{} x \leq y\\
|
|
| 14 |
\forall x^{\safe}. x\neq 0 \cimp \succ{0}x \neq 0\\
|
|
| 15 |
\forall x^{\safe}, y^{\safe}. y\leq x \cor x \leq y\\
|
|
| 16 |
\forall x^{\safe}, y^{\safe}. x\leq y \cand y\leq x \cimp x=y\\
|
|
| 17 |
\forall x^{\safe}, y^{\safe}, z^{\safe}. x\leq y \cand y\leq z \cimp x\leq z\\
|
|
| 13 |
\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\
|
|
| 14 |
\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\
|
|
| 15 |
\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\
|
|
| 16 |
\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\
|
|
| 17 |
\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\
|
|
| 18 | 18 |
|0|=0\\ |
| 19 |
\forall x^{\safe}, y^{\safe}.x\neq 0 \cimp |\succ{0}x|=\succ{}( |x|) \cand |\succ{0}x|= \succ{}(|x|) \\
|
|
| 19 |
\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\
|
|
| 20 | 20 |
|\succ{}0|=\succ{} 0\\
|
| 21 |
\forall x^{\safe}, y^{\safe}. x\leq y \cimp |x|\leq |y|\\
|
|
| 22 |
\forall x^{\safe}, y^{\normal}. |x\smsh y|=\succ{}( |x|\cdot |y|)\\
|
|
| 21 |
\forall x^{\safe}, y^{\safe}. (x\leq y \cimp |x|\leq |y|)\\
|
|
| 22 |
\forall x^{\normal}, y^{\normal}. |x\smsh y|=\succ{}( |x|\cdot |y|)\\
|
|
| 23 | 23 |
\forall y^{\normal}. 0 \smsh y=\succ{} 0\\
|
| 24 |
\forall x^{\safe}. 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)\\
|
|
| 24 |
\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)))\\
|
|
| 25 | 25 |
\forall x^{\normal}, y^{\normal}. x \smsh y = y \smsh x\\
|
| 26 |
\forall x^{\safe}, y^{\safe}, z^{\normal}. |x|= |y| \cimp x\smsh z = y\smsh z\\
|
|
| 27 |
\forall x^{\safe}, u^{\safe}, v^{\safe}, y^{\normal}. |x|= |u|+ |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y)\\
|
|
| 26 |
\forall x^{\normal}, y^{\normal}, z^{\normal}. ( |x|= |y| \cimp x\smsh z = y\smsh z)\\
|
|
| 27 |
\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}. (|x|= |u|+ |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\
|
|
| 28 | 28 |
\forall x^{\safe}, y^{\safe}. x\leq x+y\\
|
| 29 |
\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\\
|
|
| 29 |
\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))\\
|
|
| 30 | 30 |
\forall x^{\safe}, y^{\safe}. x+y=y+x\\
|
| 31 | 31 |
\forall x^{\safe}. x+0=x\\
|
| 32 | 32 |
\forall x^{\safe}, y^{\safe}. x+\succ{}y=\succ{}(x+y)\\
|
| 33 | 33 |
\forall x^{\safe}, y^{\safe}, z^{\safe}. (x+y)+z=x+(y+z)\\
|
| 34 |
\forall x^{\safe}, y^{\safe}, z^{\safe}. x+y \leq x+z \leftrightarrow y\leq z\\
|
|
| 35 |
\forall x^{\normal} x\cdot 0=0\\
|
|
| 34 |
\forall x^{\safe}, y^{\safe}, z^{\safe}. ( x+y \leq x+z \ciff y\leq z)\\
|
|
| 35 |
\forall x^{\safe} 0\cdot x =0\\
|
|
| 36 | 36 |
\forall x^{\normal}, y^{\safe}. x\cdot(\succ{}y)=(x\cdot y)+x\\
|
| 37 | 37 |
\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
|
| 38 | 38 |
\forall x^{\normal}, y^{\safe}, z^{\safe}. x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
|
| 39 |
\forall x^{\normal}, y^{\safe}, z^{\safe}. x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \leftrightarrow y\leq z)\\
|
|
| 40 |
\forall x^{\normal} x\neq 0 \cimp |x|=\succ{}(\hlf{x})\\
|
|
| 41 |
\forall x^{\safe}, y^{\normal}. x= \hlf{y} \leftrightarrow (\succ{0}x=y \cor \succ{}(\succ{0}x)=y)
|
|
| 39 |
\forall x^{\normal}, y^{\safe}, z^{\safe}. (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
|
|
| 40 |
\forall x^{\normal} . (x\neq 0 \cimp |x|=\succ{}(\hlf{x}))\\
|
|
| 41 |
\forall x^{\safe}, y^{\safe}. ( x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
|
|
| 42 | 42 |
\end{array}
|
| 43 | 43 |
%\end{equation}
|
| 44 | 44 |
$$ |
| 45 | 45 |
|
| 46 |
It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
|
|
| 47 |
\begin{proposition}
|
|
| 48 |
[Length induction] |
|
| 49 |
The axiom schema of formulae, |
|
| 50 |
\begin{equation}
|
|
| 51 |
\label{eqn:lind}
|
|
| 52 |
( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
|
|
| 53 |
\end{equation}
|
|
| 54 |
for formulae $A \in \Sigma^\safe_i$ |
|
| 55 |
is equivalent to $\cpind{\Sigma^\safe_i}$.
|
|
| 56 |
\end{proposition}
|
|
| 57 |
\begin{proof}
|
|
| 58 |
Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
|
|
| 59 |
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|)$. |
|
| 60 |
\end{proof}
|
|
| 61 | 46 |
|
| 62 |
Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.
|
|
| 63 |
We will freely use this in place of polynomial induction whenever it is convenient. |
|
| 47 |
|
|
| 48 |
|
|
| 49 |
% |
|
| 50 |
%It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
|
|
| 51 |
%\begin{proposition}
|
|
| 52 |
% [Length induction] |
|
| 53 |
% The axiom schema of formulae, |
|
| 54 |
% \begin{equation}
|
|
| 55 |
% \label{eqn:lind}
|
|
| 56 |
% ( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
|
|
| 57 |
% \end{equation}
|
|
| 58 |
% for formulae $A \in \Sigma^\safe_i$ |
|
| 59 |
% is equivalent to $\cpind{\Sigma^\safe_i}$.
|
|
| 60 |
%\end{proposition}
|
|
| 61 |
%\begin{proof}
|
|
| 62 |
% Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
|
|
| 63 |
% 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|)$. |
|
| 64 |
%\end{proof}
|
|
| 65 |
% |
|
| 66 |
%Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.
|
|
| 67 |
%We will freely use this in place of polynomial induction whenever it is convenient. |
|
Formats disponibles : Unified diff