Révision 259 CSL17/tech-report/arithmetic.tex
| arithmetic.tex (revision 259) | ||
|---|---|---|
| 28 | 28 |
\forall u^\normal. \safe(u) \\ |
| 29 | 29 |
\safe (0) \\ |
| 30 | 30 |
\forall x^\safe . \safe (\succ{} x) \\
|
| 31 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
|
| 32 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
|
| 33 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y )
|
|
| 34 | 31 |
\end{array}
|
| 35 | 32 |
\qquad |
| 36 | 33 |
\begin{array}{l}
|
| ... | ... | |
| 74 | 71 |
\forall x^{\safe}, y^{\safe}, z^{\safe}. (x+y)+z=x+(y+z)\\
|
| 75 | 72 |
\forall x^{\safe}, y^{\safe}, z^{\safe}. ( x+y \leq x+z \ciff y\leq z)\\
|
| 76 | 73 |
\forall x^{\safe} 0\cdot x =0\\
|
| 77 |
\forall x^{\normal}, y^{\safe}. x\cdot(\succ{}y)=(x\cdot y)+x\\
|
|
| 74 |
\forall x^{\safe}, y^{\normal}. x\cdot(\succ{}y)=(x\cdot y)+x\\
|
|
| 75 |
%\text{\anupam{check above normal/safe! Pretty sure should be other way around.}}\\
|
|
| 78 | 76 |
\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
|
| 79 | 77 |
\forall x^{\normal}, y^{\safe}, z^{\safe}. x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
|
| 80 | 78 |
\forall x^{\normal}, y^{\safe}, z^{\safe}. (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
|
| ... | ... | |
| 88 | 86 |
|
| 89 | 87 |
|
| 90 | 88 |
|
| 89 |
|
|
| 91 | 90 |
It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
|
| 92 | 91 |
\begin{proposition}
|
| 93 | 92 |
[Length induction] |
| ... | ... | |
| 182 | 181 |
\end{remark}
|
| 183 | 182 |
|
| 184 | 183 |
|
| 184 |
\begin{example}
|
|
| 185 |
[Some basic theorems] |
|
| 186 |
We give proofs of the following, that are sometimes included as basic axioms, in $\arith^1$: |
|
| 187 |
\[ |
|
| 188 |
\begin{array}{l}
|
|
| 189 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
|
| 190 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
|
| 191 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y ) \\
|
|
| 192 |
\forall u^\normal ,x^\safe . u \succ{} x = u + ux
|
|
| 193 |
\end{array}
|
|
| 194 |
\] |
|
| 195 |
\todo{Proof: Patrick? The final two should require PIND.}
|
|
| 196 |
\end{example}
|
|
| 185 | 197 |
|
| 186 | 198 |
|
| 187 |
|
|
| 188 | 199 |
\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
|
| 189 | 200 |
|
| 190 | 201 |
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 x^{\safe}, \exists! y^{\safe}. A_f$. 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)$.
|
Formats disponibles : Unified diff