数式がHTMLではうまく書けないので、文章で説明することにする。
まず、関数ｆが計算可能とは、あるプログラムＵが存在して、そのプログラムに任意の入力ｘを与えた場合、停止して結果が、ｆ（ｘ）であるようなものである。
簡単な例でいえば２倍するような関数はｘを２とすればｆ（ｘ）は４である。つまりこの４というものを、停止して結果をちゃんと返すプログラムが書けるかどうかというものである。
さて、Haltは２変数関数で、Halt(a,x)と書く、aはプログラム、xはそのプログラムへの入力である。この関数は１を返せば、計算が停止し、０を返せば停止しない関数であるとする。
この証明として、入力ａ、ｘをもつプログラムＵを仮定し、この結果がＨａｌｔ（ａ，ｘ）であればよい。
さて、ここで対角線論法を使う。あるプログラムＸがある。引数は一つとする。この中でＵの引数をいずれもプログラムＸの引数とする。Ｕが１を返した場合は無限ループに入り、０を返した場合は１を返すとする。
さて、このプログラムＸの引数にプログラムＸ自身を代入する。つまりＵはプログラムＸがプログラムＸを引数でとった場合に停止するかどうかという判定を行う。（つまり無限回をあらわしている）停止するとすると、Ｕは１を返すが、１は無限ループに入ってしまう。またＵが０を返すと、Ｘは１を返す。となると、Ｈａｌｔ（Ｘ、Ｘ）は１でなければならないから、矛盾する。
なお、tステップ以内に終わるかどうかというHaltInTimeという関数は計算可能である。
これは、ｔを１ずつ増やしながら、ｔステップ以内で停止できるかどうかをチェックし、停止できれば停止したという値を返せばよい。
