$`\newcommand{\derive}{ \vdash }%
\newcommand{\deduce}{ \mathop{\|\!-} }%
\newcommand{\afford}{ \mathrel{\|} }%
\newcommand{\Sign}[1]{ \mathscr{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\In}{ \text{ in } }
\newcommand{\ImpL}{ \Leftarrow }
\newcommand{\sto}{ \longrightarrow }
%`$次は同じ意味。
- $`\mathscr{L} \deduce_\mathscr{D} \Gamma \sto B`$
- $`\mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (,) \sto B`$
- $`\mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (\vdash B)`$
圏論的論理のチュートリアル - (新) 檜山正幸のキマイラ飼育記 メモ編 によれば、次も同じ意味。
- $`\Gamma \mid \Xi \vdash \psi`$
少し違う点／同じ点は、
- $`\Gamma`$ は型コンテキストで論理式を含まない。$`\mathscr{L}`$ は型コンテキストだけでなく、論理式を含んでもよい。
- $`\Xi \vdash \psi`$ と $`\Gamma \sto B`$ は（書き方以外）まったく同じ。
- $`\Xi`$ を $`\Phi, \Psi`$ に分解して、$`\Gamma \mid \Phi, \Psi \vdash \psi`$ と書いて、一部の論理式を移動して、$`\Gamma, \Phi \mid \Psi \vdash \psi`$ とすれば同じになる。
