Loading article…
数理論理学において、判断（または命題）とは、メタ言語における記述または表明のことである。例えば、一階述語論理における典型的な判断としては、文字列が整形式論理式であること、あるいは命題が真であることなどが挙げられる。同様に、判断は対象言語の式における自由変数の出現、あるいは命題の証明可能性を主張することもある。一般に、判断はメタ理論において帰納的に定義可能なあらゆる表明となり得る。
推論システムを形式化する際に判断が用いられます。論理公理は判断を表し、推論規則の前提は一連の判断として形成され、結論もまた判断です（したがって、証明の仮説と結論は判断です）。ヒルベルト型推論システムの変種の特徴は、推論規則のいずれにおいても文脈が変更されないことです。一方、自然演繹とシーケント計算には、文脈を変更する規則が含まれています。したがって、仮説判断ではなくトートロジーの導出可能性のみに関心がある場合は、ヒルベルト型推論システムを、推論規則に比較的単純な形式の判断のみが含まれるように形式化することができます。他の2つの推論システムでは同じことはできません。推論規則の一部で文脈が変更されるため、トートロジーの導出可能性を証明するためだけにそれらを使用したい場合でも、仮説判断を回避できるように形式化することはできません。
様々な計算体系におけるこの基本的な多様性により、同じ基本的な考え方（例えば演繹定理）がヒルベルト式の演繹体系ではメタ定理として証明されなければならないのに対し、自然演繹では推論規則として明示的に宣言できるといった違いが生じる。
型理論では、数理論理学と同様の概念がいくつか用いられており（例えば、カリー＝ハワード対応など、両分野間の関連性を生み出している）、数理論理学における判断の概念における抽象化は、型理論の基礎においても活用できる。