 Although unprovable in \(\mathbf{HA},\) MP is realizable by an argument which uses Markov’s Principle informally. But realizability is a fundamentally nonclassical interpretation. In \(\mathbf{HA}\) it is possible to express an axiom of recursive choice CT (for “Church’s Thesis”), which contradicts LEM but is (constructively) realizable. Hence by Nelson’s Theorem, \(\mathbf{HA}\) \(+\) MP \(+\) CT is consistent.