% LaTex2e
\documentclass[12pt]{article}
\usepackage{amssymb,latexsym}

\def\symb{{\rm Symb}}
\def\conj{{\wedge}}
\def\infdisj{{\bigvee{\kern -.25in} \bigvee}}
\def\infconj{{\bigwedge{\kern -.25in} \bigwedge}}
\def\implies{{\to}}
\def\Oh{{\cal O}}

\begin{document}

\begin{flushright}
  A. Miller\\
  March 2001 \\
  7.15 of Ash-Knight
\end{flushright}

This answers a question raised by Charlie McCoy when he
was giving a topics course on a prepublication copy of the
book\footnote{Ash, C. J.; Knight, J.; Computable structures and the
hyperarithmetical hierarchy. Studies in Logic and the Foundations of
Mathematics, 144. North-Holland Publishing Co., Amsterdam, 2000. xvi+346 pp.
ISBN: 0-444-50072-3}
 by Ash and Knight.
 
Fix a recursive language $L$.
Define $\symb$ to be the infinite (recursive) set consisting
of
\begin{enumerate}
 \item all atomic formulas of $L$
 \item $\neg$, $\conj$, $\implies$
 \item $\exists x\;\;\;\; $ for each variable $x$, and
 \item $\infdisj\;$, $\;\;\infconj$
\end{enumerate}

For $a\in \Oh$ define $S_a$ be the set of all triples
$(s,a,e)$ with $s\in\symb$ and $e\in\omega$.  Also define
$S_{<a}$ to be the union of all $S_b$ for $b<_oa$.

For each $H\subseteq \omega$ and $e\in \omega$ define
$$H_e=\{n: (e,n)\in H\}$$ and let $W$ give the usual enumeration
of the recursively enumerable sets.

\medskip\noindent For $i\in S_a$ inductively define $\psi^H_i$ as follows:

\begin{enumerate}

\item If $i=(\rho, a, j)$ and $\rho$ atomic,  then
$\psi^H_i=\rho$

\item If $i=(\neg, a, j)$ and $j\in S_{<a}$ then
$\psi^H_i=\neg\psi^H_j$

\item If $i=(\conj, a, (n,m))$ and $n,m\in S_{<a}$, then
$\psi^H_i= (\psi^H_n\;\conj\; \psi^H_m)$

\item If $i=(\implies, a, (n,m))$ and $n,m\in S_{<a}$, then
$\psi^H_i= (\psi^H_n\;\implies\; \psi^H_m)$


\item If $i=(\exists x, a, j)$ and $j\in S_{<a}$, then
$\psi^H_i= \exists x \;\;\psi^H_j$

\item If $i=(\;\infdisj\;, a, e)$, then
$\psi^H_i= \infdisj\;\{\psi^H_j: j\in H_e\cap S_{<a}\}$

\item If $i=(\;\infconj\;, a, e)$, then
$\psi^H_i= \infconj\;\{\psi^H_j: j\in H_e\cap S_{<a}\}$


\item Otherwise, define $\psi^H_i$ to be $F$ (the symbol for false),
 e.g., in case 2 if $j\notin S_{<a}$.  Or $T$ it makes no difference.
Similarly, empty infinite conjunctions or disjunctions can be
assigned $T$ or $F$.

\end{enumerate}

\noindent {\bf Main Lemma.}

Suppose $a\in \Oh$
and $H$ is hyperarithmetic set which is effectively defined by
$S_a$, i.e. there exists a recursive $h:\omega\to S_a(T,F)$
(codes for infinitary propositional language on $T,F$)
such that  for all $n$
$$n\in H \;\;\mbox{ iff } \;\;\psi^W_{h(n)} \mbox{ is true}$$
Assume that the order type of $a$ is a limit ordinal and $b+b<a$ for
all $b<a$.

Then there exists a recursive $f:S_{<a}\to S_{<a+a}$ so that
for every $i\in S_{<a}$ we have that $\psi^H_i$ and $\psi^W_{f(i)}$
are logically equivalent, i.e., $\psi^H_i\equiv\psi^W_{f(i)}$

\bigskip\noindent
Proof.
In fact, we construct $f$ with the additional property that
if $i\in S_b$, then $f(i)\in S_{a+3(b+1)}$.  Addition here is
the usual $+_o$ operation on the elements of Kleene's $\Oh$.

The steps in the definition of $f(i)$ are all trivial except
for the infinite disjunction or conjunction cases.  For example:
\par\noindent
If $i=(\conj, b, (n,m))$, then $f(i)=(\conj, a+3(b+1), (f(n),f(m)))$.

\par\noindent
If $i=(\rho, b, e)$ where $\rho$ atomic, then $f(i)=(\rho, a+3(b+1), e)$.

\medskip\noindent
Now suppose $i=(\;\infdisj\;, b, e)$.  Note that

\medskip
$\psi^H_i= \;\;\infdisj\;\{\psi^H_j: j\in H_e\cap S_{<b}\}
\equiv \infdisj\;\{(\psi^W_{h(e,j)}\conj\psi^H_{j}): j\in S_{<b}\}$

$\;\;\;\;\;\;\equiv \;\infdisj\;\{(\psi^W_{h(e,j)}\conj\psi^W_{f(j)}): j\in S_{<b}\}$

\medskip
\noindent We construct $g$ recursive so that
$$(\psi^W_{h(e,j)}\conj\psi^W_{f(j)})\equiv \psi^W_{g(j)}$$
as follows:

Suppose
$h(e,j)=(s_1,a,e_1)$ and $f(j)=(s_2,a+3(c+1),e_2)$.  Then
define
$$g(j)=(\conj, a+3(c+1)+1,(h(e,j),f(j)))$$ and define
$f(i)=(\;\infdisj\;, a+3(b+1), e)$  where $W_e=\{g(j):j\in S_{<b}\}$.
Note that
$c+1\leq_ob$ implies
$3(c+1)+1\leq_o 3b+1<_o3(b+1)$
and hence $W_e\subseteq S_{<a+3(b+1)}$
as we needed to show the logical equivalence:

\medskip
$\psi^W_{f(i)}=\;\;\infdisj\;\{\psi^W_k: k\in W_e\}\equiv
\;\;\infdisj\;\{\psi^W_{g(j)}: j\in S_{<b}\}$

\medskip
\noindent The infinite conjunction case is similar except we use

$\infconj\;\{(\psi^W_{h(e,j)}\implies\psi^W_{f(j)}): j\in S_{<b}\}$

\bigskip\noindent This proves the Main Lemma.

\bigskip
Given $K\subseteq \bigcup_{a\in\Oh} S_a$
hyperarithmetic, it is easy to construct $H$ hyperarithmetic and
$j$ so that
$\infdisj\;\{\psi_i^W :i\in K\}\equiv \psi_j^H$.
By the main lemma we can find $k$ with $\psi_j^H\equiv\psi_k^W$.
Hence the recursive infinitary formulas are closed under
hyperarithmetic disjunctions.


I think the usual ``change into normal form" arguments allow for
an effective translation of these codes into the codes that Ash-Knight use
(and back).

\end{document}