命題論理の証明パターン

はてなブログ 論理 お絵描き 本編ネタ

\require{color} \newcommand{\hyp}{\mbox{-}}% \newcommand{\To}{\Rightarrow}% \newcommand{\F}[1]{ \langle\![{#1}]\!\rangle }% \newcommand{\As}{\;::\;}%

連言導入パターン

\langle \hyp, \hyp\rangle_{A,B,C} : {\bf ND}(A, B)\times{\bf ND}(A, C)\to {\bf ND}(A, B\land C) \mbox{ in }{\bf Set}\\ \langle F, G\rangle := copy ; (F\otimes G) ; \F{\land\hyp cons}\\ \xymatrix{ {} &{}\ar[d]_-A &{} \\ {\textcolor{green}{\land}} %2,1 &*{\bullet}\ar[dl] \ar[dr] &{\:\:\:\:} %2,3 \\ *[F]{F} \ar[dr]_-B &{} &*[F]{G} \ar[dl]^-C \\ {} &*{\blacktriangledown} \ar[d]_-{B\land C} &{\:\:\:\:} %4,3 \\ {} &{} &{} \save "2,1" . "4,3" *[F.]\frm{} }

選言消去パターン

[ \hyp, \hyp]_{A,B,C} : {\bf ND}(A, C)\times{\bf ND}(B, C)\to {\bf ND}(A\lor B, C) \mbox{ in }{\bf Set}\\ [ F, G] := \F{\lor\hyp decons} ; (F\oplus G) ; merge\\ \xymatrix{ {} &{}\ar[d]_-{A\lor B} &{} \\ {\textcolor{green}{\lor}} %2,1 &*{\blacktriangle}\ar[dl]_-A \ar[dr]^-B &{\:\:\:\:} %2,3 \\ *[F]{F} \ar[dr]_-C &{} &*[F]{G} \ar[dl]^-C \\ {} &*{\bullet} \ar[d]_-{C} &{\:\:\:\:} %4,3 \\ {} &{} &{} \save "2,1" . "4,3" *[F.]\frm{} }

選言消去パターン 2

(\hyp;[ \hyp, \hyp])_{X,A,B,C} :{\bf ND}(X, A\lor B)\times {\bf ND}(A, C)\times{\bf ND}(B, C)\to {\bf ND}(X, C) \mbox{ in }{\bf Set}\\ H;[ F, G] := H;(\F{\lor\hyp decons} ; (F\oplus G) ; merge)\\ \xymatrix{ {} &{}\ar[d]_-X &{} \\ {} &*[F]{H} \ar[d]_-{A\lor B} &{} \\ {\textcolor{green}{\lor}} %3,1 &*{\blacktriangle}\ar[dl]_-A \ar[dr]^-B &{\:\:\:\:} %3,3 \\ *[F]{F} \ar[dr]_-C &{} &*[F]{G} \ar[dl]^-C \\ {} &*{\bullet} \ar[d]_-{C} &{\:\:\:\:} %5,3 \\ {} &{} &{} \save "3,1" . "5,3" *[F.]\frm{} }