停止性問題しかり、ﾃﾞｨｵﾌｧﾝﾄｽ方程式しかり、計算機で証明できない問題はたくさんあるわけで。
「定理」は有限文字列で表現できるから
「この世のすべての定理」を列挙することは一応できるけど
それらすべての真偽を判定することはできないと言うことか。