\section{Introduction}
\label{sec: Introduction} 
Prenex normal form theorem is one of the most basic theorems on theories based on classical first-order predicate logic.
In contrast, it does not hold for intuitionistic theories in general.
Therefore it does not make sense to consider an arithmetical hierarchy in an intuitionistic theory.
On the other hand, if one reasons in some semi-classical arithmetic which lies in-between classical arithmetic and  intuitionistic arithmetic, one can take an equivalent formula of the prenex normal form for any formula with low complexity.
Akama et al.\cite{ABHK04} introduces the classes of formulas $\mathrm{E}_k$ and $\mathrm{U}_k$ which corresponds to the classes of classical $\Sigma_k$ and $\Pi_k$ formulas respectively, and showed that the former is equivalent to the class of formulas of $\Sigma_k$ form and the latter is so for $\Pi_k$ over some semi-classical arithmetic respectively.
This prenex normal form theorem justifies their investigation on the arithmetical hierarchy in the context of intuitionistic first-order arithmetic.
Unfortunately, however, there are some crucial errors in their proof of the prenex normal form theorem \cite[Theorem 2.7]{ABHK04}.
In this paper, we revisit their formulation and modify their prenex normal form theorem in an appropriate way.

In Section \ref{sec: Preparation}, we recall the definitions and basic properties.
In Section \ref{sec: CE}, we provide a simple counterexample of \cite[Theorem 2.7]{ABHK04}.
In Section \ref{sec: PNFT}, we show the corrected version of the prenex normal form theorem (see Theorem \ref{thm: PNFT}).
In addition, we also present the simplified version of the prenex normal form theorem for formulas which do not contain the disjunction (see Theorem \ref{thm: PNFT for df-formulas}).
In Section \ref{sec: conservativity}, we carry out some generalization of a well-known result that classical arithmetic is $\Pi_2$-conservative over intuitionistic arithmetic with respect to semi-classical arithmetic.
In Section \ref{sec: Optimality}, using the generalized conservation result in Section \ref{sec: conservativity}, we characterize several prenex normal form theorems with respect to semi-classical arithmetic.
In particular, among other things, we show that for any theory ${T}$ in-between intuitionistic arithmetic and classical arithmetic, ${T}$ proves a semi-classical principle $\DNE{(\Pi_k \lor \Pi_k)}$ if and only if ${T}$ satisfies the prenex normal form theorem for $ \mathrm{U}_{k'}$ and $\Pi_{k'}$ for all $k' \leq k$ (see Theorem \ref{thm: characterization of PNFT(Ukp,Pk)}).








Throughout this paper, we work basically over intuitionistic arithmetic.
When we use some principle (including induction hypothesis [I.H.]) which is not available in intuitionistic arithmetic, it will be exhibited explicitly.
As regards basic reasoning over intuitionistic first-order logic, we refer the reader to see \cite[Section 6.2]{vD13}.

\section{Preparation}\label{sec: Preparation}
Throughout this paper, we work with a standard formulation of intuitionistic arithmetic $\mathsf{HA}$ described e.g.~in \cite[Section 1.3]{Tro73}, which has function symbols for all primitive recursive functions.
We work in the language containing all the logical constants $\forall, \exists, \to, \land, \lor, \perp$.
Let ${T}$ denote a theory (e.g. $\mathsf{HA}$), and ${\rm P}$ and ${\rm Q}$ denote schemata (e.g. logical principles).
Then ${T} + {\rm P}$ denotes the theory obtained from ${T}$ by adding ${\rm P}$ into the axioms.
In particular, the classical variant $\mathsf{PA}$ is defined as $\mathsf{HA} + {\rm LEM}$, where ${\rm LEM}$ is the axiom scheme of the law of excluded middle.
We write ${T} \vdash {\rm Q}$ (or ${T} $ proves ${\rm Q}$) if any instance of ${\rm Q}$ is provable in ${T}$.
 We write ${T} \vdash {\rm P}+{\rm Q}$ if ${T} \vdash {\rm P}$ and ${T} \vdash {\rm Q}$.


\begin{notation}
For a formula $\varphi$, $\FV{\varphi}$ denotes the set of free variables in $\varphi$.
Quantifier-free formulas are denoted with subscript ``qf'' as $\QF{\varphi}$.
In addition, a list of variables is denoted with an over-line as $\ol{x}$.
In particular, a list of quantifiers of the same kind is denoted as $\exists \ol{x}$ and  $\forall \ol{x}$ respectively.
\end{notation}

\begin{definition}
\label{def: Sigma_k and Pi_k}
\noindent
The classes $\Sigma_k$ and $\Pi_k$ of formulas are defined as follows:
\begin{itemize}
\item
$\Sigma_0$, as well as $\Pi_0$, is the class of all quantifier-free formulas;
\item
$\Pi_{k+1}$ is the class of all formulas of form
$Q_1 \ol{x_1} \cdots Q_{k+1} \ol{x_{k+1}} \, \QF{\varphi}$;
    \item 
$\Sigma_{k+1}$ is the class of all formulas of form
$Q'_1 \ol{x_1} \cdots Q'_{k+1} \ol{x_{k+1}} \, \QF{\varphi}$;
\end{itemize}
where
$Q_i$ represents $\forall$ for odd $i$ and $\exists$ for even $i$
and
$Q'_i$ represents $\exists$ for odd $i$ and $\forall$ for even $i$.
Following \cite{ABHK04}, we define the classes $\Sigma_k$ and $\Pi_k$ in the non-cumulative manner (namely, each $Q_i \ol{x_i} $ and $Q'_i \ol{x_i}$ must not be empty).
A formula $\varphi$ is of {\bf prenex normal form} if $\varphi \in \Sigma_k \cup \Pi_k$ for some $k$. 
\end{definition}
\noindent


\begin{remark}
\label{rem: sigma_k and pi_k}
Since the list of variables can be contracted into one variable in $\mathsf{HA}$ by using a fixed primitive recursive pairing function (see e.g. \cite[1.3.9]{Tro73}), one may assume that for each natural number $k>0$, a formula in $\Sigma_k$ is of form $\exists x \varphi(x)$ with some $\varphi(x) \in \Pi_{k-1}$ and a formula in $\Pi_k$ is of form $\forall x \psi(x)$ with some $\psi(x) \in \Sigma_{k-1}$ without loss of generality.
\end{remark}

\begin{lemma}
\label{lem: sigma_k and pi_k}
Let $k$ be a natural number.
Let $\varphi$ be in $\Pi_k$ and $\psi$ be in $\Sigma_k$.
Then, for all natural numbers $i,j$, there exist $\varphi', \psi'\in \Pi_{k+i}$ and $\varphi'', \psi'' \in \Sigma_{k+j}$ such that $\FV{\varphi}=\FV{\varphi'}=\FV{\varphi''}$, $\FV{\psi}=\FV{\psi'}=\FV{\psi''}$,
$
\mathsf{HA} \vdash  \varphi \leftrightarrow \varphi' \leftrightarrow \varphi''   $
and $\mathsf{HA} \vdash \psi \leftrightarrow \psi' \leftrightarrow \psi''$.
\end{lemma}
\begin{proof}
Straightforward by the fact that
\begin{equation*}
\label{eq: adding quantifier}
\mathsf{HA} \vdash \xi \leftrightarrow \forall z \xi  \leftrightarrow \exists z \xi
\end{equation*}
for any $ z\notin \FV{\xi}$.
\end{proof}


\begin{definition}
For a class $\Gamma$ of formulas,
$\Gamma (\ol{x})$ denotes the class of formulas $\varphi$ in $\Gamma$ such that $\FV{\varphi} \subseteq \{ \ol{x}\}$.
\end{definition}


\begin{remark}
\label{rem: identification on Sigma_k and Pi_k}
In the light of Lemma \ref{lem: sigma_k and pi_k}, throughout this paper, we identify the classes $\Sigma_k$ and $\Pi_k$ with the classes defined as in Definition \ref{def: Sigma_k and Pi_k} with allowing the quantifiers $Q_i$ and $Q'_i$ to be empty.
Under this identification, for all $k$ and $k'$ such that $k< k' $, $\Pi_k (\ol{x}) $ and $\Sigma_k (\ol{x})$ are considered to be sub-classes of $ \Sigma_{k'} (\ol{x}) \cap \Pi_{k'} (\ol{x})$.
We frequently use this property in what follows.
\end{remark}

Recall the logical principles from \cite{ABHK04} and related principles:
 \begin{definition}\label{def: LP}
Let $\Gamma$ and $\Gamma'$ be classes of formulas.
\noindent
\begin{itemize}
    \item 
$\LEM{\Gamma}:\,  \forall x \left( \varphi (x) \lor \neg \varphi (x) \right)$ where $\varphi (x)
\in \Gamma(x)$.
\item
$\DML{\Gamma}:\,  \forall x \left( \neg (\varphi (x) \land \psi (x)) \to \neg \varphi (x) \lor \neg \psi (x) \right)$ where $\varphi (x), \psi (x) \in \Gamma(x)$.
    \item 
$\DNE{\Gamma}:\,  \forall x \left( \neg \neg \varphi (x) \to \varphi (x) \right) $ where $\varphi (x) \in \Gamma(x)$.
    \item 
$\DNE{(\Gamma \lor \Gamma')}:\,  \forall x \left( \neg \neg (\varphi (x) \lor \psi (x)) \to \varphi (x) \lor \psi (x) \right)$ where $\varphi (x)  \in \Gamma(x)$ and $\psi(x) \in \Gamma'(x)$.
\item
$\DNS{\Gamma}: \, \forall x \left(\forall  y \neg \neg \varphi(x,y ) \to \neg \neg \forall y \varphi(x,y) \right)$ where $\varphi(x,y ) \in \Gamma (x,y)$.
\item
Let ${\rm P} \in \{\LEM{\Gamma}, \DML{\Gamma}, \DNE{\Gamma}, \DNE{(\Gamma \lor \Gamma')} , \DNS{\Gamma}\}$.\\          
$\NN{{\rm P}}:\,  \neg \neg \xi$ where $\xi$ is an instance of ${\rm P} $.
\end{itemize}
 \end{definition}
 \noindent
 Note that our logical principles are equivalent also to those defined with lists of quantifiers of the same kind (cf. Remark \ref{rem: sigma_k and pi_k}).
 
\begin{remark}\label{rem: On formulations}
One has to care about the formulation of the double negated variants.
That is, one has to take the double negations of the universal closure of the original logical principles as in Definition \ref{def: LP}.
The double negated variants defined as such are not provable in $\mathsf{HA}$, which has been overlooked in the proof of \cite[Theorem 2.7]{ABHK04} (see also Section \ref{sec: CE}).
In fact, one may think of the double negated versions as variants of the double negation shift principle (see \cite{FK18}).
In addition, our double negated versions are equivalent to (the universal closures of) those with allowing free variables (cf. \cite[Remark 2.5]{FK18}).
\end{remark}

\begin{remark}
\label{rem: NNDNS <-> DNS}
For any class $\Gamma$ of formulas, 
$\DNS{\Gamma} $ is intuitionistically equivalent to $\NN{\DNS{\Gamma} }$ since
$$
\begin{array}{cl}
     & \forall x \left(  \forall y \neg \neg \varphi  \to  \neg \neg   \forall y \varphi  \right)  \\
 \longleftrightarrow    & \forall x \neg \neg \left(  \forall y \neg \neg \varphi  \to   \neg \neg \forall y \varphi  \right) \\
  \longleftrightarrow    & \neg \neg  \forall x \neg \neg \left(  \forall y \neg \neg \varphi  \to   \neg \neg \forall y \varphi  \right) \\
    \longleftrightarrow  &\neg \neg \forall x  \left(  \forall y \neg \neg \varphi  \to  \neg \neg  \forall y \varphi  \right).\\
\end{array}
$$
 \end{remark}
 
Next we reformulate the classes of formulas studied in \cite{ABHK04}.
The classes $\mathrm{F}_k, \mathrm{U}_k$ and $\mathrm{E}_k$ in Definition \ref{def: Classes} below were  dealt with in \cite{ABHK04} informally.
Here we shall introduce them and two additional classes $\mathrm{U}_k^+$ and $\mathrm{E}_k^+$ in a formal manner.
\begin{definition}\label{def: alp}
An alternation path is a finite sequence of $+$ and $-$ in which $+$ and $-$ appear alternatively.
For an alternation path $s$, let $i(s)$ denote the first symbol of $s$ if $s \not \equiv \ang{\, }$ (empty sequence); $ \times$ if $s \equiv \ang{\, }$.
Let $s^{\perp}$ denote an alternation path which is obtained by switching $+$ and $-$ in $s$, and let $l(s) $ denote the length of $s$.
\end{definition}

\begin{definition}\label{def: ALT(vp)}
For a formula $\varphi$, the set of alternation paths $\alt{\varphi}$ of $\varphi$ is defined as follows:
\begin{itemize}
    \item 
    If $\varphi$ is quantifier-free, then $\alt{\varphi} := \{ \ang{\, } \}$;
    \item
    Otherwise, $\alt{\varphi}$ is defined inductively by the following rule:
    \begin{itemize}
        \item 
        If $\varphi \equiv \neg \varphi_1$, then $\alt{\varphi} := \{ s^{\perp} \mid s\in \alt{\varphi_1}\}$;
        \item
        If $\varphi \equiv \varphi_1 \land \varphi_2$ or $\varphi \equiv \varphi_1 \lor \varphi_2$, then $\alt{\varphi} := \alt{\varphi_1} \cup \alt{\varphi_2}$;
        \item
        If $\varphi \equiv \varphi_1 \to \varphi_2$, then $\alt{\varphi} := \{ s^{\perp} \mid s \in \alt{\varphi_1}\} \cup \alt{\varphi_2}$;
\item
If $\varphi \equiv \forall x \varphi_1 $, then $\alt{\varphi} :=\{s \mid s\in \alt{\varphi_1} \text{ and } i(s)\equiv -\} \cup \{-s \mid s\in \alt{\varphi_1} \text{ and } i(s)\not \equiv - \} $;
\item
If $\varphi \equiv \exists x \varphi_1 $, then $\alt{\varphi} :=\{s \mid s\in \alt{\varphi_1} \text{ and } i(s)\equiv + \} \cup \{+s \mid s\in \alt{\varphi_1} \text{ and } i(s)\not \equiv + \} $.
    \end{itemize}
\end{itemize}
In addition, for a formula $\varphi$, the degree $\degree{\varphi}$ of $\varphi$ is defined as 
$$\degree{\varphi} := \max \{l(s) \mid s \in \alt{\varphi}  \} .$$


\end{definition}








\begin{definition}
\label{def: Classes}
The classes $\mathrm{F}_k, \mathrm{U}_k, \mathrm{E}_k $ (from \cite[Definition 2.4]{ABHK04}), $\mathrm{U}_k^+ $ and $ \mathrm{E}_k^+ $ of formulas are defined as follows:
\begin{itemize}
    \item
    $\mathrm{F}_k := \{ \varphi \mid \degree{\varphi}=k  \}    $;
    \item
    $\mathrm{U}_0:=\mathrm{E}_0:=\mathrm{F}_0$;
    \item
$\mathrm{U}_{k+1} := \{ \varphi \in \mathrm{F}_{k+1} \mid i(s) \equiv - \text{ for all }s\in \alt{\varphi} \text{ such that }l(s) =k+1 \}$;
\item
$\mathrm{E}_{k+1} := \{ \varphi \in \mathrm{F}_{k+1} \mid i(s) \equiv + \text{ for all }s\in \alt{\varphi} \text{ such that }l(s) =k+1  \}$;
    \item
$\begin{displaystyle}
\mathrm{U}_k^+ := \mathrm{U}_k \cup \bigcup_{i<k} \mathrm{F}_i
\end{displaystyle}
$;
    \item
$\begin{displaystyle}
\mathrm{E}_k^+ := \mathrm{E}_k \cup \bigcup_{i<k} \mathrm{F}_i
\end{displaystyle}
$. 
\end{itemize}
\end{definition}
\begin{remark}
\label{rem: Ekp and Ukp}
A similar property as Lemma \ref{lem: sigma_k and pi_k} also holds for $\mathrm{U}_k^+$ and $\mathrm{E}_k^+$:
for any $\varphi \in \mathrm{U}_k^+$ and $\psi\in \mathrm{E}_k^+$, there exist $\varphi'\in \mathrm{U}_k$ and $\psi' \in \mathrm{E}_k$ such that $\FV{\varphi}=\FV{\varphi'}$, $\FV{\psi}=\FV{\psi'}$, $\mathsf{HA} \vdash \varphi \leftrightarrow \varphi'$ and $\mathsf{HA} \vdash \psi \leftrightarrow \psi'$.
\end{remark}

Note $\mathrm{F}_0 =\Sigma_0 =\Pi_0$.
For each formula  $\varphi \in \mathrm{E}_k$ (resp. $\psi \in \mathrm{U}_k$) of $\mathsf{PA}$,
one can take a formula $\varphi' \in \Sigma_k$ (resp. $\psi' \in \Pi_k$) of $\mathsf{PA}$ which is equivalent to $\varphi$ (resp. $\psi$) over $\mathsf{PA}$.
On the other hand, this is not the case for $\mathsf{HA}$.
In what follows, we study what kind of semi-classical arithmetic in-between $\mathsf{PA}$ and $\mathsf{HA}$ captures this property for each $k$.
In fact, Akama et al. \cite{ABHK04} has already undertaken this.
In particular, \cite[Theorem 2.7]{ABHK04} asserts the following:
\begin{enumerate}
    \item 
     For any $\varphi \in \mathrm{E}_k$,
        there exists $\varphi' \in \Sigma_k$  such that
    $$
    \mathsf{HA}  + \DNE{\Sigma_k} \vdash \varphi \leftrightarrow \varphi'.
$$
\item
 For any $\varphi \in \mathrm{U}_k$,
        there exists $\varphi' \in \Pi_k$  such that
    $$
    \mathsf{HA}  + \DNE{(\Pi_k \lor \Pi_k)} \vdash \varphi \leftrightarrow \varphi'.
$$
\end{enumerate}
However, the first assertion is wrong as we show in Section \ref{sec: CE}.



\section{A counter example}
\label{sec: CE}
 Recall that \cite[Theorem 2.7]{ABHK04} asserts that
 for any $\varphi \in \mathrm{E}_k$,
        there exists $\varphi' \in \Sigma_k$  such that
    $$
    \mathsf{HA}  + \DNE{\Sigma_k} \vdash \varphi \leftrightarrow \varphi'.
$$
However, there are some errors in the proof.
In particular, in \cite[page 5, lines 15-17]{ABHK04}, it is written that
``
Since the double negations of ${\rm DNE}$ is intuitionistically provable, $\vdash_{\mathsf{HA}} \NN{A_0} \leftrightarrow \NN{\exists x_0. C_0 }$ (which means $\mathsf{HA} \vdash  \NN{A_0} \leftrightarrow \NN{\exists x_0 C_0 }$ in our notation)
''.
As studied in \cite{FK18}, however, the double negations of (the universal closure of) ${\rm DNE}$ is not provable in $\mathsf{HA}$, and hence, their proof actually uses some double negated logical principles in the sense of Definition \ref{def: LP}.
Our counterexample below
shows that such a use of some additional principle is unavoidable.


Recall the arithmetical form of Church's thesis from \cite[3.2.14]{Tro73}:
$$
\mathrm{CT_0}: \forall x \exists y \,\varphi (x,y) \to \exists e \forall x \exists v \left({\rm T}(e,x,v) \land \varphi (x, {\rm U}(v))  \right),
$$
where
${\rm T}$ and ${\rm U}$ are the standard primitive recursive predicate and function from the Kleene normal form theorem.
Note that $\mathrm{CT_0}$ is a sort of combination of so-called  Church's thesis stating that every function is recursive and the countable choice principle (see \cite[4.3.2]{ConstMathI}).

\begin{proposition}
\label{prop: counterexample}
The following sentence
$$
\varphi_0:\equiv \neg \forall x \left( \neg  \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u)=0 \right) \lor \neg  \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u)\neq 0 \right) \right)
$$
is not equivalent to any sentence $\varphi_0 ' \in \Sigma_1 $ over $\mathsf{HA} +\DNE{\Sigma_1}$.
\end{proposition}
\begin{proof}
We first claim that $\mathsf{HA} + \mathrm{CT_0}$ proves $\varphi_0$.
For the sake of contradiction, assume 
\begin{equation}\label{eq: nonrec}
\forall x \left( \neg \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u)=0 \right) \lor \neg \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u)\neq 0 \right) \right)
\end{equation}
and reason in $\mathsf{HA} + \mathrm{CT_0}$.
Since
$\varphi_1\lor \varphi_2 \leftrightarrow \exists k\left( (k=0 \to \varphi_1) \land (k\neq 0 \to \varphi_2) \right)$ (see \cite[1.3.7]{Tro73}),
by $\mathrm{CT_0}$, there exists $e$ such that
$$
\forall x \exists v
\left(
\begin{array}{l}
{\rm T}(e,x,v) \\
\land  \left({\rm U}(v)=0 \to \neg \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u)=0 \right) \right) \\
\land  \left({\rm U}(v)\neq 0 \to \neg \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u) \neq 0 \right) \right)
\end{array}
\right).
$$
In particular, for that $e$, there exists $v_e$ such that ${\rm T}(e,e,v_e)$,
$$
{\rm U}(v_e)=0 \to \neg \exists u \left( {\rm T}(e,e,u) \land {\rm U}(u)=0 \right)
$$
and 
$$
 {\rm U}(v_e)\neq 0 \to \neg \exists u \left( {\rm T}(e,e,u) \land {\rm U}(u) \neq 0 \right).
 $$
Since  ${\rm U}(v_e)=0 \lor {\rm U}(v_e) \neq 0$, we obtain a contradiction straightforwardly.


If $\varphi_0 $ is equivalent to some sentence $\varphi_0 ' \in \Sigma_1 $ over $\mathsf{HA} +\DNE{\Sigma_1}$, we have
$\mathsf{HA} + \DNE{\Sigma_1} +\mathrm{CT_0} \vdash \varphi_0 '$
from the above claim.
Since $\varphi_0' \in \Sigma_1$, by the soundness of Kleene realizability  (see \cite[3.2.22]{Tro73}), we have that
$$\mathsf{HA} + \DNE{\Sigma_1}  \vdash \varphi_0 ',$$
and hence, $\mathsf{HA} + \DNE{\Sigma_1}  \vdash \varphi_0 $.
On the other hand, since
$$\forall x \left( 
\neg \left(
 \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u)=0 \right) \land  \exists u \left( {\rm T}(x,x,u) \land {\rm U}(u)\neq 0 \right)
\right) \right)
$$
is provable in $\mathsf{HA}$, we have
$\mathsf{HA} +\DML{\Sigma_1} \vdash \eqref{eq: nonrec}$.
Therefore we have
$$
\mathsf{HA} + \DNE{\Sigma_1} + \DML{\Sigma_1} \vdash \perp,$$
and hence, $\mathsf{PA} \vdash \perp$, which is a contradiction. 
\end{proof}

\begin{remark}
One can easily see that $\varphi_0 $ in Proposition \ref{prop: counterexample} is in $\mathrm{E}_1$.
Thus Proposition \ref{prop: counterexample} shows that $\varphi_0 $ is a counterexample of \cite[Theorem 2.7]{ABHK04} for $k=1$.
\end{remark}




\section{Basic lemmata}
In this section, we show several lemmata which we use in the proofs of our prenex normal form theorems.
\begin{lemma}
\label{lem: HA+P |- vp => HA+NNP |- NNvp}
For any logical principle ${\rm P}$ in Definition \ref{def: LP} and any formula $\varphi$ (possibly containing free variables), if $\mathsf{HA} + {\rm P} \vdash \varphi$, then $\mathsf{HA} + {\rm \NN{P}} \vdash \NN{\varphi}$.
\end{lemma}
\begin{proof}
Assume $\mathsf{HA} + {\rm P} \vdash \varphi$.
Then there exists finite instances $\psi_1, \dots, \psi_k$ of ${\rm P}$ such that
$\mathsf{HA} + \psi_1 + \dots + \psi_k \vdash \varphi$.
Since $\mathsf{HA}$ satisfies the deduction theorem, we have that $\mathsf{HA}$ proves $\psi_1 \land \dots \land \psi_k \to \varphi$, and hence, $\NN{\left(\psi_1 \land \dots \land \psi_k \to \varphi\right)}$, which is equivalent to $\NN{\psi_1} \land \dots \land \NN{\psi_k} \to \NN{\varphi}$.
Then we have $\mathsf{HA} + {\rm \NN{P}} \vdash \NN{\varphi}$.
\end{proof}

\begin{corollary}
\label{cor: HA+P |- vp_1 <-> vp_2 => HA+NNP |- NNvp_1 <-> NNvp_2}
For any logical principle ${\rm P}$ in Definition \ref{def: LP} and any formulas $\varphi_1$ and $\varphi_2$ (possibly containing free variables), if $\mathsf{HA} + {\rm P} \vdash \varphi_1 \leftrightarrow \varphi_2$, then $\mathsf{HA} + {\rm \NN{P}} \vdash \NN{\varphi_1} \leftrightarrow \NN{\varphi_2}$.
\end{corollary}
\begin{proof}
Immediate from Lemma \ref{lem: HA+P |- vp => HA+NNP |- NNvp} and the fact that $\NN{\left(\varphi_1 \leftrightarrow \varphi_2\right)}$ is intuitionistically equivalent to $\NN{\varphi_1} \leftrightarrow \NN{\varphi_2}$.
\end{proof}

\begin{lemma}
\label{lem: basic facts on arithmetical hierarchy} 
Let $k$ be a natural number.
Let $\varphi_1$ and $\varphi_2$ be formulas in $\Sigma_k$, and let $\varphi_3$ and $\varphi_4$ be formulas in $\Pi_k$.
Then the following hold:
\begin{enumerate}
    \item
        \label{item: Sigma land}
     There exists a formula $\varphi \in \Sigma_k$ such that $\FV{\varphi}= \FV{\varphi_1}\cup \FV{\varphi_2} $ and $\mathsf{HA} \vdash \varphi \leftrightarrow  \varphi_1 \land \varphi_2$;
    \item
    \label{item: Pi land}
     There exists a formula $\varphi' \in \Pi_k$ such that $\FV{\varphi'}= \FV{\varphi_3}\cup \FV{\varphi_4} $ and $\mathsf{HA} \vdash \varphi' \leftrightarrow  \varphi_3 \land \varphi_4$.

\end{enumerate}
\end{lemma}
\begin{proof}
Straightforward by simultaneous induction on $k$.
\end{proof}

\begin{lemma}
\label{lem: exists AvB}
For any formulas $\varphi_1$ and $\varphi_2$ in $\Sigma_k$,

 there exists a formula $\varphi \in \Sigma_k $ such that $\FV{\varphi}= \FV{\varphi_1}\cup \FV{\varphi_2} $ and $\mathsf{HA} \vdash \varphi \leftrightarrow  \varphi_1 \lor \varphi_2$.
\end{lemma}
\begin{proof}
Note that $\varphi_1 \lor \varphi_2$ is equivalent to
\begin{equation*}\label{eq: vp3 or vp4 without v}
\exists k \left(\left(k=0 \to \varphi_1 \right) \land \left( k\neq 0 \to \varphi_2 \right) \right)
\end{equation*}
over $\mathsf{HA}$ (see \cite[1.3.7]{Tro73}).
Since $\QF{\varphi} \to \exists x \psi(x)$ and  $\QF{\varphi} \to \forall x \psi(x)$ are equivalent to $\exists x\left(\QF{\varphi} \to  \psi(x)\right)$ and  $\forall x \left( \QF{\varphi} \to \psi(x) \right)$ respectively over $\mathsf{HA}$ when $x \notin \FV{\QF{\varphi}}$, our assertion follows from Lemma \ref{lem: basic facts on arithmetical hierarchy} straightforwardly.
\end{proof}

\begin{lemma}
\label{lem: basic facts on our classes} 
Let $k$ be a natural number greater than $0$.
\begin{enumerate}
    \item
    \label{item: EU and}
    If $\varphi_1 \land \varphi_2$ is in $\mathrm{U}_k^+$ (resp. $\mathrm{E}_k^+$) if and only if both of $\varphi_1 $ and $\varphi_2$ are in  $\mathrm{U}_k^+$ (resp. $\mathrm{E}_k^+$).
    \item
        \label{item: EU or}
    $\varphi_1 \lor \varphi_2$ is in $\mathrm{U}_k^+$ (resp. $\mathrm{E}_k^+$) if and only if both of $\varphi_1 $ and $\varphi_2$ are in  $\mathrm{U}_k^+$ (resp. $\mathrm{E}_k^+$).
    \item
            \label{item: EU to}
 $\varphi_1 \to \varphi_2$ is in $\mathrm{U}_k^+$ (resp. $\mathrm{E}_k^+$) if and only if $\varphi_1 $ is in $\mathrm{E}_k^+$ (resp. $\mathrm{U}_k^+$) and $\varphi_2$ is in  $\mathrm{U}_k^+$ (resp. $\mathrm{E}_k^+$).
 
 \item
         \label{item: U forall}
 $\forall x \varphi_1$ is in $\mathrm{U}_k^+$ if and only if $\varphi_1$ is in $\mathrm{U}_k^+$.
 \item
          \label{item: E exists}
 $\exists x \varphi_1$ is in $\mathrm{E}_k^+$ if and only if  $\varphi_1$ is in $\mathrm{E}_k^+$.
  \item
         \label{item: E forall}
$\forall x \varphi_1$ is in $\mathrm{E}_{k+1}^+$ if and only if it is  in $\mathrm{U}_k^+$.
   \item
            \label{item: U exists}
$\exists x \varphi_1$ is in $\mathrm{U}_{k+1}^+$ if and only if it is in $\mathrm{E}_k^+$.
   \begin{comment}
   \item
   \label{item: F forall}
   $\forall x \varphi_1$ is in $\mathrm{F}_{k}^+$ if and only if it is in $\mathrm{U}_k^+$.
\item
   \label{item: F exists}
   $\exists x \varphi_1$ is in $\mathrm{F}_{k}^+$ if and only if it is in $\mathrm{E}_k^+$.
\end{comment}
\end{enumerate}
\end{lemma}
\begin{proof}
\eqref{item: EU and}:
Assume $\varphi_1 \land \varphi_2 \in \mathrm{U}_k^+$.
Then $l(s) \leq k$ for all $s \in \alt{ \varphi_1 \land \varphi_2} = \alt{ \varphi_1} \cup \alt{ \varphi_2}$.
\begin{itemize}
\item
If $l(s) < k$ for all $s \in \alt{ \varphi_1}$, then $\varphi_1$ is in $\begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i  \subseteq \mathrm{U}_k^+
\end{displaystyle}
$.
\item
Otherwise, there is $s_0 \in \alt{ \varphi_1}$ such that $l(s_0)=k$.
Then, since $\varphi_1 \land \varphi_2 \notin \begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i 
\end{displaystyle}
$, we have $\varphi_1 \land \varphi_2 \in \mathrm{U}_k$.
Then, for each $s \in \alt{\varphi_1}$ such that $l(s)=k$, we have $i(s)\equiv - $ since $s \in \alt{\varphi_1 \land \varphi_2 }$.
Thus $\varphi_1 \in \mathrm{U}_k \subseteq \mathrm{U}_k^+$.
\end{itemize}
We also have $\varphi_2 \in \mathrm{U}_k^+$ in the same manner.

For the converse direction, assume that $\varphi_1 $ and $\varphi_2$ are in $\mathrm{U}_k^+$.
Then, for all $s\in \alt {\varphi_1 \land \varphi_2}$, since $s\in \alt{\varphi_1}$ or $s\in \alt{\varphi_2}$, we have $l(s)\leq k$, in particular, $i(s) \equiv -$ if $l(s)=k$.
Thus $\varphi_1 \land \varphi_2 $ is in $\mathrm{U}_k^+$.



As for the case of $\mathrm{E}_k^+$, an analogous proof works.

\noindent
\eqref{item: EU or}:
Analogous to \eqref{item: EU and}.

\noindent
\eqref{item: EU to}:
Assume $\varphi_1 \to \varphi_2 \in \mathrm{U}_k^+$.
Let $s$ be in $\alt{\varphi_1 }$.
By the definition of $\alt{\varphi_1 \to \varphi_2}$, we have $s^{\perp} \in \alt{\varphi_1 \to \varphi_2}$ and $l(s) \leq k$.
\begin{itemize}
\item
If $l(s) < k$ for all $s \in \alt{ \varphi_1}$, then $\varphi_1$ is in $\begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i  \subseteq \mathrm{E}_k^+
\end{displaystyle}
$.
\item
Otherwise,  there is $s_0 \in \alt{ \varphi_1}$ such that $l(s_0)=k$.
Since ${s_0}^{\perp} \in \alt{\varphi_1 \to \varphi_2}$, we have $\varphi_1 \to \varphi_2 \in \mathrm{U}_k$.
Then, for each $s \in \alt{\varphi_1}$ such that $l(s)=k$, we have $i(s^{\perp})\equiv -$, and hence, $i(s)\equiv +$.
Thus $\varphi_1 \in \mathrm{E}_k \subseteq \mathrm{E}_k^+$.
\end{itemize}
We also have $\varphi_2 \in \mathrm{U}_k^+$ in the same manner.

For the converse direction, assume $\varphi_1 \in \mathrm{E}_k^+$ and $\varphi_2 \in \mathrm{U}_k^+$.
Since $\degree{\varphi_1}\leq k$ and $\degree{\varphi_2}\leq k$, we have $\degree{\varphi_1 \to \varphi_2}\leq k$.
\begin{itemize}
\item
If $\degree{\varphi_1 \to \varphi_2}<k$, then $\varphi_1 \to \varphi_2\in 
\begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i  \subseteq \mathrm{U}_k^+
\end{displaystyle}
$.
\item
If $\degree{\varphi_1 \to \varphi_2}=k$, for all $s\in \alt{\varphi_1 \to \varphi_2}$ such that $l(s)=k$, we have $s\in \alt{\varphi_2}$ or $s\equiv {s_0}^{\perp}$ for some $s_0\in \alt{\varphi_1}$.
In the former case, we have $i(s) \equiv -$ by $\varphi_2 \in \mathrm{U}_k^+$.
In the latter case, we have  $i(s_0) \equiv +$ by $\varphi_1 \in \mathrm{E}_k^+$, and hence, $i(s)\equiv -$.

\end{itemize}

One can also show that $\varphi_1 \to \varphi_2$ is in $\mathrm{E}_k^+$ if and only if $\varphi_1 $ is in $\mathrm{U}_k^+$ and $\varphi_2$ is in $\mathrm{E}_k^+$
analogously.

\noindent
\eqref{item: U forall}:
Assume $\forall x \varphi_1 \in \mathrm{U}_k^+$.
\begin{itemize}
\item
If $\forall x \varphi_1 \notin \mathrm{U}_k$, then $\forall x \varphi_1 \in \begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i 
\end{displaystyle}$.
Since $\degree{\varphi_1}\leq \degree{\forall x \varphi_1} <k$, we have $\varphi_1 \in \begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i \subseteq \mathrm{U}_k^+
\end{displaystyle}$.
\item
Otherwise, $\degree{\varphi_1}\leq \degree{\forall x \varphi_1} =k$.
If $\degree{\varphi_1}< k$, then we have $\varphi_1 \in \begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i \subseteq \mathrm{U}_k^+
\end{displaystyle}$.
Assume $\degree{\varphi_1}= k$.
Let  $s$ be an alternation path of $\varphi_1$ such that $l(s)=k$.
If $i(s) \not \equiv -$, by the definition of $\alt{\forall x \varphi_1}$, we have $-s\in \alt{\forall x \varphi_1}$, which contradicts $\degree{\forall x \varphi_1} =k$ since $l(-s)=k+1$.
Then we have $i(s)\equiv -$.
Thus we have $\varphi_1 \in \mathrm{U}_k \subseteq \mathrm{U}_k^+$.
\end{itemize}
For the converse direction, assume  $\varphi_1  \in \mathrm{U}_k^+$.
\begin{itemize}
    \item 
If $\varphi_1 \notin \mathrm{U}_k$, then $\varphi_1 \in \begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i 
\end{displaystyle}$.
Thus $\degree{\varphi_1}<k$, and hence, $\degree{\forall x \varphi_1}\leq k$.
If $\degree{\forall x \varphi_1}< k$, then $\forall x \varphi_1  \in \begin{displaystyle}
\bigcup_{i<k} \mathrm{F}_i 
\end{displaystyle} \subseteq \mathrm{U}_k^+$.
If $\degree{\forall x \varphi_1}= k$, since $i(s)\equiv -$ for all $s\in \alt{\forall x \varphi_1}$, we have $\forall x \varphi_1  \in \mathrm{U}_k  \subseteq \mathrm{U}_k^+$.
\item
Otherwise, $\degree{\varphi_1}=k$ and $i(s)\equiv -$ for all $s \in \alt{\varphi_1}$ such that $l(s) =k$.
By the definition of $\alt{\forall x\varphi_1}$, for all $s \in  \alt{ \forall x \varphi_1}$, we have $l(s)\leq k$, and hence, $\degree{\forall x\varphi_1}= k$.
In addition, again by the definition of $\alt{\forall x\varphi_1}$, we have $i(s)=-$ for all $s\in \alt{\forall x \varphi_1}$ such that $l(s) =k$.
Thus $\forall x \varphi_1  \in \mathrm{U}_k  \subseteq \mathrm{U}_k^+$.
\end{itemize}


\noindent
\eqref{item: E exists}:
Analogous to \eqref{item: U forall}.

\noindent
\eqref{item: E forall}:
Assume $\forall x \varphi_1 \in \mathrm{E}_{k+1}^+$.
Since $i(s)\equiv -$ for all $s\in \alt{\forall x \varphi_1}$, $\forall x \varphi_1$ is not in $\mathrm{E}_{k+1}$.
Then $\forall x \varphi_1 \in \begin{displaystyle}
\bigcup_{i\leq k} \mathrm{F}_i 
\end{displaystyle}$, and hence, $\degree{\forall x \varphi_1} \leq k$.
\begin{itemize}
\item
If $\degree{\forall x \varphi_1} < k$, then $\forall x \varphi_1 \in \begin{displaystyle}
\bigcup_{i< k} \mathrm{F}_i  \subseteq \mathrm{U}_k^+
\end{displaystyle}
$.
\item
If $\degree{\forall x \varphi_1} = k$, since $i(s) \equiv -$ for all $s\in \alt{\forall x \varphi_1}$, we have $\forall x \varphi_1 \in \mathrm{U}_k\subseteq \mathrm{U}_k^+$.
\end{itemize}

The converse direction is trivial since $ \mathrm{U}_k^+ \subseteq
 \begin{displaystyle}
\bigcup_{i< k+1} \mathrm{F}_i  \subseteq \mathrm{E}_{k+1}^+
\end{displaystyle}
$.

\noindent
\eqref{item: U exists}:
Analogous to \eqref{item: E forall}.
\begin{comment}
\noindent
\eqref{item: F forall}:
Since $\mathrm{U}_k^+\subseteq \mathrm{F}_k^+$, it suffices to show the ``only if'' direction.
Assume $\forall x \varphi_1 \in \mathrm{F}_{k}^+$.
\begin{itemize}
    \item 
If $\degree{\forall x \varphi_1}< k$, we have $\forall x \varphi_1 \in \mathrm{F}_{k-1}^+ \subseteq  \mathrm{U}_{k}^+$.
\item
If $\degree{\forall x \varphi_1}=k$, since $i(s) \equiv -$ for all $s\in \alt{\forall x \varphi_1}$, we have $\forall x \varphi_1 \in \mathrm{U}_k\subseteq \mathrm{U}_k^+$.
\end{itemize}

\noindent
\eqref{item: F exists}:
Analogous to \eqref{item: F forall}.
\end{comment}
\end{proof}



\begin{lemma}
\label{lem: HA+NNS_{k-1}-DNE |- NN(Pk v Pk) <-> NNPk}
Let $k$ be a natural number.
For all $\varphi_1$ and $\varphi_2$ in $\Pi_k$, there exists $\varphi \in \Pi_k$ such that $\FV{\varphi} = \FV{\varphi_1} \cup \FV{\varphi_2}$ and
$\mathsf{HA} + \NN{\DNE{\Sigma_{k-1}}} \, (\mathsf{HA}$ if $k=0)$ proves
$\neg \neg (\varphi_1 \lor \varphi_2) \leftrightarrow \neg \neg \varphi $.
\end{lemma}
\begin{proof}
Without loss of generality, assume $k>0$, $\varphi_1 :\equiv \forall x \rho_1(x)$ and $\varphi_2 :\equiv \forall y \rho_2(y)$ where $\rho_1(x), \rho_2(y) \in \Sigma_{k-1}$ (see Remark \ref{rem: sigma_k and pi_k}).
By Lemma \ref{lem: exists AvB}, it suffices to show
\begin{equation*}
\mathsf{HA} +     \NN{\DNE{\Sigma_{k-1}}} \vdash \neg \neg \left( \forall x \rho_1(x) \lor \forall y \rho_2(y)\right) \leftrightarrow \neg \neg \forall x,y \left( \rho_1(x) \lor \rho_2 (y) \right).
\end{equation*}
The implication from the left to the right is straightforward.
The converse implication is shown as follows: 
$$
\begin{array}{cl}
& \neg \neg \forall x,y \left( \rho_1(x) \lor \rho_2 (y) \right)
 \\
\underset{ \NN{\DNE{\Sigma_{k-1}}}}{\longleftrightarrow}&\neg \neg \forall x,y \left( \neg \neg \rho_1(x) \lor \neg \neg \rho_2 (y) \right)
 \\
\longrightarrow & \forall x,y \neg \neg  \left( \neg \neg \rho_1(x) \lor \neg \neg \rho_2 (y) \right)
 \\
\longleftrightarrow &
\neg \exists x,y \neg \left( \neg \neg \rho_1(x) \lor \neg \neg \rho_2 (y) \right)
 \\
\longleftrightarrow &  \neg \exists x,y \left( \neg \rho_1(x) \land \neg \rho_2 (y) \right)
 \\
 \longleftrightarrow &  \neg  \left(\neg \neg \exists x \neg \rho_1(x) \land \neg \neg \exists y \neg \rho_2 (y) \right)
 \\
  \longleftrightarrow &  \neg  \left(\neg \forall  x \neg \neg \rho_1(x) \land \neg \forall y \neg  \neg \rho_2 (y) \right)
 \\
 \longleftrightarrow&  \neg \neg  \left(\forall  x \neg \neg \rho_1(x) \lor \forall y \neg  \neg \rho_2 (y) \right)\\
 \underset{ \NN{\DNE{\Sigma_{k-1}}}}{\longleftrightarrow}&
  \neg \neg  \left(\forall  x  \rho_1(x) \lor \forall y \rho_2 (y) \right).
\end{array}
$$
\end{proof}

\begin{lemma}
\label{lem: NP and NS}
Let $k$ be a natural number.
\begin{enumerate}
    \item 
    \label{item: NP}
    For all $\varphi \in \Pi_k$, there exists $\psi \in \Sigma_k$ such that
$\FV{\varphi} = \FV{\psi}$ and
$\mathsf{HA} + \DNE{\Sigma_k} $ proves $ \neg \varphi \leftrightarrow \psi$.
\item
\label{item: NS}
For all $\varphi \in \Sigma_k$, there exists $\psi \in \Pi_k$ such that
$\FV{\varphi} = \FV{\psi}$ and
$\mathsf{HA} + \DNE{\Sigma_{k-1}} \, (\mathsf{HA}$ if $k=0) $ proves $\neg \varphi \leftrightarrow \psi$.
\end{enumerate}
\begin{proof}
By simultaneous induction on $k$.
The base case is trivial.
In what follows, we show the induction step for $k+1$.

Let $\varphi :\equiv \forall x \rho(x)$ where $\rho(x) \in \Sigma_{k}$.
By induction hypothesis, there exists $\rho'(x) \in \Pi_{k}$ such that
$\FV{\rho(x)} =\FV{\rho'(x)}$ and
$$
\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash \neg \rho(x)  \leftrightarrow \rho'(x) .
$$
Then $\mathsf{HA} + \DNE{\Sigma_{k+1}}$ proves
$$
\begin{array}{cl}
     & \neg \forall x \rho(x) \\
\underset{\DNE{\Sigma_{k}}}{\longleftrightarrow}     &  \neg \forall x \neg \neg \rho(x)\\
\longleftrightarrow &  \neg \neg \exists x \neg \rho(x)\\
\underset{\text{[I.H.] } \DNE{\Sigma_{k-1}}}{\longleftrightarrow}&  \neg \neg \exists x \rho'(x)\\
\underset{\DNE{\Sigma_{k+1}}}{\longleftrightarrow}     &  \exists x \rho'(x),\\
\end{array}
$$
which is in $\Sigma_{k+1}$.

Next, let $\varphi :\equiv \exists x \rho(x)$ where $\rho(x) \in \Pi_{k}$.
By induction hypothesis, there exists $\rho'(x) \in \Sigma_{k}$ such that
$\FV{\rho(x)} =\FV{\rho'(x)}$ and
$$
\mathsf{HA} + \DNE{\Sigma_{k}} \vdash \neg \rho(x)  \leftrightarrow \rho'(x) .
$$
Then $\mathsf{HA} + \DNE{\Sigma_{k}}$ proves
$$
\neg \exists x \rho(x) \leftrightarrow \forall x \neg  \rho(x)
\underset{\text{[I.H.] } \DNE{\Sigma_{k}}}{\longleftrightarrow}
\forall x  \rho'(x),
$$
which is in $\Pi_{k+1}$.
\end{proof}


\end{lemma}

\begin{lemma}
\label{lem: NPk <-> NNSk}
Let $k$ be a natural number.
For all $\varphi \in \Pi_k$, there exists $\psi \in \Sigma_k$ such that
$\FV{\varphi} = \FV{\psi}$ and
$\mathsf{HA} + \NN{\DNE{\Sigma_k}} \vdash  \neg \varphi \leftrightarrow \neg \neg \psi$.
\end{lemma}
\begin{proof}
Let $\varphi \in \Pi_k$.
By Lemma \ref{lem: NP and NS}.\eqref{item: NP},
there exists $\psi \in \Sigma_k$ such that
$\FV{\varphi} = \FV{\psi}$ and
$\mathsf{HA} + \DNE{\Sigma_k} \vdash \neg \varphi \leftrightarrow  \psi$.
By Corollary \ref{cor: HA+P |- vp_1 <-> vp_2 => HA+NNP |- NNvp_1 <-> NNvp_2}, we have
$\mathsf{HA} + \NN{\DNE{\Sigma_k}} \vdash \neg \varphi \leftrightarrow \neg \neg \psi$.
\end{proof}


\begin{lemma}
 \label{lem: Ukp-DNS -> NNSk-1-LEM}
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} \vdash \NN{\LEM{\Sigma_{k-1}}}$ for each natural number $k>0$.
\end{lemma}
\begin{proof}
Fix an instance of $\NN{\LEM{\Sigma_{k-1}}}$
$$
\varphi :\equiv \neg \neg \forall x \left( \varphi_1(x) \lor \neg \varphi_1(x) \right),
$$
where $\varphi_1(x) \in \Sigma_{k-1}$.
Note $\left( \varphi_1(x) \lor \neg \varphi_1(x) \right) \in \mathrm{F}_{k-1} \subseteq \mathrm{U}_k^+$. 
Since $\mathsf{HA} $ proves $\forall x \neg \neg \left( \varphi_1(x) \lor \neg \varphi_1(x) \right)$,
we have that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$ \neg \neg \forall x \left( \varphi_1(x) \lor \neg \varphi_1(x) \right)$, namely, $\varphi$. 
\end{proof}

\begin{corollary}
\label{cor: Ukp-DNS -> NNSk-1-DNE}
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} \vdash \NN{\DNE{\Sigma_{k-1}}}$  for each natural number $k>0$.
\end{corollary}
\begin{proof}
Immediate from Remark \ref{rem: NNDNS <-> DNS}, Lemma \ref{lem: Ukp-DNS -> NNSk-1-LEM} and the fact that $\LEM{\Sigma_{k-1}}$ implies $\DNE{\Sigma_{k-1}}$.
\end{proof}

\begin{remark}
\label{rem: UkpDNS <-> UkDNS}
By Remark \ref{rem: Ekp and Ukp}, $\DNS{\mathrm{U}_k^+}$ is equivalent to $\DNS{\mathrm{U}_k}$ over $\mathsf{HA}$.
Then $\DNS{\mathrm{U}_k^+}$ can be replaced by $\DNS{\mathrm{U}_k}$ throughout the paper.
\end{remark}


\section{Prenex normal form theorems}\label{sec: PNFT}
In this section, we show the modified version of \cite[Theorem 2.7]{ABHK04}.
Prior to that, we first show a variant of the prenex normal form theorem:
\begin{lemma}
\label{PNFT_of_NE_k_and_NNU_k}
For each natural number $k$ and a formula $\varphi$ (possibly containing free variables),
if $\varphi \in \mathrm{U}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} + \DNS{\mathrm{U}_k^+}  \vdash \neg \neg \varphi \leftrightarrow \neg \neg \varphi'.$$
    
\end{lemma}
\begin{proof}
By simultaneous induction on $k$, we show the following two statements (which are in fact equivalent):
\begin{enumerate}
    \item 
    \label{eq: item for NE_k in PNFT}
    if $\varphi \in \mathrm{E}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} + \DNS{\mathrm{U}_k^+}  \vdash \neg \varphi \leftrightarrow \neg \neg \varphi'; 
    $$
        \item 
        \label{eq: item for NNU_k in PNFT}
    if $\varphi \in \mathrm{U}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} + \DNS{\mathrm{U}_k^+}  \vdash \neg \neg \varphi \leftrightarrow \neg \neg \varphi'.$$

\end{enumerate}
The base case is trivial (one can take $\varphi'$ as $\varphi$ itself).
In what follows, we show the induction step.


For the induction step, assume the items \ref{eq: item for NE_k in PNFT} and \ref{eq: item for NNU_k in PNFT} for $k-1$.
We show the items \ref{eq: item for NE_k in PNFT} and \ref{eq: item for NNU_k in PNFT} for $k$
simultaneously by induction on the structure of formulas.
When $\varphi$ is a  prime  formula, by Lemma \ref{lem: sigma_k and pi_k}, we have $\varphi'$ which satisfies the requirement.
For the induction step, assume that the items \ref{eq: item for NE_k in PNFT} and \ref{eq: item for NNU_k in PNFT} hold for $\varphi_1$ and $\varphi_2$.
When it is clear from the context, we suppress the argument on free variables.

The case of $\varphi_1 \land \varphi_2$:
First, assume $\varphi_1 \land \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{E}_k^+$.
By induction hypothesis, there exist $\varphi_1' ,\varphi_2' \in \Pi_k$ such that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} \vdash (\neg \varphi_1 \leftrightarrow \neg \neg \varphi_1' ) \land ( \neg \varphi_2 \leftrightarrow \neg \neg \varphi_2')$.
By Lemma \ref{lem: HA+NNS_{k-1}-DNE |- NN(Pk v Pk) <-> NNPk}, there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi'} = \FV{\varphi_1'} \cup \FV{\varphi_2'}$ and
$$\mathsf{HA} +\NN{\DNE{\Sigma_{k-1}}} \vdash \neg \neg (\varphi_1' \lor \varphi_2') \leftrightarrow \neg \neg \varphi'.$$
By Corollary \ref{cor: Ukp-DNS -> NNSk-1-DNE}, $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
\begin{array}{cl}
& \neg (\varphi_1 \land \varphi_2) \\
\longleftrightarrow & \neg  (\neg \neg \varphi_1 \land \neg \neg \varphi_2) \\
\underset{\text{[I.H.] } \DNS{\mathrm{U}_k^+}}{\longleftrightarrow} &  \neg  (\neg \varphi_1' \land  \neg \varphi_2') \\
\longleftrightarrow & \neg \neg (\varphi_1' \lor  \neg \varphi_2') \\
\underset{\NN{\DNE{\Sigma_{k-1}}}}{\longleftrightarrow} & \neg \neg \varphi'.
\end{array}
$$


Next, assume $\varphi_1 \land \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{U}_k^+$.
By induction hypothesis, there exist $\varphi_1' ,\varphi_2' \in \Pi_k$ such that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} \vdash (\neg \neg \varphi_1 \leftrightarrow \neg \neg \varphi_1' ) \land ( \neg \neg \varphi_2 \leftrightarrow \neg \neg \varphi_2')$.
By Lemma \ref{lem: basic facts on arithmetical hierarchy}, there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi'} = \FV{\varphi_1'} \cup \FV{\varphi_2'}$ and $\mathsf{HA} \vdash \varphi' \leftrightarrow \varphi_1' \land \varphi_2'$.
Then $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
\neg \neg (\varphi_1 \land \varphi_2) \leftrightarrow \neg \neg \varphi_1 \land \neg \neg \varphi_2 \underset{\text{[I.H.] }\DNS{\mathrm{U}_k^+} }{\longleftrightarrow}  \neg \neg \varphi_1' \land \neg \neg \varphi_2' \leftrightarrow \neg \neg (\varphi_1' \land \varphi_2') \leftrightarrow \neg \neg \varphi'.
$$

The case of $\varphi_1 \lor \varphi_2$:
First, assume $\varphi_1 \lor \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{E}_k^+$.
By induction hypothesis, there exist $\varphi_1' ,\varphi_2' \in \Pi_k$ such that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} \vdash (\neg \varphi_1 \leftrightarrow \neg \neg \varphi_1' ) \land ( \neg \varphi_2 \leftrightarrow \neg \neg \varphi_2')$.
By Lemma \ref{lem: basic facts on arithmetical hierarchy}, there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi'} = \FV{\varphi_1'} \cup \FV{\varphi_2'}$ and $\mathsf{HA} \vdash \varphi' \leftrightarrow \varphi_1' \land \varphi_2'$.
Then $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
\begin{array}{cl}
& \neg (\varphi_1 \lor \varphi_2)\\
\longleftrightarrow & \neg \varphi_1 \land \neg \varphi_2\\
\underset{\text{[I.H.] }\DNS{\mathrm{U}_k^+} }{\longleftrightarrow} & \neg \neg \varphi_1' \land  \neg \neg \varphi_2'\\
\longleftrightarrow & \neg \neg (\varphi_1' \land \varphi_2')\\
\longleftrightarrow & \neg \neg \varphi'.
\end{array}
$$

Next,  assume $\varphi_1 \lor \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{U}_k^+$.
By induction hypothesis, there exist $\varphi_1' ,\varphi_2' \in \Pi_k$ such that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} \vdash (\neg \neg \varphi_1 \leftrightarrow \neg \neg \varphi_1' ) \land ( \neg \neg \varphi_2 \leftrightarrow \neg \neg \varphi_2')$.
By Lemma \ref{lem: HA+NNS_{k-1}-DNE |- NN(Pk v Pk) <-> NNPk}, there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi'} = \FV{\varphi_1'} \cup \FV{\varphi_2'}$ and
$$\mathsf{HA} +\NN{\DNE{\Sigma_{k-1}}} \vdash \neg \neg (\varphi_1' \lor \varphi_2') \leftrightarrow \neg \neg \varphi'.$$
By Corollary \ref{cor: Ukp-DNS -> NNSk-1-DNE}, $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
\begin{array}{cl}
& \neg \neg (\varphi_1 \lor \varphi_2)\\
\longleftrightarrow& \neg \neg ( \neg \neg \varphi_1 \lor \neg \neg \varphi_2)\\
\underset{\text{[I.H.] }\DNS{\mathrm{U}_k^+} }{\longleftrightarrow} & \neg \neg ( \neg \neg \varphi_1' \lor \neg \neg \varphi_2')\\
\longleftrightarrow &\neg \neg ( \varphi_1' \lor \varphi_2')\\
\underset{\NN{\DNE{\Sigma_{k-1}}}}{\longleftrightarrow}& \neg \neg \varphi'. 
\end{array}
$$

The case of $\varphi_1 \to \varphi_2$:
First, assume $\varphi_1 \to \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{U}_k^+ $ and $\varphi_2 \in \mathrm{E}_k^+$.
By induction hypothesis, there exist $\varphi_1' ,\varphi_2' \in \Pi_k$ such that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} $ proves  $\neg \neg \varphi_1 \leftrightarrow \neg \neg \varphi_1' $ and $ \neg \varphi_2 \leftrightarrow \neg \neg \varphi_2'$.
By Lemma \ref{lem: basic facts on arithmetical hierarchy}, there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi'} = \FV{\varphi_1'} \cup \FV{\varphi_2'}$ and $\mathsf{HA} \vdash \varphi' \leftrightarrow \varphi_1' \land \varphi_2'$.
Then $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
\begin{array}{cl}
& \neg (\varphi_1 \to \varphi_2)\\
\longleftrightarrow & \neg \neg \varphi_1 \land \neg \varphi_2\\
\underset{\text{[I.H.] }\DNS{\mathrm{U}_k^+} }{\longleftrightarrow} & \neg \neg \varphi_1' \land \neg \neg \varphi_2'\\
\longleftrightarrow & \neg \neg (\varphi_1' \land \varphi_2')\\
\longleftrightarrow & \neg \neg \varphi'.
\end{array}
$$

Next, assume $\varphi_1 \to \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{E}_k^+ $ and $\varphi_2 \in \mathrm{U}_k^+$.
By induction hypothesis, there exist $\varphi_1' ,\varphi_2' \in \Pi_k$ such that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves $\neg \varphi_1 \leftrightarrow \neg \neg \varphi_1'  $ and $ \neg \neg \varphi_2 \leftrightarrow \neg \neg \varphi_2'$.
By Lemma \ref{lem: HA+NNS_{k-1}-DNE |- NN(Pk v Pk) <-> NNPk}, there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi'} = \FV{\varphi_1'} \cup \FV{\varphi_2'}$ and
$$\mathsf{HA} +\NN{\DNE{\Sigma_{k-1}}} \vdash \neg \neg (\varphi_1' \lor \varphi_2') \leftrightarrow \neg \neg \varphi'.$$
By Corollary \ref{cor: Ukp-DNS -> NNSk-1-DNE}, $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
\begin{array}{cl}
& \neg \neg (\varphi_1 \to \varphi_2)\\
\longleftrightarrow & \neg (\neg \neg \varphi_1 \land \neg \varphi_2)\\
\underset{\text{[I.H.] }\DNS{\mathrm{U}_k^+} }{\longleftrightarrow} & \neg( \neg \varphi_1' \land \neg \varphi_2')\\
\longleftrightarrow & \neg \neg (\varphi_1' \lor \varphi_2')\\
\underset{\NN{\DNE{\Sigma_{k-1}}} }{\longleftrightarrow} &  \neg \neg \varphi'.
\end{array}
$$

The case of $\forall x \varphi_1(x)$:
First, assume $\forall x \varphi_1(x) \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\forall x \varphi_1(x) \in \mathrm{U}_{k-1}^+$.
By the item \ref{eq: item for NNU_k in PNFT} for $k-1$, there exists $\varphi' \in \Pi_{k-1}$ such that
$$
\mathsf{HA} + \DNS{\mathrm{U}_{k-1}^+} \vdash \neg \neg \forall x \varphi_1(x)  \leftrightarrow \neg \neg \varphi'.
$$
By Lemma \ref{lem: NPk <-> NNSk}, there exists $\varphi''\in \Sigma_{k-1} \subseteq \Pi_k$ (see Remark \ref{rem: identification on Sigma_k and Pi_k}) such that $\FV{\varphi'}= \FV{\varphi''}$ and
$$
\mathsf{HA} +\NN{\DNE{\Sigma_{k-1}}} \vdash \neg  \varphi' \leftrightarrow \neg \neg \varphi''.
$$
By Corollary \ref{cor: Ukp-DNS -> NNSk-1-DNE}, $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
\neg \forall x \varphi_1(x)  \underset{\text{[I.H.] }\DNS{\mathrm{U}_{k-1}^+} }{\longleftrightarrow}  \neg  \varphi' \underset{\NN{\DNE{\Sigma_{k-1}}} }{\longleftrightarrow} \neg \neg \varphi'' .
$$

Next, assume $\forall x \varphi_1(x) \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1(x) \in \mathrm{U}_{k}^+$.
By induction hypothesis, there exists $\varphi_1'(x) \in \Pi_{k}$ such that
$$
\mathsf{HA} + \DNS{\mathrm{U}_{k}^+} \vdash \neg \neg  \varphi_1(x)  \leftrightarrow \neg \neg \varphi_1' (x).
$$
Then $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
 \neg \neg \forall x \varphi_1(x)  
 \underset{\DNS{\mathrm{U}_{k}^+}}{\longleftrightarrow}  \forall x \neg \neg  \varphi_1(x)   
\underset{\text{[I.H.] }\DNS{\mathrm{U}_{k}^+} }{\longleftrightarrow} \forall x \neg \neg  \varphi_1'(x)
 \underset{\DNS{\mathrm{U}_{k}^+}}{\longleftrightarrow}   \neg \neg \forall x \varphi_1'(x).   
$$

The case of $\exists x \varphi_1(x)$:
First, assume $\exists x \varphi_1(x) \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1(x) \in \mathrm{E}_{k}^+$.
By induction hypothesis, there exists $\varphi_1'(x) \in \Pi_{k}$ such that
$$
\mathsf{HA} + \DNS{\mathrm{U}_{k}^+} \vdash \neg \varphi_1(x) \leftrightarrow \neg \neg \varphi_1'(x).
$$
Then $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
 \neg \exists x \varphi_1(x) 
 \leftrightarrow  \forall x  \neg \varphi_1(x) 
\underset{\text{[I.H.] }\DNS{\mathrm{U}_{k}^+} }{\longleftrightarrow} \forall x \neg \neg  \varphi_1'(x)
 \underset{\DNS{\mathrm{U}_{k}^+}}{\longleftrightarrow}   \neg \neg \forall x \varphi_1'(x).
 $$
 
 Next, assume  that $\exists x \varphi_1(x) \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\exists x \varphi_1(x) \in \mathrm{E}_{k-1}^+$.
By the item \ref{eq: item for NE_k in PNFT} for $k-1$, there exists $\varphi' \in \Pi_{k-1}$ such that
$$
\mathsf{HA} + \DNS{\mathrm{U}_{k-1}^+} \vdash \neg  \exists x \varphi_1(x)  \leftrightarrow \neg \neg \varphi'.
$$
By Lemma \ref{lem: NPk <-> NNSk}, there exists $\varphi''\in \Sigma_{k-1} \subseteq \Pi_k$ (see Remark \ref{rem: identification on Sigma_k and Pi_k}) such that $\FV{\varphi'}= \FV{\varphi''}$ and
$$
\mathsf{HA} +\NN{\DNE{\Sigma_{k-1}}} \vdash \neg  \varphi' \leftrightarrow \neg \neg \varphi''.
$$
By Corollary \ref{cor: Ukp-DNS -> NNSk-1-DNE}, $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ proves
$$
 \neg \neg  \exists x \varphi_1(x)  \underset{\text{[I.H.] }\DNS{\mathrm{U}_{k-1}^+} }{\longleftrightarrow} \neg  \varphi'\underset{\NN{\DNE{\Sigma_{k-1}}}  }{\longleftrightarrow} \neg \neg \varphi''.
$$
\end{proof}



The following lemma is used a lot of times implicitly in the proof of our prenex normal form theorem (Theorem \ref{thm: PNFT}).
\begin{lemma}[cf. Fact 2.2 in \cite{ABHK04}]
\label{lem: k -> k-1}
Let $k$ be a natural number.
\begin{enumerate}
    \item 
    \label{item: s_k+1-DNE -> (p_k v p_k)-DNE}
    $\mathsf{HA} + \DNE{\Sigma_{k+1}} \vdash \DNE{(\Pi_{k} \lor \Pi_{k})}$.
    \item
        \label{item: (p_k+1 v p_k+1)-DNE -> s_k-DNE}
$\mathsf{HA} +\DNE{(\Pi_{k+1} \lor \Pi_{k+1})} \vdash \DNE{\Sigma_{k}}$.   
  \item
        \label{item: NN(p_k+1 v p_k+1)-DNE -> NNs_k-DNE}
$\mathsf{HA} +\NN{\DNE{(\Pi_{k+1} \lor \Pi_{k+1})}} \vdash \NN{\DNE{\Sigma_{k}}}$.    

\item
\label{item: sk-DNE -> pk+1-DNE}
$
\mathsf{HA} +  \DNE{\Sigma_{k}} \vdash \DNE{\Pi_{k+1}}
$.
\end{enumerate}
\end{lemma}
\begin{proof}
\eqref{item: s_k+1-DNE -> (p_k v p_k)-DNE}:
For formulas $\varphi_1$ and $\varphi_2$ in $\Pi_{k}$, $\varphi_1 \lor \varphi_2$ is equivalent (over $\mathsf{HA}$) to
\begin{equation*}\label{eq: p1 v p1 without v}
\exists k \left(\left(k=0 \to \varphi_1 \right) \land \left( k\neq 0 \to \varphi_2 \right) \right),
\end{equation*}
which is equivalent to some $\varphi \in \Sigma_{k+1}$ such that $\FV{\varphi}= \FV{\varphi_1 \lor \varphi_2}$ over $\mathsf{HA}$ by Lemma \ref{lem: basic facts on arithmetical hierarchy}.\eqref{item: Pi land}.
Therefore any instance of $\DNE{(\Pi_{k} \lor \Pi_{k})}$ is derived from some instance of $\DNE{\Sigma_{k+1}}$.

        \eqref{item: (p_k+1 v p_k+1)-DNE -> s_k-DNE}:
       
        Any instance of $\DNE{\Sigma_{k}}$ is derived from some instance of 
        $\DNE{(\Pi_{k+1} \lor \Pi_{k+1})}$ since $\varphi \in \Sigma_k$ is equivalent to $\forall y \varphi \in \Pi_{k+1}$ with a variable $y$ not occurring freely in $\varphi$ (cf. Lemma \ref{lem: sigma_k and pi_k}). 

\eqref{item: NN(p_k+1 v p_k+1)-DNE -> NNs_k-DNE}:
Immediate from \eqref{item: (p_k+1 v p_k+1)-DNE -> s_k-DNE} and Corollary \ref{cor: HA+P |- vp_1 <-> vp_2 => HA+NNP |- NNvp_1 <-> NNvp_2}.

       
\eqref{item: sk-DNE -> pk+1-DNE}:
Note that $\neg \neg \forall x \varphi (x)$ implies  $\neg \neg \forall x \neg \neg \varphi (x)$, which is intuitionistically equivalent to $\forall x \neg \neg \varphi (x)$.
Then any instance of $\DNE{\Pi_{k+1}}$ is derived from some instance of $\DNE{\Sigma_{k}}$.
\end{proof}

We are now ready to show the modified version of \cite[Theorem 2.7]{ABHK04}.


\begin{theorem}
\label{thm: PNFT}
For each natural number $k$ and a formula $\varphi$ (possibly containing free variables),
the following hold:
\begin{enumerate}
        \item 
        \label{eq: item for Sigma_k in PNFT}
    if $\varphi \in \mathrm{E}_k^+$, then
        there exists $\varphi' \in \Sigma_k$  such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA}  + \DNE{\Sigma_k} +\DNS{\mathrm{U}_k^+} \vdash \varphi \leftrightarrow \varphi';
    $$
     \item 
    \label{eq: item for Pi_k in PNFT}
    if $\varphi \in \mathrm{U}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} + \DNE{(\Pi_k\lor \Pi_k)}  \vdash \varphi \leftrightarrow \varphi' .
    $$
\end{enumerate}
\end{theorem}
\begin{proof}
For the proof, we prepare the following auxiliary assertion (which is in fact a consequence from the item \ref{eq: item for Pi_k in PNFT}):
\begin{enumerate}
\setcounter{enumi}{2}
\item 
    \label{eq: item for NNPi_k in PNFT}
    if $\varphi \in \mathrm{E}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} + \NN{\DNE{(\Pi_k\lor \Pi_k)}}  \vdash \neg \varphi \leftrightarrow \neg \neg \varphi'.
    $$
    \end{enumerate}
We show the items \ref{eq: item for Sigma_k in PNFT}, \ref{eq: item for Pi_k in PNFT} and 
\ref{eq: item for NNPi_k in PNFT} by induction on $k$ simultaneously.
The base case is trivial (one can take $\varphi'$ as $\varphi$ itself).  In what follows, we show the induction step.

Assume the items \ref{eq: item for Sigma_k in PNFT}, \ref{eq: item for Pi_k in PNFT} and \ref{eq: item for NNPi_k in PNFT} for $k-1$.
Since $\mathsf{HA} + \DNE{\Pi_{k-1}} \vdash \DNS{\Pi_{k-1}}$, by the item \ref{eq: item for Pi_k in PNFT} for $k-1$, we have
\begin{equation}
\label{eq: HA + Pk-1Pk-1DNE |- Uk-1pDNS}
\mathsf{HA} + \DNE{\left(\Pi_{k-1}\lor \Pi_{k-1}\right)} \vdash \DNS{\mathrm{U}_{k-1}^+}.
\end{equation}
We show the items \ref{eq: item for Sigma_k in PNFT}, \ref{eq: item for Pi_k in PNFT} and \ref{eq: item for NNPi_k in PNFT} simultaneously by induction on the structure of formulas.
When $\varphi$ is a  prime  formula, by Lemma \ref{lem: sigma_k and pi_k}, we have $\varphi'$ which satisfies the requirement.
For the induction step, assume that the items \ref{eq: item for Sigma_k in PNFT}, \ref{eq: item for Pi_k in PNFT} and \ref{eq: item for NNPi_k in PNFT} hold for $\varphi_1$ and $\varphi_2$.
When it is clear from the context, we suppress the argument on free variables.



The case of $\varphi_1 \land \varphi_2$:
For the second item, assume $\varphi_1 \land \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{U}_k^+$.
By induction hypothesis, there exist $\varphi_1' ,\varphi_2' \in \Pi_k$ such that
$\mathsf{HA} +\DNE{(\Pi_k\lor \Pi_k)} $ proves $\varphi_1 \leftrightarrow \varphi_1'$ and $\varphi_2 \leftrightarrow \varphi_2'$.
By Lemma \ref{lem: basic facts on arithmetical hierarchy}, there exists $\varphi' \in \Pi_k$ such that $\mathsf{HA} \vdash \varphi' \leftrightarrow \varphi_1'\land \varphi_2'$.
Then $\mathsf{HA} +\DNE{(\Pi_k\lor \Pi_k)}$ proves
$$\varphi_1 \land \varphi_2
\underset{\text{[I.H.] }\DNE{(\Pi_k\lor \Pi_k)} }{\longleftrightarrow} \varphi_1' \land \varphi_2' \leftrightarrow \varphi'.$$

For the first and third items, assume $\varphi_1 \land \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{E}_k^+$.
Then we have $\varphi'\in \Sigma_k$ such that $ \mathsf{HA} +\DNE{\Sigma_k} + \DNS{\mathrm{U}_k^+} \vdash \varphi_1 \land \varphi_2 \leftrightarrow \varphi'$ as in the second item.
On the other hand, by induction hypothesis, there exist  $\varphi_1'' ,\varphi_2'' \in \Pi_k$ such that
$\mathsf{HA} + \NN{\DNE{(\Pi_k\lor \Pi_k)}} $ proves  $\neg \varphi_1 \leftrightarrow \neg \neg \varphi_1''  $ and  $ \neg \varphi_2 \leftrightarrow \neg \neg  \varphi_2''$.
In addition, by Lemma \ref{lem: HA+NNS_{k-1}-DNE |- NN(Pk v Pk) <-> NNPk}, there exists $\varphi'' \in \Pi_k$ such that
$\mathsf{HA} + \NN{\DNE{\Sigma_{k-1}}} \vdash \neg \neg \varphi'' \leftrightarrow \neg \neg (\varphi_1'' \lor \varphi_2'')$.
Then, by Lemma \ref{lem: k -> k-1}, we have that $\mathsf{HA} +  \NN{\DNE{(\Pi_k\lor \Pi_k)}}$ proves
$$
\begin{array}{cl}
&\neg (\varphi_1 \land \varphi_2) \\
\longleftrightarrow& \neg (\neg \neg \varphi_1 \land \neg \neg  \varphi_2)\\
\longleftrightarrow& \neg \neg (\neg \varphi_1 \lor \neg \varphi_2)\\
\underset{\text{[I.H.] }\NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}}{\longleftrightarrow} & \neg \neg (\neg \neg \varphi_1'' \lor \neg \neg \varphi_2'' )\\
\longleftrightarrow& \neg (\neg \varphi_1'' \land \neg \varphi_2'')\\
\longleftrightarrow&\neg \neg (\varphi_1'' \lor \varphi_2'')\\
\underset{\NN{\DNE{\Sigma_{k-1}}}}{\longleftrightarrow}&\neg \neg \varphi''.
\end{array}
$$




The case of  $\varphi_1 \lor \varphi_2$:
For the second item, assume $\varphi_1 \lor \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{U}_k^+$.
Then, by induction hypothesis, there exist $\rho_1(x_1), \rho_2(x_2) \in \Sigma_{k-1}$ such that
$\mathsf{HA} + \DNE{(\Pi_k\lor \Pi_k)}  $ proves  $\varphi_1 \leftrightarrow \forall x_1 \rho_1(x_1) $ and  $\varphi_2 \leftrightarrow \forall x_2 \rho_2(x_2) $.
By Lemma \ref{lem: k -> k-1}, $\mathsf{HA} + \DNE{(\Pi_k\lor \Pi_k)}   $ proves
$$
\begin{array}{cl}
& \forall x_1 \rho_1(x_1) \lor \forall x_2 \rho_2(x_2)\\
\longrightarrow& \forall x_1, x_2 \left( \rho_1(x_1) \lor \rho_2(x_2)\right)\\
\longrightarrow& \neg \left( \exists x_1 \neg \rho_1 (x_1) \land  \exists x_2 \neg \rho_2 (x_2) \right) \\
\longleftrightarrow& \neg \left( \neg \neg  \exists x_1 \neg \rho_1 (x_1) \land  \neg \neg  \exists x_2 \neg \rho_2 (x_2) \right) \\
\underset{\DNE{\Sigma_{k-1}}}{\longleftrightarrow} &\neg \left( \neg \forall x_1 \rho_1 (x_1) \land  \neg \forall x_2 \rho_2 (x_2) \right) \\
\longleftrightarrow & \neg \neg \left( \forall x_1 \rho_1 (x_1) \lor  \forall x_2 \rho_2 (x_2) \right) \\
\underset{\DNE{(\Pi_k\lor \Pi_k)}}{\longrightarrow} &\forall x_1 \rho_1 (x_1) \lor  \forall x_2 \rho_2 (x_2).
\end{array}
$$
By Lemma \ref{lem: exists AvB},
there exists  $\xi(x_1, x_2)  \in \Sigma_{k-1}$ such that $\mathsf{HA} \vdash \xi(x_1, x_2) \leftrightarrow \rho_1(x_1) \lor \rho_2(x_2)$.
Then we have that $\mathsf{HA} + \DNE{(\Pi_k\lor \Pi_k)}  $ proves
$$
\begin{array}{cl}
&\varphi_1 \lor \varphi_2\\
\underset{\text{[I.H.] }\DNE{(\Pi_k\lor \Pi_k)}}{\longleftrightarrow}& \forall x_1 \rho_1 (x_1) \lor \forall x_2 \rho_2 (x_2)\\
\underset{\DNE{(\Pi_k\lor \Pi_k)}}{\longleftrightarrow} & \forall x_1, x_2 \left( \rho_1(x_1) \lor \rho_2(x_2)\right)\\
\longleftrightarrow& \forall x_1, x_2\,  \xi(x_1, x_2) \in \Pi_k.
\end{array}$$


For the first and third items, assume $\varphi_1 \lor \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1,\varphi_2 \in \mathrm{E}_k^+$.
By induction hypothesis, there exist $\rho_1(x_1), \rho_2(x_2) \in \Pi_{k-1}$ such that $\mathsf{HA} + \DNE{\Sigma_k} + \DNS{\mathrm{U}_k^+} $ proves  $\varphi_1 \leftrightarrow \exists x_1 \rho_1(x_1) $ and $ \varphi_2 \leftrightarrow \exists x_2 \rho_2(x_2) $.
By the item \ref{eq: item for Pi_k in PNFT} for $k-1$, there exists $\xi(x_1, x_2) \in \Pi_{k-1}$ such that  
 $$\mathsf{HA}  + \DNE{(\Pi_{k-1}\lor \Pi_{k-1})} \vdash \xi(x_1,x_2) \leftrightarrow \rho_1(x_1) \lor \rho_2(x_2).$$
By  Lemma
\ref{lem: k -> k-1}, we have that $\mathsf{HA} + \DNE{\Sigma_k} + \DNS{\mathrm{U}_k^+} $ proves
$$
\begin{array}{cl}
&\varphi_1 \lor \varphi_2 \\
\underset{\text{[I.H.] }\DNE{\Sigma_k},\, \DNS{\mathrm{U}_k^+}}{\longleftrightarrow} & \exists x_1 \rho_1 (x_1) \lor \exists x_2 \rho_2 (x_2)\\
\longleftrightarrow &\exists x_1, x_2 (\rho_1(x_1) \lor \rho_2(x_2)) \\
\underset{\text{[I.H.] }\DNE{(\Pi_{k-1}\lor \Pi_{k-1})}}{\longleftrightarrow} &\exists x_1, x_2\, \xi(x_1, x_2).
\end{array}
$$
Thus we are done for the first item.
For the third item, by induction hypothesis, there exist  $\varphi_1'' ,\varphi_2'' \in \Pi_k$ such that
$\mathsf{HA} + \NN{\DNE{(\Pi_k\lor \Pi_k)}}$ proves $\neg \varphi_1 \leftrightarrow \neg \neg \varphi_1''$ and $ \neg \varphi_2 \leftrightarrow \neg \neg  \varphi_2''$.
In addition, by Lemma \ref{lem: basic facts on arithmetical hierarchy}, there exists $\varphi'' \in \Pi_k$ such that
$\mathsf{HA} \vdash \varphi'' \leftrightarrow \varphi_1'' \land \varphi_2''$.
Then $\mathsf{HA} +  \NN{\DNE{(\Pi_k\lor \Pi_k)}}$ proves
$$
\neg (\varphi_1 \lor \varphi_2 ) \leftrightarrow \neg \varphi_1 \land \neg \varphi_2 \underset{\text{[I.H.] }\NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}}{\longleftrightarrow}  \neg \neg \varphi_1'' \land \neg \neg \varphi_2'' \leftrightarrow \neg \neg (\varphi_1'' \land \varphi_2'') \leftrightarrow \neg \neg \varphi''.
$$

The case of $\varphi_1 \to \varphi_2$:
\begin{comment}
==================================================================
For the second item, assume $\varphi_1 \to \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{E}_k^+$ and $\varphi_2 \in \mathrm{U}_k^+$.
By induction hypothesis, there exist  $ \rho_1(x_1), \rho_2(x_2)\in \Sigma_{k-1}$ such that
$\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}} \vdash \neg \varphi_1 \leftrightarrow \neg \neg \forall x_1 \rho_1(x_1)$
and
$\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})}  \vdash \varphi_2 \leftrightarrow \forall x_2 \rho_2(x_2)$.
By Lemma \ref{lem: basic facts on our classes}, we have that $\neg \rho_1(x_1) \to \rho_2(x_2)$ is in $\mathrm{E}_{k-1}^+$.
Then,
by the item \ref{eq: item for NNPi_k in PNFT} for $k-1$,
there exists $\xi(x_1, x_2)  \in \Pi_{k-1}$ such that
$$
\mathsf{HA} + \NN{\DNE{(\Pi_{k-1}\lor \Pi_{k-1}) }}  \vdash 
 \neg  \left( \neg \rho_1(x_1) \to \rho_2(x_2) \right) \leftrightarrow \neg \neg \xi(x_1, x_2).$$
In addition, by Lemma \ref{lem: NP and NS}, there exists $\xi'(x_1, x_2)\in \Sigma_{k-1}$ such that $\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash \neg \xi(x_1, x_2)\leftrightarrow \xi'(x_1, x_2) $.
Then, using Lemma \ref{lem: k -> k-1}, we have that $\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})} $ proves
$$
\begin{array}{cl}
&\varphi_1 \to \varphi_2\\
\underset{\text{[I.H.] }\DNE{(\Pi_{k}\lor \Pi_{k})}}{\longleftrightarrow} & \varphi_1 \to \forall x_2 \rho_2 (x_2)\\
\underset{\DNE{\Pi_k}}{\longleftrightarrow} & \varphi_1 \to \neg \neg \forall x_2 \rho_2 (x_2)\\
\longleftrightarrow &  \neg \neg \varphi_1 \to  \neg \neg  \forall x_2 \rho_2 (x_2) \\
\underset{\text{[I.H.] } \NN{\DNE{(\Pi_k \lor \Pi_k)}}}{\longleftrightarrow} & \neg \forall x_1 \rho_1(x_1) \to  \neg \neg  \forall x_2 \rho_2 (x_2)\\
\underset{\DNE{\Sigma_{k-1}} }{\longleftrightarrow} & \neg \neg \exists x_1 \neg \rho_1(x_1) \to  \neg \neg  \forall x_2 \rho_2 (x_2)\\
\longleftrightarrow & \neg \neg \forall x_1, x_2 \left( \neg \rho_1(x_1) \to  \rho_2 (x_2) \right)\\
\longrightarrow & \forall x_1, x_2  \neg \neg \left( \neg \rho_1(x_1) \to  \rho_2 (x_2) \right)\\
\underset{\text{[I.H.] } \NN{\DNE{(\Pi_{k-1} \lor \Pi_{k-1})}}}{\longleftrightarrow} & \forall x_1, x_2  \neg \xi(x_1, x_2)\\
\underset{\DNE{\Sigma_{k-1}} }{\longleftrightarrow} &\forall x_1, x_2  \xi'(x_1, x_2) \\
\end{array}
$$
and also
$$
\begin{array}{cl}
&\forall x_1, x_2  \neg \neg \left( \neg \rho_1(x_1) \to  \rho_2 (x_2) \right)\\
\longleftrightarrow & \forall x_1, x_2  \left( \neg \rho_1(x_1) \to  \neg \neg \rho_2 (x_2) \right)\\
\underset{\DNE{\Sigma_{k-1}} }{\longleftrightarrow} &\forall x_1, x_2  \left( \neg \rho_1(x_1) \to  \rho_2 (x_2) \right)\\
\longleftrightarrow &  \exists x_1 \neg \rho_1(x_1) \to \forall x_2 \rho_2 (x_2)\\
\longrightarrow & \neg \forall x_1 \neg \neg \rho_1(x_1) \to \forall x_2 \rho_2 (x_2)\\
\underset{\DNE{\Sigma_{k-1}} }{\longleftrightarrow} & \neg \forall x_1  \rho_1(x_1) \to \forall x_2 \rho_2 (x_2)\\
\underset{\text{[I.H.] }\DNE{(\Pi_{k}\lor \Pi_{k})}}{\longleftrightarrow} & \neg \neg \varphi_1 \to \varphi_2\\
\longrightarrow & \varphi_1 \to \varphi_2.
\end{array}
$$
Thus we have shown $\mathsf{HA} +  \DNE{(\Pi_{k}\lor \Pi_{k})} \vdash (\varphi_1 \to \varphi_2) \leftrightarrow \forall x_1, x_2  \xi'(x_1, x_2) $, which is in $\Pi_k$.

[Alternative proof of this part with using $\DNS{\mathrm{U}_{k-1}^+}$]
==============================================================================================================
\end{comment}
For the second item, assume $\varphi_1 \to \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{E}_k^+$ and $\varphi_2 \in \mathrm{U}_k^+$.
By induction hypothesis, there exist  $ \rho_1(x_1), \rho_2(x_2)\in \Sigma_{k-1}$ such that
$\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}} \vdash \neg \varphi_1 \leftrightarrow \neg \neg \forall x_1 \rho_1(x_1)$
and
$\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})}  \vdash \varphi_2 \leftrightarrow \forall x_2 \rho_2(x_2)$.
By Lemma \ref{lem: basic facts on our classes}, we have that $\neg \rho_1(x_1) \to \rho_2(x_2)$ is in $\mathrm{E}_{k-1}^+$.
Then,
by the item \ref{eq: item for Sigma_k in PNFT} for $k-1$,
there exists $\xi(x_1, x_2)  \in \Sigma_{k-1}$ such that
$$
\mathsf{HA} + \DNE{\Sigma_{k-1}} + \DNS{\mathrm{U}_{k-1}^+} \vdash 
\xi(x_1, x_2) \leftrightarrow  \left( \neg \rho_1(x_1) \to \rho_2(x_2) \right).$$
Then, using Lemma \ref{lem: k -> k-1} and \eqref{eq: HA + Pk-1Pk-1DNE |- Uk-1pDNS},
we have that $\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})} $ proves
$$
\begin{array}{cl}
&\varphi_1 \to \varphi_2\\
\underset{\text{[I.H.] }\DNE{(\Pi_{k}\lor \Pi_{k})}}{\longleftrightarrow} & \varphi_1 \to \forall x_2 \rho_2 (x_2)\\
\underset{\DNE{\Pi_k}}{\longleftrightarrow} & \varphi_1 \to \neg \neg \forall x_2 \rho_2 (x_2)\\
\longleftrightarrow &  \neg \neg \varphi_1 \to  \neg \neg  \forall x_2 \rho_2 (x_2) \\
\underset{\text{[I.H.] }\NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}}{\longleftrightarrow} & \neg \forall x_1 \rho_1(x_1) \to  \neg \neg  \forall x_2 \rho_2 (x_2)\\
\underset{\DNE{\Sigma_{k-1}} }{\longleftrightarrow} & \neg \neg \exists x_1 \neg \rho_1(x_1) \to  \neg \neg  \forall x_2 \rho_2 (x_2)\\
\longleftrightarrow & \neg \neg \forall x_1, x_2 \left( \neg \rho_1(x_1) \to  \rho_2 (x_2) \right)\\
\underset{\text{[I.H.] }\DNE{\Sigma_{k-1}} , \, \DNS{\mathrm{U}_{k-1}^+}  }{\longleftrightarrow} &\neg \neg \forall x_1, x_2 \, \xi( x_1, x_2)\\
\underset{\DNE{\Pi_k}}{\longleftrightarrow} &\forall x_1, x_2 \, \xi( x_1, x_2) \in \Pi_k.\\
\end{array}
$$



For the first and third items, assume $\varphi_1 \to \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{U}_k^+$ and $\varphi_2 \in \mathrm{E}_k^+$.
By induction hypothesis, there exists
$ \rho_2(x_2) \in \Pi_{k-1}$  such that
$\mathsf{HA} + \DNE{\Sigma_{k}} +  \DNS{\mathrm{U}_k^+} \vdash  \varphi_2 \leftrightarrow  \exists x_2 \rho_2(x_2) $.
In addition, by Lemma \ref{PNFT_of_NE_k_and_NNU_k}, there exists $ \rho_1(x_1)\in \Sigma_{k-1}$ such that
$\mathsf{HA} + \DNS{\mathrm{U}_k^+} \vdash \neg \neg \varphi_1 \leftrightarrow \neg \neg \forall x_1 \rho_1(x_1)$.
By Lemma \ref{lem: basic facts on our classes}, we have $\neg \rho_2(x_2) \to  \neg \rho_1(x_1)$ is in $\mathrm{U}_{k-1}^+$.
Then,
by the item \ref{eq: item for Pi_k in PNFT} for $k-1$,
there exists $\xi(x_1, x_2) \in \Pi_{k-1}$ such that
$$
\mathsf{HA} + \DNE{(\Pi_{k-1}\lor \Pi_{k-1})} \vdash \xi(x_1, x_2) \leftrightarrow  \left(\neg \rho_2(x_2) \to  \neg \rho_1(x_1) \right).$$
Then, using Lemma \ref{lem: k -> k-1}, we have that $\mathsf{HA} + \DNE{\Sigma_{k}}+ \DNS{\mathrm{U}_k^+}$ proves
$$
\begin{array}{cl}
& \varphi_1 \to \varphi_2 \\
\underset{\text{[I.H.] }\DNE{\Sigma_{k}}, \, \DNS{\mathrm{U}_k^+}}{\longleftrightarrow}& \varphi_1 \to  \exists x_2 \rho_2(x_2)\\
\underset{\DNE{\Sigma_k}}{\longleftrightarrow}&  \varphi_1 \to \neg \neg  \exists x_2 \rho_2(x_2)\\
\longleftrightarrow& \neg \neg \varphi_1 \to \neg \neg  \exists x_2 \rho_2(x_2)\\
\underset{ \DNS{\mathrm{U}_k^+}}{\longleftrightarrow}&\neg \neg  \forall x_1 \rho_1(x_1) \to \neg \neg  \exists x_2 \rho_2(x_2)\\
\longleftrightarrow&\neg \neg \exists x_2 \left( \forall x_1 \rho_1(x_1) \to \rho_2(x_2) \right) \\
\underset{\DNE{\Pi_{k-1}}}{\longleftrightarrow}&\neg \neg \exists x_2 \left(\neg  \rho_2(x_2) \to \neg \forall x_1 \rho_1(x_1)  \right) \\
\underset{\DNE{\Sigma_{k-1}}}{\longleftrightarrow}&\neg \neg \exists x_2 \left(\neg  \rho_2(x_2) \to \neg \neg \exists x_1  \neg  \rho_1(x_1)  \right) \\
\longleftrightarrow &\neg \neg \exists x_2 \neg \neg \exists x_1  \left(\neg  \rho_2(x_2) \to  \neg  \rho_1(x_1)  \right) \\
\underset{\text{[I.H.] } \DNE{(\Pi_{k-1}\lor \Pi_{k-1})}}{\longleftrightarrow}&\neg \neg \exists x_1, x_2 \, \xi (x_1, x_2)\\
\underset{ \DNE{\Sigma_k}}{\longleftrightarrow}& \exists x_1, x_2 \, \xi (x_1, x_2) \in \Sigma_k .\\
\end{array}
$$
Thus we are done for the first item.
For the third item, by induction hypothesis, there exist
$\varphi_1', \varphi_2' \in \Pi_k$ such that
$\mathsf{HA} + \DNE{(\Pi_k \lor \Pi_k)} \vdash  \varphi_1 \leftrightarrow \varphi_1'$
and
$\mathsf{HA} + \NN{\DNE{(\Pi_k \lor \Pi_k)}} \vdash \neg \varphi_2 \leftrightarrow \neg \neg \varphi_2'$.
On the other hand, by Lemma \ref{lem: basic facts on arithmetical hierarchy}, there exists $\xi' \in \Pi_k$ such that $\mathsf{HA} \vdash \varphi_1' \land \varphi_2' \leftrightarrow \xi'$.
Then $\mathsf{HA} +\NN{\DNE{(\Pi_k \lor \Pi_k)}} $ proves
$$
\neg( \varphi_1 \to \varphi_2) \leftrightarrow (\neg \neg \varphi_1 \land \neg \varphi_2)\underset{\text{[I.H.] } \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}}{\longleftrightarrow} \neg \neg \varphi_1' \land \neg \neg \varphi_2' \leftrightarrow \neg \neg (\varphi_1' \land \varphi_2') \leftrightarrow \neg \neg \xi'.
$$



The case of $\forall x  \varphi_1 (x )$:
For the second item, assume $\forall x  \varphi_1 (x ) \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 (x ) \in \mathrm{U}_k^+$.
By induction hypothesis, there exists $\varphi_1'(x )  \in \Pi_{k}$ such that $\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})} \vdash \varphi_1(x ) \leftrightarrow \varphi_1'(x )$.
Then $\forall x  \varphi_1 (x )$ is equivalent to  $\forall x  \varphi_1'(x ) \in \Pi_k$ over 
$\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})}  $.

For the first and third items, assume  $\forall x  \varphi_1 (x ) \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\forall x \varphi_1 (x ) \in \mathrm{U}_{k-1}^+$.
Then,
by the item \ref{eq: item for Pi_k in PNFT} for $k-1$, there exists $\xi \in \Pi_{k-1} \subseteq \Sigma_k$ (see Remark \ref{rem: identification on Sigma_k and Pi_k}) such that
\begin{equation}
\label{eq: con of IH for k-1}
\mathsf{HA} + \DNE{(\Pi_{k-1}\lor \Pi_{k-1})} \vdash \forall x \varphi_1(x ) \leftrightarrow \xi.
\end{equation}
By Lemma \ref{lem: k -> k-1}, we are done for the first item.
For the third item, by Lemma \ref{lem: NP and NS}, there exists $\xi'\in \Sigma_{k-1} \subseteq \Pi_k$ (see Remark \ref{rem: identification on Sigma_k and Pi_k}) such that $\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash \neg \xi \leftrightarrow \xi'$.
By Corollary \ref{cor: HA+P |- vp_1 <-> vp_2 => HA+NNP |- NNvp_1 <-> NNvp_2}, we have $\mathsf{HA} + \NN{\DNE{\Sigma_{k-1}}} \vdash \neg \xi \leftrightarrow  \neg \neg \xi'$.
In addition, 
$$\mathsf{HA} + \NN{\DNE{(\Pi_{k-1}\lor \Pi_{k-1})}} \vdash \neg \neg  \forall x \varphi_1(x ) \leftrightarrow \neg \neg \xi $$
follows from \eqref{eq: con of IH for k-1}.
Then, by Lemma \ref{lem: k -> k-1}, we have that $\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}  $ proves
$$
\neg \forall x \varphi_1(x ) \underset{\text{[I.H.] } \NN{\DNE{(\Pi_{k-1}\lor \Pi_{k-1})}}}{\longleftrightarrow} \neg \xi \underset{ \NN{\DNE{\Sigma_{k-1}}}}{\longleftrightarrow} \neg \neg \xi'.
$$
Thus we have shown the third item.

The case of $\exists x  \varphi_1 (x )$:
For the second item, assume $\exists x  \varphi_1 (x ) \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $ \exists x \varphi_1 (x ) \in \mathrm{E}_{k-1}^+$.
Then, 
by the item \ref{eq: item for Sigma_k in PNFT} for $k-1$, there exists $\xi  \in \Sigma_{k-1}\subseteq \Pi_k$ (see Remark \ref{rem: identification on Sigma_k and Pi_k}) such that $\mathsf{HA} +\DNE{\Sigma_{k-1}} + \DNS{\mathrm{U}_{k-1}^+} \vdash \exists x \varphi_1(x ) \leftrightarrow \xi$.
By Lemma \ref{lem: k -> k-1} and \eqref{eq: HA + Pk-1Pk-1DNE |- Uk-1pDNS}, we have
$\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})} \vdash \exists x \varphi_1(x ) \leftrightarrow \xi$.



For the first and third items, assume $\exists x  \varphi_1 (x ) \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 (x ) \in \mathrm{E}_k^+$.
By induction hypothesis, there exist $\varphi_1'(x )  \in \Sigma_{k}$ and $\varphi_1''(x )  \in \Pi_k$ such that $\mathsf{HA}  +\DNE{\Sigma_{k}} +\DNS{\mathrm{U}_{k}^+} \vdash \varphi_1(x ) \leftrightarrow \varphi_1'(x )$
and $\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}} \vdash \neg \varphi_1 (x) \leftrightarrow \neg \neg \varphi_1'' (x)$.
Then $\exists x  \varphi_1 (x )$ is equivalent to $\exists x  \varphi_1'(x ) \in \Sigma_k$ over 
$\mathsf{HA} +\DNE{\Sigma_{k}} +\DNS{\mathrm{U}_{k}^+} $.
Thus we are done for the first item.
For the third item, since $\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}$ proves
$$
\neg  \exists x \varphi_1(x )\leftrightarrow \forall x \neg  \varphi_1(x )  \underset{ \text{[I.H.] }\NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}}{\longleftrightarrow}   \forall x \neg  \neg \varphi_1''(x ) ,
$$
we have that $\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}$ proves
$$
\neg  \exists x \varphi_1(x )\leftrightarrow \neg \neg   \forall x \neg  \neg \varphi_1''(x ) .
$$
On the other hand, the latter is equivalent to $ \neg \neg   \forall x \varphi_1''(x ) $ in the presence of $ \NN{\DNE{\Pi_{k}}}$.
Thus we have $\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}} \vdash \neg  \exists x \varphi_1(x )\leftrightarrow \neg \neg   \forall x \varphi_1''(x )$.
\end{proof}

\begin{comment}
\begin{corollary}
For each natural number $k$ and a formula $\varphi$ of $\mathsf{HA}$,
 if $\varphi \in \mathrm{U}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} +\DNE{\Sigma_{k-1}} + \NN{\DNE{(\Pi_k\lor \Pi_k)}}  \vdash \NN{\varphi} \leftrightarrow \varphi'.
    $$
\end{corollary}
\begin{proof}
Immediate from Theorem \ref{thm: PNFT}.\eqref{eq: item for NNPi_k in PNFT} and Lemma \ref{lem: k -> k-1}.\eqref{item: sk-DNE -> pk+1-DNE}.
\end{proof}
\end{comment}


\begin{corollary}
\label{cor: pk v pk -DNE -> Ukp-DNE}
$\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}}  \vdash \DNS{\mathrm{U}_k^+} .$
\end{corollary}
\begin{proof}
Since $\DNS{\mathrm{U}_k^+} $ is intuitionistically equivalent to $\NN{\DNS{\mathrm{U}_k^+} }$ (see Remark \ref{rem: NNDNS <-> DNS}), it suffices to show $\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})}  \vdash \DNS{\mathrm{U}_k^+} $.
By Theorem \ref{thm: PNFT}.\eqref{eq: item for Pi_k in PNFT}, any formulas $\varphi \in \mathrm{U}_k^+$ is equivalent to some  $\varphi' \in \Pi_k$ such that $\FV{\varphi} = \FV{\varphi'}$ over $\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})}$.
Since $\mathsf{HA} + \DNE{\Pi_k} \vdash \DNS{\Pi_k}$, we have $\mathsf{HA} + \DNE{(\Pi_{k}\lor \Pi_{k})}  \vdash \DNS{\mathrm{U}_k^+} $.
\end{proof}

\begin{remark}
Corollary \ref{cor: pk v pk -DNE -> Ukp-DNE} shows that
Lemma \ref{PNFT_of_NE_k_and_NNU_k} (equivalent to item \ref{eq: item for NE_k in PNFT} in the proof of Lemma \ref{PNFT_of_NE_k_and_NNU_k}) is a stronger statement of the item \ref{eq: item for NNPi_k in PNFT} in the proof of Theorem \ref{thm: PNFT}.
On the other hand, it is still open whether $\mathsf{HA} + \DNS{\mathrm{U}_k^+}$ is a proper subsystem of $\mathsf{HA} + \NN{\DNE{(\Pi_{k}\lor \Pi_{k})}} $.
\end{remark}

\begin{remark}
It follows from Theorem \ref{thm: PNFT} and the results in Section \ref{sec: CE} that $\mathsf{HA} + \DNE{\Sigma_1}$ does not prove $\DNS{\mathrm{U}_1^+}$.
\end{remark}

At the end of this section, we study the prenex normal form theorem for formulas which do not contain the disjunction $\lor$.
In fact, the proof of Theorem \ref{thm: PNFT} suggests that the unusual form $\DNE{(\Pi_k \lor \Pi_k)}$ of the double negation elimination is caused from the argument especially in the case of $\varphi_1 \lor \varphi_2$.
On the other hand, if a formula $\varphi$ does not contain $\lor$, one can intuitionistically derive the original formula $\varphi$ from a formula of the prenex normal form which is classically equivalent to $\varphi$ (cf. \cite[Lemma 6.2.1]{vD13}).
Then the proof of the prenex normal form theorem for those formulas becomes to be fairly simple.


\begin{theorem}
\label{thm: PNFT for df-formulas}
For each natural number $k$ and a formula $\varphi$ (possibly containing free variables) which does not contain $\lor$,
the following hold:
\begin{enumerate}
        \item 
        \label{eq: item for Sigma_k in PNFT for df-formulas}
    if $\varphi \in \mathrm{E}_k^+$, then
        there exists $\varphi' \in \Sigma_k$  such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA}  + \DNE{\Sigma_k} \vdash \varphi \leftrightarrow \varphi';
    $$
     \item 
    \label{eq: item for Pi_k in PNFT for df-formulas}
    if $\varphi \in \mathrm{U}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} + \DNE{\Sigma_{k-1}} \,\, (\mathsf{HA} \text{ if }k=0)  \vdash \varphi \leftrightarrow \varphi' .
    $$
\end{enumerate}
\end{theorem}
\begin{proof}
We mimic the proof of  Theorem \ref{thm: PNFT}. 
Thus we first prepare the following auxiliary assertion (which
is in fact a consequence from the item \ref{eq: item for Pi_k in PNFT for df-formulas}):
\begin{enumerate}
\setcounter{enumi}{2}
\item 
    \label{eq: item for NE_k in PNFT for df-formulas}
    if $\varphi \in \mathrm{E}_k^+$, then there exists $\varphi' \in \Pi_k$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    $$
    \mathsf{HA} + \neg \neg \DNE{\Sigma_{k-1}}  \vdash \neg \varphi \leftrightarrow \neg \neg  \varphi'.
    $$
    \end{enumerate}
Then we show the items \ref{eq: item for Sigma_k in PNFT for df-formulas}, \ref{eq: item for Pi_k in PNFT for df-formulas} and 
\ref{eq: item for NE_k in PNFT for df-formulas} by induction on $k$ simultaneously.
The base case is trivial.
Most of the parts for the induction step is the same as those for Theorem \ref{thm: PNFT}.
The same proof works since the logical principle in the items \ref{eq: item for Sigma_k in PNFT for df-formulas} and \ref{eq: item for Pi_k in PNFT for df-formulas} implies both of them for $k-1$ and  the logical principle in the item \ref{eq: item for NE_k in PNFT for df-formulas}
is the double negation of the logical principle in the item  \ref{eq: item for Pi_k in PNFT for df-formulas} as in Theorem \ref{thm: PNFT}.


Only the difference with the proof of Theorem \ref{thm: PNFT} is in proving the item \ref{eq: item for Sigma_k in PNFT} for $\varphi : \equiv \varphi_1 \to \varphi_2\in \mathrm{E}_k^+$, where we use Lemma \ref{PNFT_of_NE_k_and_NNU_k}.

Here one can use the item \ref{eq: item for Pi_k in PNFT for df-formulas}
instead of Lemma \ref{PNFT_of_NE_k_and_NNU_k}.
This is because $\DNE{\Sigma_k}$ includes $\DNE{\Sigma_{k-1}}$ while the verification theory of the item \ref{eq: item for Sigma_k in PNFT} in Theorem \ref{thm: PNFT} contains  the verification theory of Lemma \ref{PNFT_of_NE_k_and_NNU_k}.
To be absolutely clear, we present the proof of this part:
Let $ \varphi_1 \to \varphi_2\in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $ \varphi_1 \in \mathrm{U}_k^+$ and $\varphi_2\in \mathrm{E}_k^+$.
By induction hypothesis,
there exists 
$\rho_1(x_1)  \in \Sigma_{k-1}$ and 
$ \rho_2(x_2) \in \Pi_{k-1}$  such that
$\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash \varphi_1 \leftrightarrow \forall x_1 \rho_1(x_1)$
and
$\mathsf{HA} + \DNE{\Sigma_{k}}  \vdash  \varphi_2 \leftrightarrow  \exists x_2 \rho_2(x_2) $.
By Lemma \ref{lem: basic facts on our classes}, we have $\neg \rho_2(x_2) \to  \neg \rho_1(x_1)$ is in $\mathrm{U}_{k-1}^+$.
Then,
by the item \ref{eq: item for Pi_k in PNFT} for $k-1$,
there exists $\xi(x_1, x_2) \in \Pi_{k-1}$ such that
$$
\mathsf{HA} +  \DNE{\Sigma_{k-2}} \vdash \xi(x_1, x_2) \leftrightarrow  \left(\neg \rho_2(x_2) \to  \neg \rho_1(x_1) \right).$$
Then
$\mathsf{HA} + \DNE{\Sigma_{k}}$ proves
$$
\begin{array}{cl}
& \varphi_1 \to \varphi_2 \\
\underset{\text{[I.H.] }\DNE{\Sigma_{k}}}{\longleftrightarrow}& \varphi_1 \to  \exists x_2 \rho_2(x_2)\\
\underset{\DNE{\Sigma_k}}{\longleftrightarrow}&  \varphi_1 \to \neg \neg  \exists x_2 \rho_2(x_2)\\
\underset{\text{[I.H.] }\DNE{\Sigma_{k-1}}}{\longleftrightarrow}&  \forall x_1 \rho_1(x_1) \to \neg \neg  \exists x_2 \rho_2(x_2)\\
\longleftrightarrow&\neg \neg \exists x_2 \left( \forall x_1 \rho_1(x_1) \to \rho_2(x_2) \right) \\
\underset{\DNE{\Pi_{k-1}}}{\longleftrightarrow}&\neg \neg \exists x_2 \left(\neg  \rho_2(x_2) \to \neg \forall x_1 \rho_1(x_1)  \right) \\
\underset{\DNE{\Sigma_{k-1}}}{\longleftrightarrow}&\neg \neg \exists x_2 \left(\neg  \rho_2(x_2) \to \neg \neg \exists x_1  \neg  \rho_1(x_1)  \right) \\
\longleftrightarrow &\neg \neg \exists x_2 \neg \neg \exists x_1  \left(\neg  \rho_2(x_2) \to  \neg  \rho_1(x_1)  \right) \\
\underset{\text{[I.H.] }\DNE{\Sigma_{k-2}}}{\longleftrightarrow}&\neg \neg \exists x_1, x_2 \, \xi (x_1, x_2)\\
\underset{ \DNE{\Sigma_k}}{\longleftrightarrow}& \exists x_1, x_2 \, \xi (x_1, x_2) \in \Sigma_k .\\
\end{array}
$$
\begin{comment}
Assume the items \ref{eq: item for Sigma_k in PNFT for df-formulas}, \ref{eq: item for Pi_k in PNFT for df-formulas} and \ref{eq: item for NE_k in PNFT for df-formulas} for $k-1$.
We show the items \ref{eq: item for Sigma_k in PNFT for df-formulas}, \ref{eq: item for Pi_k in PNFT for df-formulas} and \ref{eq: item for NE_k in PNFT for df-formulas} for $k$ simultaneously by induction on the structure of formulas which do not contain $\lor$.
When $\varphi$ is a prime formula, they are trivial.
For the induction step, assume that items \ref{eq: item for Sigma_k in PNFT for df-formulas}, \ref{eq: item for Pi_k in PNFT for df-formulas} and \ref{eq: item for NE_k in PNFT for df-formulas} hold for $\varphi_1$ and $\varphi_2$.


The case of $\varphi_1 \land \varphi_2$ is verified exactly as in the proof of Theorem \ref{thm: PNFT}.

The case of $\varphi_1 \land \varphi_2$：
The second item is verified as in in the proof of Theorem \ref{thm: PNFT}.

The first and second items are verified by a routine inspection.
For the third item, assume $\varphi_1 \land \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1, \varphi_2 \in \mathrm{E}_k^+$.
By induction hypothesis, there exist  $\rho_1'(x_1) ,  \rho_2'(x_2) \in \Sigma_{k-1}$ such that
$\mathsf{HA} +\DNE{\Sigma_{k-1}}$ proves $\neg \varphi_1 \leftrightarrow \forall x_1 \rho_1'(x_1)$ and $\neg \varphi_2 \leftrightarrow \forall x_2 \rho_2'(x_2)$.
By Lemma \ref{lem: basic facts on our classes}, we have $\neg \rho_2 (x_2) \to \rho_1(x_1) $ is in $\mathrm{E}_{k-1}^+$. 
Then, by the item \ref{eq: item for Sigma_k in PNFT for df-formulas} for $k-1$, there exists $\xi(x_1, x_2)\in \Sigma_{k-1}$ such that
$$
\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash \xi(x_1, x_2) \leftrightarrow (\neg \rho_2 (x_2) \to \rho_1(x_1)  ).
$$
Then $\mathsf{HA} + \DNE{\Sigma_{k-1}} $ proves
$$
\begin{array}{cl}
&\neg (\varphi_1 \land \varphi_2)\\
\longleftrightarrow & \varphi_1 \to \neg \varphi_2\\
\underset{\text{[I.H.] }\DNE{\Sigma_{k-1}}}{\longleftrightarrow} &\varphi_1 \to \forall x_2 \rho_2(x_2)\\
\longleftrightarrow &  \forall x_2 \left(\varphi_1 \to  \rho_2(x_2) \right)\\
\underset{\DNE{\Sigma_{k-1}}}{\longleftrightarrow} & \forall x_2 \left(\neg \rho_2(x_2) \to \neg \varphi_1 \right)\\
\underset{\text{[I.H.] }\DNE{\Sigma_{k-1}}}{\longleftrightarrow} & \forall x_2 \left(\neg \rho_2(x_2) \to \forall x_1 \rho_1(x_1) \right)\\
\longleftrightarrow &  \forall x_1, x_2 \left(\neg \rho_2(x_2) \to  \rho_1(x_1) \right)\\[2pt]
\underset{\text{[I.H.] }\DNE{\Sigma_{k-1}}}{\longleftrightarrow} & \forall x_1, x_2 \, \xi(x_1, x_2).
\end{array}
$$


The case of $\varphi_1 \to \varphi_2$:
The first item is verified by imitating the corresponding proof of Theorem \ref{thm: PNFT}.
For the second item, assume $\varphi_1 \to \varphi_2 \in \mathrm{U}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{E}_k^+$ and $\varphi_2 \in \mathrm{U}_k^+$.
By induction hypothesis, there exist $\rho_1'(x_1), \rho_2'(x_2) \in \Sigma_{k-1}$ such that
$\mathsf{HA} +\DNE{\Sigma_{k-1}}$ proves $\neg \varphi_1 \leftrightarrow \forall x_1 \rho_1'(x_1)$ and $ \varphi_2 \leftrightarrow \forall x_2 \rho_2'(x_2)$.
Using these equivalences, as in the corresponding proof of Theorem \ref{thm: PNFT}, one obtains $\psi\in \Pi_k$ such that $\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash (\varphi_1 \to \varphi_2) \leftrightarrow \psi$.
For the third item, $\varphi_1 \to \varphi_2 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{U}_k^+$ and $\varphi_2 \in \mathrm{E}_k^+$.
By induction hypothesis, there exist $\varphi_1', \varphi_2' \in \Pi_k$ such that
$\mathsf{HA} +\DNE{\Sigma_{k-1}}$ proves $\varphi_1 \leftrightarrow \varphi_1' $ and $\neg \varphi_2 \leftrightarrow \varphi_2'$.
Using Lemma \ref{lem: k -> k-1}.\eqref{item: sk-DNE -> pk+1-DNE}, we have that $\mathsf{HA} +\DNE{\Sigma_{k-1}}$ proves
$$
\begin{array}{cl}
     & \neg( \varphi_1 \to \varphi_2)  \\
\longleftrightarrow     & \neg \neg \varphi_1  \land \neg \neg \neg \varphi_2 \\
\underset{\text{[I.H.] }\DNE{\Sigma_{k-1}}}{\longleftrightarrow}     & \neg \neg \varphi_1'  \land \neg \neg \varphi_2' \\
\longleftrightarrow  & \neg \neg ( \varphi_1' \land \varphi_2')\\
\underset{\DNE{\Sigma_{k-1}}}{\longleftrightarrow} & \varphi_1' \land \varphi_2'.
\end{array}
$$

The case of  $\forall x \varphi_1$:
The second item is verified by a routine inspection.
For the first and third items, assume $\forall x \varphi_1 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\forall x \varphi_1 \in \mathrm{U}_{k-1}^+$.
By the item \ref{eq: item for Pi_k in PNFT for df-formulas} for $k-1$, there exists $\varphi'\in \Pi_{k-1} \subseteq \Sigma_k$ (see Remark \ref{rem: identification on Sigma_k and Pi_k}) such that $\mathsf{HA} +\DNE{\Sigma_{k-2}}$ (and hence, $\mathsf{HA} +\DNE{\Sigma_{k-1}}$) proves $\forall x \varphi_1 \leftrightarrow \varphi'$.
Thus we have shown the first item.
In addition, by Lemma \ref{lem: NP and NS}, there exists $\varphi''\in \Sigma_{k-1}$ such that $\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash \neg \varphi' \leftrightarrow \varphi''$.
Then $\mathsf{HA}+\DNE{\Sigma_{k-1}}$ proves
$$
\neg \forall x \varphi_1 \underset{\text{[I.H.] }\DNE{\Sigma_{k-2}}}{\longleftrightarrow} \neg \varphi' \underset{\DNE{\Sigma_{k-1}}}{\longleftrightarrow} \varphi''.
$$
Thus we have shown the third item.

The case of $\exists x \varphi_1$:
For the first and third items, assume $exists x \varphi_1 \in \mathrm{E}_k^+$.
By Lemma \ref{lem: basic facts on our classes}, we have $\varphi_1 \in \mathrm{E}_k^+$.
By induction hypothesis, there exist $\varphi_1'(x) \in \Sigma_k^+$ and $\varphi_1''(x) \in \Pi_k$ such that
$\mathsf{HA} + \DNE{\Sigma_k} \vdash \varphi_1(x) \leftrightarrow \varphi_1'(x)$ and $\mathsf{HA} + \DNE{\Sigma_{k-1}} \vdash \neg \varphi_1(x) \leftrightarrow \varphi_1''(x)$.
Then $\mathsf{HA} + \DNE{\Sigma_k} \vdash \exists x \varphi_1(x) \leftrightarrow \exists x \varphi_1'(x)$.
Thus we have shown the first item.
In addition, $\mathsf{HA} + \DNE{\Sigma_{k-1}}$ proves
$$
\neg \exists x \varphi_1(x) \leftrightarrow \forall x \neg \varphi_1(x) \underset{\text{[I.H.] }\DNE{\Sigma_{k-1}}}{\longleftrightarrow} \forall x \varphi_1'' (x).
$$
Thus we have shown the third item.
\end{comment}
\end{proof}


\begin{remark}
It follows from Theorem \ref{thm: PNFT} and Corollary \ref{cor: pk v pk -DNE -> Ukp-DNE} that $\LEM{\mathrm{E}_k^+}$, $\LEM{\mathrm{U}_k^+}$ and $\DNE{\mathrm{U}_k^+}$ are equivalent to $\LEM{\Sigma_k}$, $\LEM{\Pi_k}$ and $\DNE{(\Pi_k \lor \Pi_k)}$ respectively  over $\mathsf{HA}$ (cf. \cite[Corollary 2.9]{ABHK04}).
This may not be the case for $\DNE{\mathrm{E}_k^+}$ and $\DNE{\Sigma_k}$.
On the other hand, Theorem \ref{thm: PNFT for df-formulas} implies that $\mathsf{HA} + \DNE{\Sigma_k}$ proves the double negation elimination for all formulas in $\mathrm{E}_k^+$ which do not contain $\lor.$
\end{remark}

\section{A conservation result}
\label{sec: conservativity}
In this section, we generalize a well-known fact that $\mathsf{PA} $ is $\Pi_2$-conservative over $\mathsf{HA}$ in the context of semi-classical arithmetic (see Theorem \ref{thm: conservation results for PNF -> Pi_k+2}).
The fact is normally shown by applying the negative translation followed by the Friedman A-translation (see e.g. \cite[Chapter 14]{Koh08}).
As for the negative translation, there are several equivalent forms (see \cite[Section 1.10.1]{Tro73}).
Here we employ Kuroda's negative translation among them.

\begin{definition}[cf. Definition 10.1 in \cite{Koh08}]
\label{def: NT}
Let $\varphi$ be a $\mathsf{HA}$-formula.
Then its negative translation $\varphi^N$ is defined as $\varphi^N :\equiv \neg \neg  \SN{\varphi}$, where $\SN{\varphi}$ is defined by induction on the logical structure of $\varphi$ as follows: 
\begin{itemize}
    \item 
    $\SNP{\varphi_{\rm p}} :\equiv \varphi_{\rm p}$ if $\varphi_{\rm p}$ is a prime formula;
    \item
    $\SN{(\varphi_1 \circ \varphi_2)} :\equiv \SNP{\varphi_1} \circ \SNP{\varphi_2}$, where $\circ \in \{ \land, \lor, \to \}$;
    \item
    $\SN{(\exists x \varphi_1)} :\equiv \exists x \SNP{\varphi_1}$;
    \item
    $\SN{(\forall x \varphi_1)} :\equiv \forall x \neg \neg \SNP{\varphi_1}$.
\end{itemize}
\end{definition}

\begin{remark}
\label{rem: NT preserving FVs}
By induction on the structure of formulas, one can show $\FV{\varphi} = \FV{\SN{\varphi}} =\FV{\varphi^N}$ for all formulas $\varphi$.
When it is clear from the context, we suppress the argument on free variables.
\end{remark}

\begin{lemma}
\label{lem: vp -> vp*}
For any $\mathsf{HA}$-formula $\varphi$ of the prenex normal form, $\mathsf{HA} $ proves $\varphi \to \SN{\varphi}$.
\end{lemma}
\begin{proof}
By induction on the structure of formulas of the prenex normal form.
\end{proof}

\begin{proposition}
\label{Soundness of NT}
For any $\mathsf{HA}$-formula $\varphi$, if $\mathsf{PA} \vdash \varphi$, then $\mathsf{HA} \vdash \varphi^N$.
\end{proposition}
\begin{proof}
By induction on the length of the derivations (see the proof of \cite[Proposition 10.3]{Koh08}).
\end{proof}

\begin{lemma}
\label{lem: equivalence of vp and vp' over semi-classical arithmetic}
Let $k$ be a natural number.
\begin{enumerate}
    \item
    \label{item: vp'<-> vp in Sigma_k}
    For any $\mathsf{HA}$-formula $\varphi\in \Sigma_k$, $\mathsf{HA} + \DNE{\Sigma_{k}}$ proves $\varphi^N \leftrightarrow \varphi$.
    \item
    \label{item: vp'<-> vp in Pi_k}
     For any $\mathsf{HA}$-formula $\varphi\in \Pi_k$, $\mathsf{HA} + \DNE{\Sigma_{k-1}}$ $(\mathsf{HA}$ if $k=0)$ proves $\varphi^N \leftrightarrow \varphi$.
\end{enumerate}
\end{lemma}
\begin{proof}
By simultaneous induction on $k$.
The base case is trivial.
For the induction step, assume the items \ref{item: vp'<-> vp in Sigma_k} and \ref{item: vp'<-> vp in Pi_k} for $k$ to show those for $k+1$.
For the first item, let  $\exists x \varphi_1 \in \Sigma_{k+1}$ where $\varphi_1 \in \Pi_k$.
We have that $\mathsf{HA} + \DNE{\Sigma_{k+1}}$ proves
$$
\left( \exists x \varphi_1 \right)^N\equiv \neg \neg \exists x \SNP{\varphi_1}
\leftrightarrow
\neg \neg \exists x \neg \neg \SNP{\varphi_1}
\underset{\text{[I.H.] }\DNE{\Sigma_{k-1}}}{\longleftrightarrow} \neg \neg \exists x \varphi_1 \underset{\DNE{\Sigma_{k+1}}}{\longleftrightarrow}
\exists x \varphi_1 .
$$
For the second item, let $\forall x \varphi_1 \in \Pi_{k+1}$ where $\varphi_1 \in \Sigma_k$.
Since $\DNE{\Pi_{k+1}}$ is derived from $\DNE{\Sigma_k}$ (see Lemma \ref{lem: k -> k-1}.\eqref{item: sk-DNE -> pk+1-DNE}), we have that $\mathsf{HA} + \DNE{\Sigma_k}$ proves
$$
\left( \forall x \varphi_1 \right)^N\equiv \neg \neg \forall x \neg \neg \SNP{\varphi_1} \underset{\text{[I.H.] }\DNE{\Sigma_k}}{\longleftrightarrow} \neg \neg \forall x \varphi_1 \underset{\DNE{\Pi_{k+1}}}{\longleftrightarrow}
\forall x \varphi_1 .
$$


\end{proof}

Let $\mathsf{HA}^{*} $ denote $\mathsf{HA}$ in the extended language where a predicate symbol ${*} $ of arity $0$, which behaves as a “place holder”, is added.
In particular, $\mathsf{HA}^{*}$ has $\perp \to *$ as an axiom.
To make our arguments absolutely clear, we prefer to add the distinguished new predicate ${*} $
rather than discussing about A-translation inside the original language as done in \cite{Fri78, Koh08}.

\begin{definition}[A-translation \cite{Fri78}]
\label{def: A-translation}
For a $\mathsf{HA}$-formula $\varphi$, we define $\varphi^{*} $ as a formula obtained from $\varphi$ by replacing all the prime formulas $\varphi_{\rm p}$ in $\varphi$ with $\varphi_{\rm p} \lor {*} $.
Officially, $\varphi^{*} $ is defined by induction on the logical structure of $\varphi$ as in Definition \ref{def: NT}.
In particular, $\perp^{*} :\equiv  \left(\perp \lor \, {*} \right)$, which is equivalent to  ${*} $ over $\mathsf{HA}^{*} $.
In what follows, $\neg_{*}\, \varphi$ denotes $\varphi \to {*} $.
\end{definition}


\begin{remark}
\label{rem: dollar-translation preserving FVs}
By induction on the structure of formulas, one can show $\FV{\varphi} =\FV{\varphi^{*}}$ for all $\mathsf{HA}$-formulas $\varphi$.
\end{remark}

\begin{proposition}[Cf. Lemma 2 in \cite{Fri78}]
\label{prop: A-translation}
For any $\mathsf{HA}$-formula $\varphi$, if $\mathsf{HA} \vdash \varphi$, then $\mathsf{HA}^{*} \vdash \varphi^{*} $.
\end{proposition}
\begin{proof}
By induction on the length of the derivations.
\end{proof}

\begin{remark}
An analogous assertion of Proposition \ref{prop: A-translation} holds for $\mathsf{HA} +\LEM{\Sigma_1}$ and $\mathsf{HA}^{*} +\LEM{\Sigma_1}$ instead of $\mathsf{HA}$ and $\mathsf{HA}^{*}$ respectively  (see \cite[Lemma 3.1]{KS14}).
\end{remark}

The following substitution result is important in the application of the A-translation:
\begin{lemma}[Cf. Theorem 6.2.4 in \cite{vD13}]
\label{lem: Substitution}
Let $X$ be a set of $\mathsf{HA}$-sentences and $\varphi$ be a $\mathsf{HA}^{*} $-formula.
If $\mathsf{HA}^{*} + X \vdash \varphi$, then $\mathsf{HA} + X \vdash \varphi[\psi/{*}]$ for any $\mathsf{HA}$-formula $\psi$ such that the free variables of $\psi$ are not bounded in $\varphi$, where $\varphi[\psi/{*}]$ is the $\mathsf{HA}$-formula obtained from $\varphi$ by replacing all the occurrences of ${*}$ in $\varphi$ with $\psi$.
\end{lemma}
\begin{proof}
Fix a set $X$ of $\mathsf{HA}$-sentences.
By induction on $k$,
one can show straightforwardly that for any $k$ and any $\mathsf{HA}^{*} $-formula $\varphi$, if $\mathsf{HA}^{*} + X \vdash \varphi$ with the proof of length $k$, then $\mathsf{HA} + X \vdash \varphi[\psi/{*} ]$ for any $\mathsf{HA}$-formula $\psi$ such that the free variables of $\psi$ is not bounded in $\varphi$.
The variable condition is used to verify the case of axioms and rules for quantifiers.
\end{proof}

The following lemma is a key for our generalized conservation results.
\begin{lemma}
\label{lem: key lemma on vp*A in semi-classical arithemtic}
Let $k$ be a natural number.
\begin{enumerate}
    \item
    \label{item: vp*A <-> vp* v A for vp in Sigma_k}
    For any $\mathsf{HA}$-formula $\varphi\in \Sigma_k$, $\mathsf{HA}^{*} + \LEM{\Sigma_{k-1}}$ $(\mathsf{HA}^{*} $ if $k=0)$ proves $\left( \SN{\varphi}\right)^{*} \leftrightarrow \SN{\varphi} \lor {*} $.
    \item
        \label{item: vp*A <-> vp* v A for vp in Pi_k}
     For any $\mathsf{HA}$-formula $\varphi\in \Pi_k$, $\mathsf{HA}^{*} + \LEM{\Sigma_{k}}$ proves $\left( \SN{\varphi}\right)^{*} \leftrightarrow \SN{\varphi} \lor {*} $.
\end{enumerate}
\end{lemma}
\begin{proof}
We show the items \ref{item: vp*A <-> vp* v A for vp in Sigma_k} and \ref{item: vp*A <-> vp* v A for vp in Pi_k} simultaneously by induction on $k$.

The base case:
Since every quantifier-free formula $\QF{\varphi}$ such that $\FV{\QF{\varphi}}=\{\ol{x} \} $ is equivalent to a prime formula $t(\ol{x})=0$ for some closed term $t$ (see e.g. \cite[Proposition 3.8]{Koh08}), by Proposition \ref{prop: A-translation}, it suffices to show the assertions only for prime formulas.
Since
$\left(\SNP{\varphi_{\rm p}}\right)^{*} \equiv {\varphi_{\rm p}}^{*} \equiv \varphi_{\rm p} \lor {*} \equiv \SNP{\varphi_{\rm p}} \lor {*}$,
we are done.

The induction step:
Assume that the items \ref{item: vp*A <-> vp* v A for vp in Sigma_k} and \ref{item: vp*A <-> vp* v A for vp in Pi_k} hold for $k$.
We first show the item 1 for $k+1$.
Let $\varphi_1\in \Pi_k$.
Since
$$\left(\SNP{\exists x \varphi_1}\right)^{*} \equiv \left( \exists x\, \SNP{\varphi_1}\right)^{*} \equiv \exists x \left(\SNP{\varphi_1}\right)^{*}, $$
by induction hypothesis, we have
$$
\mathsf{HA}^{*} + \LEM{\Sigma_k} \vdash\left(\SNP{\exists x \varphi_1}\right)^{*} \leftrightarrow \exists x \left(\SNP{\varphi_1} \lor {*} \right).$$
Since $\mathsf{HA}^{*} $ proves $\exists x \left(\SNP{\varphi_1} \lor {*} \right) \leftrightarrow \left(\exists x \, \SNP{\varphi_1} \lor {*} \right) \equiv \left( \SNP{\exists x \varphi_1 } \lor {*} \right)$,
we have
$$
\mathsf{HA}^{*} + \LEM{\Sigma_k} \vdash \left(\SNP{\exists x \varphi_1}\right)^{*} \leftrightarrow  \left( \SNP{ \exists x \varphi_1} \lor {*} \right).$$
Thus we have shown the item \ref{item: vp*A <-> vp* v A for vp in Sigma_k} for $k+1$.

Next, we show the item 2 for $k+1$.
Let $\varphi_2\in \Sigma_k$.
We shall show that $\mathsf{HA}^{*} + \DNE{\Sigma_k}$ (and hence, $\mathsf{HA}^{*} + \LEM{\Sigma_{k+1}}$) proves
$\SNP{\forall x \varphi_2} \lor {*} \to
\left( \SNP{ \forall x \varphi_2} \right)^{*} $.
By Lemma \ref{lem: equivalence of vp and vp' over semi-classical arithmetic}.\eqref{item: vp'<-> vp in Sigma_k}, we have
\begin{equation}
\label{eq: vp2 <-> NNvp_2*}
\mathsf{HA}+\DNE{\Sigma_k} \vdash \varphi_2 \leftrightarrow \left(\varphi_2 \right)^N \equiv \neg \neg \SNP{\varphi_2}.
\end{equation}
Then we have that
$\mathsf{HA}^{*} + \DNE{\Sigma_k}$ proves
$$
\SNP{\forall x \varphi_2}\lor {*} \equiv  \left(  \forall x \neg \neg \SNP{\varphi_2}  \lor {*} \right) \leftrightarrow \forall x \varphi_2 \lor {*} .
$$
By Lemma \ref{lem: vp -> vp*}, $\mathsf{HA}$ proves $\varphi_2 \to \SNP{\varphi_2}$.
Then, using induction hypothesis and the fact that $\DNE{\Sigma_{k}}$ derives $\LEM{\Sigma_{k-1}}$, we have that $\mathsf{HA}^{*} + \DNE{\Sigma_k}$ proves
$$
\begin{array}{rcl}
\SNP{\forall x \varphi_2} \lor {*}
&\underset{\DNE{\Sigma_k}}{\longleftrightarrow}& \forall x \varphi_2 \lor {*}\\
&\longrightarrow &  \forall x \SNP{\varphi_2} \lor {*}\\[2pt]
& \longrightarrow & \forall x (\SNP{\varphi_2} \lor {*})  \\[2pt]
& \underset{\text{[I.H.] }\LEM{\Sigma_{k-1}}}{\longleftrightarrow} &\forall x \left(\SNP{\varphi_2} \right)^{*}\\
& \longrightarrow & \forall x \left(\left( \left(\SNP{\varphi_2} \right)^{*} \to {*} \right) \to {*} \right)\\
&\longleftrightarrow & \left( \SNP{\forall x \varphi_2}\right)^{*} .
\end{array}
$$
In the following, we show the converse direction:
\begin{equation}
    \label{eq: the direction -> of item 2 for k+1}
\mathsf{HA}^{*} + \LEM{\Sigma_{k+1}} \vdash \left( \SNP{\forall x \varphi_2} \right)^{*}  \to \SNP{\forall x \varphi_2} \lor {*} .
\end{equation}
Reason in $\mathsf{HA}^{*} + \LEM{\Sigma_{k+1}} $.
Suppose $\left( \SNP{\forall x \varphi_2 } \right)^{*} $, equivalently, \begin{equation}
\label{eq: forall x vp2 * dollar}
\forall x \left(\left( \left(\SNP{\varphi_2} \right)^{*} \to {*} \right) \to {*} \right).
\end{equation}
By induction hypothesis,
$\eqref{eq: forall x vp2 * dollar} $ is equivalent to  $\forall x \left(\left(\SNP{\varphi_2} \lor {*}  \to {*} \right) \to {*} \right)$, which is intuitionistically equivalent to
\begin{equation*}
        \label{eq: forall x dd vp2 *}
\forall x \left(\left(\SNP{\varphi_2} \to {*} \right)\to {*} \right) .
\end{equation*}
Then we have
\begin{equation}
    \label{eq: exists x N vp2* -> d}
\exists x \neg \SNP{\varphi_2} \to {*}  .
\end{equation}
By Lemma \ref{lem: NP and NS}.\eqref{item: NS}, there exists $\psi_2 \in \Pi_k$ such that $\FV{\varphi_2}=\FV{\psi_2}$ and $\neg \varphi_2$ is equivalent to $\psi_2$.
Since $\exists x \psi_2\in \Sigma_{k+1}$, by $\LEM{\Sigma_{k+1}}$, we have
$\exists x \psi_2 \lor \neg \exists x \psi_2$, and hence, 
\begin{equation*}
\exists x \neg \varphi_2 \lor \forall x \neg \neg \varphi_2 .
\end{equation*}
Then, by \eqref{eq: vp2 <-> NNvp_2*}, we obtain
\begin{equation*}
\exists x \neg \SNP{\varphi_2} \lor \forall x \neg \neg \SNP{\varphi_2} .
\end{equation*}
In the former case, we have ${*}$ by \eqref{eq: exists x N vp2* -> d}.
In the latter case, we have $\SNP{\forall x {\varphi_2}}$.
Thus we have shown \eqref{eq: the direction -> of item 2 for k+1}.
\end{proof}

\begin{lemma}
\label{lem: basic facts on *}
Let $\varphi$ be a $\mathsf{HA}^{*} $-formula.
\begin{enumerate}
    \item 
    \label{item: vp -> ddvp}
$\mathsf{HA}^{*} \vdash \varphi \to \neg_{*} \neg_{*} \varphi$.
\item
\label{item: Advp <-> dEvp}
$\mathsf{HA}^{*} \vdash \forall x \neg_{*} \varphi \leftrightarrow \neg_{*} \exists x \varphi$.
\item
\label{item: dddvp -> dvp}
$\mathsf{HA}^{*} \vdash  \neg_{*} \neg_{*} \neg_{*} \varphi \to \neg_{*} \varphi$.
    \item
    \label{item: Eddvp -> ddEvp}
    $\mathsf{HA}^{*} \vdash \exists x \neg_{*} \neg_{*} \varphi \to \neg_{*} \neg_{*} \exists  x \varphi$.
\end{enumerate}
\end{lemma}
\begin{proof}
\eqref{item: vp -> ddvp}, \eqref{item: Advp <-> dEvp} and \eqref{item: dddvp -> dvp} are immediate from the definition of $\neg_{*} $ (see Definition \ref{def: A-translation}).
\eqref{item: Eddvp -> ddEvp} follows from \eqref{item: vp -> ddvp}, \eqref{item: Advp <-> dEvp} and \eqref{item: dddvp -> dvp}.
\end{proof}

\begin{lemma}
\label{lem: vp -> vp'A for any vp:PNF}
For any $\mathsf{HA}$-formula $\varphi$ of the prenex normal form, $\mathsf{HA}^{*} \vdash \varphi \to \left(\varphi^N \right)^{*} $.
\end{lemma}
\begin{proof}
Since there exists a closed term $t$ such that $\mathsf{HA} \vdash \QF{\varphi}(x_1, \dots, x_k) \leftrightarrow t(x_1, \dots, x_k) =0 $ for each quantifier-free formula $\QF{\varphi}$ such that $\FV{\QF{\varphi}}=\{x_1, \dots, x_k \}$ (see e.g. \cite[Proposition 3.8]{Koh08}), by Proposition \ref{Soundness of NT} and Proposition \ref{prop: A-translation},
one can assume that formulas of the prenex normal form consist of the formulas of form $Q_{1}x_1 \dots Q_{k}x_k \, \varphi_{\rm p} $ where $Q_i$s are quantifiers and $\varphi_{\rm p}$ is prime.
We show our assertion by induction on the structure of formulas of this form.

For a prime formula $\varphi_{\rm p}$, it is trivial to see that $\mathsf{HA}^{*} $ proves
$$
\varphi_{\rm p} \to \varphi_{\rm p} \lor {*} \to  \neg_{*} \neg_{*} \left(  \varphi_{\rm p} \lor {*}  \right) \leftrightarrow  \left(\left(\varphi_{\rm p}\right)^N \right)^{*}.
$$

Assume the assertion for $\varphi$.
Then, using Lemma \ref{lem: basic facts on *},
$\mathsf{HA}^{*}$ proves
$$
\begin{array}{r}
\exists x \varphi 
\underset{\text{[I.H.]}}{\longrightarrow}
\exists x \left(\varphi^N \right)^{*} 
\equiv
\exists x \left(\neg \neg \SN{\varphi} \right)^{*}
\leftrightarrow
\exists x \neg_{*} \neg_{*} \left(\SN{\varphi} \right)^{*} 
\to
\neg_{*} \neg_{*} \exists x  \left(\SN{\varphi} \right)^{*} \\
\leftrightarrow
\left(\left( \exists x \varphi \right)^N \right)^{*}
\end{array}
$$
and
$$
\begin{array}{r}
\forall x \varphi 
\underset{\text{[I.H.]}}{\longrightarrow}
\forall x \left(\varphi^N \right)^{*} 
\equiv
\forall x \left(\neg \neg \SN{\varphi} \right)^{*}
\leftrightarrow
\forall x \neg_{*} \neg_{*} \left(\SN{\varphi} \right)^{*} 
\to \neg_{*} \neg_{*} \forall x \neg_{*} \neg_{*} \left(\SN{\varphi} \right)^{*} \\
\leftrightarrow
\left(\left( \forall x \varphi \right)^N \right)^{*} .
\end{array}
$$
\end{proof}


\begin{theorem}
\label{thm: conservation results for PNF -> Pi_k+2}
Let $k$ be a natural number.
For any formulas $\varphi \in \Pi_{k+2}$ and $\psi$ of the prenex normal form, if $\mathsf{PA} \vdash \psi \to \varphi$, then $\mathsf{HA} + \LEM{\Sigma_k} \vdash \psi \to \varphi$.
\end{theorem}
\begin{proof}
Let $\varphi :\equiv \forall x \exists y \varphi_1$ where $\varphi_1\in \Pi_k$.  
Since one can freely replace the bound variables, assume that the free variables of $ \exists y \varphi_1 $ are not bounded in $\psi$ and $x$ does not occur in $\psi$ without loss of generality.

Suppose $\mathsf{PA} \vdash \psi \to \forall x \exists y \varphi_1$.
By Proposition \ref{Soundness of NT}, we have that
$\mathsf{HA}$ proves $\neg \neg (\SN{\psi} \to \forall x \neg \neg \exists y\, \SNP{\varphi_1})$, which is intuitionistically equivalent to $\neg \neg \SN{\psi} \to  \forall x  \neg \neg \exists y\, \SNP{\varphi_1}$, namely, $\psi^N \to  \forall x  \neg \neg \exists y \, \SNP{\varphi_1}$.
Then we have
$$
\mathsf{HA} \vdash \psi^N \to   \neg \neg \exists y \, \SNP{\varphi_1} .
$$
By Proposition \ref{prop: A-translation}, we have
$$
\mathsf{HA}^{*} \vdash \left(\psi^N\right)^{*} \to   \neg_{*} \neg_{*} \exists y \left( \SNP{\varphi_1}\right)^{*} ,
$$
and hence,
$$
\mathsf{HA}^{*} \vdash \psi \to  \neg_{*} \neg_{*} \exists y \left( \SNP{\varphi_1}\right)^{*}
$$
by Lemma \ref{lem: vp -> vp'A for any vp:PNF}.
Then, by Lemma \ref{lem: key lemma on vp*A in semi-classical arithemtic}.\eqref{item: vp*A <-> vp* v A for vp in Pi_k}, we have that
$\mathsf{HA}^{*} +\LEM{\Sigma_k} $ proves
$$\psi \to  \neg_{*} \neg_{*} \exists y \left( \SNP{\varphi_1} \lor {*} \right),$$
 which is intuitionistically equivalent to 
 $$\psi \to  \neg_{*} \neg_{*} \exists y \, \SNP{\varphi_1} .$$
Since the free variables of $ \exists y \varphi_1 $ are not bounded in $\psi$, using Lemma \ref{lem: Substitution} with Remark \ref{rem: NT preserving FVs}, we have
 \begin{equation}
\label{eq: cons afrer applying A-translation}
\mathsf{HA} +\LEM{\Sigma_k} \vdash \psi \to \left( (\exists y \, \SNP{\varphi_1} \to \exists y \varphi_1) \to \exists y \varphi_1\right).
 \end{equation}
On the other hand, by Lemma \ref{lem: equivalence of vp and vp' over semi-classical arithmetic}.\eqref{item: vp'<-> vp in Pi_k} and the fact that $ \LEM{\Sigma_k}$ derives $\DNE{\Sigma_k}$, we have that $\mathsf{HA} +\LEM{\Sigma_k}$ proves
\begin{equation*}
\label{eq: HA + Sk-1-DNE |- vp* -> vp}
 \SNP{\varphi_1} \to \neg \neg \SNP{\varphi_1} \equiv \left(\varphi_1\right)^N \underset{ \DNE{\Sigma_{k-1}}}{\longleftrightarrow}  \varphi_1.
\end{equation*}
and hence, $\exists y \, \SNP{\varphi_1} \to \exists y \varphi_1$.
Then, by \eqref{eq: cons afrer applying A-translation}, we have $\mathsf{HA} +\LEM{\Sigma_k} \vdash \psi \to \exists y \varphi_1$.
By our assumption, $x$ does not occur in $\psi$, and hence, $\mathsf{HA} +\LEM{\Sigma_k} \vdash \psi \to \forall x \exists y \varphi_1 $ follows.
\end{proof}

We have shown Theorem \ref{thm: conservation results for PNF -> Pi_k+2} in order to prove the optimality of our prenex normal form theorems in Section \ref{sec: PNFT} (see Section \ref{sec: Optimality}).
On the other hand, the conservation result on semi-classical arithmetic itself is interesting.
This will be studied comprehensively in \cite{FK20-2}.








\section{Characterizations}\label{sec: Optimality}
\begin{notation}
Let ${T} $ be an extension of $\mathsf{HA}$.
Let $\Gamma$ and $\Gamma'$ be classes of $\mathsf{HA}$-formulas.

  Then  $\PNFT{\Gamma}{\Gamma'} $ denotes the following statement:
  for any $\varphi \in \Gamma$, there exists $\varphi' \in \Gamma'$ such that $\FV{\varphi}=\FV{\varphi'}$ and
    ${T}  \vdash \varphi \leftrightarrow \varphi' $.
\end{notation}

Under this notation, Theorem \ref{thm: PNFT} asserts (modulo Remark \ref{rem: sigma_k and pi_k}) that

for a semi-classical theory $T$ containing 

$\mathsf{HA} +  \DNE{(\Pi_k\lor \Pi_k)} $, 
$\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ 
holds for all $k' \leq k$ as well as the analogous assertion for $\mathrm{E}_k$ and $\Sigma_k$.
It is natural to ask whether the verification theories
are optimal.
In this section, among other things (see Table \ref{table: PNFT}), we show that this is exactly the case:
\begin{enumerate}
    \item 
    For a theory ${T}$ in-between $\mathsf{HA} $ and $\mathsf{PA}$,
 ${T} \vdash \DNE{(\Pi_k\lor \Pi_k)}$ if and only if $\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ for all $k' \leq k$. (Theorem \ref{thm: characterization of PNFT(Ukp,Pk)})
\item
 For a theory ${T}$ in-between $\mathsf{HA} +\LEM{\Pi_{k-1}} $ ($\mathsf{HA}$ if $k=0$) and $\mathsf{PA}$,
 ${T} \vdash \DNE{\Sigma_k} + \DNS{\mathrm{U}_k^+} $ if and only if $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$ for all $k' \leq k$.
 (Theorem \ref{thm: characterization of PNFT(Ek,Sk)})
\end{enumerate}




\begin{lemma}
\label{lem: PNFT(Uk, Ok) + Sk-1-LEM => PkPk-DNE}
Let ${T} $ be a theory in-between $\mathsf{HA} +\LEM{\Sigma_{k-2}}\, (\mathsf{HA}$ if $k<2)$ and $\mathsf{PA}$.
If $\PNFT{\mathrm{U}_{k}}{\Pi_{k}}$, then ${T} \vdash \DNE{(\Pi_{k}\lor \Pi_{k})}$.
\end{lemma}
\begin{proof}
Fix an instance of $\DNE{(\Pi_{k}\lor \Pi_{k})}$
$$
\varphi :\equiv \forall x \left(\neg\neg \left(\varphi_1(x) \lor \varphi_2(x) \right) \to \varphi_1(x) \lor \varphi_2(x)  \right),
$$
where $\varphi_1(x), \varphi_2(x) \in \Pi_{k}(x)$.
Since $\neg\neg \left(\varphi_1(x) \lor \varphi_2(x) \right) $ and $ \varphi_1(x) \lor \varphi_2(x)$ are in $\mathrm{U}_{k}$, by our assumption, there exist $\rho(x)$ and $\rho'(x)$ in $\Pi_{k}(x)$ such that
${T} $ proves $ \rho(x) \leftrightarrow \varphi_1(x) \lor \varphi_2(x) $  and $\rho'(x) \leftrightarrow \neg \neg \left(\varphi_1(x) \lor \varphi_2(x)\right) $.
Since $\mathsf{PA} \vdash \varphi$ and $\mathsf{PA}$ is an extension of ${T}$, we have $\mathsf{PA} \vdash  \rho'(x) \to \rho(x) $.
By Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have that $\mathsf{HA} +\LEM{\Sigma_{k-2}}$ proves $\rho'(x) \to \rho(x)$, and hence, $\forall x\left(
\rho'(x) \to \rho(x) \right)$.
Since ${T}$ is an extension of $\mathsf{HA} + \LEM{\Sigma_{k-2}}$, we have ${T} \vdash \forall x\left(\rho'(x) \to \rho(x) \right)$, and hence, ${T} \vdash \varphi$.
\end{proof}


\begin{lemma}
\label{lem: PNFT(Uk, Pk)=>Sk-1-LEM}
Let ${T} $ be a theory in-between $\mathsf{HA} $ and $\mathsf{PA}$.
If $\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ for all $k' \leq k$, then ${T} \vdash \LEM{\Sigma_{k-1}}$.
\end{lemma}
\begin{proof}
By induction on $k$.
The base case is trivial.
For the induction step, assume $\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ for all $k' \leq k+1$.
Then, by induction hypothesis, we have  ${T} \vdash \LEM{\Sigma_{k-1}}$.
Fix an instance of $\LEM{\Sigma_{k}}$
$$
\varphi :\equiv \forall x (\varphi_1(x) \lor \neg \varphi_1(x)),
$$
where $\varphi_1(x) \in \Sigma_{k}(x)$.
Since $\varphi \in \mathrm{U}_{k+2}$, by our assumption, there exists a sentence $\varphi' \in \Pi_{k+1}$ such that
${T} \vdash \varphi \leftrightarrow \varphi'$.
Since $\mathsf{PA} \vdash \varphi$, we have $\mathsf{PA} \vdash \varphi'$.
Then, by Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have $\mathsf{HA} + \LEM{\Sigma_{k-1}} \vdash \varphi'$, and hence, ${T} \vdash \varphi'$.
Thus we have ${T} \vdash \varphi$.
\end{proof}


\begin{theorem}
\label{thm: characterization of PNFT(Ukp,Pk)}
Let ${T} $ be a theory in-between $\mathsf{HA} $ and $\mathsf{PA}$.
Then ${T} \vdash \DNE{(\Pi_k\lor \Pi_k)}$ if and only if $\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ for all $k' \leq k$.
\end{theorem}
\begin{proof}
The ``only if'' direction is immediate from Theorem \ref{thm: PNFT}.\eqref{eq: item for Pi_k in PNFT} and Lemma \ref{lem: sigma_k and pi_k}.
We show the converse direction.
Assume $\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ for all $k' \leq k$.
Let $k>0$ without loss of generality. 
By Lemma \ref{lem: PNFT(Uk, Pk)=>Sk-1-LEM}, ${T} \vdash \LEM{\Sigma_{k-1}}$.
Then, by Lemma \ref{lem: PNFT(Uk, Ok) + Sk-1-LEM => PkPk-DNE}, we have ${T} \vdash \DNE{(\Pi_k\lor \Pi_k)} $.
\end{proof}

\begin{definition}
Let $\Gamma$ be a class of formulas.
Then $\dn{\Gamma}$ denotes the class of $\mathsf{HA}$-formulas $\neg \neg \varphi$ where $\varphi \in \Gamma$, and  $\n{\Gamma}$ denotes that for $\neg \varphi$ where $\varphi \in \Gamma$.
\end{definition}

\begin{comment}
========================= Cut? ==================================
\begin{lemma}
\label{lem: PNFT(NNUk, NNPk) + NNSk-1-LEM => Uk-DNS}
Let ${T} $ be a theory in-between $\mathsf{HA} + \NN{\DNE{\Sigma_k}} $ and $\mathsf{PA}$.
If $\PNFT{\dn{\mathrm{U}_{k+1}}}{\dn{\Pi_{k+1}}}$, then ${T} \vdash \DNS{\mathrm{U}_{k+1}}$.
\end{lemma}
\begin{proof}
Since $\DNS{\mathrm{U}_{k+1}}$ is intuitionistically equivalent to $\NN{\DNS{\mathrm{U}_{k+1}}}$ (See Remark \ref{rem: NNDNS <-> DNS}), it suffices to show ${T} \vdash \NN{\DNS{\mathrm{U}_{k+1}}}$.
Fix an instance of $\NN{\DNS{\mathrm{U}_{k+1}}}$
$$
\varphi :\equiv \neg \neg \forall x \left(\forall y \neg \neg \varphi_1(x,y)  \to \neg \neg \forall y \varphi_1(x,y)  \right),
$$
where $\varphi_1(x, y) \in \mathrm{U}_{k+1}(x,y)$.
Since  $ \neg \neg \forall y \varphi_1(x,y)\in \mathrm{U}_{k+1}(x)$ and  $ \neg \neg \varphi_1(x,y) \in \mathrm{U}_{k+1}(x,y)$, by our assumption, there exist $\rho(x)\in \Pi_{k+1}(x)$ and $\rho'(x,y)\in \Pi_{k+1}(x,y)$ such that
${T} $ proves $\neg \neg \rho(x) \leftrightarrow \neg \neg \forall y \varphi_1(x,y)  $ and  $\neg \neg \rho'(x,y) \leftrightarrow \neg \neg \varphi_1(x,y) $.
Let $\psi :\equiv \forall x \left( \forall y \rho'(x,y) \to \rho(x)
\right)$.
Since $\mathsf{PA}$ is an extension of ${T}$ and $\mathsf{PA} \vdash \varphi$, we have $\mathsf{PA} \vdash \forall y \rho'(x,y) \to \rho(x)$.
Then, by Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have
that $\mathsf{HA} + \LEM{\Sigma_{k-1}}$ proves $\forall y \rho'(x,y) \to \rho(x)$, and hence, $\psi$.
By Lemma \ref{lem: HA+P |- vp => HA+NNP |- NNvp}, we have
$\mathsf{HA} + \NN{\LEM{\Sigma_{k-1}}} \vdash \neg \neg \psi$.
On the other hand, by Lemma \ref{lem: k -> k-1}.\eqref{item: sk-DNE -> pk+1-DNE}, we have $\mathsf{HA} +\DNE{\Sigma_k} \vdash \forall x,y (\rho'(x,y) \leftrightarrow \neg \neg \rho'(x,y))$,
Then, by Lemma \ref{lem: HA+P |- vp => HA+NNP |- NNvp}, we have  $\mathsf{HA} +\NN{\DNE{\Sigma_k}} \vdash \neg \neg \forall x,y (\rho'(x,y) \leftrightarrow \neg \neg \rho'(x,y))$.
Since $\DNE{\Sigma_k}$ implies $\LEM{\Sigma_{k-1}}$ (cf. \cite[Theorem 3.1.(i)]{ABHK04}), we have $\mathsf{HA} + \NN{\DNE{\Sigma_k}} 
\vdash
\neg \neg \forall x \left(
\forall y \neg \neg  \rho'(x,y) \to \neg\neg  \rho(x)
\right)$.
Since ${T}$ is an extension of $\mathsf{HA} + \NN{\DNE{\Sigma_k}} $,
we have ${T} \vdash \varphi$.
\end{proof}
========================= Cut? ==================================
\end{comment}

\begin{lemma}
\label{lem: PNFT(NNUk, NNPk)=>NNSk-1-LEM}
Let ${T} $ be a theory in-between $\mathsf{HA} $ and $\mathsf{PA}$.
If $\PNFT{\dn{\mathrm{U}_{k'}}}{\dn{\Pi_{k'}}}$ for all $k' \leq k$, then ${T} \vdash \NN{\LEM{\Sigma_{k-1}}}$.
\end{lemma}
\begin{proof}
By induction on $k$.
The base case is trivial.
For the induction step, assume $\PNFT{\dn{\mathrm{U}_{k'}}}{\dn{\Pi_{k'}}}$ for all $k' \leq k+1$.
Then, by induction hypothesis, ${T}$ proves $\NN{\LEM{\Sigma_{k-1}}}$.
Fix an instance of $\NN{\LEM{\Sigma_{k}}}$
$$
\varphi :\equiv \neg \neg \forall x (\varphi_1(x) \lor \neg \varphi_1(x)),
$$
where $\varphi_1(x) \in \Sigma_{k}(x)$.
Since $\varphi \in \dn{\mathrm{U}_{k+1}}$, by our assumption, there exists a sentence $\varphi' \in \Pi_{k+1}$ such that
${T} \vdash \varphi \leftrightarrow \neg \neg \varphi'$.
Since $\mathsf{PA} \vdash \forall x (\varphi_1(x) \lor \neg \varphi_1(x))$, we have $\mathsf{PA} \vdash \varphi'$.
Then, by Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have $\mathsf{HA} + \LEM{\Sigma_{k-1}} \vdash \varphi'$, and hence, $\mathsf{HA} + \NN{\LEM{\Sigma_{k-1}}} \vdash \neg\neg \varphi'$ by Lemma \ref{lem: HA+P |- vp => HA+NNP |- NNvp}.
Then ${T} \vdash \varphi$.
\end{proof}

\begin{theorem}
\label{thm: characterization of PNFT(NNUkp,NNPk)}
Let ${T} $ be a theory in-between $\mathsf{HA} $ and $\mathsf{PA}$.
The following are pairwise equivalent:
\begin{enumerate}
    \item 
    \label{item: PNFT(NEk. NNPk)}
    $\PNFT{\n{\mathrm{E}_{k'}}}{ \dn{\Pi_{k'}}}$ for all $k' \leq k$;
    \item
        \label{item: PNFT(NNUk. NNPk)}
    $\PNFT{\dn{\mathrm{U}_{k'}}}{ \dn{\Pi_{k'}}}$ for all $k' \leq k$;
 

    \item
    \label{item: T|-Ukp-DNS}
    ${T} \vdash  \DNS{\mathrm{U}_k^+}$.
\end{enumerate}
\end{theorem}
\begin{proof}
The equivalence of \eqref{item: PNFT(NEk. NNPk)} and \eqref{item: PNFT(NNUk. NNPk)} is trivial (cf. the proof of Lemma \ref{PNFT_of_NE_k_and_NNU_k}).
In addition, $(\ref{item: T|-Ukp-DNS} \to \ref{item: PNFT(NNUk. NNPk)})$ is immediate from Lemma \ref{PNFT_of_NE_k_and_NNU_k}.
In what follows, we show $(\ref{item: PNFT(NNUk. NNPk)} \to \ref{item: T|-Ukp-DNS})$.
Assume $\PNFT{\dn{\mathrm{U}_{k'}}}{\dn{\Pi_{k'}}}$ for all $k' \leq k$.
Since $\DNS{\mathrm{U}_{k}^+}$ is intuitionistically equivalent to $\NN{\DNS{\mathrm{U}_{k}^+}}$ (See Remark \ref{rem: NNDNS <-> DNS}), it suffices to show ${T} \vdash \NN{\DNS{\mathrm{U}_{k}^+}}$.
Let $k>0$ without loss of generality. 
Fix an instance of $\NN{\DNS{\mathrm{U}_k^+}}$
$$\varphi :\equiv \neg \neg \forall x \left( \forall y \neg \neg \varphi_1(x,y) \to  \neg \neg \forall y  \varphi_1(x,y)  \right)$$
where $\varphi_1(x,y)\in \mathrm{U}_k^+(x,y)$.
By  Lemma \ref{lem: basic facts on our classes}, we have that $\forall y\neg \neg \varphi_1(x,y)$ and  $\forall y\varphi_1(x,y)$ are in $\mathrm{U}_k^+(x)$.
Since $i(s) \equiv -$ for all alternation paths $s$ of $\forall y\neg \neg \varphi_1(x,y)$ and $\forall y \varphi_1(x,y)$, it is straightforward to show that there exists $k'\leq k$ such that $\forall y\neg \neg \varphi_1(x,y)$ and  $\forall y\varphi_1(x,y)$ are in $\mathrm{U}_{k'}(x)$.
Then, by $\PNFT{\dn{\mathrm{U}_{k'}}}{ \dn{\Pi_{k'}}}$,
there exist $\rho(x), \rho'(x)\in \Pi_{k'}(x)$
such that
${T} $ proves  $\neg \neg \rho(x) \leftrightarrow \neg \neg \forall y \varphi_1(x,y) $ and  $\neg \neg \rho'(x) \leftrightarrow \neg \neg \forall y \neg \neg \varphi_1(x,y) $.
Since $\mathsf{PA}$ is an extension of ${T}$ and $\mathsf{PA} \vdash \varphi$, we have $\mathsf{PA} \vdash \rho'(x) \to \rho(x)$.
Then, by Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have
that $\mathsf{HA} + \LEM{\Sigma_{k'-2}} \, (\mathsf{HA}$ if $k'<2)$ proves $\rho'(x) \to \rho(x)$, and hence, $\forall x \left( \neg \neg \rho'(x) \to \neg \neg \rho(x) \right)$.
By Lemma \ref{lem: HA+P |- vp => HA+NNP |- NNvp}, we have
\begin{equation*}
\label{eq: HA+NNSk'-2 |- psi}
\mathsf{HA} + \NN{\LEM{\Sigma_{k'-2}}} \vdash \neg \neg \forall x \left( \neg \neg \rho'(x) \to \neg \neg \rho(x) \right) .   
\end{equation*}
On the other hand,
by Lemma \ref{lem: PNFT(NNUk, NNPk)=>NNSk-1-LEM} and our assumption, we have

${T} \vdash \NN{\LEM{\Sigma_{k-1}}}$.
Then we have
$$
{T} \vdash \neg \neg \forall x \left( \neg \neg \forall y \neg \neg \varphi_1(x,y) \to \neg \neg \forall y \varphi_1(x,y)
\right),
$$
and hence, ${T} \vdash \varphi$.
\end{proof}

\begin{remark}
Theorem \ref{thm: characterization of PNFT(NNUkp,NNPk)} shows that the verification theory for Lemma \ref{PNFT_of_NE_k_and_NNU_k} is optimal.
\end{remark}


\begin{definition}\label{def: Gamma-v}
Let $\Gamma$ be a class of $\mathsf{HA}$-formulas.
$\df{\Gamma}$ denotes the class of formulas in $\Gamma$ which do not contain $\lor$.
\end{definition}

\begin{lemma}
\label{lem: PNFT(Ekm, Sk) + Pk-1-LEM => Sk-DNE}
Let ${T} $ be a theory in-between $\mathsf{HA} +\LEM{\Pi_{k-1}} $ $(\mathsf{HA}$ if $k=0)$ and $\mathsf{PA}$.
If $\PNFT{\df{\mathrm{E}_{k'}}}{\Sigma_{k'}}$ for all $k' \leq k$, then ${T} \vdash \DNE{\Sigma_{k}}$.
\end{lemma}
\begin{proof}
By induction on $k$.
The base case is trivial.
For the induction step, assume the assertion for $k$ and let ${T}$ be a theory in-between $\mathsf{HA} +\LEM{\Pi_{k}}$ and $\mathsf{PA}$.
Assume also that $\PNFT{\df{\mathrm{E}_{k'}}}{\Sigma_{k'}}$ holds for all $k' \leq k+1$.
Then, by induction hypothesis, ${T}$ proves $\DNE{\Sigma_{k}}$.
Since ${T}$ contains $\mathsf{HA} +\LEM{\Pi_{k}},$ we have ${T} \vdash \LEM{\Sigma_{k}}$ by \cite[Theorem 3.1(ii)]{ABHK04}.
Fix an instance of $\DNE{\Sigma_{k+1}}$
$$
\varphi :\equiv \forall x ( \neg \neg \varphi_1(x) \to \varphi_1(x)),
$$
where $\varphi_1(x) \in \Sigma_{k+1}(x)$.
Without loss of generality, one can assume that $\varphi_1(x)$ does not contain $\lor$ (cf. \cite[Proposition 3.8]{Koh08}).
Since $\neg \neg \varphi_1(x)\in \df{\mathrm{E}_{k+1}}$, 
By $\PNFT{\df{\mathrm{E}_{k+1}}}{\Sigma_{k+1}}$, there exists $\varphi_1'(x) \in \Sigma_{k+1}(x)$ such that ${T} \vdash \neg \neg \varphi_1(x) \leftrightarrow \varphi_1' (x)$.
Since $\mathsf{PA}$ is an extension of ${T}$ and $\mathsf{PA} \vdash \varphi$, we have $\mathsf{PA} \vdash \varphi_1' (x) \to \varphi_1(x)$.
Then, by Lemma \ref{lem: sigma_k and pi_k} and Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have that
$\mathsf{HA} + \LEM{\Sigma_{k}} $ proves $ \varphi_1' (x) \to \varphi_1(x)$, and hence, 
$\forall x \left(
\varphi_1' (x) \to \varphi_1(x)
\right)$.
Since ${T}$ is an extension of $\mathsf{HA}  + \LEM{\Sigma_{k}}$, we have ${T} \vdash \varphi$.
\end{proof}

\begin{lemma}
\label{lem: PNFT(Ek,Sk) + Pk-1-LEM => PNFT(NEk, NNSk)}
Let ${T} $ be an extension of $\mathsf{HA} + \NN{\DNE{\Sigma_{k-1}}} $ $(\mathsf{HA}$ if $k=0)$.
If $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$ for all $k' \leq k$, then $\PNFT{\n{\mathrm{E}_{k'}}}{\dn{\Pi_{k'}}}$ for all $k' \leq k$.
\end{lemma}
\begin{proof}
Assume $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$ for all $k' \leq k$.
Fix $k' \leq k$ and
$\varphi \in \mathrm{E}_{k'}$.
By $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$, there exists $\varphi'\in \Sigma_{k'}$ such that $\FV{\varphi} = \FV{\varphi'}$ and ${T} \vdash \varphi \leftrightarrow \varphi'$.
Then
\begin{equation*}
\label{eq: vp <-> vp'}
{T} \vdash \neg \varphi \leftrightarrow \neg \varphi'.
\end{equation*}
On the other hand, by Lemma \ref{lem: NP and NS}.\eqref{item: NS}, there exists $\varphi'' \in \Pi_{k'}$ such that  $\FV{\varphi'} = \FV{\varphi''}$ and $\mathsf{HA} + \DNE{\Sigma_{k'-1}} \vdash \neg \varphi' \leftrightarrow \varphi''$.
Then, by Corollary \ref{cor: HA+P |- vp_1 <-> vp_2 => HA+NNP |- NNvp_1 <-> NNvp_2}, we have
\begin{equation*}
\label{eq: nvp' <-> nnvp'}
\mathsf{HA} + \NN{\DNE{\Sigma_{k'-1}}} \vdash \neg \varphi' \leftrightarrow \neg \neg \varphi'' .
\end{equation*}
Then $\FV{\neg \varphi} =\FV{\neg \neg \varphi''}$ and ${T} \vdash \neg \varphi \leftrightarrow \neg \neg \varphi''$.
Thus we have shown $\PNFT{\n{\mathrm{E}_{k'}}}{\dn{\Sigma_{k'}}}$.
\end{proof}

\begin{theorem}
\label{thm: characterization of PNFT(Ek,Sk)}
Let ${T} $ be a theory in-between $\mathsf{HA} + \LEM{\Pi_{k-1}}$ $(\mathsf{HA}$ if $k=0)$ and $\mathsf{PA}$.
Then ${T} \vdash \DNE{\Sigma_k} + \DNS{\mathrm{U}_k^+}$ if and only if $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$ for all $k' \leq k$.
\end{theorem}
\begin{proof}
The ``only if'' direction is immediate from Theorem \ref{thm: PNFT}.\eqref{eq: item for Sigma_k in PNFT} and Lemma \ref{lem: sigma_k and pi_k}.
We show the converse direction.
Assume $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$ for all $k' \leq k$.
Let $k>0$ without loss of generality. 
By Lemma \ref{lem: PNFT(Ekm, Sk) + Pk-1-LEM => Sk-DNE}, we have ${T} \vdash \DNE{\Sigma_{k}}$.
In addition, by Lemma \ref{lem: PNFT(Ek,Sk) + Pk-1-LEM => PNFT(NEk, NNSk)} and Theorem \ref{thm: characterization of PNFT(NNUkp,NNPk)}, we have ${T} \vdash  \DNS{\mathrm{U}_k^+}$.
\end{proof}

\begin{remark}
It is still open whether the assumption that ${T}$ contains $\LEM{\Pi_{k-1}}$ can be omitted in Theorem \ref{thm: characterization of PNFT(Ek,Sk)}.
\end{remark}



\begin{remark}
\label{rem: impossibility of PNFT}
Akama et al. \cite{ABHK04} shows that $\LEM{\Pi_k}$ does not derive $\DNE{\Sigma_k} $ and $\DNE{\Sigma_k}$  does not derive $\DNE{(\Pi_k \lor \Pi_k)}$.
Theorem \ref{thm: characterization of PNFT(Ek,Sk)} reveals that the prenex normal form theorem for $\mathrm{E}_k$ and $\Sigma_k$ does not hold in $\mathsf{HA} + \LEM{\Pi_k}$, and Theorem \ref{thm: characterization of PNFT(Ukp,Pk)} reveals that the prenex normal form theorem for $\mathrm{U}_k$ and $\Pi_k$ does not hold in $\mathsf{HA} + \DNE{\Sigma_k}$.
\end{remark}

\begin{corollary}
\label{cor: characterization of PNFT(Ek,Sk)+PNFT(Uk,Pk)}
Let ${T} $ be a theory in-between $\mathsf{HA} $
and $\mathsf{PA}$.
Then ${T} \vdash \DNE{\Sigma_k} + \DNE{\left( \Pi_k \lor \Pi_k \right)}$ if and only if $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$ and $\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ for all $k' \leq k$.
\end{corollary}
\begin{proof}
Let ${T} $ be a theory in-between $\mathsf{HA} $
and $\mathsf{PA}$.
The ``only if'' direction follows from Theorem \ref{thm: PNFT}, Corollary \ref{cor: pk v pk -DNE -> Ukp-DNE} and Lemma \ref{lem: sigma_k and pi_k}.

For the converse direction, assume that $\PNFT{\mathrm{E}_{k'}}{\Sigma_{k'}}$ and $\PNFT{\mathrm{U}_{k'}}{\Pi_{k'}}$ hold for all $k' \leq k$.
By Theorems \ref{thm: characterization of PNFT(Ukp,Pk)}, we have ${T} \vdash \DNE{\left( \Pi_k \lor \Pi_k \right)}$.
Since $\LEM{\Pi_{k-1}}$ is derived from $ \DNE{\left( \Pi_k \lor \Pi_k \right)}$ (cf. \cite[Theorem 3.1(1)]{ABHK04}), by Theorem \ref{thm: characterization of PNFT(Ek,Sk)}, we also have ${T} \vdash \DNE{\Sigma_k}$.
\end{proof}


In the following, we show the optimality of Theorem \ref{thm: PNFT for df-formulas} (see Theorem \ref{thm: Optimality of PNFT for df-formulas}).


\begin{lemma}\label{lem: PNFT(NNUkm, Pk) + Pk-2-LEM => Sk-1-DNE}
Let ${T} $ be a theory in-between $\mathsf{HA} +\LEM{\Pi_{k-2}} $ $(\mathsf{HA}$ if $k<2)$ and $\mathsf{PA}$.
If $\PNFT{\df{\left(\dn{\mathrm{U}_{k'}}\right)}}{\Pi_{k'}}$ for all $k' \leq k$, then ${T} \vdash \DNE{\Sigma_{k-1}}$.
\end{lemma}
\begin{proof}
By induction on $k$.
The base case is trivial.
For the induction step, assume the assertion for $k$ and let ${T}$ be a theory in-between $\mathsf{HA} +\LEM{\Pi_{k-1}}$ and $\mathsf{PA}$.
Assume also that $\PNFT{\df{\left(\dn{\mathrm{U}_{k'}}\right)}}{\Pi_{k'}}$ holds for all $k' \leq k+1$.
Then, by induction hypothesis, ${T}$ proves $\DNE{\Sigma_{k-1}}$.
Since ${T}$ contains $\mathsf{HA} +\LEM{\Pi_{k-1}},$ we have ${T} \vdash \LEM{\Sigma_{k-1}}$ by \cite[Theorem 3.1(ii)]{ABHK04}.
Fix an instance of $\DNE{\Sigma_{k}}$
$$
\varphi :\equiv \forall x ( \neg \neg \varphi_1(x) \to \varphi_1(x)),
$$
where $\varphi_1(x) \in \Sigma_{k} (x)$.
Without loss of generality, one can assume that $\varphi_1(x)$ does not contain $\lor$ (cf. \cite[Proposition 3.8]{Koh08}).
From  the  perspective  of  Remark \ref{rem: identification on Sigma_k and Pi_k},  $\varphi_1(x)$ is in $\Pi_{k+1} (x)$.
Then, by $\PNFT{\df{\left(\dn{\mathrm{U}_{k+1}}\right)}}{\Pi_{k+1}}$, there exists $\varphi_1'(x)\in \Pi_{k}(x)$ such that ${T} \vdash \neg \neg \varphi_1(x) \leftrightarrow \varphi_1' (x)$.
Since $\mathsf{PA}$ is an extension of ${T}$ and $\mathsf{PA} \vdash \varphi $, we have $\mathsf{PA} \vdash  \varphi_1' (x) \to \varphi_1(x)$.
By Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have that
$\mathsf{HA} + \LEM{\Sigma_{k-1}}$ proves  $\varphi_1' (x) \to \varphi_1(x)$, and hence,
$\forall x \left( \varphi_1' (x) \to \varphi_1(x) \right)$.
Since ${T}$ is an extension of $\mathsf{HA} + \LEM{\Sigma_{k-1}}$, we have
$T \vdash \varphi$.
\end{proof}


\begin{theorem}
\label{thm: Optimality of PNFT for df-formulas}
\noindent
\begin{enumerate}
    \item 
        \label{item: Characterization of PNFT(E_k^df, Sigmak)}
    Let ${T} $ be a theory in-between $\mathsf{HA} + \LEM{\Pi_{k-1}}$ $(\mathsf{HA}$ if $k=0)$ 
and $\mathsf{PA}$.
Then ${T} \vdash \DNE{\Sigma_k}$  if and only if $\PNFT{\df{\mathrm{E}_{k'}}}{\Sigma_{k'}}$ for all $k' \leq k$.
    \item
    \label{item: Characterization of PNFT(U_k^df, Pik)}
   Let ${T} $ be a theory in-between $\mathsf{HA} + \LEM{\Pi_{k-2}}$ $(\mathsf{HA}$ if $k<2)$ 
and $\mathsf{PA}$.
Then ${T} \vdash \DNE{\Sigma_{k-1}}$  if and only if $\PNFT{\df{\mathrm{U}_{k'}}}{\Pi_{k'}}$ for all $k' \leq k$.
\end{enumerate}
\end{theorem}
\begin{proof}
\eqref{item: Characterization of PNFT(E_k^df, Sigmak)}:
The ``only if'' direction is by Theorem \ref{thm: PNFT for df-formulas}.\eqref{item: Characterization of PNFT(E_k^df, Sigmak)}.
The converse direction is by Lemma \ref{lem: PNFT(Ekm, Sk) + Pk-1-LEM => Sk-DNE}.
 
\eqref{item: Characterization of PNFT(U_k^df, Pik)}:
The ``only if'' direction is by Theorem \ref{thm: PNFT for df-formulas}.\eqref{item: Characterization of PNFT(U_k^df, Pik)}.
Note that any formula in $\df{\left(\dn{\mathrm{U}_{k'}}\right)}$ is in $\df{\mathrm{U}_{k'}}$.
Then the converse direction follows from Lemma \ref{lem: PNFT(NNUkm, Pk) + Pk-2-LEM => Sk-1-DNE}.
\end{proof}


At the end of this section, we characterize some variants of prenex normal form theorems.


\begin{theorem}
\label{thm: characterization of PNFT(NEk,Pk)}
Let ${T} $ be a theory in-between $\mathsf{HA} + \LEM{\Pi_{k-2}}$ $(\mathsf{HA}$ if $k<2)$ and $\mathsf{PA}$.
Then ${T} \vdash \DNE{\Sigma_{k-1}} +\DNS{\mathrm{U}_k^+}$ if and only if $\PNFT{\dn{\mathrm{U}_{k'}}}{\Pi_{k'}}$ for all $k' \leq k$.
\end{theorem}
\begin{proof}
We first show the ``only if'' direction.
Let $k>0$ without loss of generality.
Assume ${T} \vdash \DNE{\Sigma_{k-1}} +\DNS{\mathrm{U}_k^+}$ and fix $k' \leq k$.
Since ${T} \vdash \DNS{\mathrm{U}_{k'}^+}$, by Lemma \ref{PNFT_of_NE_k_and_NNU_k}, for any $\varphi \in \mathrm{U}_{k'}^+$, there exists $\varphi'\in \Pi_{k'}$ such that $\FV{\varphi} = \FV{\varphi'}$ and
$$
{T} \vdash \neg \neg \varphi \leftrightarrow \neg \neg \varphi' .
$$
Since ${T} \vdash \DNE{\Sigma_{k-1}}$, by Lemma \ref{lem: k -> k-1}.\eqref{item: sk-DNE -> pk+1-DNE}, we have $T \vdash  \neg \neg  \varphi' \leftrightarrow \varphi'$, and hence, $T \vdash  \neg \neg  \varphi \leftrightarrow \varphi'$.
Thus we have $\PNFT{\dn{\mathrm{U}_{k'}}}{\Pi_{k'}}$.

Next, we show the converse direction.
Assume that $\PNFT{\dn{\mathrm{U}_{k'}}}{\Pi_{k'}}$ holds for all $k' \leq k$.
By Lemma \ref{lem: PNFT(NNUkm, Pk) + Pk-2-LEM => Sk-1-DNE}, we have ${T} \vdash \DNE{\Sigma_{k-1}}$.
\begin{comment}
by induction on $k$.
The base case is trivial.
For the induction step, assume the assertion for $k$ to show that for $k+1$.
Assume that ${T}$ is a theory in-between $\mathsf{HA} + \LEM{\Pi_{k-1}}$ and $\mathsf{PA}$, and $\PNFT{\dn{\mathrm{U}_{k'}}}{\Pi_{k'}}$ holds for all $k' \leq k+1$.
We first show ${T} \vdash \DNE{\Sigma_{k}}$.
By induction hypothesis, we have ${T} \vdash \DNE{\Sigma_{k-1}}$.
Since $T$ contains $\LEM{\Pi_{k-1}}$, by \cite[Theorem 3.1.(ii)]{ABHK04}, we have ${T} \vdash \LEM{\Sigma_{k-1}}$.
Fix an instance of $\DNE{\Sigma_k}$
$$
\varphi :\equiv \forall x (\neg \neg \varphi_1(x) \to \varphi_1(x))
$$
where $ \varphi_1(x) \in \Sigma_k(x)$.
From the perspective of Remark \ref{rem: identification on Sigma_k and Pi_k}, $ \varphi_1(x)$ is in $\Pi_{k+1}(x)$.
Then, by 
$\PNFT{\dn{\mathrm{U}_{k+1}}}{\Pi_{k+1}}$, there exists $\varphi_1'(x)\in \Pi_{k+1}(x)$ such that ${T} \vdash \neg \neg \varphi_1(x) \leftrightarrow \varphi_1' (x)$.
Since $\mathsf{PA}$ is an extension of ${T}$ and $\mathsf{PA} \vdash \neg \neg \varphi_1(x) \to \varphi_1(x)$, we have $\mathsf{PA} \vdash  \varphi_1' (x) \to \varphi_1(x)$.
By Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have
$$
\mathsf{HA} + \LEM{\Sigma_{k-1}} \vdash \varphi_1' (x) \to \varphi_1(x),
$$
and hence,
$$
{T} \vdash \neg \neg \varphi_1 (x) \to \varphi_1(x).
$$
Then $T \vdash \varphi$.
Thus we have shown ${T} \vdash \DNE{\Sigma_k}$.
\end{comment}
On the other hand, by the assumption, we have $\PNFT{\dn{\mathrm{U}_{k'}}}{\dn{\Pi_{k'}}}$ for all $k' \leq k$, and hence,
${T} \vdash \DNS{\mathrm{U}_{k}^+}$
by Theorem \ref{thm: characterization of PNFT(NNUkp,NNPk)}.
\end{proof}


\begin{theorem}
\label{thm: characterization of PNFT(NEkdf, NNPk) and PNFT(NNUkdf, NNPk)}
Let ${T} $ be a theory in-between $\mathsf{HA} + \neg \neg \LEM{\Pi_{k-2}}$ $(\mathsf{HA}$ if $k<2)$ and $\mathsf{PA}$.
The following are pairwise equivalent:
\begin{enumerate}
    \item 
    \label{item: PNFT(NEkdf, NNPk)}
    $\PNFT{\df{\left(\n{\mathrm{E}_{k'}}\right)}}{ \dn{\Pi_{k'}}}$ for all $k' \leq k$;
    \item
        \label{item: PNFT(NNUkdf, NNPk)}
    $\PNFT{\df{\left(\dn{\mathrm{U}_{k'}}\right)}}{ \dn{\Pi_{k'}}}$ for all $k' \leq k$;
 

    \item
    \label{item: T|-NNSk-1DNE}
    ${T} \vdash   \neg \neg \DNE{\Sigma_{k-1}}$.
\end{enumerate}
\end{theorem}
\begin{proof}
The  equivalence  of  \eqref{item: PNFT(NEkdf, NNPk)}  and  \eqref{item: PNFT(NNUkdf, NNPk)}  is  trivial  (cf.   the  proof  of  Lemma \ref{PNFT_of_NE_k_and_NNU_k}).
In addition, $(\ref{item: T|-NNSk-1DNE} \to \ref{item: PNFT(NEkdf, NNPk)})$ is immediate from the item \ref{eq: item for NE_k in PNFT for df-formulas} in the proof of Theorem \ref{thm: PNFT for df-formulas}.
Then it suffices to show $( \ref{item: PNFT(NEkdf, NNPk)} \to \ref{item: T|-NNSk-1DNE})$.
We show this by induction on $k$.
The base case is trivial.
For the induction step, assume the assertion for $k$ and let ${T}$ be a theory in-between  $\mathsf{HA} + \neg \neg \LEM{\Pi_{k-1}}$ and $\mathsf{PA}$.
Assume also that $\PNFT{\df{\left(\n{\mathrm{E}_{k'}}\right)}}{ \dn{\Pi_{k'}}}$ holds for all $k' \leq k+1$.
Then, by induction hypothesis, we have
${T} \vdash \neg \neg \DNE{\Sigma_{k-1}}$.
Since ${T}$ contains $\mathsf{HA} +\neg \neg 
\LEM{\Pi_{k-1}},$ we have ${T} \vdash \neg \neg \LEM{\Sigma_{k-1}}$ by \cite[Theorem 3.1(ii)]{ABHK04}.
Fix an instance of $\neg \neg \DNE{\Sigma_{k}}$
$$
\varphi :\equiv  \neg \neg \forall x ( \neg \neg \varphi_1(x) \to \varphi_1(x)),
$$
where $\varphi_1(x) \in \Sigma_{k} (x)$.
Without loss of generality, one can assume that $\varphi_1(x)$ does not contain $\lor$ (cf. \cite[Proposition 3.8]{Koh08}).
Note $\forall x ( \neg \neg \varphi_1(x) \to \varphi_1(x)) \in
\df{\mathrm{U}_{k+1}}$, and hence, $\varphi \in \df{\left(\n{\mathrm{E}_{k+1}}\right)}$.
By $\PNFT{\df{\left(\n{\mathrm{E}_{k+1}}\right)}}{ \dn{\Pi_{k'}}}$, there exists a sentence $\varphi'\in \Pi_{k+1}$ such that
${T} \vdash \varphi \leftrightarrow \neg \neg \varphi' $.
Since $\mathsf{PA}$ is an extension of ${T}$ and $\mathsf{PA} \vdash \varphi$, we have $\mathsf{PA} \vdash \varphi'$.
By Theorem \ref{thm: conservation results for PNF -> Pi_k+2}, we have $    \mathsf{HA} + \LEM{\Sigma_{k-1}} \vdash \varphi'$.
Then, by Lemma \ref{lem: HA+P |- vp => HA+NNP |- NNvp}, we have
\begin{equation*}
    \mathsf{HA} + \neg \neg \LEM{\Sigma_{k-1}} \vdash \neg \neg \varphi'.
\end{equation*}
Since ${T} $ is an extension of $\mathsf{HA} + \neg \neg \LEM{\Sigma_{k-1}}$,
we have ${T} \vdash \varphi$.
\end{proof}

All of our characterization results are of the following form: For any theory ${T} $ in-between $\mathsf{HA} + {\rm Q}_k$ and $\mathsf{PA}$,
${T} \vdash {\rm P}_k$ if and only if $\PNFT{\Gamma_{k'}}{\Delta_{k'}}$ holds for all $k' \leq k$, where ${\rm P}_k, {\rm Q}_k$ are logical principles and $\Gamma_{k'}, \Delta_{k'}$
are classes of formulas.
Based on this representation, our results are summarized in
Table \ref{table: PNFT}, where it is also possible to replace $\DNS{\mathrm{U}_k^+}$ by $\DNS{\mathrm{U}_k}$ (see Remark \ref{rem: UkpDNS <-> UkDNS}).
\begin{table}[htbp]
    \centering
$$
    \begin{array}{|c|c|c|c|}
\hline
{\rm P}_k& (\Gamma_k, \Delta_k)&{\rm Q}_k& \\
\hline
\hline
\NN{\DNE{\Sigma_{k-1}}}&\left( \df{\left(\dn{\mathrm{U}_k}\right)}, \dn{\Pi_k}  \right)&\NN{\LEM{\Pi_{k-2}}}&\text{Theorem \ref{thm: characterization of PNFT(NEkdf, NNPk) and PNFT(NNUkdf, NNPk)}}\\[4pt]
\hline
\DNS{\mathrm{U}_k^+} & \left( \dn{\mathrm{U}_k}, \dn{\Pi_k}  \right) &\emptyset & \text{Theorem \ref{thm: characterization of PNFT(NNUkp,NNPk)}}\\[2pt]
 \hline
 \DNE{\Sigma_{k-1}}& \left( \df{\mathrm{U}_k}, \Pi_k  \right) & \LEM{\Pi_{k-2}}&\text{Theorem \ref{thm: Optimality of PNFT for df-formulas}.\eqref{item: Characterization of PNFT(U_k^df, Pik)}}\\[2pt]
 \hline
\DNE{\Sigma_{k-1}}+\DNS{\mathrm{U}_k^+} &\left( \dn{\mathrm{U}_k}, \Pi_k  \right) & \LEM{\Pi_{k-2}}& \text{Theorem \ref{thm: characterization of PNFT(NEk,Pk)}}\\[2pt]
\hline
\DNE{\Sigma_k} & \left(\df{\mathrm{E}_k}, \Sigma_k \right) & \LEM{\Pi_{k-1}}&\text{Theorem \ref{thm: Optimality of PNFT for df-formulas}.\eqref{item: Characterization of PNFT(E_k^df, Sigmak)}}\\[2pt]
\hline
\DNE{\Sigma_k} +\DNS{\mathrm{U}_k^+} & \left(\mathrm{E}_k, \Sigma_k \right) & \LEM{\Pi_{k-1}}&\text{Theorem \ref{thm: characterization of PNFT(Ek,Sk)}}\\[2pt]
\hline
\DNE{(\Pi_k \lor \Pi_k)}  & \left(\mathrm{U}_k, \Pi_k \right) & \emptyset &\text{Theorem \ref{thm: characterization of PNFT(Ukp,Pk)}}\\[2pt]
\hline
\DNE{\Sigma_k}+\DNE{(\Pi_k \lor \Pi_k)}  & \left(\mathrm{U}_k, \Pi_k \right) \& \left(\mathrm{E}_k, \Sigma_k \right) & \emptyset &\text{Corollary \ref{cor: characterization of PNFT(Ek,Sk)+PNFT(Uk,Pk)}}\\[2pt]
\hline
    \end{array}
    $$
    \caption{Characterizations of the prenex normal form theorems}
    \label{table: PNFT}
\end{table}


\section*{Acknowledgements}
The authors thank to Ulrich Kohlenbach for his helpful comments.
The first author was supported by JSPS KAKENHI Grant Numbers JP18K13450 and JP19J01239, and the second author by JP19K14586.



\bibliographystyle{abbrv}
