Elementary inductive definitions in HA: From strictly positive towards monotone (Q920089)

An elementary inductive definition (e.i.d.) is given by a formula A(P,x) in the language of the intuitionistic arithmetic HA expanded with a single one-place predicate variable P, containing at most one numerical variable free, without an unbounded universal quantifier occurring in front of a positive subformula containing P, and without an unbounded existential quantifier in front of a negative subformula containing P. It has been proved classically that if A(P,x) is an e.i.d. (therefore, it is monotone), then the approximation defining its least fixed-point \(P^ A_{\infty}\) closes up at or before stage \(\omega\), so \(P^ A_{\infty}=P^ A_{\omega}\) \((P^ A_{\infty}\) is defined by the approximation: \(P^ A_ 0x:\Leftrightarrow A(\lambda x.\perp,x),\quad P^ A_{\beta +1}x:\Leftrightarrow A(P^ A_{\beta},x),\quad P^ A_{\lambda}x:\Leftrightarrow \exists \mu <\lambda P^ A_{\mu}x,\) lim \(\lambda\), \(P^ A_{\infty}x:\Leftrightarrow \exists \mu P^ A_{\mu}x).\) However, intuitionistically, this is only true (in general) for strictly positive e.i.d., i.e. formulae A(P,x) built up from atomic formulae Pt, from HA-formulae \(\phi\) (these do not contain P), by means of the operators \(\exists\), \(\forall y<s\), \(\wedge\), \(\vee.\) The main result of the paper is to prove that if we extend the class of strictly positive e.i.d. by adding an operator J satisfying the conditions: (i) \(Q\to J(Q)\), (ii) J(Q\(\wedge R)\to J(Q)\wedge J(R)\), (iii) J(J(Q))\(\to J(Q)\), then \(P^ A_{\infty}=P^ A_{\omega +\omega}\) is HA-definable, i.e. the approximation closes up at or before stage \(\omega +\omega\), intuitionistically. Note that \(\neg \neg\) is such an operator J.