\documentclass{amsart}
\usepackage{amsthm}


\input{macros}

\begin{document}
	\section{Logical operations as programs}
	
	Any polynomial-time predicate can be conservatively added to BC with only safe inputs.
	Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments. 
	
	\section{Soundness}
	We show that any provably convergent function of $I\Sigma^{N}_i$ is in $\Box_i$.
	
	\subsection{Interpreting $\Pi_{i-1}$ formulae as programs}
	Each $\Pi_{i-1}$ formula is directly interpreted, as in usual WFM, as a descriptive program evaluating whether it is true or not.
	We define it by induction on formula structure:


	\[
	\begin{array}{rcl}
	\wit{s,t}{s=t} (;x) & \dfn & =(;s,t) \\
	\smallskip
	\wit{t}{N(t)} (;x) & \dfn & =(;x,t)\\
	\smallskip
	\wit{t}{\Box N(t)} (u;) & \dfn & =(;u,t) \\
	\smallskip
	\wit{\vec t}{A\star B} (;x) & \dfn & \star (; \wit{\vec t}{A} (;x), \wit{\vec t}{B} (;x) ) \\
	\smallskip
	\wit{\vec t}{\exists x^N . A(x)} (;x) & \dfn & \begin{cases}
	1 & \exists a^N . \wit{a , \vec t}{A(a)} (;x) = 1 \\
	0 & \text{otherwise} 
	\end{cases} \\
	\smallskip
	\wit{\vec t}{\forall x^N . A(x)} (;x) & \dfn & 
	\begin{cases}
	0 & \exists a^N. \wit{a, \vec t}{ A(a)} (;x) = 0 \\
	1 & \text{otherwise}
	\end{cases}
	\end{array}
	\]
	
	(Notice that, by free-cut elimination, $\Box$-formulae are always of the form $\Box N(t)$, so any composite formulae can be assumed to have only safe arguments. 
	We can also assume that they always occur on the LHS of a sequent.)
	\subsection{Witness predicate for $\Sigma_i$ formulae}
%	We give the witness predicate for $\Sigma_i$ formulae assumed to be in prenex form.
	When $A,B$ are $\Sigma_{i}$ we define:
		\[
		\begin{array}{rcl}
		\wit{\vec t}{A\star B} (;\vec x , \vec y) & \dfn & \star (; \wit{\vec t}{A} (;\vec x), \wit{\vec t}{B} (;\vec y) ) \\
		\smallskip
		\wit{\vec t}{\exists  x . A( x)} (; x, \vec x) & \dfn & \wit{a, \vec t}{A( a)}(;\vec x) \left[ x^N /  a\right]
		\end{array}
		\]
	(Notice that this covers all $\Sigma_i$ formulae).
	
	\subsection{Witness extraction invariant}
%	We will show the following result:
	
	We will show that, if there is a proof $\pi$ of $\Gamma \seqar \Delta$, then there are programs $\vec f$ such that:
	\[
	\wit{\vec t}{\bigwedge \Gamma} (; \vec x)
	\quad \implies \quad
	\wit{\vec t}{\bigvee \Delta } (; \vec f (; \vec x) )
	\]
	
	\subsection{Defining the programs}
	We define the extracted programs inductively on a free-cut free proof.
	
	\begin{itemize}
	\item $\forall$ right case. Auxiliary formula $A$ must be $\Pi_{i-1}$ by free-cut elimination.
		\[
		\dfrac{N(a), \Gamma \seqar \Delta , A(a)}{\Gamma \seqar \Delta , \forall x^N. A(x)}
		\]
		By the inductive hypothesis we have functions $\vec f^\Delta , \vec f^A$ such that:
		\[
		\wit{a , \vec t}{N(a)} (;x)
		\wedge 
		\wit{a , \vec t}{\bigwedge \Gamma} (\vec u; \vec x)
		\implies
		\wit{a , \vec t}{\bigvee \Delta}{ (; \vec f^\Delta (\vec u ; x , \vec x))}
		\vee
		\wit{a , \vec t}{ A} (; \vec f^A (\vec u ; x , \vec x) )
		\]
		Since $A$ is $\Pi_{i-1}$ we can forget about $\vec f^A$.
		We define $\vec g^\Delta , \vec g^{\forall x^N . A}$ as follows:
		\[
		\begin{array}{rcl}
		\vec g^{\forall x^N . A} (\vec u ; \vec x) & \dfn & 0 \\
		\vec g^\Delta (\vec u ; \vec x) & \dfn & 
		\vec f^\Delta ( \vec u ;  \mu a^N . ( \wit{a , \vec t}{A} (;0) = 0 ) , \vec x )
		\end{array}
		\]
		(Notice that the minimisation program has the same complexity as the witness predicate for $\forall x^N . A(x)$, i.e.\ $\Pi_{i-1}$.)
	\item Contraction right case. Need to test the witness predicate using conditional. (No need for $\mu$s.).
	Given such a step,
	\[
	\dfrac{\Gamma \seqar \Delta , A , A}{\Gamma \seqar \Delta , A}
	\]
	by the inductive hypothesis we have programs $\vec f^\Delta , \vec f^0 , \vec f^1$ such that:
	\[
	\wit{\vec t}{\bigwedge \Gamma} (\vec u ; \vec x)
	\implies
	\wit{\vec t}{\bigvee \Delta} (; \vec f^\Delta (\vec u ; \vec x) )
	\vee
	\wit{\vec t}{A} (;\vec f^0 (\vec u ; \vec x))
	\vee
	\wit{\vec t}{A} (; \vec f^1 (\vec u ; \vec x))
	\]
	Construct the programs $\vec g^\Delta, \vec g^A$ as follows:
	\[
	\begin{array}{rcl}
	\vec g^\Delta (\vec u ; \vec x) & \dfn & \vec f^\Delta (\vec u ; \vec x) \\
	\vec g^A (\vec u; \vec x) & \dfn & 
	\begin{cases}
	\vec f^0 (\vec u ; \vec x) & \wit{\vec t}{A} (;\vec f^0(\vec u ; \vec x) =1 ) \\
	\vec f^1 (\vec u ; \vec x) & \text{otherwise}
	\end{cases} 
	\end{array}
	\]
	\item Induction. NB: Can assume no side-formulae on the right!!
	\[
	\dfrac{\Box N(a), \Gamma, A(a) \seqar A(s_i a)}{\Box N(s), \Gamma , A(0) \seqar A(s)}
	\]
	We need to keep track of all the terms in the witness predicate.
	\[
%	\begin{array}{rl}
%	&\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)
%	\\
%	\implies & 
%	\wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^A (u , \vec u ; \vec x , \vec y)  )
%	\vee
%	\wit{a , t(a), t(s_i a), \vec t}{\bigvee \Delta} (; \vec f^\Delta (u , \vec u ; \vec x , \vec y)  )
%	\end{array}
\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)
\implies 
\wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^i (u , \vec u ; \vec x , \vec y)  )
	\]
	Define $\vec g$ by safe recursion as follows:
	\[
	\begin{array}{rcl}
	\vec g (0 , \vec u ; \vec x , \vec y) & \dfn & \vec y \\
	\vec g (s_i u, \vec u ; \vec x , \vec y) & \dfn & \vec f^i ( u, \vec u; \vec x, \vec g (u, \vec u ; \vec x , \vec y) )
	\end{array}
	\]
	\end{itemize}
	\subsection{Proof of correctness}
	
\end{document}