|
1 |
\documentclass{amsart}
|
|
2 |
\usepackage{amsthm}
|
|
3 |
|
|
4 |
|
|
5 |
\input{macros}
|
|
6 |
|
|
7 |
\begin{document}
|
|
8 |
\section{Logical operations as programs}
|
|
9 |
|
|
10 |
Any polynomial-time predicate can be conservatively added to BC with only safe inputs.
|
|
11 |
Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments.
|
|
12 |
|
|
13 |
\section{Soundness}
|
|
14 |
We show that any provably convergent function of $I\Sigma^{N}_i$ is in $\Box_i$.
|
|
15 |
|
|
16 |
\subsection{Interpreting $\Pi_{i-1}$ formulae as programs}
|
|
17 |
Each $\Pi_{i-1}$ formula is directly interpreted, as in usual WFM, as a descriptive program evaluating whether it is true or not.
|
|
18 |
We define it by induction on formula structure:
|
|
19 |
|
|
20 |
|
|
21 |
\[
|
|
22 |
\begin{array}{rcl}
|
|
23 |
\wit{s,t}{s=t} (;x) & \dfn & =(;s,t) \\
|
|
24 |
\smallskip
|
|
25 |
\wit{t}{N(t)} (;x) & \dfn & =(;x,t)\\
|
|
26 |
\smallskip
|
|
27 |
\wit{\vec t}{A\star B} (;x) & \dfn & \star (; \wit{\vec t}{A} (;x), \wit{\vec t}{B} (;x) ) \\
|
|
28 |
\smallskip
|
|
29 |
\wit{\vec t}{\exists x^N . A(x)} (;x) & \dfn & \begin{cases}
|
|
30 |
1 & \exists a^N . \wit{a , \vec t}{A(a)} (;x) = 1 \\
|
|
31 |
0 & \text{otherwise}
|
|
32 |
\end{cases} \\
|
|
33 |
\smallskip
|
|
34 |
\wit{\vec t}{\forall x^N . A(x)} (;x) & \dfn &
|
|
35 |
\begin{cases}
|
|
36 |
0 & \exists a^N. \wit{a, \vec t}{ A(a)} (;x) = 0 \\
|
|
37 |
1 & \text{otherwise}
|
|
38 |
\end{cases}
|
|
39 |
\end{array}
|
|
40 |
\]
|
|
41 |
|
|
42 |
\subsection{Witness predicate for $\Sigma_i$ formulae}
|
|
43 |
% We give the witness predicate for $\Sigma_i$ formulae assumed to be in prenex form.
|
|
44 |
When $A,B$ are $\Sigma_{i}$ we define:
|
|
45 |
\[
|
|
46 |
\begin{array}{rcl}
|
|
47 |
\wit{\vec t}{A\star B} (;\vec x , \vec y) & \dfn & \star (; \wit{\vec t}{A} (;\vec x), \wit{\vec t}{B} (;\vec y) ) \\
|
|
48 |
\smallskip
|
|
49 |
\wit{\vec t}{\exists x . A( x)} (; x, \vec x) & \dfn & \wit{a, \vec t}{A( a)}(;\vec x) \left[ x^N / a\right]
|
|
50 |
\end{array}
|
|
51 |
\]
|
|
52 |
(Notice that this covers all $\Sigma_i$ formulae).
|
|
53 |
|
|
54 |
\subsection{Witness extraction invariant}
|
|
55 |
% We will show the following result:
|
|
56 |
|
|
57 |
We will show that, if there is a proof $\pi$ of $\Gamma \seqar \Delta$, then there are programs $\vec f$ such that:
|
|
58 |
\[
|
|
59 |
\wit{\vec t}{\bigwedge \Gamma} (; \vec x)
|
|
60 |
\quad \implies \quad
|
|
61 |
\wit{\vec t}{\bigvee \Delta } (; \vec f (; \vec x) )
|
|
62 |
\]
|
|
63 |
|
|
64 |
\subsection{Defining the programs}
|
|
65 |
We define the extracted programs inductively on a free-cut free proof.
|
|
66 |
|
|
67 |
\begin{itemize}
|
|
68 |
\item $\forall$ cases: auxiliary formula ($A$) must be $\Pi_{i-1}$ by free-cut elimination.
|
|
69 |
\[
|
|
70 |
\dfrac{N(a), \Gamma \seqar \Delta , A(a)}{\Gamma \seqar \Delta , \forall x^N. A(x)}
|
|
71 |
\]
|
|
72 |
|
|
73 |
\end{itemize}
|
|
74 |
\subsection{Proof of correctness}
|
|
75 |
|
|
76 |
\end{document}
|