Révision 220 CSL17/appendix-arithmetic.tex
| appendix-arithmetic.tex (revision 220) | ||
|---|---|---|
| 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)$,
|
| 5 | 5 |
|
| 6 |
|
|
| 7 |
\[ |
|
| 8 |
\begin{array}{l}
|
|
| 9 |
\safe (0) \\ |
|
| 10 |
\forall x^\safe . \safe (\succ{} x) \\
|
|
| 11 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
|
| 12 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
|
| 13 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y )\\
|
|
| 14 |
\forall x^\safe, y^\safe . \safe(x+y)\\ |
|
| 15 |
\forall u^\normal, x^\safe . \safe(u\times x) \\ |
|
| 16 |
\forall u^\normal , v^\normal . \safe (u \smsh v)\\ |
|
| 17 |
\forall u^\normal \safe(u) \\ |
|
| 18 |
\forall u^\safe \safe(\hlf{u})\\
|
|
| 19 |
\forall u^\normal \safe(|x|) |
|
| 20 |
\end{array}
|
|
| 21 |
\] |
|
| 22 |
|
|
| 6 | 23 |
$$ |
| 7 | 24 |
%\begin{equation}
|
| 8 | 25 |
\begin{array}{l}
|
Formats disponibles : Unified diff