Révision 266
| CSL17/tech-report/arithmetic.tex (revision 266) | ||
|---|---|---|
| 77 | 77 |
\item $\forall x^{\safe}, y^{\safe}. x\leq x+y$
|
| 78 | 78 |
\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))$
|
| 79 | 79 |
\item $\forall x^{\safe}, y^{\safe}. x+y=y+x$ \label{axiom21}
|
| 80 |
\item $\forall x^{\safe}. x+0=x$
|
|
| 81 |
\item $\forall x^{\safe}, y^{\safe}. x+\succ{}y=\succ{}(x+y)$
|
|
| 80 |
\item $\forall x^{\safe}. x+0=x$ \label{axiom22}
|
|
| 81 |
\item $\forall x^{\safe}, y^{\safe}. x+\succ{}y=\succ{}(x+y)$ \label{axiom23}
|
|
| 82 | 82 |
\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. (x+y)+z=x+(y+z)$
|
| 83 | 83 |
\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ( x+y \leq x+z \ciff y\leq z)$
|
| 84 | 84 |
\item $\forall x^{\safe} 0\cdot x =0$
|
| 85 |
\item $\forall x^{\normal}, y^{\safe}. x\cdot(\succ{}y)=(x\cdot y)+x$ \label{axiom27}
|
|
| 86 |
\item $\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x$
|
|
| 85 |
%\item $\forall x^{\normal}, y^{\safe}. x\cdot(\succ{}y)=(x\cdot y)+x$ \label{axiom27} %% version with alternative sorting
|
|
| 86 |
\item $\forall x^{\safe}, y^{\normal}. x\cdot(\succ{}y)=(x\cdot y)+x$ \label{axiom27}
|
|
| 87 |
\item $\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x$
|
|
| 87 | 88 |
\item $\forall x^{\normal}, y^{\safe}, z^{\safe}. x\cdot(y+z)=(x\cdot y)+(x\cdot z)$ \label{axiom29}
|
| 88 | 89 |
\item $\forall x^{\normal}, y^{\safe}, z^{\safe}. (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))$
|
| 89 | 90 |
\item $\forall x^{\normal} . (x\neq 0 \cimp |x|=\succ{}(\hlf{x}))$
|
| ... | ... | |
| 225 | 226 |
\begin{array}{l}
|
| 226 | 227 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
| 227 | 228 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
| 228 |
%\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y ) \\
|
|
| 229 |
\forall u^\normal . (u = 0 \cor \exists v^\normal.\ u = \succ{} v ) \\
|
|
| 229 |
%\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y ) \\ %% version 1: Anupam
|
|
| 230 |
%\forall u^\normal . (u = 0 \cor \exists v^\normal.\ u = \succ{} v ) %% version 2: Patrick
|
|
| 231 |
\forall u^\normal . (u = 0 \cor \exists y^\safe. u = \succ{} v ) \\ %% version 3: after discussion
|
|
| 230 | 232 |
\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux
|
| 231 | 233 |
\end{array}
|
| 232 | 234 |
\] |
| ... | ... | |
| 242 | 244 |
\begin{itemize}
|
| 243 | 245 |
\item For the first statement, assume $\succ{} (x)=0$ in order to derive a contradiction. From axiom \ref{axiom1} we deduce $x \leq x$, and so by transitivity (axiom \ref{axiom<=transitivity}) we have $x\leq 0$. So axiom \ref{axiom3} gives us $x=0$, and so $x=\succ{} (x)$. Finally with axiom \ref{axiom2} we conclude with a contradiction.
|
| 244 | 246 |
\item For statement 2 assume $\succ{} x= \succ{} y$ and, in view of a contradiction, $x\neq y$. Let us apply axiom \ref{axiom6} and assume we are in the case where $x\leq y$ (the case $y\leq x$ is symmetric). By axiom \ref{axiom4}, using the assumption $x\neq y$ we deduce $\succ{} x \leq y$. So as $\succ{} x = \succ{} y$ we can derive that $\succ{} y \leq y$. So by using axiom \ref{axiom1} we obtain that $\succ{} y = y$, hence axiom \ref{axiom2} gives us a contradiction, so we are done.
|
| 245 |
\item For statement 3 we proceed by induction on $u$ on the formula $A(u)= (u=0) \cup \exists^{\normal} v. u=\succ{} v$. The formula $A(0)$ obviously holds. Let us assume $A(u)$ and prove $A(\succ{0} u)$ (the case for $A(\succ{1} u)$ will be similar). By $A(u)$ we deduce that either $u=0$, in which case we also have $\succ{0} u=0$, hence $A(\succ{0} u)$ also holds, or there is a $v$ such that $u=\succ{} v$. In this latter case we have $\succ{0} u=2\cdot(\succ{} v)=2 v +2$ (by axiom \ref{axiom29}), hence have $\succ{0} u=\succ{} (\succ{} (2\cdot v))$, and so $A(\succ{0} u)$ holds.
|
|
| 247 |
\item For statement 3 we proceed by induction on $u$ on the formula %$A(u)= (u=0) \cup \exists^{\normal} v. u=\succ{} v$.
|
|
| 248 |
$A(u)= (u=0) \cup \exists^{\safe} v. u=\succ{} v$. Note that this formula is in $\Sigma^{\safe}_1$, so we can do induction on it in $\arith^1$.
|
|
| 249 |
The formula $A(0)$ obviously holds. Let us assume $A(u)$ and prove $A(\succ{0} u)$ (the case for $A(\succ{1} u)$ will be similar). By $A(u)$ we deduce that either $u=0$, in which case we also have $\succ{0} u=0$, hence $A(\succ{0} u)$ also holds, or there is a $y$ such that $u=\succ{} y$. In this latter case we have $\succ{0} u=2\cdot(\succ{} y)=2 v +2$ (by axiom \ref{axiom29}), hence have $\succ{0} u=\succ{} (\succ{} (2\cdot y))$, and so $A(\succ{0} u)$ holds.
|
|
| 246 | 250 |
|
| 247 | 251 |
By induction we conclude that $\forall^{\normal} u. A(u)$ holds.
|
| 248 |
\item For statement 4 we just use axiom \ref{axiom27} followed by the $+$ commutativity axiom \ref{axiom21}.
|
|
| 252 |
\item Statement 4: |
|
| 253 |
%For statement 4 we just use axiom \ref{axiom27} followed by the $+$ commutativity axiom \ref{axiom21}.
|
|
| 254 |
Let $u$ be in $\normal$ and $x$ in $\safe$, and try to prove $u\succ{} x=u+ux$. We have $\succ{} x=x+1$ by axioms \ref{axiom23} and \ref{axiom22} , so $u\succ{} x= u(x+1)$, so from axiom \ref{axiom29} we deduce $ u\succ{} x= u(x+1)=ux+u$, and by axiom \ref{axiom21} we conclude that $ u\succ{} x=u+ux$.
|
|
| 249 | 255 |
\end{itemize}
|
| 250 | 256 |
\end{proof}
|
| 251 | 257 |
It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
|
Formats disponibles : Unified diff