Révision 168 CSL17/arithmetic.tex

arithmetic.tex (revision 168)
1 1 
\section{An arithmetic for the polynomial hierarchy}
2 
Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.
2 3 

  		





  
  4
  
    

  		





  3
  5
  
    
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)


  		





  4
  6
  
    

  		





  5
  7
  
    
Use base theory + sharply bounded quantifiers.


  		





  6
  8
  
    

  		





  7
  9
  
    
\anupam{Perhaps use prefix quantifier instead of sharply bounded (a la Ignatovic?), since plays nicer with sharply bounded lemma?}


  		





  8
  10
  
    

  		





  
  11
  
    

  		





  
  12
  
    

  		





  9
  13
  
    
\begin{definition}


  		





  10
  14
  
    
[Quantifier hierarchy]


  		





  11
  15
  
    
We define:


  		





  ......




  15
  19
  
    
\end{itemize}	


  		





  16
  20
  
    
\end{definition}


  		





  17
  21
  
    

  		





  
  22
  
    

  		





  
  23
  
    
\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}


  		





  
  24
  
    

  		





  
  25
  
    

  		





  18
  26
  
    
\begin{definition}


  		





  19
  27
  
    
Define the theory $\arith^i$ consisting of the following axioms:


  		





  20
  28
  
    
\begin{itemize}


  		





  21
  29
  
    
	\item $\basic$;


  		





  22
  30
  
    
	\item $\cpind{\Sigma^\safe_i } $:


  		





  23
  
  
    
	\item $\forall \vec x \in \normal . \exists  y \in \safe .  A \cimp \forall \vec x \in \normal .\exists y\in \normal . A$ (raising) .


  		





  24
  31
  
    
\end{itemize}


  		





  
  32
  
    
and an inference rule:


  		





  
  33
  
    
\[


  		





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


  		





  
  35
  
    
\]


  		





  25
  36
  
    
\end{definition}


  		





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


  		





  26
  38
  
    

  		





  27
  
  
    

  		





  28
  39
  
    
\begin{lemma}


  		





  29
  40
  
    
[Sharply bounded lemma]


  		





  30
  41
  
    
Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.


  		





  ......




  42
  53
  
    
\end{proof}


  		





  43
  54
  
    

  		





  44
  55
  
    
Notice that $\prefix$ suffices to encode usual sharply bounded inequalities,


  		





  45
  
  
    
since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$.


  		





  
  56
  
    
since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$.


  		





  
  57
  
    

  		





  
  58
  
    

  		





  
  59
  
    
\subsection{Graphs of some basic functions}


  		





  
  60
  
    
Todo: $+1$,  


  		





  
  61
  
    

  		





  
  62
  
    
\subsection{Encoding sequences in the arithmetic}


  		





  
  63
  
    
\todo{}


  		





  
  64
  
    

  		





  
  65
  
    
\anupam{Assume we have a $\Sigma^\safe_1$ predicate $\beta(i,x,y)$, expressing that the $i$th element of the sequence $x$ is $y$, such that $\arith^1 \proves \forall i^\normal , x^\safe . \exists ! y^\safe . \beta (i,x,y)$.}


  		





  
  66
  
    

  		





  
  67
  
    

  		





  
  68
  
    
\subsection{A sequent calculus presentation}


  		





  
  69
  
    
\todo{Write out usual first-order sequent calculus}


  		





  
  70
  
    

  		





  
  71
  
    
\subsection{Free-cut free normal form of proofs}


  		





  
  72
  
    
\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}


  		












Formats disponibles :
  Unified diff