# Markov's principle from constant domain logic

I am looking for a proof of and/or a reference for the result that Markov's principle can be proved in the framework of constant domain logic. By constant domain logic, I mean intuitionistic logic plus the axiom

$$\forall x(P(x) \,\vee\, Q) \to \forall xP(x) \,\vee\,Q \quad$$ where x is not free in $$Q$$.

This result is alluded to, without proof, in the entry about intuitionistic logic in the Stanford encyclopedia of philosophy: https://stanford.library.sydney.edu.au/archives/fall2008/entries/logic-intuitionistic/#KriSemForIntLog (I have found no other reference.)

• $\forall x\,(A(x)\lor\neg A(x))\to\forall y\,(\neg A(y)\lor\exists x\,A(x))\to\forall y\,\neg A(y)\lor\exists x\,A(x)$. So, that’s even stronger than MP: decidability is preserved by existential quantification. Mar 12, 2020 at 13:07
• Thank you. If you re-post that as an answer I will mark this as solved. Also, if you happen to have a reference where this (or similar) was first noticed, I'd be happy to know. Mar 12, 2020 at 22:51

$$\forall x(A(x) \vee \neg A(x)) \:\to\: \forall x (\exists y A(y) \vee \neg A(x)) \:\to\: \exists y A(y) \vee \forall x(\neg A(x))$$