Pure first order logic formulations of Markov's principle

Question

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate: $\neg \neg \exists x P \to \exists x P$

Its formulation is well known in the context of arithmetic, and it is well known that adding it to Heyting Arithmetic gives rise to a constructive system: when $A \lor B$ is provable, either $A$ is provable or $B$ is provable; when $\exists x \, A(x)$ is provable, there is a $t$ such that $A(t)$ is provable.

However I think it is not clear how one could formulate it in the context of pure intuitionistic first order logic (if it does make sense at all).

Various sources ([1], [2]) state it as "$\neg \neg \exists x P \to \exists x P$ for $P$ $\forall, \to$-free". Another tempting formulation would be $\forall x (P \lor \neg P) \to \neg \neg \exists x P \to \exists x P$ for any propositional $P$. As far as I can see, these two formulations are not comparable. Both these axioms, though, share the property that if we add them to pure intuitionistic first order logic we still obtain a constructive system (this is proved in [1] for the first axiom; I couldn't find references for the second axiom, but a proof can be obtained with a very similar argument).

Is there a more general analog of Markov's rule for first-order logic which preserves the disjunction property and other proof-theoretic properties of constructive systems? Or alternatively, is there some other source justifying the choice of the formalization used in [1,2] for Markov's principle?

[1] H. Herbelin, An intuitionistic logic that proves Markov's principle https://hal.inria.fr/inria-00481815/ [2] U. Berger, A Computational Interpretation of Open Induction http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=1319627

Answer 1

This is not an answer to the question, but rather a comment which benefits from proper formatting.

For me personally, Markov's principle is specifically associated with the natural numbers and not with some other set. By that I mean that I don't think of $$ \neg\neg \exists x \in X{:}\ P(x) \quad\Longrightarrow\quad \exists x \in X{:}\ P(x) $$ (with $P$ restricted in some form, as you detailed) as a reasonable constructive principle, if $X$ is some arbitrary set.

Recall that there is a concrete reason why some schools of constructive mathematics accept Markov's principle: consider the algorithmic interpretation. The property $P$ is such that we can test in some finite way, for any natural number $n$, whether $P(n)$ holds or not. The assumption that $\neg\neg\exists n \in \mathbb{N}{:}\ P(n)$ means that there is some number $n$ such that $P(n)$ holds, but we do not know such a number (we are not given a witness of the existential statement). But we can find such a number on our own, thereby providing a witness of the statement $\exists n \in \mathbb{N}{:}\ P(n)$, by checking $P(0)$, $P(1)$, $P(2)$, and so on. This algorithm terminates (but we couldn't provide an upper bound for its runtime).

For an arbitrary set $X$ in place of $\mathbb{N}$, no analogous approach is possible. Therefore I can't quite fathom what you're driving at. (Markov's principle certainly works for some relatives of $\mathbb{N}$, for instance $\mathbb{N}^2$, which we can too search in a sequential manner.)