Интуиционистская арифметика с принципами Маркова и P

Abstract

We consider the theory HA+M+P, where M is Markov’s principle (any, see [1]), P is the following, classically true, principle $(\neg\varphi \rightarrow \exists x \psi (x)) \rightarrow \exists x(\neg \varphi \rightarrow \psi(x))$ (also see [1]). We prove that such theory has numerical existentiality (and, of course, disjunctivity) and get some corollaries from this fact.