Révision 260 CSL17/tech-report/arithmetic.tex
| arithmetic.tex (revision 260) | ||
|---|---|---|
| 198 | 198 |
|
| 199 | 199 |
\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
|
| 200 | 200 |
|
| 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)$.
|
|
| 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 \vec 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)$.
|
|
| 202 | 202 |
|
| 203 | 203 |
Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine: |
| 204 | 204 |
\begin{itemize}
|
| ... | ... | |
| 207 | 207 |
%\item Predecessor $p$: $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
|
| 208 | 208 |
\item Conditional $C$: |
| 209 | 209 |
$$\begin{array}{ll}
|
| 210 |
\forall x^{\safe} , y_{\epsilon}^{\safe}, y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=\epsilon)\cand (y=y_{\epsilon})\\
|
|
| 210 |
\forall x^{\safe} , y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
|
|
| 211 | 211 |
& \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
|
| 212 | 212 |
& \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
|
| 213 | 213 |
\end{array}
|
Formats disponibles : Unified diff