判断(はんだん、または)あるいは主張 とは、数理論理学においてメタ言語における言明あるいは表明のことである。

解説 例えば、一階述語論理における典型的な判断は、「ある文字列が整式である」こと、あるいは「ある命題が真である」ことである。同様に、判断は対象言語のある表現における自由変数の出現を主張することもあれば、命題の証明可能性を主張することもある。一般に、判断とはメタ理論において帰納的に定義可能な任意の主張のことである。

判断は演繹体系を形式化する際に用いられる。論理的公理は判断を表現し、推論規則の前提は判断の列として形成され、その結論もまた判断である(したがって、証明の仮定と結論はいずれも判断である)。ヒルベルト流の演繹体系の変種に特徴的な点は、その推論規則のいずれにおいても文脈が変化しないということである。一方、自然演繹とシークエント計算は、いずれも文脈を変化させる規則をいくつか含んでいる。したがって、仮言的な判断ではなくトートロジーの導出可能性のみに関心があるならば、ヒルベルト流の演繹体系を、その推論規則がかなり単純な形式の判断のみを含むように形式化することができる。他の二つの演繹体系については同じことはできない。というのも、それらの推論規則の一部において文脈が変化するため、たとえトートロジーの導出可能性を証明するためだけに用いようとしたとしても、仮言的な判断を避けられるようには形式化できないからである。

さまざまな計算体系の間にあるこの基本的な多様性により、同じ基本的な思想(例えば演繹定理)が、ヒルベルト流の演繹体系ではとして証明されなければならないのに対し、自然演繹では推論規則として明示的に宣言できるというような違いが生じうる。

型理論においては、数理論理学における概念と類似の概念がいくつか用いられている(これにより両分野の間に、例えばカリー=ハワード同型対応のようなつながりが生じる)。数理論理学における判断という概念における抽象化は、型理論の基礎においても同様に利用することができる。

関連項目

数理論理学

出典

外部リンク