演繹可能性メタ命題

半形式証明スクリプト 論理

$`\newcommand{\deduce}{ \mathop{\|\!-} }%
\newcommand{\afford}{ \mathrel{\|} }%
\newcommand{\Sign}[1]{ \mathscr{#1} }
%`$

$`\Sign{A}`$ は背景指標〈background signature〉として、シーケント $`\Gamma \to A`$ が演繹可能〈deducible〉であることを次のように書く。

$`\quad
\Sign{A} \deduce \Gamma \to A
`$

まったく同じことを次のようにも書く。

$`\quad
\Sign{A} \afford \Gamma \vdash A
`$

この書き方から背景指標を省略した形が：

$`\quad
\Gamma \vdash A
`$

さらに言えば、演繹システムの名前 $`S`$ も入れて次のように書くのが正確。

$`\quad
\Sign{A} \deduce_S \Gamma \to A
`$

背景指標を省略した場合は：

$`\quad
\Gamma \vdash_S A
`$

参考（新しい順）：