いっとくけど、述語論理の場合
定理でない式は手続きが停止しないから
気をつけてね

これ、ゲーデルの不完全性定理の系だから

定理なら必ず証明できるのが完全性定理
定理か否か決定する手続きが存在しないのが非決定性