On the contrapositive of countable choice (Q627434)

Relations between some principles in the framework of elementary intuitionistic analysis, EL, and intuitionistic arithmetic, HA, are considered. These principles are: the contrapositive of countable choice \[ \text{CCC:}\quad\forall f\,\exists x\,P(x,f(x))\to\exists x\,\forall y\,P(x,y), \] double negation elimination for \(\Sigma_2^0\)-formulas \[ \Sigma_2^0\text{-DNE:}\quad\neg\neg\exists x\,\forall y\,P(x,y)\to\exists x\,\forall y\,P(x,y), \] and the law of excluded middle for \(\Sigma_1^0\)-formulas \[ \Sigma_1^0\text{-LEM:}\quad\exists x\,P(x)\lor\forall x\,\neg P(x). \] In all three principles, \(P\) is a decidable predicate. Proposition 1. \(\text{EL}\vdash\Sigma_2^0\text{-DNE}\leftrightarrow\text{CCC}\). If \(f\) ranges over the recursive functions, CCC can be stated in an arithmetical form \(\text{CCC}^\circ\) using Kleene's predicate \(T\) and function \(U\). Proposition 2. (a) \(\text{HA}+\Sigma_2^0\text{-DNE}\vdash\text{CCC}^\circ\). (b) \(\text{HA}+\text{CCC}^\circ\vdash\Sigma_1^0\text{-LEM}\). (c) \(\text{HA}+\text{CCC}^\circ\vdash\Sigma_2^0\text{-DNE}\). It follows that \(\text{HA}\vdash\Sigma_2^0\text{-DNE}\leftrightarrow\text{CCC}^\circ\). Let S be an extension of HA. A predicate \(R\) is called: externally recursive in S, if there is a numeral \(t\) such that \[ \text{S}\vdash\forall x\,\exists z\,(T(t,x,z)\land(R(x)\leftrightarrow U(z)=0)); \] internally recursive in S, if \[ \text{S}\vdash\exists e\,\forall x\,\exists z\,(T(e,x,z)\land(R(x)\leftrightarrow U(z)=0)); \] decidable in S, if \[ \text{S}\vdash\forall x\,(R(x)\lor\neg R(x)). \] The following proposition is proved by using formalized realizability. Proposition 3. (a) In \(\text{HA}+\text{ECT}_0\), every decidable predicate is externally recursive. (b) In \(\text{HA}+\text{CT}_0\), every decidable predicate is internally recursive. Here \(\text{CT}_0\) and \(\text{ECT}_0\) are standard arithmetical forms of Church's thesis and extended Church's thesis, respectively.