root / CharacterizingPH / qpvbc.tex @ 146
Historique | Voir | Annoter | Télécharger (4,34 ko)
| 1 |
\documentclass{amsart}
|
|---|---|
| 2 |
\usepackage{amsthm}
|
| 3 |
\usepackage{hyperref}
|
| 4 |
\usepackage[dvipsnames]{xcolor}
|
| 5 |
|
| 6 |
\input{macros}
|
| 7 |
|
| 8 |
\begin{document}
|
| 9 |
\section{Extending the basic BC framework}
|
| 10 |
\begin{itemize}
|
| 11 |
\item Any polynomial-time predicate can be conservatively added to BC with only safe inputs. |
| 12 |
\item Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments. |
| 13 |
\item Can add G\"odel's $\beta$ functions with a safe input: |
| 14 |
\end{itemize}
|
| 15 |
|
| 16 |
|
| 17 |
\section{QPVBC}
|
| 18 |
|
| 19 |
\subsection{Bellantoni's system $\pvbci{}$}
|
| 20 |
(give definition) |
| 21 |
|
| 22 |
|
| 23 |
\begin{definition}
|
| 24 |
[Provably total function] |
| 25 |
\end{definition}
|
| 26 |
|
| 27 |
|
| 28 |
\subsection{Extensions by induction principles}
|
| 29 |
We define the systems $\pvbci i$ as $\pvbci{} + \Sigma^\sigma_i$-induction.
|
| 30 |
|
| 31 |
\section{Soundness}
|
| 32 |
We show that provably total functions of $\pvbci i$ are in $\fphi i$. |
| 33 |
|
| 34 |
The following is our main result: |
| 35 |
\begin{theorem}
|
| 36 |
If $\pvbci i \proves \forall \vec u^\normal , \vec x^\sigma . \exists \vec y^\sigma. A(\vec u , \vec x , \vec y)$, then there are $\mubci i $ programs $\vec f (\vec u ; \vec x)$ such that $\pvbci i \proves\forall \vec u^\normal , \vec x^\sigma . A(\vec u , \vec x , \vec f (\vec u ; \vec x) ) $. |
| 37 |
\end{theorem}
|
| 38 |
|
| 39 |
\begin{definition}
|
| 40 |
[Witness predicate] |
| 41 |
The \emph{witness predicate} is a $\mubci{}$ program $\wit{\vec a}{A}$, parametrised by variables $\vec a$ and a formula $A$ whose free variables are amongst $\vec a$, defined as follows.
|
| 42 |
If $A$ is a $\Pi_{i}$ formula then:
|
| 43 |
\[ |
| 44 |
\begin{array}{rcl}
|
| 45 |
\wit{\vec u; \vec x}{s=t} (\vec u ; \vec x, w) & \dfn & =(;s,t) \\
|
| 46 |
\smallskip |
| 47 |
\wit{\vec u; \vec x}{s\neq t} (\vec u ; \vec x, w) & \dfn & \neg (;=(;s,t)) \\
|
| 48 |
\smallskip |
| 49 |
\wit{\vec u ; \vec x}{A\cor B} (\vec u ; \vec x , w) & \dfn & \cor (; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\
|
| 50 |
\smallskip |
| 51 |
\wit{\vec u ; \vec x}{A\cand B} (\vec u ; \vec x , w) & \dfn & \cand(; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\
|
| 52 |
\smallskip |
| 53 |
\wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ;\vec x, w) & \dfn & \begin{cases}
|
| 54 |
1 & \exists x^\safe . \wit{\vec u; \vec x, x }{A(x)} (\vec u ;\vec x , x, w) = 1 \\
|
| 55 |
0 & \text{otherwise}
|
| 56 |
\end{cases} \\
|
| 57 |
\smallskip |
| 58 |
\wit{\vec u; \vec x}{\forall x^\safe . A(x)} (\vec u ;\vec x , w) & \dfn &
|
| 59 |
\begin{cases}
|
| 60 |
0 & \exists x^\sigma. \wit{\vec u ; \vec x , x}{ A(x)} (\vec u; \vec x , x) = 0 \\
|
| 61 |
1 & \text{otherwise}
|
| 62 |
\end{cases}
|
| 63 |
\end{array}
|
| 64 |
\] |
| 65 |
We now define $\Wit{\vec a}{A}$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec a$.
|
| 66 |
\[ |
| 67 |
\begin{array}{rcl}
|
| 68 |
\Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , w) & \dfn & \wit{\vec u ; \vec x}{A} (\vec u ; \vec x) \text{ if $A$ is $\Pi_i$} \\
|
| 69 |
\smallskip |
| 70 |
\Wit{\vec u ; \vec x}{A \cor B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B) ) \\
|
| 71 |
\smallskip |
| 72 |
\Wit{\vec u ; \vec x}{A \cand B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B) ) \\
|
| 73 |
\smallskip |
| 74 |
\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( \vec u ; \vec x , w , \vec w )
|
| 75 |
\end{array}
|
| 76 |
\] |
| 77 |
|
| 78 |
|
| 79 |
\end{definition}
|
| 80 |
|
| 81 |
\nb{use (de)pairing to make sure only $i$ $\mu$s are used to express a $\Pi_i$ predicate.}
|
| 82 |
|
| 83 |
\begin{proposition}
|
| 84 |
For $\Sigma_{i+1}$ formulae $A$, $\Wit{\vec u ; \vec x}{A}$ is a $\mubci{i} $ program.
|
| 85 |
\end{proposition}
|
| 86 |
|
| 87 |
Before proving the main theorem, we will need the following `witnessing lemma': |
| 88 |
|
| 89 |
\begin{lemma}
|
| 90 |
If $\pvbci{i+1} $ proves a $\Sigma^\safe_{i+1}$-sequent $\Gamma \seqar \Delta$ with free variables $\vec u^\normal , \vec x^\safe$ then there are $\mubci {i}$ functions $\vec f$ such that $\pvbci {i+1} \proves \Wit{\vec u , \vec x}{\bigwedge \Gamma} (\vec u ; \vec x , \vec y) \cimp \Wit{\vec u , \vec x}{\bigvee \Delta } (\vec u ; \vec x, \vec f (\vec u ; \vec x , \vec y) )$.
|
| 91 |
\end{lemma}
|
| 92 |
\begin{proof}
|
| 93 |
By induction on the size of a $\pvbci{i+1} $ proof.
|
| 94 |
Interesting steps below: |
| 95 |
\begin{itemize}
|
| 96 |
\item $\neg$-right |
| 97 |
\item $\exists$-right |
| 98 |
\item $\forall$-right |
| 99 |
\item Contraction-right: |
| 100 |
\item induction |
| 101 |
\end{itemize}
|
| 102 |
\end{proof}
|
| 103 |
|
| 104 |
\section{Completeness}
|
| 105 |
|
| 106 |
|
| 107 |
\end{document}
|