1
$\begingroup$

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

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ $\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. $\endgroup$
    – Emil Jeřábek
    Mar 12 '20 at 13:07
  • $\begingroup$ 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. $\endgroup$
    – Erik D
    Mar 12 '20 at 22:51
0
$\begingroup$

Emil Jeřábek answered in a comment:

$\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))$

So, that’s even stronger than MP: decidability is preserved by existential quantification.

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.