ダブルターンスタイル

論理学では、記号⊨、⊧、またはは二重回転木戸記号と呼ばれる。これは、「含意する」、「モデル化する」、「意味上の帰結である」、または「より強い」と読まれることが多い。^[1]これは、真ん中に1本のバーがあり、統語的帰結を表す回転木戸記号（意味上の とは対照的） と密接に関連している。${\displaystyle \models}$ ${\displaystyle \vdash}$

二重回転木戸は二項関係です。文脈によっていくつかの異なる意味を持ちます。

• 左側に一組の文、右側に一つの文を置いて意味上の帰結 を示し、左側の文がすべて真であれば、右側の文も必ず真であることを示します (例 )。この用法は、統語上の帰結 を表す単線の回転木馬記号と密接に関連しています。${\displaystyle \Gamma \vDash \varphi }$
• 満足性 を示し、左側にモデル（または真理構造）があり、右側に文の集合がある場合、構造が文の集合のモデルである（または満たす）ことを示します（例： ）。これは通常、変数割り当ての範囲を制限するとともに帰納的に行われ、各変数記号をその中の値にマッピングする関数が成り立つ場合があります。^[2]${\displaystyle {\mathcal {A}}\models \Gamma }$${\displaystyle {\mathcal {A}}}$
  • この文脈では、前のリストの意味論的帰結は「与えられたモデルに対して、ならば」と述べることができます。${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {A}}\models \Gamma }$${\displaystyle {\mathcal {A}}\vDash \varphi }$
• トートロジーを表すには、 。つまり、この表現は空集合の意味上の帰結であるということです。${\displaystyle \vDash \varphi }$${\displaystyle \varphi}$
• この記号は次のように使用することもできます: ⊭ は、「含意しない」という文を表します。

TeXでは、ターンスタイル記号 ⊨ と はそれぞれコマンドとから取得され ます。 ${\displaystyle \models}$\vDash\models

Unicode では、 U+22A8 ⊨ TRUE ( ⊨, ⊨ )でエンコードされ、その反対はU+22AD ⊭ NOT TRUE ( ⊭ ) です。

LaTeXには、ターンスタイル パッケージがあります。このパッケージは、ダブル ターンスタイルを含むさまざまな方法でこの記号を発行し、その下または上の適切な場所にラベルを配置することができます。記事「論理学者のためのツール」は、このパッケージの使用に関するチュートリアルです。

• 論理記号のリスト
• 数学記号の一覧
• 回転式改札口⊢