Some intuitionistic equivalents of classical principles for degree 2 formulas (Q2368911)

This paper is concerned with the study of intuitionistic equivalences between mathematical theorems in frequent use, on the one hand, and classical logical principles like Excluded Middle, Markov's Principle, and König's Lemma restricted to \(\Sigma^0_2\)-formulas, on the other hand, provided universal quantification over maps is restricted to (effectively given families of) recursive maps. Among the mathematical statements and definitions treated are (weak) infinity axioms, various definitions of the notion of quasi-well-ordering, convergence principles, and several versions of Dickson's Lemma. For example, it is shown that the restriction of Excluded Middle to \(\Sigma^0_2\)-formulas is equivalent (in the context of intuitionistic arithmetic with function quantifiers and Dependent Choice) to the principle that any effectively decidable set is either finite or infinite, that the said version of Markov's Principle is equivalent both to the principle ``every recursive sequence over the set of natural numbers which does not change value infinitely many times is stationary'' and to ``any effectively decidable set which is not infinite is finite'', and that König's Lemma for \(\Sigma^0_2\)-formulas is likewise equivalent to one version of Dickson's Lemma (for recursive sequences).