命題論理の導出計算における導出原理適用の制限
M2008MM030 山田敏成
指導教員：佐々木克巳

1

はじめに

節 C に到る R0 の導出図を次のように定義しておく。

本論文は、命題論理を対象とし、正導出であり、かつ、定義 2.2(R0 の導出図)
線形導出でもある導出計算 (線形正導出) と、線形正導出(1) 節 C が節集合 S に属すときには、C だけの制約条件を少し弱めた導出計算について考察する。本からなる図は S から C に到る R0 の導出図であ稿の 1 節では、小野 [1] にもとづいて命題論理の導出原理る。と三つの導出計算 R0 、正導出、線形導出を紹介する。2
節では、線形正導出の完全性に対する反例をあげること、(2) S から節 C1 に到る R0 の導出図 P1 と S
および、この完全性において対象を制限したときの一つから節 C2 に到る R0 の導出図 P2 がすでに定義の性質を述べる。この性質から、ここであげる反例が最されているとする。さらに C1 と C2 から導出も簡単なものの一つになっていることが導かれる。そし原理により節 C が得られるものとする。このとて、3 節では、線形正導出の制約条件を少し弱めた導出計
き、つぎのように与えられる図は S から C に到算について述べる。
る R0 の導出図である。

2

命題論理の導出計算

この節では、[1] にもとづいて、命題論理の導出原理と三つの導出計算 R0 、正導出、線形導出を紹介する。
まず、命題論理を導入する。命題変数に表すために、p, q, r, · · · などの記号を用いる。論理結合子は ∧(かつ)、∨(または)、⊃(ならば)、¬(でない) を用いる。これらの論理結合子を繰り返し用いることにより、通常の方法で論理式を定義する。

{P1}
＼／＼ ／
C2C1P2＼

図 2.1／CS から C に到る R0 の導出図

節集合 S から節 C に到る R0 の導出図が存在するとき、R0 で、S から C は導出可能であるという。

定義 2.1(トートロジー) 命題変数へのすべての真理値の与え方について、論理式 A の真理値が真であるとき、
定義 2.3 節 C がリテラルの集合 {A1 , · · · , Ak } である∧
A はトートロジーという。
とき C は、論理式 A1 ∧ · · · ∧ Ak を表すものとする。と∧くに、 □は恒真な論理式を表すものとする。空でないつぎに、命題論理の導出原理を導入する。命題変数ま節集合 S = {C1 , · · · , Cm } に対し S の論理和標準形表現
たは命題変数の前に否定記号を一つつけた論理式のこと
d(S) ををリテラルという。二つのリテラル A と B が相補的であ∧∧d(S) = ( C1 ) ∨ · · · ∨ ( Cm )るとは B = ¬A であるか A = ¬B であることとする。リと定める。
テラル A と相補的なリテラルを A∗ と表す。すなわち

A が p のとき A∗ = ¬p
A が ¬p のとき A∗ = pである。
リテラルの有限集合を節という。空集合の場合には空節とよび、それを□で表す。節の有限集合を節集合という。
二つの節 C1 と C2 に対し、C1 に属す一つのリテラルA の相補的なリテラル A∗ が C2 に属しているとする。このとき節 (C1 − {A}) ∪ (C2 − {A∗ }) を C1 と C2 からの導出節という。二つの節から導出節を作りだす操作のことを導出原理という。
導出原理を繰り返し適用し、節集合から一つの節を導き出す過程を記述するために、命題論理の導出計算 R0 を導入する。R0 が扱うのは節であり、R0 のただ一つの論理的操作は導出原理であるものとする。これらのことをより明確な形で述べるために、与えられた節集合 S からR0 の導出可能性と、トートロジーの間にはつぎの関係がある。
補助定理 2.1(導出計算 R0 の完全性)
S を任意の空でない節集合とする。このとき、d(S) がトートロジーであるための必要十分条件は、R0 で、S から□が導出可能になることである。
上で定義した R0 の導出を制限した導出も知られている。以下では、その例である、正導出と線形導出について述べる。
定義 2.4(正導出) 節 C に含まれるリテラルがすべて命題変数であるとき、C を正節と呼ぶことにする。与えられた導出図 P に現われるすべての導出原理の適用において、一方の節が正節であるとき、P を正導出による導出

図という。さらに、節集合 S から節 C に到る正導出の導出図が存在するとき、正導出で、S から C は導出可能であるであるという。

形正導出の完全性が予想されるが、この予想には反例がある。
定理 3.1

節集合 S を正導出が完全であることは、[1] の練習問題と補助定理
S = {{a}, {¬a, b}, {¬a, c}, {¬b, ¬c}}
2.1 から示される。すなわち、つぎの補助定理が成立する。 とおく。このとき、つぎの 2 条件が成立する。
補助定理 2.2(正導出の完全性) S を任意の空でない節集合とする。このとき、d(S) がトートロジーであるための必要十分条件は、正導出で、S から□が導出可能になることである。
定義 2.5(線形導出) 節集合 S から空節□に到る導出
図 P に対し、P の中の節の列 C0 , C1 , · · · , Cn およびD0 , D1 , · · · , Dn−1 が存在して、つぎの 3 条件を満たす
とき、P は線形導出による導出図であるという。

(1) C0 ∈ S かつ Cn = □である。
(2) 各 k ≥ 0 に対し、Ck+1 は Ck と Dk からの導出節である。
(3) 各 k ≥ 0 に対し、Dk ∈ S またはある j ≤ kに対し Dk = Cj である。
また、節集合 S から節 C に到る線形導出の導出図が存在するとき、線形導出で、S から C は導出可能であるであるという。
線形導出が完全であることは Chang and Lee [2] で述べてある。すなわち、つぎの補助定理が成立する。

(1) d(S) はトートロジーである。
(2) S から□に到る線形正導出による導出図は存在しない。
証明 補助定理 2.1 より、d(S) がトートロジーであることを示すには、S から□が R0 で導出可能であることを示せばよい。これは、つぎの図 3.1 で示される。

{a}
＼

図 3.1

{¬a, b}／{b}{¬b, ¬c}＼ ／{¬c} {¬a, c}＼ ／{¬a} {a}＼ ／□S から□に到る R0 の導出図

つぎに、S から□に到る線形正導出による導出図 P が存在すると仮定する。線形導出であることから P はつぎの図 3.2 の形をしている。

C0D0＼ ／
C1D1＼ ／C2D2＼ ／3 線形正導出．
この節では、線形正導出の完全性に対する反例をあげ．
ること、および、この完全性において対象を制限したと．
きの一つの性質を述べる。この性質からここであげる反Cn−1
Dn−1
例が最も簡単なものの一つになっていることが導かれる。
＼ ／まず、線形正導出を定義しておく。
□
図 3.2 線形導出による導出図 P
定義 3.1(線形正導出) 節集合 S から節 C に到る R0 の
ただし、
C0 , C1 , · · · , Cn 、および、D0 , D1 , · · · , Dn−1 は導出図 P が 2 条件
定義 2.5 の条件を満たす。
(1) 正導出による導出図である
S に属す正節は {a} だけなので、C0 か D0 は {a}(2) 線形導出による導出図であるである。C0 = {a} としても一般性は失われない。こを満たすとき、P は線形正導出による導出図という。まのとき、(D0 , C1 ) = ({¬a, b}, {b}) または (D0 , C1 ) =た、節集合 S から節 C に到る線形正導出の導出図が存在({¬a, c}, {c}) である。どちらの場合でも D1 = {¬b, ¬c} でするとき、線形正導出で、S から C が導出可能であるとあるので、(D1 , C2 ) = ({¬b, ¬c}, {¬c}) または (D1 , C2 ) =いう。
({¬b, ¬c}, {¬b}) である。どちらの C2 も正節でない。P
は正導出による導出図なので D2 は正節で、定義 2.5 の条
補助定理 2.2 と補助定理 2.3 で、正導出、および線形導件より D2 ∈ S である。よって D2 = {a} である。した出の完全性が成立することを述べた。この結果から、線がって、どちらの C2 に対しても、C2 と D2 から導出節
補助定理 2.3(線形導出の完全性) S を任意の空でない節集合とする。このとき、d(S) がトートロジーであるための必要十分条件は、線形導出で、S から□が導出可能になることである。

を導くことはできない。これは P が導出図であることに矛盾する (図 3.3 参照)。
■ある。
正節

N!節N!節N!節＼ ／＼／正節
N!節
図 3.5 C を導出節とする導出原理の適用{a}{¬a, b}{a}{¬a, c}＼ ／＼ ／{b} {¬b, ¬c}{c} {¬b, ¬c}＼ ／＼ ／定理 3.2 の証明 S から C に到る正導出による導出図を{¬c}×{¬b}×P とする。P の中の N!節を C1 とする。C1 が D1 と D2＼ ／＼ ／からの導出節とすると、P が正導出による導出図なので、図 3.3 線形正導出でないことを示す図
D1 と D2 のうち一つが正節でもう一つが非 N 節である。
上の反例では、節集合 S に節 {¬b, ¬c} が存在した。そ これは補助定理 3.3 に矛盾する。これより、C は導出節
1こで、S に {¬b, ¬c} のような、否定のリテラルを二個以 ではない。すなわち、P の中の N!節はどれも導出節でな上持つ節が存在しない場合について考える。
く、S の元である。さらに、補助定理 3.3 より、導出節は節 C は、C に属す否定のリテラルが一個以下のとき N どれも正節である。これより、P は S から C に到る線形節、二個以下のとき N2 節、ちょうど一個のとき N!節、 正導出による導出図である。
ちょうど二個のとき N2!節とよぶことにする。
以下では、節集合 S に非 N 節が存在しない。すなわち、定理 3.2 の逆は明らかなので、補助定理 2.1 よりつぎがS のどの節も N 節である場合を考える。
成立する。
定理 3.2 節集合 S において、S のどの節も N 節とする。
このとき、S から正節 C に到る正導出による導出図があるならば、S から C に到る線形正導出による導出図がある。

系 3.4 節集合 S において、S のどの節も N 節とする。
このとき、d(S) がトートロジーであるための必要十分条
件は、線形正導出で、S から□が導出可能になることである。

上の定理を証明するために、つぎの補助定理を示す。

定理 3.1 の S に属する N2!節は一つだけで、他の要素はどれも N 節であった。したがって、系 3.4 より定理 3.1の例は最も簡単な反例の一つといえる。

補助定理 3.3 節集合 S において、S のどの節も N 節とする。さらに、S から節 C に到る正導出による導出図をP とする。このとき、P に現れる節はすべて N 節である。
証明 P の中に現れる節の数を n(P) として、n(P) についての帰納法で題意を示す。
n(P) = 1 のとき：P を構成する節は一つだけで、それは C である。C ∈ S だから C は N 節である。
n(P) ＞ 1 のとき：C を導出節とする導出原理の適用がある。すなわち、ある C1 と C2 が存在して、C1 と C2 から正導出によって C が導出されている。P の中に、S から C1 に到る正導出による導出図 P1 がある。また、P の中に、S から C2 に到る正導出による導出図 P2 がある。
すなわち、P はつぎの形である。

{P1}
＼／＼ ／
C2C1P24

線形 N 導出定理 3.2 では、S のどの節も N 節の場合に、S から正節に到る R0 の導出図が存在すれば、S から C に到る線形正導出による導出図が存在することを示した。また、定理 3.1 より S の中に N2!節がある場合は、S から正節 Cに到る R0 の導出図があっても、S から正節 C に到る線形正導出による導出図があるとは限らないことがわかった。そこで、線形正導出の条件を少し弱めて、線形 N 導出を考えてみることにした。
定義 4.1(線形 N 導出)
導出図 P が 2 条件

節集合 S から節 C に到る R0 の

(1) P におけるすべての導出原理の適用において、一方の節が N 節である
(2) P は線形導出による導出図であるを満たすとき、P を線形 N 導出による導出図という。また、節集合 S から節 C に到る線形 N 導出の導出図が存在するとき、線形 N 導出で、S から C は導出可能である
n(P) ＞ n(P1 ) と n(P) ＞ n(P2 ) と帰納法の仮定により、 という。
P1 に現われる節および P2 に現われる節は、すべて N 節
しかし、研究の結果、線形 N 導出の完全性は成立しなである。とくに、C1 と C2 も N 節である。したがって、C1 と C2 は正節と N!節かあるいはどちらも N!節である。 い。すなわち、d(S) がトートロジーであっても、S から正節と N!節の場合、C は正節で、どちらも N!節の場合、 □に到る線形 N 導出による導出図は存在しない場合があC は N!節である (図 3.5 参照)。P に現われる節は、C か ることがわかった。
P1 に現われるか P2 に現われるかなので、どれも N 節で＼／C
図 3.4 導出図 P

定理 4.1

節集合 S をS = {{a}, {b}, {¬a, ¬b, c}, {¬a, ¬b, d}, {¬a, ¬b, e},{¬a, ¬b, f }, {¬c, ¬d, g}, {¬e, ¬f, h}, {¬g, ¬h}}
とおく。このとき、つぎの 2 条件が成立する。

(1) d(S) はトートロジーである。
(2) S から□に到る線形 N 導出による導出図は存在しない。
証明 補助定理 2.1 より、d(S) がトートロジーであることを示すには、S から□が R0 で導出可能であることは修士論文で示してある。
S から□に到る線形 N 導出による導出図 P が存在するとして、矛盾を導く。定義 2.5 より、P に C0 , C1 , · · · , Cn
および D0 , D1 , · · · , Dn−1 が存在して、これらの節は定義
2.5 の条件をみたす。
C0 , D0 ∈ S で、P が線形 N 導出による導出図である
ことより、一般性を欠くことなく、

C0 . . .
{a}｜ D0 . . .
｜{¬a, ¬b, c}
C1 ／ . . .
{¬b, c}｜ D1 . . .
{b} ／ ＼ {¬c, ¬d, g}
C2 ／ . . .
{c}{¬b, ¬d, g}｜ D2 . . .
{¬c, ¬d, g}｜／ {b}C3 ／ . . .
{¬d, g}｜ D3 . . .
{¬a, ¬b, d} ／ ＼ {¬g, ¬h}C4 ／ . . .
{¬a, ¬b, g}{¬d, ¬h} ×｜ D4 . . .
{a} ／＼ {b}C5 ／ . . .
{¬b, g}{¬a, g}｜ D5 . . .
{b} ／ ＼ {¬g, ¬h} ／ ＼ {a}C6 ／ . . .
{g}{¬b, ¬h} {¬a, ¬h} {g}｜ D6 . . . {¬g, ¬h} ＼ {b} ＼ ／ {a} ／ {¬g, ¬h}C7 ／ . . .
{¬h}｜ D7 . . .
｜{¬e, ¬f, h}
C8 ／ . . .
{¬e, ¬f } ×
図 4.1(1) の図上の図で□は現われない。これは、(∗) に矛盾する。
(1)(C0 , D0 ) = ({a}, {¬a, ¬b, c}),(2) のとき、S の c と d を入れ変えても S であること(2)(C0 , D0 ) = ({a}, {¬a, ¬b, d}),から、
(1) と同様に示される。
(3)(C0 , D0 ) = ({a}, {¬a, ¬b, e}),(3) のとき、(1) と同様に、つぎの図から矛盾を示すこ(4)(C0 , D0 ) = ({a}, {¬a, ¬b, f }),とができる。
(5)(C0 , D0 ) = ({b}, {¬a, ¬b, c}),C0 . . .
{a}(6)(C0 , D0 ) = ({b}, {¬a, ¬b, d}),｜ D0 . . .
｜{¬a, ¬b, e}(7)(C0 , D0 ) = ({b}, {¬a, ¬b, e}),C／.
.
.
{¬b,e}
1(8)(C0 , D0 ) = ({b}, {¬a, ¬b, f })｜ D1 . . .
{b} ／ ＼ {¬e, ¬f, h}のいずれかが成り立つと仮定できる。以下では、上の各C ／...
{e}{¬b, ¬f, h}
場合について、C1 , D1 , C2 , D2 , . . . を求めることを行う。 2｜ D2 . . .
{¬e, ¬f, h}｜／ {b}わかりやすくするため、Ci が求められていて、条件
C3 ／ . . .
{¬f, h}Ci と Di ∈ S から線形 N 導出の導出原理により｜ D3 . . .
{¬a, ¬b, f } ／ ＼ {¬g, ¬h}Ci+1 が導かれる
C4 ／ . . .
{¬a, ¬b, h}{¬f, ¬h} ×を満たす (Di , Ci+1 ) が (Di,1 , Ci+1,1 ), . . . , (Di,k ,｜ D4 . . .
{a} ／＼ {b}Ci+1,k ) のとき、すなわち、
C5 ／ . . .
{¬b, h}{¬a, h}CiDi,j｜ D5 . . .
{b} ／ ＼ {¬g, ¬h} ／ ＼ {a}＼／C6 ／ . . .
{h}{¬b, ¬g} {¬a, ¬g} {h}Ci+1,j｜ D6 . . . {¬g, ¬h} ＼ {b} ＼ ／ {a} ／ {¬g, ¬h}(j = 1, . . . , k) のように適用する図がかけるとき、これを、 C7 ／ . . .
{¬g}｜ D7 . . .
｜{¬c, ¬d, g}
Ci
C8 ／ . . .
{¬c, ¬d} ×
Di,1 ／ Di,2 | . . . ＼ Di,k
Ci+1,1 Ci+1,2 . . . Ci+1,k
図 4.2 (3) の図のように表す。k = 0 のときは、

Ci ×と表す。P が S から□に到る R0 の導出図であることより、ある i に対して、Ci = □となるから、上の手順でできる図に□が現われる (∗)。
以下、場合分けして矛盾を導く。
(1) のとき：上で定めた図は以下の図 4.1 のようになる。

(4) のとき、S の e と f を入れ替えても S であることから、(3) と同様に示される。
(5)〜(8) のとき、S の a と b を入れ変えても S であることから、(1)〜(4) と同様にそれぞれ示される。
■

参考文献[1] 小野寛晰,「情報科学における論理」, 日本評論社,1994.
[2] C. Chang and R. C. Lee, “Symbolic logic and mechanical theorem proving”, Academic Press, 1973.