Révision 185

CharacterizingPH/LCC17/lcc2017.tex (revision 185)
164 164 

  		





  165
  165
  
    
\section{An implicit theory for $\ph$}


  		





  166
  166
  
    
%As we mentioned, the goal of this work-in-progress is to arrive at an implicit characterisation of PH. 


  		





  167
  
  
    
We explain our approach for this work-in-progress in more detail here, referring to previous work when analogous methods are used.


  		





  
  167
  
    
We explain our approach in more detail here, deferring our main result to the end of this section and referring to previous work when analogous methods are used.


  		





  168
  168
  
    

  		





  169
  169
  
    
\subsection{Implicit programs for $\ph$}


  		





  170
  170
  
    
Since we want to remain at ground type, the natural programs in which to extract our witnesses will come from recursion theoretic characterisations, cf.\ the table above. Indeed, as we have already mentioned, we are not aware of any `higher-type' characterisation of $\ph$. 


  		





  ......




  220
  220
  
    
%	TODO or skip? If so just say that we formalise the standard argument (with explanation, e.g.\ minimisation, WOP, induction) but rely on safety of quantification rather than boundedness, which should come for free by inspection.


  		





  221
  221
  
    
%	


  		





  222
  222
  
    
	\subsection{Putting it all together}


  		





  
  223
  
    
	Due to space constraints, we only briefly describe our work here.


  		





  223
  224
  
    
	


  		





  224
  
  
    
To summarise the main goal of this work-in-progress, we are aiming for a variation of the following result:


  		





  
  225
  
    
Due to space considerThe main result of this work is the following


  		





  
  226
  
    
\begin{theorem}


  		





  
  227
  
    
	First-order arithmetic, axiomatised appropriately 


  		





  
  228
  
    
\end{theorem}


  		





  225
  229
  
    
	


  		





  226
  230
  
    
	


  		





  227
  
  
    
\begin{conjecture*}


  		





  228
  
  
    
	First-order classical modal logic $\mathit{S4}$ with induction restricted to non-modal formulae, over a suitable set of axioms, characterises the class $\ph$. Bounds on quantifier alternation in induction formulae delimit the levels of $\ph$.


  		





  229
  
  
    
\end{conjecture*}


  		





  
  231
  
    
%\begin{conjecture*}


  		





  
  232
  
    
%	First-order classical modal logic $\mathit{S4}$ with induction restricted to non-modal formulae, over a suitable set of axioms, characterises the class $\ph$. Bounds on quantifier alternation in induction formulae delimit the levels of $\ph$.


  		





  
  233
  
    
%\end{conjecture*}


  		





  230
  234
  
    
% ALTERNATIVE SUGGESTION


  		





  231
  235
  
    
%\begin{conjecture*}


  		





  232
  236
  
    
%	First-order ramified classical  logic with induction restricted to \textit{safe} formulae (that is to say not containing any $N_1$), over a suitable set of axioms, characterises the class $\ph$. Bounds on quantifier alternation in induction formulae delimit the levels of $\ph$.


  		












Formats disponibles :
  Unified diff