論理と圏論：導入規則と除去規則のあいだの等式的法則 - 檜山正幸のキマイラ飼育記 (はてなBlog)

圏論では、射のあいだの等式的関係、例えば $`\langle f , g \rangle; \pi_1 = f`$ などが重要ですが、論理ではあまり言及しません。分野ごとに、興味のあり方や価値観が違うからでしょう。

論理における導入規則と除去規則のあいだの関係を、圏論的な記法で等式的法則として述べておきます。実際に論理で使うには、組み合わせや調整が必要です。$`\newcommand{\In}{\text{ in }}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\id}{\mathrm{id} }
`$

連言の導入と除去

$`f:X \to A \In \cat{C}`$
$`g:X \to B \In \cat{C}`$
$`\langle f, g\rangle : X \to A\times B \in \cat{C}`$ （デカルト・ペア）
$`\pi_1 : A\times B \to A \In \cat{C}`$ （第一射影）
$`\pi_2 : A\times B \to B \In \cat{C}`$ （第二射影）
$`\langle f , g \rangle; \pi_1 = f`$ （等式的法則）
$`\langle f , g \rangle; \pi_2 = g`$ （等式的法則）

選言の導入と除去

$`f:A \to Y \In \cat{C}`$
$`g:B \to Y \In \cat{C}`$
$`(\!| f \mid g |\!) : A + B \to Y \in \cat{C}`$ （余デカルト・コペア）
$`\iota_1 : A \to A + B \In \cat{C}`$ （第一入射）
$`\iota_2 : B \to A + B \In \cat{C}`$ （第二入射）
$`\iota_1 ; (\!| f \mid g |\!) = f`$ （等式的法則）
$`\iota_2 ; (\!| f \mid g |\!) = g`$ （等式的法則）

真の導入と除去

$`f:A \to B \In \cat{C}`$
$`!_A : A \to {\bf 1} \In \cat{C}`$ （終対象への唯一射）
$`!_B : B \to {\bf 1} \In \cat{C}`$ （終対象への唯一射）
$`f ; !_B = !_A`$ （等式的法則）
$`a : {\bf 1} \to A \In \cat{C}`$ （終対象からの射、命題 $`A`$ の成立の根拠が $`a`$）

偽の導入と除去

$`f:A \to B \In \cat{C}`$
$`\theta_A : {\bf 0} \to A \In \cat{C}`$ （始対象からの唯一射）
$`\theta_B : {\bf 0} \to B \In \cat{C}`$ （始対象からの唯一射）
$`\theta_A ; f = \theta_B`$ （等式的法則）
$`a : A \to {\bf 0}\In \cat{C}`$ （始対象への射、命題 $`A`$ の矛盾の根拠が $`a`$）

含意の導入と除去

$`f:X \times A \to B \In \cat{C}`$
$`[A, B] = B^A \in |\cat{C}|`$ （指数対象）
$`\mrm{right\_ev}_{A, B}: [A, B]\times A \to B \In \cat{C}`$ （右評価射）
$`\mrm{RightCurry}_{X, A, B}: \cat{C}(X\times A, B) \to \cat{C}(X, [A, B]) \In {\bf Set}`$ （右カリー化）
$`( \mrm{RightCurry}_{X, A, B}(f) \times \id_A) ; \mrm{right\_ev}_{A, B} = f`$ （等式的法則）

全称の導入と除去

$`(f_i: X \to A_i \In \cat{C})_{i\in I}`$ （射のインデックス族）
$`\langle f_i \rangle_{i\in I} : X \to \prod_{i\in I}A_i \In \cat{C}`$ （一般化タプル）
$`\pi_k : \prod_{i\in I}A_i \to A_k \In \cat{C}`$ （一般化射影）
$`\langle f_i \rangle_{i\in I}; \pi_k = f_k`$ （等式的法則）

存在の導入と除去

$`(f_i: A_i \to Y \In \cat{C})_{i\in I}`$ （射のインデックス族）
$`(\!| f_i |\!)_{i\in I} : \sum_{i\in I}A_i \to Y \In \cat{C}`$ （一般化コタプル）
$`\iota_k : A_k \to \sum_{i\in I}A_i \In \cat{C}`$ （一般化入射）
$`\iota_k ; (\!| f_i |\!)_{i\in I} = f_k`$ （等式的法則）

依存カリー化については今日は述べません。依存カリー化はカリー化の一般化と捉えることもできますが、特殊な極限を計算したら、たまたまカリー化になっていた、という感じです。依存カリー化がカリー化を包摂することは、「棚からぼた餅」的現象でしょう。なお、依存カリー化に繋げるには、カリー化の等式的法則を次の形に書いておいたほうが便利です。

$`a:{\bf 1} \to A \In \cat{C}`$
$`( \mrm{RightCurry}_{X, A, B}(f) \times a) ; \mrm{right\_ev}_{A, B} = (\id_X \times a);f`$ （等式的法則）