「型理論のコロン、ターンスタイル、カンマ」への追記ですが別記事にします。
ターンスタイルをオーバーロードすることの弊害は、（ターンスタイルに限らないけど）ターンスタイルが表す複数の意味がゴッチャになりがちなことです。もちろん、区別できる人はいいのですが、「同じ記号を使っているから同じ意味だろう」と考えがちです。
ターンスタイルが使われる可能性がある“場面”は：
- 射（主に関数）のプロファイル宣言
- 構文的対象（項とか文とか呼ばれる）の整形式性〈well-formedness〉の宣言
- 演繹系（「演繹系とオペラッド」参照）における、構文的対象の導出可能性〈derivability〉の（メタレベルの）宣言
- 意味論的構造（例：インスティチューション）における、構文的対象の妥当性〈validity〉の（メタレベルの）宣言
4番の意味でターンスタイルを使うのは見たことないですが、ないとも言い切れません。
プロファイル宣言は、圏論の意味での射の域・余域の仕様です。高次圏〈n-圏〉の高次射〈k-射〉、複圏〈オペラッド〉の複射、多圏の多射のプロファイルもあります。
構文的対象が整形式〈well-formed〉だとは、コミュニケーションに使われる記号的・図形的表現がデタラメではなくて（真偽はともかくとして）解釈可能であることです。整形式な構文的対象は、文法（構文生成規則の集まり）で定義されます。
構文的対象が導出可能〈derivable〉とは、とある演繹系において、当該の構文的対象に対する導出ツリーが存在することです。導出可能を演繹可能〈deducible〉とか証明可能〈provable〉ともいいます。導出可能性もある種の文法で定義されますが、生成規則は導出規則とか推論規則と呼ばれます。
構文的対象が妥当〈valid〉だとは、特定のモデルあるいはすべてのモデルに対して“成立している”ことです。直感的に言えば、事実と照らし合わせて正しいことです。
指標〈signature〉は構文的対象ですが、公理系を表現できます。なんらかの演繹系を $`\mathscr{D}`$ 、なんらかの意味論的構造（インスティチューションを想定します）を $`\mathscr{I}`$ として、$`\mathscr{D}`$ と $`\mathscr{I}`$ は同じ構文的対象〈文〉の集合を備えているとします。
演繹系における導出可能性を '$`\Vvdash`$' で、意味論的構造における妥当性を '$`\models`$' で表すことにします。$`s`$ を文だとして、$`s`$ の導出可能性と妥当性は次のように書けます。
$`\quad \Vvdash_\Sigma s \text{ in }\mathscr{D}`$
$`\quad M \models_\Sigma s \text{ in }\mathscr{I}`$
左側に何を書くかは、'$`\Vvdash`$' と '$`\models`$' では違っています。
- '$`\Vvdash`$' では、追加の仮説／コンテキスを左側に書く。何も書いてなければ追加の仮説／コンテキスはない。
- '$`\models`$' では、モデルを左側に書く。何も書いてなければ「すべてのモデルで妥当」を意味する。
通常、$`\mathscr{D}, \mathscr{I}`$ は暗黙に固定されているとして明示されません。
論理・モデル理論の普通の記号は、'$`\Vvdash`$' ではなくて '$`\vdash`$' です。型理論では、'$`\vdash`$' や '$`\Vdash`$' が文 $`s`$ のなかに入っているオブジェクトレベルの記号なので、メタレベルの記号に '$`\Vvdash`$' を使ったのです。
