Révision 215 CSL17/arithmetic.tex

arithmetic.tex (revision 215)
134 134
135 135 
Let us give a few examples of formulas representing basic functions.
136 136 
\begin{itemize}
137 
\item Successor $\succ{}$: $\forall^{\safe} x, \exists^{\safe} y. y=x+1.$
137 
\item Projection $\pi_k^{m,n}$: $\forall^{\normal} u_1, \dots, u_m,  \forall^{\safe} x_{m+1}, \dots, x_{m+n}, \exists^{\safe} y. y=x_k$.
138 
\item Successor $\succ{}$: $\forall^{\safe} x, \exists^{\safe} y. y=x+1.$. The formulas for the binary successors $\succ{0}$, $\succ{1}$ and the constant functions $\epsilon^k$ are defined in a similar way.
139 
\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
138 140 
\item Conditional $C$:
139 141 
$$\begin{array}{ll}
140 142 
\forall^{\safe} x, y_{\epsilon}, y_0, y_1, \exists^{\safe} y. & ((x=\epsilon)\cand (y=y_{\epsilon})\\
......
143 145 
\end{array}
144 146 
$$
145 147 
\end{itemize}
146 
\patrick{to be continued}
147 148 

  		





  
  149
  
    

  		





  148
  150
  
    
\subsection{Encoding sequences in the arithmetic}


  		





  149
  151
  
    
\todo{}


  		





  150
  152
  
    

  		












Formats disponibles :
  Unified diff