Nelson's theorem is a soundness theorem that relates Heyting arithmetic and Kleene's realizability semantics.
More specifically, the theorem is
Nelson's theorem. If is derivable in , and the derivation only uses realizable formulas, then is realizable.
Nelson's theorem has implications for the consistency of non-classical extensions of Heyting arithmetic.
Consider Markov's principle, i.e. the formula
This is obviously reliazable in Kleene realizability, even if not necessarily intuitionistically true. According to Nelson's theorem, any theorems derived from the rules of and is realizable. Hence, the logic is consistent.
A similar game can be played for Church's thesis.
Nelson, D., 1947, “Recursive functions and intuitionistic number theory,” Transactions of the American Mathematical Society, 61: 307–368.