3.4 命題代数

3.4.1 論理式の正規系

任意の命題論理式には、積和形 (sum-of-products) あるいは選言標準形 (disjunctive normal form, DNF) と呼ばれる特殊な形式の同値な命題論理式が存在する。

DNF の正確な定義を示す。命題変数 \(A\) またはその否定 \(\overline{\mathstrut A}\) をリテラル (literal) と呼び、異なる変数を持つリテラルの \(\operatorname{\text{\footnotesize AND}}\) を \(\operatorname{\text{\footnotesize AND}}\) 節 (\(\operatorname{\text{\footnotesize AND}}\)-clause) と呼ぶ。\(\operatorname{\text{\footnotesize AND}}\) 節の例を示す:

\[ A \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C} \]

これに対して \(A \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ C\) は \(\operatorname{\text{\footnotesize AND}}\) 節でない: \(B\) が二度現れるからである。

そして、任意個の \(\operatorname{\text{\footnotesize AND}}\) 節の \(\operatorname{\text{\footnotesize OR}}\) を DNF と呼ぶ。DNF の例を次に示す:

\[ (A \ \operatorname{\text{\footnotesize AND}} \ B) \ \operatorname{\text{\footnotesize OR}}\ (A \ \operatorname{\text{\footnotesize AND}} \ C) \tag{3.4}\]

任意の命題論理式と同値な DNF は真理値表から直接構築できる。例えば、論理式

\[ A \ \operatorname{\text{\footnotesize AND}} \ (B \ \operatorname{\text{\footnotesize OR}}\ C) \tag{3.5}\]

の真理値表は次の通りである:

\[ \def\arraystretch{1.2}\begin{array}{ccc|c} A & B & C & A \ \operatorname{\text{\footnotesize AND}} \ (B \ \operatorname{\text{\footnotesize OR}}\ C) \\ \hline \textbf{T} & \textbf{T} & \textbf{T} & \textbf{T} \\ \textbf{T} & \textbf{T} & \textbf{F} & \textbf{T} \\ \textbf{T} & \textbf{F} & \textbf{T} & \textbf{T} \\ \textbf{T} & \textbf{F} & \textbf{F} & \textbf{F} \\ \textbf{F} & \textbf{T} & \textbf{T} & \textbf{F} \\ \textbf{F} & \textbf{T} & \textbf{F} & \textbf{F} \\ \textbf{F} & \textbf{F} & \textbf{T} & \textbf{F} \\ \textbf{F} & \textbf{F} & \textbf{F} & \textbf{F} \end{array} \]

この真理値表の第 \(1\) 行からは、\(A\), \(B\), \(C\) が全て真のとき、つまり \(A \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ C\) が真のとき論理式 \(\text{(3.5)}\) が真だと分かる。同様に第 \(2\) 行と第 \(3\) 行からは、\(A \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}\) または \(A \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ C\) が成り立つときも論理式 \(\text{(3.5)}\) が真になると分かる。この三行以外に真理値表の最後の列が \(\textbf{T}\) となる行は存在しない。よって論理式 \(\text{(3.5)}\) は次の論理式と同値である:

\[ \small(A \ \operatorname{\text{\scriptsize AND}} \ B \ \operatorname{\text{\scriptsize AND}} \ C) \ \operatorname{\text{\scriptsize OR}}\ (A \ \operatorname{\text{\scriptsize AND}} \ B \ \operatorname{\text{\scriptsize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\scriptsize OR}}\ (A \ \operatorname{\text{\scriptsize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\scriptsize AND}} \ C) \tag{3.6}\]

論理式 \(\text{(3.6)}\) は任意の \(\operatorname{\text{\footnotesize AND}}\) 節がそれぞれの命題変数からなるリテラルをちょうど一つ含むような DNF である。こういった DNF を完全 DNF (full DNF) と呼ぶ。

DNF を異なる DNF に単純化できる場合もある。例えば論理式 \(\text{(3.4)}\) と論理式 \(\text{(3.6)}\) は同値な DNF であるものの、前者の方が単純である。

真理値表で最後の列が \(\textbf{F}\) である行に同様の操作を行うと、元の論理式と同値な連言標準形 (conjunctive normal form, CNF) と呼ばれる形式の論理式が得られる ── CNF は \(\operatorname{\text{\footnotesize OR}}\) 節 (\(\operatorname{\text{\footnotesize OR}}\)-clause) の \(\operatorname{\text{\footnotesize AND}}\) であり、\(\operatorname{\text{\footnotesize OR}}\) 節は異なる命題変数からなるリテラルの \(\operatorname{\text{\footnotesize OR}}\) である。

例えば、論理式 \(\text{(3.5)}\) の真理値表の第 \(4\) 行に注目すると、\(A\), \(B\), \(C\) がそれぞれ \(\textbf{T}\), \(\textbf{F}\), \(\textbf{F}\) のとき論理式 \(\text{(3.5)}\) が偽になると分かる。この条件は「\(\operatorname{\text{\footnotesize OR}}\) 節 \(\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ B \ \operatorname{\text{\footnotesize OR}}\ C\) が \(\textbf{F}\)」に等しい！また、第 \(5\) 行からは \(\operatorname{\text{\footnotesize OR}}\) 節 \(A \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut C}\) が \(\textbf{F}\) のとき論理式 \(\text{(3.5)}\) が偽だと分かる。これは、この二つの \(\operatorname{\text{\footnotesize OR}}\) 節の \(\operatorname{\text{\footnotesize AND}}\) が \(\textbf{F}\) のとき論理式 \(\text{(3.5)}\) が偽であることを意味する。真理値表の最後の列が \(\textbf{F}\) である全ての行に対する同様の議論から、論理式 \(\text{(3.5)}\) が次に示す CNF と同値だと結論できる:

\[ \begin{aligned} &(\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ B \ \operatorname{\text{\footnotesize OR}}\ C) \ \operatorname{\text{\footnotesize AND}} \ (A \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize AND}} \ (A \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize OR}}\ C) \ \operatorname{\text{\footnotesize AND}} \ \\ &(A \ \operatorname{\text{\footnotesize OR}}\ B \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize AND}} \ (A \ \operatorname{\text{\footnotesize OR}}\ B \ \operatorname{\text{\footnotesize OR}}\ C) \end{aligned} \]

ここでも、この論理式は任意の \(\operatorname{\text{\footnotesize OR}}\) 節がそれぞれの命題変数からなるリテラルをちょうど一つ含むような CNF である。このような CNF を完全 CNF (full CNF) と呼ぶ。

論理式から完全 DNF および完全 CNF を構築する手続きは任意の真理値表に対して行えるので、次の定理が分かる:

定理 3.4.1

任意の命題論理式には、同値な完全 DNF、そして同値な完全 CNF が存在する。

3.4.2 同値性の証明

真理値表を書くことで論理式の同値性や恒真性を確認する手法はすぐに行き詰まる: 論理式に \(n\) 個の命題変数が含まれるとき、真理値表は \(2^{n}\) 個の行を持つ。つまり命題変数の個数が増えると、性質を確認するための労力は指数的に増加する。たった \(30\) 個の命題変数しか持たない論理式でも、確認しなければならない行数は十億を超える！

これとは異なる一部の場合で有効なアプローチとして、代数を使った同値性の証明がある。命題論理式に現れる論理結合子を全て考えると議論が長くなるので、これからは \(\operatorname{\text{\footnotesize AND}}\), \(\operatorname{\text{\footnotesize OR}}\), \(\operatorname{\text{\footnotesize NOT}}\) だけを考える。こうしたとき問題が起きないのは、この三つから他の論理結合子を作れるからである。例えば \(A \ \operatorname{\text{\footnotesize IMPLIES}}\ B\) は \(\operatorname{\text{\footnotesize NOT}} (A) \ \operatorname{\text{\footnotesize OR}}\ B\) と同値である。他の論理結合子については問題 3.18 で考える。

論理式を別の同値な論理式に変形する方法を定める同値公理 (equivalence axiom) と呼ばれる規則をこれから見ていく。同値な論理式の間に \(\longleftrightarrow\) を書く記法が使われている。ここに示す公理が重要なのは、あらゆる同値性がこれらの公理を使って示せるからである。まず \(\operatorname{\text{\footnotesize AND}}\) に関する公理を示す。これは数の乗算規則に似ている:

\(\operatorname{\text{\footnotesize AND}}\) の可換律 (commutativity): \[ A \ \operatorname{\text{\footnotesize AND}} \ B \longleftrightarrow B \ \operatorname{\text{\footnotesize AND}} \ A \tag{3.7}\]
\(\operatorname{\text{\footnotesize AND}}\) の結合律 (associativity): \[ (A \ \operatorname{\text{\footnotesize AND}} \ B) \ \operatorname{\text{\footnotesize AND}} \ C \longleftrightarrow A \ \operatorname{\text{\footnotesize AND}} \ (B \ \operatorname{\text{\footnotesize AND}} \ C) \tag{3.8}\]
\(\operatorname{\text{\footnotesize AND}}\) の単位律 (identity): \[ \textbf{T} \ \operatorname{\text{\footnotesize AND}} \ A \longleftrightarrow A \]
\(\operatorname{\text{\footnotesize AND}}\) の零律 (zero): \[ \textbf{F} \ \operatorname{\text{\footnotesize AND}} \ A \longleftrightarrow \textbf{F} \]
\(\operatorname{\text{\footnotesize OR}}\) に対する \(\operatorname{\text{\footnotesize AND}}\) の分配律 (distributivity): \[ A \ \operatorname{\text{\footnotesize AND}} \ (B \ \operatorname{\text{\footnotesize OR}}\ C) \longleftrightarrow (A \ \operatorname{\text{\footnotesize AND}} \ B) \ \operatorname{\text{\footnotesize OR}}\ (A \ \operatorname{\text{\footnotesize AND}} \ C ) \tag{3.9}\]

\(\operatorname{\text{\footnotesize AND}}\) の結合律 \(\text{(3.8)}\) があるために、括弧を付けない \(A \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ C\) という書き方が正当化される。この命題が \((A \ \operatorname{\text{\footnotesize AND}} \ B) \ \operatorname{\text{\footnotesize AND}} \ C\) と \(A \ \operatorname{\text{\footnotesize AND}} \ (B \ \operatorname{\text{\footnotesize AND}} \ C)\) のどちらを意味したとしても真理値は変わらない。

算術式と異なり、論理式では「和」を「乗算」に分配できる:

\(\operatorname{\text{\footnotesize AND}}\) に対する \(\operatorname{\text{\footnotesize OR}}\) の分配律 (distributivity): \[ A \ \operatorname{\text{\footnotesize OR}}\ (B \ \operatorname{\text{\footnotesize AND}} \ C) \longleftrightarrow (A \ \operatorname{\text{\footnotesize OR}}\ B) \ \operatorname{\text{\footnotesize AND}} \ (A \ \operatorname{\text{\footnotesize OR}}\ C) \tag{3.10}\]

これ以外に、算術規則に直接対応しない公理が三つある:

\(\operatorname{\text{\footnotesize AND}}\) の冪等律 (idempotence): \[ A \ \operatorname{\text{\footnotesize AND}} \ A \longleftrightarrow A \]
\(\operatorname{\text{\footnotesize AND}}\) の矛盾律 (contradiction): \[ A \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A} \longleftrightarrow \textbf{F} \tag{3.11}\]
二重否定 (double negation): \[ \operatorname{\text{\footnotesize NOT}} (\overline{\mathstrut A}) \longleftrightarrow A \tag{3.12}\]

\(\operatorname{\text{\footnotesize OR}}\) に対する同様の公理も存在する。長くなるのでここに書くことはしないが、\(\operatorname{\text{\footnotesize OR}}\) に対する恒真律だけは示しておく:

\(\operatorname{\text{\footnotesize OR}}\) に対する恒真律 (validity): \[ A \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut A} \longleftrightarrow \textbf{T} \tag{3.13}\]

最後に Deド Morganモルガンの法則 (De Morgan's law) がある。この公理は \(\operatorname{\text{\footnotesize NOT}}\) を \(\operatorname{\text{\footnotesize AND}}\) と \(\operatorname{\text{\footnotesize OR}}\) に対して分配する方法を定める:

\(\operatorname{\text{\footnotesize AND}}\) に対する De Morgan の法則: \[ \operatorname{\text{\footnotesize NOT}} (A \ \operatorname{\text{\footnotesize AND}} \ B) \longleftrightarrow \overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B} \tag{3.14}\]
\(\operatorname{\text{\footnotesize OR}}\) に対する De Morgan の法則: \[ \operatorname{\text{\footnotesize NOT}} (A \ \operatorname{\text{\footnotesize OR}}\ B) \longleftrightarrow \overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \tag{3.15}\]

ここまでに示した公理の正しさは真理値表を使って簡単に確かめられる。

これらの公理を使うと、任意の論理式を同値な完全 DNF に変形できる。例として、論理式 \(\text{(3.5)}\) を否定した次の論理式を完全 DNF に変形してみよう:

\[ \operatorname{\text{\footnotesize NOT}} ((A \ \operatorname{\text{\footnotesize AND}} \ B) \ \operatorname{\text{\footnotesize OR}}\ (A \ \operatorname{\text{\footnotesize AND}} \ C)) \tag{3.16}\]

まず、\(\operatorname{\text{\footnotesize OR}}\) に対する De Morgan の法則 \(\text{(3.15)}\) を \(\text{(3.16)}\) に適用し、\(\operatorname{\text{\footnotesize NOT}}\) を論理式の内側に移動させる。この変形によって次の論理式が得られる:

\[ \operatorname{\text{\footnotesize NOT}} (A \ \operatorname{\text{\footnotesize AND}} \ B) \ \operatorname{\text{\footnotesize AND}} \ \operatorname{\text{\footnotesize NOT}} (A \ \operatorname{\text{\footnotesize AND}} \ C) \]

続いて、\(\operatorname{\text{\footnotesize AND}}\) に対する De Morgan の法則 \(\text{(3.14)}\) を二つの \(\operatorname{\text{\footnotesize AND}}\) に適用し、次の論理式を得る:

\[ (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B}) \ \operatorname{\text{\footnotesize AND}} \ (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut C}) \tag{3.17}\]

次は \(\operatorname{\text{\footnotesize OR}}\) に対する \(\operatorname{\text{\footnotesize AND}}\) の分配律 \(\text{(3.9)}\) を繰り返し適用することで \(\text{(3.17)}\) を DNF に変換する。まず \((\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B})\) を分配し、次の論理式を得る:

\[ ((\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B}) \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A}) \ \operatorname{\text{\footnotesize OR}}\ ((\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut B}) \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \]

今度は \(\overline{\mathstrut A}\) と \(\overline{\mathstrut C}\) を分配すれば次の論理式が得られる:

\[ ((\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A}) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A})) \ \operatorname{\text{\footnotesize OR}}\ ((\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C})) \]

この変形では \(\operatorname{\text{\footnotesize AND}}\) の可換律 \(\text{(3.7)}\) を使って \(\operatorname{\text{\footnotesize AND}}\) を左から分配することを正当化している。続いて、冪等律を使って重複している \(\overline{\mathstrut A}\) を取り除く:

\[ (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A})) \ \operatorname{\text{\footnotesize OR}}\ ((\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C})) \]

後は \(\operatorname{\text{\footnotesize OR}}\) の結合律で括弧を外せば、論理式 \(\text{(3.16)}\) と同値な DNF が得られる:

\[ \overline{\mathstrut A} \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A}) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \tag{3.18}\]

最後から二番目のステップとして、この DNF を完全 DNF に変形する。この変形は \(\operatorname{\text{\footnotesize AND}}\) 節ごとに個別に行える。ここでは \(\operatorname{\text{\footnotesize AND}}\) 節 \(\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A}\) を使って説明する。この節を完全 DNF で使うには、命題変数 \(C\) を加える必要がある。そのために、\(\operatorname{\text{\footnotesize OR}}\) の恒真律と \(\operatorname{\text{\footnotesize AND}}\) の単位律から得られる次の関係を利用する:

\[ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A}) \longleftrightarrow (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A}) \ \operatorname{\text{\footnotesize AND}} \ (C \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut C}) \]

さらに \(\operatorname{\text{\footnotesize OR}}\) の分配律で \((\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A})\) を \((C \ \operatorname{\text{\footnotesize OR}}\ \overline{\mathstrut C})\) に対して分配すれば、完全 DNF で使える \(\operatorname{\text{\footnotesize AND}}\) 節が得られる:

\[ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ C) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \]

同様の処理を DNF の各 \(\operatorname{\text{\footnotesize AND}}\) 節に対して行えば、論理式 \(\text{(3.5)}\) と同値な完全 DNF がついに手に入る:

\[ \begin{aligned} & (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ C) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ C) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ C) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C} \ \operatorname{\text{\footnotesize AND}} \ B) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B}) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C} \ \operatorname{\text{\footnotesize AND}} \ A) \ \operatorname{\text{\footnotesize OR}}\ (\overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut A}) \end{aligned} \]

最後のステップとして、可換律を使って \(\operatorname{\text{\footnotesize AND}}\) 節内の命題変数と \(\operatorname{\text{\footnotesize AND}}\) 節自体をソートし、\(\operatorname{\text{\footnotesize OR}}\) の冪等律を使って同じ \(\operatorname{\text{\footnotesize AND}}\) 節を除去する。以上の変形により、重複を含まないソート済みの完全 DNF が得られる。こういった完全 DNF を標準 DNF (canonical DNF) と呼ぶ:

\[ \begin{aligned} & (A \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ C ) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ B \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ C ) \ \operatorname{\text{\footnotesize OR}}\ \\ & (\overline{\mathstrut A} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut B} \ \operatorname{\text{\footnotesize AND}} \ \overline{\mathstrut C}) \\ \end{aligned} \]

この例が示すのは、任意の命題論理式に同値公理を適用することで同値な標準 DNF を得る一般的な手続きである。つまり次の定理が成り立つ:

定理 3.4.2

同値公理を使うと、任意の命題論理式と同値な標準 DNF (および同値性の証明) が得られる。

この定理と論理式の同値性に何か関係があるだろうか？大いにある: 二つの論理式が同値だと示すには、両者を標準 DNF に変形すればよい (ただし、変形先は二つの論理式に現れる命題変数全てに関する標準 DNF とする)。もし二つの論理式が同じ標準 DNF に変形されるなら、両者は明らかに同値である。逆に、真理値表からは以前に示した方法で完全 DNF を構築できる。つまり二つの論理式が同値なら、両者は (いずれかに現れる命題変数に対応する列を持った) 真理値表において同じ真理値を持ち、同じ標準 DNF に変形される。つまり次の定理が成り立つ:

定理 3.4.3[同値公理の完全性]

二つの命題論理式が同値なのは、上記の同値公理を使って同じ論理式に変形できるとき、かつそのときに限る。

DNF ではなく CNF を使った場合でも同様のアプローチで同様の結果が得られる点に注意してほしい。

この定理があると、真理値表を使わない独創的な同値性の証明が可能になる。さらに、定理 3.4.3 は任意の二論理式間の同値性に関する証明が同値公理によって提供されることを保証する。本節のオチとしてふさわしい結果だろう。

ただ、惑わされないでほしい: 定理 3.4.3 が存在を保証する証明には標準 DNF が必要であり、標準 DNF とは本質的に元の論理式の真理値表である。一般に、同値性の代数的証明が標準形への変換より簡単になると期待できる理由はない。つまり、代数的証明が真理値表による証明 (確認) より必ず簡単になるわけではない。