Nelson's theorem

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 \phi is derivable in \textbf{HA}, and the derivation only uses realizable formulas, then \phi is realizable.

Implications for consistency

Nelson's theorem has implications for the consistency of non-classical extensions of Heyting arithmetic.

Consider Markov's principle, i.e. the formula

  (\lnot\forall x. \lnot \psi(x)) \to \exists x.\ \psi(x)
  \tag{\textbf{MP}}

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 \textbf{HA} and \textbf{MP} is realizable. Hence, the logic \textbf{HA}+\textbf{MP} is consistent.

A similar game can be played for Church's thesis.

References

• The theorem first appeared in

• The presentation here is taken from the Stanford Encyclopedia of Philosophy.