トートロジーと論理的帰結

モデル・値付けw(wα=1)を充足関係 w|=α と捉えなおす。論理式φ∈Fはモデルによって充足したり、しなかったりするが、任意のモデルに対して充足する論理式があり、トートロジーと呼ぶ。任意のモデルに対して充足しない論理式があり、矛盾と呼ぶ。αを充足する任意のモデルに対してXが充足するとき、論理的帰結と呼び、 α|=X とかく。充足関係と論理的帰結に同じ記号を割り当てるが、特に混乱はないはず。

論理的帰結に関し、 X,α |= β ⇒ X |= α→β という演繹定理が成り立つため、これを帰納的に利用することで、任意の論理的帰結の妥当性は、ある種の論理式がトートロジーであるかどうかという問題に帰結し、決定可能である。