NANDとNORの証明論

1 概要

本記事では数理論理学についての基本的な知識，とくに古典命題論理の意味論と自然演繹による証明論の知識を仮定します．

普通の論理では論理結合子として\(\wedge, \vee, \to, \neg, \bot\)あたりを使っているかと思います． それぞれ「かつ」「または」「ならば」「否定」「矛盾」です． またこれらの他に重要な論理演算としてしばしば「かつ」「または」に否定をつけたNANDとNORが挙げられます． 今回はこれらを\(\uparrow, \downarrow\)で書くことにします． \[\begin{align*}
\varphi\uparrow\psi\ &\equiv \ \neg(\varphi\wedge\psi)\\
\varphi\downarrow\psi\ \equiv \ \neg(\varphi\vee\psi)
\end{align*}\] これらの論理演算は意味論や論理回路などの文脈で扱われることが多いかと思います． そこで今回はあえて証明論的な観点からこのNANDとNORについて調べてみることにしましょう．

2 普通の論理

本記事では論理結合子として\(\wedge, \vee, \to, \neg, \bot\)を用いる論理を「普通の論理」と呼ぶことにします． 普通の論理について簡単に復習しておきましょう． 以下では命題記号は何らか与えられており，論理式といえば命題論理の論理式とします．

2.1 普通の論理の意味論と証明論

まず，普通の論理の意味論において論理結合子は以下のような真理値関数\(\{0,1\}^n\to\{0,1\}\)に解釈されます．

この解釈と命題記号への真理値割り当て（ストラクチャ）を用いて論理式の真偽，さらには恒真性が定義されます．

次に普通の論理の証明論ですが，用意した論理結合子と展開したい論理に応じて適切な推論規則を用意します． 今回は古典論理で考えるので推論規則は次の通り．

各論理結合子ごとに導入と除去規則，さらに古典論理にするために背理法規則を用意しています． これら推論規則を組み合わせて証明が定義され，それにより論理式の証明可能性が定義されます．

こうして定義された論理式の恒真性と証明可能性に対して次の完全性定理が成り立つのでした．

この定理により古典論理の証明能力が必要十分なものであることが保証されます．

2.2 普通の論理におけるNANDとNOR

普通の論理について復習したところで，普通の論理におけるNANDとNORについてみておきます． 普通の論理においてNAND \(\uparrow\)とNOR \(\downarrow\)は以下の略記（糖衣構文）として定義されます． \[\begin{align*}
\varphi\uparrow\psi\ \equiv \ \neg(\varphi\wedge\psi)\\
\varphi\downarrow\psi\ &\equiv \ \neg(\varphi\vee\psi)
\end{align*}\] よって意味論における論理結合子の解釈に従ってNANDとNORの解釈を計算すると以下の真理値表が得られます．

ここでNANDとNORの重要性として「真理値関数としての完全性」が挙げられます． 例えば論理式\(\varphi\)に対してNANDを使った論理式\(\varphi\uparrow\varphi\)の解釈を考えると以下の真理値表が得られます．

これは否定\(\neg\)の真理値表と一致していることがわかると思います． 実は他の論理結合子についても同じように真理値表が一致するような論理式をNANDのみを用いて作ることができます． さらにNANDの代わりにNORを用いても同じことができます． 詳しくは後でも出てきますが，興味のある方は演習問題として考えてみてください．

真理値関数の集合\(F\)について，任意の真理値関数\(f\colon\{0,1\}^n\to\{0,1\}\ (n\geq1)\)を\(F\)に属する関数の合成で表すことができるとき\(F\)は完全であるといいます． 論理結合子を解釈した真理値関数と同一視するとき以下の集合は完全であることが知られています．

• \(\{\wedge, \neg\}\)

• \(\{\vee, \neg\}\)

• \(\{\to, \neg\}\)

• \(\{\to, \bot\}\)

• \(\{\uparrow\}\)

• \(\{\downarrow\}\)

とくに\(\uparrow\)と\(\downarrow\)はそれ1つだけで完全な真理値関数になっています． \(\wedge\)や\(\vee\)や\(\to\)はそれ1つだけでは完全ではないので\(\uparrow\)と\(\downarrow\)はこれらよりも良い性質を持っていると言うことができます． また，2項真理値関数であってそれ1つだけで完全となるようなものはこの2つしかないことが知られています．

3 NANDとNORの証明論

さて，ここからが本題です． ここまででNANDとNORは単体で完全だから重要なのだという話をしてきました． これは論理結合子を解釈した真理値関数の性質なので意味論の話になります． ところで完全性定理によれば意味論と証明論には対応関係があるのでした． ということはこれに対応する証明論側のなんかイイ話があるのでは？証明論においても\(\wedge\)や\(\vee\)や\(\to\)が\(\uparrow\)や\(\downarrow\)に置き換えられるのでは？という疑問が湧きます．

そこでここからは実際に上記の疑問を実現してみましょう． 具体的には\(\uparrow\)や\(\downarrow\)に対する推論規則を用意して，それにより普通の論理結合子と推論規則が置き換えられることを見ていきます．

3.1 NANDによる証明論

まずはNANDによる証明論を展開します． この節では論理式は命題記号と\(\uparrow\)のみを用いて定義されたものとします． \(\uparrow\)に対する推論規則を以下のように与えます．

\(\uparrow\)の導入と除去規則，古典論理にするために背理法規則を用意しています． これらの推論規則によって普通の論理の推論規則が派生規則として実現できることを示していきます．

\(\neg\)の定義と推論規則

NANDによる論理において「否定」\(\neg\)は次のように定義します． \[\begin{align*}
\neg\varphi\ \equiv \ \varphi\uparrow\varphi
\end{align*}\] するとNANDによる論理の推論規則\(\lbrack\uparrow\mbox{背理法}\rbrack\)は普通の論理の推論規則\(\lbrack\mbox{背理法}\rbrack\)になっていることがわかります． また普通の論理の推論規則\(\lbrack\neg\mbox{導入}\rbrack\)と\(\lbrack\neg\mbox{除去}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \uparrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{\varphi\uparrow\varphi}
{\infer*
{\bot}
{\infer[1]{\varphi}{}}
}
\hspace{4.0em}
\infer[\lbrack\uparrow\mbox{除去}\rbrack]
{\bot}
{\varphi & \varphi \varphi\uparrow\varphi}
\end{gather*}\]

\(\wedge\)の定義と推論規則

NANDによる論理において「かつ」\(\wedge\)は次のように定義します． \[\begin{align*}
\varphi\wedge\psi\ &\equiv \ (\varphi\uparrow\psi)\uparrow(\varphi\uparrow\psi)
\end{align*}\] すると普通の論理の推論規則\(\lbrack\wedge\mbox{導入}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \uparrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{(\varphi\uparrow\psi)\uparrow(\varphi\uparrow\psi)}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{\varphi \psi & \infer[1]{\varphi\uparrow\psi}{}}
}
\end{gather*}\] また\(\lbrack\wedge\mbox{除去}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \uparrow\mbox{背理法} \rbrack\ 2\mbox{を解消}]
{\varphi}
{
\infer[\lbrack \uparrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{\varphi\uparrow\psi}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{
\infer[1]{\varphi}{}

\infer[1]{\varphi}{}
&
\infer[2]{\varphi\uparrow\varphi}{}
}
}

\infer*
{\varphi\uparrow\psi}
{\mbox{(左と同じ)}}
&
(\varphi\uparrow\psi)\uparrow(\varphi\uparrow\psi)
}
\end{gather*}\] \(\psi\)を導出する場合も同様に示せます．

\(\vee\)の定義と推論規則

NANDによる論理において「または」\(\vee\)は次のように定義します． \[\begin{align*}
\varphi\vee\psi\ \equiv \ (\varphi\uparrow\varphi)\uparrow(\psi\uparrow\psi)
\end{align*}\] すると普通の論理の推論規則\(\lbrack\vee\mbox{導入}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \uparrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{(\varphi\uparrow\varphi)\uparrow(\psi\uparrow\psi)}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{\varphi & \varphi \infer[1]{\varphi\uparrow\varphi}{}}
}
\end{gather*}\] \(\psi\)から導出する場合も同様に示せます． また\(\lbrack\vee\mbox{除去}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \uparrow\mbox{背理法} \rbrack\ 3\mbox{を解消}]
{\chi}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{
\infer[\lbrack \uparrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{\varphi\uparrow\varphi}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{
\infer*{\chi}{\infer[1]{\varphi}{}}
&
\infer*{\chi}{\infer[1]{\varphi}{}}

\infer[3]{\chi\uparrow\chi}{}
}
}
&
\infer[\lbrack \uparrow\mbox{導入} \rbrack\ 2\mbox{を解消}]
{\psi\uparrow\psi}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{
\infer*{\chi}{\infer[2]{\psi}{}}

\infer*{\chi}{\infer[2]{\psi}{}}
&
\infer[3]{\chi\uparrow\chi}{}
}
}

(\varphi\uparrow\varphi)\uparrow(\psi\uparrow\psi)
}
}
\end{gather*}\]

\(\to\)の定義と推論規則

NANDによる論理において「ならば」\(\to\)は次のように定義します． \[\begin{align*}
\varphi\to\psi\ &\equiv \ \varphi\uparrow(\psi\uparrow\psi)
\end{align*}\] すると普通の論理の推論規則\(\lbrack\to\mbox{導入}\rbrack\)と\(\lbrack\to\mbox{除去}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \uparrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{\varphi\uparrow(\psi\uparrow\psi)}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{
\infer*{\psi}{\infer[1]{\varphi}{}}

\infer*{\psi}{\infer[1]{\varphi}{}}
&
\infer[1]{\psi\uparrow\psi}{}
}
}
\hspace{4.0em}
\infer[\lbrack \uparrow\mbox{背理法} \rbrack\ 1\mbox{を解消}]
{\psi}
{
\infer[\lbrack \uparrow\mbox{除去} \rbrack]
{\bot}
{
\varphi

\infer[1]{\psi\uparrow\psi}{}
&
\varphi\uparrow(\psi\uparrow\psi)
}
}
\end{gather*}\]

よって普通の論理の推論規則はすべてNANDによる論理において実現できることがわかりました．

3.2 NORによる証明論

次にNORによる証明論を展開します． この節では論理式は命題記号と\(\downarrow\)のみを用いて定義されたものとします． \(\downarrow\)に対する推論規則を以下のように与えます．

\(\downarrow\)の導入と除去規則，古典論理にするために背理法規則を用意しています． これらの推論規則によって普通の論理の推論規則が派生規則として実現できることを示していきます．

\(\neg\)の定義と推論規則

NORによる論理において「否定」\(\neg\)は次のように定義します． \[\begin{align*}
\neg\varphi\ &\equiv \ \varphi\downarrow\varphi
\end{align*}\] するとNORによる論理の推論規則\(\lbrack\downarrow\mbox{背理法}\rbrack\)は普通の論理の推論規則\(\lbrack\mbox{背理法}\rbrack\)になっていることがわかります． また普通の論理の推論規則\(\lbrack\neg\mbox{導入}\rbrack\)と\(\lbrack\neg\mbox{除去}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{\varphi\downarrow\varphi}
{
\infer*
{\bot}
{\infer[1]{\varphi}{}}

\infer*
{\bot}
{\infer[1]{\varphi}{}}
}
\hspace{4.0em}
\infer[\lbrack\downarrow\mbox{除去}\rbrack]
{\bot}
{\varphi & \varphi\downarrow\varphi}
\end{gather*}\]

\(\wedge\)の定義と推論規則

NORによる論理において「かつ」\(\wedge\)は次のように定義します． \[\begin{align*}
\varphi\wedge\psi\ \equiv \ (\varphi\downarrow\varphi)\downarrow(\psi\downarrow\psi)
\end{align*}\] すると普通の論理の推論規則\(\lbrack\wedge\mbox{導入}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{(\varphi\downarrow\varphi)\downarrow(\psi\downarrow\psi)}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{\varphi & \infer[1]{\varphi\downarrow\varphi}{}}

\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{\psi & \infer[1]{\psi\downarrow\psi}{}}
}
\end{gather*}\] また\(\lbrack\wedge\mbox{除去}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \downarrow\mbox{背理法} \rbrack\ 1\mbox{を解消}]
{\varphi}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{
\infer[1]{\varphi\downarrow\varphi}{}

(\varphi\downarrow\varphi)\downarrow(\psi\downarrow\psi)
}
}
\end{gather*}\] \(\psi\)を導出する場合も同様に示せます．

\(\vee\)の定義と推論規則

NORによる論理において「または」\(\vee\)は次のように定義します． \[\begin{align*}
\varphi\vee\psi\ &\equiv \ (\varphi\downarrow\psi)\downarrow(\varphi\downarrow\psi)
\end{align*}\] すると普通の論理の推論規則\(\lbrack\vee\mbox{導入}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{(\varphi\downarrow\varphi)\downarrow(\psi\downarrow\psi)}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{\varphi \infer[1]{\varphi\downarrow\psi}{}}
}
\end{gather*}\] \(\psi\)から導出する場合も同様に示せます． また\(\lbrack\vee\mbox{除去}\rbrack\)は次のように示せます．

\[\begin{gather*}
\infer[\lbrack \downarrow\mbox{背理法} \rbrack\ 3\mbox{を解消}]
{\chi}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{\varphi\downarrow\varphi}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{
\infer*{\chi}{\infer[1]{\varphi}{}}
&
\infer[3]{\chi\downarrow\chi}{}
}

\infer*
{\bot}
{\mbox{(左と同じ)}}
}
&
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 2\mbox{を解消}]
{\psi\downarrow\psi}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{
\infer*{\chi}{\infer[2]{\psi}{}}

\infer[3]{\chi\downarrow\chi}{}
}
&
\infer*
{\bot}
{\mbox{(左と同じ)}}
}

(\varphi\downarrow\varphi)\downarrow(\psi\downarrow\psi)
}
}
\end{gather*}\]

\(\to\)の定義と推論規則

NORによる論理において「ならば」\(\to\)は次のように定義します． \[\begin{align*}
\varphi\to\psi\ &\equiv \ ((\varphi\downarrow\varphi)\downarrow\psi)\downarrow((\varphi\downarrow\varphi)\downarrow\psi)
\end{align*}\] すると普通の論理の推論規則\(\lbrack\to\mbox{導入}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 2\mbox{を解消}]
{((\varphi\downarrow\varphi)\downarrow\psi)\downarrow((\varphi\downarrow\varphi)\downarrow\psi)}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{\varphi\downarrow\varphi}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{
\infer*{\psi}{\infer[1]{\varphi}{}}

\infer[2]{(\varphi\downarrow\varphi)\downarrow\psi}{}
}
&
\infer*
{\bot}
{\mbox{(左と同じ)}}
}

\infer[2]{(\varphi\downarrow\varphi)\downarrow\psi}{}
}
&
\infer*
{\bot}
{\mbox{(左と同じ)}}
}
\end{gather*}\] また\(\lbrack\to\mbox{除去}\rbrack\)は次のように示せます． \[\begin{gather*}
\infer[\lbrack \downarrow\mbox{背理法} \rbrack\ 2\mbox{を解消}]
{\psi}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{
\infer[\lbrack \downarrow\mbox{導入} \rbrack\ 1\mbox{を解消}]
{(\varphi\downarrow\varphi)\downarrow\psi}
{
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{\varphi \infer[1]{\varphi\downarrow\varphi}{}}
&
\infer[\lbrack \downarrow\mbox{除去} \rbrack]
{\bot}
{\infer[1]{\psi}{} \infer[2]{\psi\downarrow\psi}{}}
}
&
((\varphi\downarrow\varphi)\downarrow\psi)\downarrow((\varphi\downarrow\varphi)\downarrow\psi)
}
}
\end{gather*}\]

よって普通の論理の推論規則はすべてNORによる論理において実現できることがわかりました．

4 まとめ

ここまでで確認したことから今回用意したNANDやNORによる論理はどちらも普通の論理と等価であり，古典論理を定めることがわかります．

正確にはこれを結論付けるにはここまでやってきたことの逆，つまりNANDによる論理やNORによる論理の推論規則が普通の論理において派生規則となっていることを示す必要があります． それを示すには余白が足りないのでこれは読者への演習問題としておきましょう．