2重ターンスタイル(double turnstile)とは、で表現される記号である。
定義[]
論理式の集合のことをと表記することにする。このとき、と書いた場合、に含まれる論理式は全て真でなければならず、またCを偽とするような真理値の割り当ては存在しないことを示す。
言い換えれば、と書いたとき、もしの内部式に一つでも偽の値を取るような論理式がある場合、あるいはCが偽になるような場合、この式は成立しないことになる。
同時に、という表記も可能である。この場合、左側に論理式の空集合があると仮定される。このとき、「真理値が真であるべきものは存在しない」、つまり「無条件に」と解釈できるため、Cは無条件にCになるということになる。言い換えると、はトートロジーである。
逆に、右側に何も置かないことが可能である。この場合、と表記できる。この場合、左側に真となるべき論理式が存在しないことになる。定義上、右側には真になる何かしらの論理式が必要であった。その論理式が存在しないということは、この場合は常に矛盾することになる
