Révision 266 CSL17/tech-report/arithmetic.tex

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