計算機は計算機の停止性を判定できないが、
実際には、計算機は止まるか止まらないかの二者択一しかないだろう。
同様に、真か偽ではある命題も、形式的に証明できるとはかぎらない。