FANDOM


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 $と表記できる。この場合、左側に真となるべき論理式が存在しないことになる。定義上、右側には真になる何かしらの論理式が必要であった。その論理式が存在しないということは、この場合は常に矛盾することになる