Révision 227 CSL17/soundness.tex

soundness.tex (revision 227)
43 43 
%
44 44 
%Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems.
45 45 

  		





  46
  
  
    
Let us say that a sorting $(\vec u ; \vec x)$ of the variables $\vec u , \vec x$ is \emph{compatible} with a formula $A$ if each variable of $\vec x$ occurs hereditarily safe with respect to the $\bc$-types of terms (see App.~\ref{appendix:arithmetic}). 


  		





  
  46
  
    

  		





  47
  47
  
    
In the presence of a compatible sorting, we may easily define functions that \emph{evaluate} safe formulae in $\mubc$:


  		





  48
  48
  
    

  		





  49
  49
  
    

  		





  ......




  55
  55
  
    
We will use the programs $\charfn{}{}$ in the witness functions we define below.


  		





  56
  56
  
    
Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Pi^\safe_{i-1}$.


  		





  57
  57
  
    
For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'.


  		





  
  58
  
    
Notice that, while we write $p(l)$ below, we really mean a polynomial in the \emph{length} of $l$, as a slight abuse of notation.


  		





  58
  59
  
    

  		





  59
  60
  
    

  		





  60
  61
  
    
\begin{definition}


  		





  ......




  156
  157
  
    
		Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\safe . A(\vec u ; x)$. By inversion and Thm.~\ref{thm:normal-form} there is a $\arith^i$ proof $\pi$ of $\normal (\vec u ) \seqar \exists x^\safe. A(\vec u ; x )$ in typed variable normal form.


  		





  157
  158
  
    
By Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f^\pi$ with $\wit{\vec u ;}{\exists x^\safe . A} (l, \vec u ; f(\vec u \mode l;)) =1$.


  		





  158
  159
  
    
By the definition of $\wit{}{}$ and Prop.~\ref{prop:wit-rfn} we have that $\exists x . A(\vec u \mode l; x)$ is true just if $A(\vec u \mode l ; \beta (q(l), 1 ; f(\vec u \mode l;) ))$ is true.


  		





  159
  
  
    
Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ suffices.


  		





  
  160
  
    
Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ suffices to finish the proof.


  		





  160
  161
  
    
	\end{proof}


  		












Formats disponibles :
  Unified diff