Révision 227 CSL17/appendix-arithmetic.tex

appendix-arithmetic.tex (revision 227)
4 4 
%$\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
5 5
6 6
7 
 \[
8 
 \begin{array}{l}
9 
 \safe (0) \\
10 
 \forall x^\safe . \safe (\succ{} x) \\
11 
 \forall x^\safe . 0 \neq \succ{} (x) \\
12 
 \forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
13 
 \forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )\\
14 
 \forall x^\safe, y^\safe . \safe(x+y)\\
15 
 \forall u^\normal, x^\safe . \safe(u\times x) \\
16 
 \forall u^\normal , v^\normal . \safe (u \smsh v)\\
17 
 \forall u^\normal \safe(u) \\
18 
 \forall u^\safe \safe(\hlf{u})\\
19 
 \forall u^\normal \safe(|x|)
20 
 \end{array}
21 
 \]
22
23 7 
$$
24 8 
%\begin{equation}
25 9 
\begin{array}{l}
......
57 41 
   \forall x^{\safe}, y^{\normal}.     x= \hlf{y} \leftrightarrow (\succ{0}x=y \cor \succ{}(\succ{0}x)=y)
58 42 
 \end{array}
59 43 
%\end{equation}
60 
$$
44 
$$
45 

  		





  
  46
  
    
It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:


  		





  
  47
  
    
\begin{proposition}


  		





  
  48
  
    
	[Length induction]


  		





  
  49
  
    
	The axiom schema of formulae,


  		





  
  50
  
    
	\begin{equation}


  		





  
  51
  
    
	\label{eqn:lind}


  		





  
  52
  
    
	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)


  		





  
  53
  
    
	\end{equation}


  		





  
  54
  
    
	for formulae $A \in \Sigma^\safe_i$


  		





  
  55
  
    
	is equivalent to $\cpind{\Sigma^\safe_i}$.


  		





  
  56
  
    
\end{proposition}


  		





  
  57
  
    
\begin{proof}


  		





  
  58
  
    
	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.


  		





  
  59
  
    
	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.


  		





  
  60
  
    
\end{proof}


  		





  
  61
  
    

  		





  
  62
  
    
Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.


  		





  
  63
  
    
We will freely use this in place of polynomial induction whenever it is convenient.


  		












Formats disponibles :
  Unified diff