Révision 238

CSL17/arithmetic.tex (revision 238)
8 8 
%The formula $A \cimp B$ will be a notation for $\neg A \cor B$.
9 9 
%We will also use as shorthand notations:
10 10 
%$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$
11 
\textit{Atomic formulas} formulas are of the form $(s\leq t)$, for terms $s,t$.
11 
\textit{Atomic formulas} formulas are of the form $s\leq t$, for terms $s,t$.
12 12 
 We will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of a subformula of the form $\neg \neg A$.
13 13
14 14
......
20 20 
We include a similar set of axioms for direct comparison, although in our setting these are not minimal.
21 21 
Indeed, $\#$ can be defined using induction in our setting.
22 22 

  		





  23
  
  
    
The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function symbols.


  		





  24
  
  
    
It also states the fundamental algebraic properties, i.e.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.


  		





  
  23
  
    
The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function and predicate symbols.


  		





  
  24
  
    
It also states fundamental algebraic properties, e.g.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.


  		





  25
  25
  
    
For instance, we include the following axioms:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}


  		





  26
  26
  
    
\[


  		





  27
  27
  
    
\begin{array}{l}


  		





  ......




  107
  107
  
    
\[


  		





  108
  108
  
    
 \dfrac{\proves \forall \vec x^\normal . \exists  y^\safe .  A }{ \proves \forall \vec x^\normal .\exists y^\normal . A}


  		





  109
  109
  
    
\]


  		





  110
  
  
    
We will write $\arith^i \proves A$ if $A$ is a logical consequence of the axioms of $\arith^i$, in the usual way.


  		





  
  110
  
    
We will write $\arith^i \proves A$ if $A$ is a logical consequence of the axioms and rules of $\arith^i$, in the usual way.


  		





  111
  111
  
    
\end{definition}


  		





  112
  112
  
    
%\patrick{I think in the definition of  $\arith^i$ we should impose that the formulas considered are \textit{integer positive}, that is to say that the only negative occurrences of atoms $\safe(t)$, $\normal(t)$ are those occurring in $\forall^{\safe}$ and $\forall^{\normal}$.  Indeed I don't think this can be just proved to be a consequence of a kind of 'normal form' of proofs, as we had discussed (see sect 4.4)}


  		





  113
  113
  
    
%


  		





  114
  114
  
    
%\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}


  		





  115
  115
  
    

  		





  116
  116
  
    
\begin{remark}


  		





  117
  
  
    
Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$, and indeed we believe there is a way to present these results in such a framework.


  		





  
  117
  
    
Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$ (which subsumes necessitation), and indeed we believe there is a way to present these results in such a framework.


  		





  118
  118
  
    
However, the proof theory of first-order modal logics, in particular free-cut elimination results used for witnessing, is not sufficiently developed to carry out such an exposition.	


  		





  119
  119
  
    
	\end{remark}


  		





  120
  120
  
    

  		





  ......




  125
  125
  
    
\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}


  		





  126
  126
  
    
%Todo: $+1$,  


  		





  127
  127
  
    

  		





  128
  
  
    
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 ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. 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)$.


  		





  
  128
  
    
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)$.


  		





  129
  129
  
    
 


  		





  130
  
  
    
Let us give a few examples for basic functions representable in $\arith^1$:


  		





  
  130
  
    
Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine:


  		





  131
  131
  
    
\begin{itemize}


  		





  132
  
  
    
\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$.


  		





  133
  
  
    
\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.


  		





  134
  
  
    
\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$


  		





  
  132
  
    
\item Projection $\pi_k^{m,n}$: $\forall u_1^{\normal} , \dots, u_m^{\normal} ,  \forall x_{m+1}^{\safe} , \dots, x^{\safe} _{m+n}, \exists y^{\safe} . y=x_k$.


  		





  
  133
  
    
%\item Successor $\succ{}$: $\forall x^{\safe} , \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.


  		





  
  134
  
    
%\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$


  		





  135
  135
  
    
\item Conditional $C$: 


  		





  136
  136
  
    
$$\begin{array}{ll}


  		





  137
  137
  
    
\forall^{\safe} x, y_{\epsilon}, y_0, y_1, \exists^{\safe} y. & ((x=\epsilon)\cand (y=y_{\epsilon})\\


  		





  ......




  139
  139
  
    
                                                                                                   & \cor( \exists^{\safe}z.(x=\succ{1}z) \cand (y=y_1)))\


  		





  140
  140
  
    
\end{array}


  		





  141
  141
  
    
$$


  		





  142
  
  
    
\item Addition:


  		





  143
  
  
    
$\forall^{\safe} x, y,  \exists^{\safe} z. z=x+y$. 


  		





  
  142
  
    
%\item Addition:


  		





  
  143
  
    
%$\forall^{\safe} x, y,  \exists^{\safe} z. z=x+y$. 


  		





  144
  144
  
    
\item Prefix:


  		





  145
  
  
    

  		





  146
  145
  
    
  This is a predicate that we will need for technical reasons, in the completeness proof. The predicate $\pref(k,x,y)$ holds if the prefix of string $x$


  		





  147
  146
  
    
  of length $k$ is $y$. It is defined as:


  		





  148
  147
  
    
  $$\begin{array}{ll}


  		












Formats disponibles :
  Unified diff