# Pure first order logic formulations of Markov's principle

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

• "Here are two non-arithmetic analogs of the arithmetic Markov's principle; which if either deserves the title of 'Markov's principle for first-order logic'?" Is that all you're asking, or do you want more than justification for a name? – Matt F. Nov 30 '16 at 17:37
• @MattF. Yes, that's what I am asking. However having two uncomparable principles makes me think that there should be a more general form, and that neither of the two should be really acceptable. – Matteo Dec 1 '16 at 13:58
• So I would revise the question by 1) reminding people that the disjunction property means "when $A \vee B$ is provable, then $A$ is provable or $B$ is provable", and 2) asking: "What is the most general analog of Markov's rule for first-order logic which preserves the disjunction property and other proof-theoretic properties of constructive systems?" – Matt F. Dec 1 '16 at 16:54
• @MattF. Thank you for the suggestion, I tried to improve the question accordingly – Matteo Dec 2 '16 at 13:57
• Can you give an idea how you prove admissibility of the second scheme? I also think it helps if you specify even more. Two variants of your question: 1)Is there a more general class MR of first-order propositions, such that for a constructive first-order theory T (with disjunction and existence property) and a P(x) in MR: if T proves $\neg\neg\exists$x[P(x)], then T proves $\exists$xP(x)? 2)Is there such a class MR that when added to intuitionistic first-order logic as axioms, preserves the constructivity of any constructive theory T? To me 1) and 2) are not equivalent. – Frank Waaldijk Dec 3 '16 at 8:59

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.)