演繹システム (2)

$`\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 }
%`$
対応があまりピッタリではないが。

演繹システム	類似の既存用語
sys-prop	論理定数
sys-deriv	論理公理
sys-reas	推論規則
sys-equiv	論理法則
user-prop	？
user-deriv	分野公理
user-reas	分野推論規則
user-equiv	分野論理法則

システムを次のように置く。

$`\quad \mathscr{D} = (\mathscr{D}_\mathrm{prop}, \mathscr{D}_\mathrm{deriv}, \mathscr{D}_\mathrm{reas}, \mathscr{D}_\mathrm{equiv})`$

ライブラリは：

$`\quad \mathscr{L} = (\mathscr{L}_\mathrm{prop}, \mathscr{L}_\mathrm{deriv}, \mathscr{L}_\mathrm{reas}, \mathscr{L}_\mathrm{equiv})`$

演繹可能性は：

$`\quad \mathscr{L} \deduce_\mathscr{D} \Gamma \sto B`$

演繹定理から：

$`\quad \mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (,) \sto B`$

あるいは、

$`\quad \mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (\vdash B)`$