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

1more comment