Révision 182

CSL17/arithmetic.tex (revision 182)
1 1 
\section{An arithmetic for the polynomial hierarchy}
2 
Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$. We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$.
2 
%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$.
3 
Our base language is defined by the set of functions (and constants) symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|\}$ and the set of predicate symbols
4 
 $\{\leq, \safe, \normal \}$.
5 
We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$.
6 
We will also use as shorthand notations:
7 
$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$
8 
We call \textit{atomic formulas} formulas of the form $(s\leq t)$ or $(s=t)$.
9 
 As we are in classical logic, 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 subformula of the form $\neg \neg A$.
3 10 

  		





  4
  
  
    
The $\basic$ axioms are as follows:


  		





  
  11
  
    
Now, let us describe the axioms we are considering.The $\basic$ axioms are as follows:


  		





  5
  12
  
    
\[


  		





  6
  13
  
    
\begin{array}{l}


  		





  7
  14
  
    
\safe (0) \\


  		





  ......




  33
  40
  
    
Use base theory + sharply bounded quantifiers.


  		





  34
  41
  
    

  		





  35
  42
  
    

  		





  36
  
  
    

  		





  37
  
  
    

  		





  38
  43
  
    
\begin{definition}


  		





  39
  44
  
    
[Quantifier hierarchy]


  		





  40
  45
  
    
$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded.


  		





  ......




  71
  76
  
    
\[


  		





  72
  77
  
    
 \dfrac{\forall \vec x^\normal . \exists  y^\safe .  A }{ \forall \vec x^\normal .\exists y^\normal . A}


  		





  73
  78
  
    
\]


  		





  74
  
  
    
%\patrick{For $\forall \vec x^\normal . \exists  y^\safe .  A$ closed ?} 


  		





  75
  79
  
    
\end{definition}


  		





  
  80
  
    
\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)}


  		





  
  81
  
    

  		





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


  		





  77
  83
  
    

  		





  78
  84
  
    
\begin{lemma}


  		





  ......




  308
  314
  
    
  Then, one can check that for all rules but the quantifier rules and the cut rule, if the conclusion is well-typed, then so are the two premises.  For the remaining rules, $\forall-r$ and $\exists-l$ are unproblematic, because of the observation above. Let us now examine the case of $\exists-r$, with a $\safe$ label, and the other rules can be treated in the same way. In the premise we get a formula $\safe(t) \cand A(t)$. Then what we do is that, if  $\vec u$ denote the free variables of $t$, we add to the context of all sequents of the proof $\normal(\vec u)$. We obtain in this way a valid proof new proof,  and the premises of the rule have become well-typed.


  		





  309
  315
  
    
       \end{proof}


  		





  310
  316
  
    
     


  		





  311
  
  
    
     \patrick{ TODO: define integer-positive sequents and proofs.}


  		





  
  317
  
    
     \patrick{As mentioned after Def 14, I don't think that we can prove that the proofs we consider are equivalent to integer positive proofs, by arguing that negative occurrences $\neg \safe(t)$ could be replaced by 'false', by using the lemma above. Indeed even if for all its free variables we have $\safe(\vec x)$, $\normal(\vec u)$ on the l.h.s. of the sequent, it is not clear to me why that would prove $\safe(t)$. My proposition is thus to restrict 'by definition' of $\arith^i$ to integer positive formulas.}


  		





  312
  318
  
    
     


  		





  313
  319
  
    
 \begin{theorem}


  		





  314
  320
  
    
   Assume the $\arith^i$ sequent calculus proves a closed formula $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$. Then there exists a proof $\pi$ of the sequent 


  		












Formats disponibles :
  Unified diff