ゲーデル『不完全性定理』(林晋、八杉満利子 訳)

すなわち,有限的な数論をある分量だけ含むような任意の無矛盾な形式系において,決定不能な算術の命題が存在し,さらに,そのようなシステムの無矛盾性は,そのシステム内では証明できない,という事実を,厳密に証明できるのである.