2重ターンスタイル

2重ターンスタイル(double turnstile)とは、$\models$で表現される記号である。

定義

論理式の集合$A_{1},A_{2},..,A_{n}$のことを$\Gamma$と表記することにする。このとき、$\Gamma \models C$と書いた場合、$\Gamma$に含まれる論理式は全て真でなければならず、またCを偽とするような真理値の割り当ては存在しないことを示す。

言い換えれば、$\Gamma \models C$と書いたとき、もし$\Gamma$の内部式に一つでも偽の値を取るような論理式がある場合、あるいはCが偽になるような場合、この式は成立しないことになる。

同時に、$\models C$という表記も可能である。この場合、左側に論理式の空集合があると仮定される。このとき、「真理値が真であるべきものは存在しない」、つまり「無条件に」と解釈できるため、Cは無条件にCになるということになる。言い換えると、$\models C$はトートロジーである。

逆に、右側に何も置かないことが可能である。この場合、$\Gamma \models$と表記できる。この場合、左側に真となるべき論理式が存在しないことになる。定義上、右側には真になる何かしらの論理式が必要であった。その論理式が存在しないということは、この場合は常に矛盾することになる