形式体系とは？

けいしきたいけい

記号・公理・推論規則を明示的に規定した、機械的に証明を検証できる論理体系です。

形式体系とは、アルファベット（記号集合）・整式（well-formed formula）の定義・公理・推論規則を厳密に規定した論理的枠組みのことである。証明とはこの体系内の規則のみを用いた有限列であり、機械的に検証可能である。ヒルベルトの形式主義に基づく数学の厳密化プログラムと深く結びついており、ゲーデルの不完全性定理もこの概念を前提とする。