シーケント計算の再解釈 3

$`\newcommand{\LLambda}{\mathrm{L}\Lambda}
\newcommand{\Llambda}{\mathrm{L}\lambda}
\newcommand{\RLambda}{\mathrm{R}\Lambda}
\newcommand{\Rlambda}{\mathrm{R}\lambda}
\newcommand{\Dia}{\diamondsuit}
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\conc}{\mathop{\#} }
\newcommand{\Subst}[1]{ \begin{bmatrix} #1 \end{bmatrix} }
%`$

次のオペレーターを考える。$`\alpha, \beta\in \mrm{TypeCtx}`$

• $`\Dia_\alpha^\beta : \mrm{Prop}[\alpha]\to \mrm{Prop}[\alpha\conc\beta]`$
• $`\forall_\alpha^\beta : \mrm{Prop}[\alpha\conc\beta]\to \mrm{Prop}[\alpha]`$
• $`\exists_\alpha^\beta : \mrm{Prop}[\alpha\conc\beta]\to \mrm{Prop}[\alpha]`$

命題レベルの左右カリー化。$`\Gamma, \Delta \in \mrm{PropCtx}, Q\in \mrm{Prop}`$

• $`\LLambda_{\Gamma, Q}^\Delta: \mrm{MultiDeriv}(\Delta\conc\Gamma, Q) \to \mrm{MultiDeriv}(\Gamma, [\Delta\triangleright Q])`$
• $`\RLambda_{\Gamma, Q}^\Delta: \mrm{MultiDeriv}(\Gamma\conc\Delta, Q) \to \mrm{MultiDeriv}(\Gamma, [Q \triangleleft \Delta])`$

関数レベルの左右カリー化。$`\alpha, \beta \in \mrm{TypeCtx}, Y\in \mrm{Type}`$

• $`\Llambda_{\alpha, Y}^\beta: \mrm{MultiFunc}(\beta\conc\alpha, Y) \to \mrm{MultiFunc}(\alpha, [\beta \triangleright Y])`$
• $`\Rlambda_{\alpha, Y}^\beta: \mrm{MultiFunc}(\alpha\conc\beta) \to \mrm{MultiFunc}(\alpha, [Y\triangleleft \beta])`$

多関数 $`f:\alpha \to \beta`$ による置換

• $`f^*: \mrm{Prop}[\beta] \to \mrm{Prop}[\alpha]`$
• $`f^* Q = Q\Subst{f}`$

これに加えて：

1. 連言の濃縮・希釈 バンチ演算
2. 選言の濃縮・希釈 バンチ演算
3. 全称命題の濃縮・希釈 拡大バンチ演算
4. 存在命題の濃縮・希釈 拡大バンチ演算
5. 同値置換 プレポスト結合 知識ベース使用 バンチ演算
6. 各種のマージ 導出への演算
7. ド・モルガン双対移動 導出への演算
8. プレ結合 知識ベース使用 導出への演算
9. ポスト結合 知識ベース使用 導出への演算
10. カット