自然演繹の証明図を作成する手順
2010SE052

市川貴之

指導教員：佐々木克巳

はじめにていない) どの仮定にも自由変数としては現れないような対象変数とする．(⊃ E)，(∧I)，(∧E)，(∨I)，(⊥)，(∃I)，
本研究の目的は，[1] にしたがって，自然演繹の体系 NK(∀E) が直前の論理式にのみ依存する局所的な推論規則での証明図を作成し，また，その作成の手順を説明するこあるのに対し，(⊃ I)，(∨E)，(RAA)，(∀I)，(∃E) は証とである．その説明は，NK の証明図における各推論規明全体に関係した大域的な推論規則であるという違いが則に対応して行い，どの段階で何が行われているのかをある．
明らかにする．卒業論文では１４の証明図を対象とした
NK の証明図とはこれらの推論規則を繰り返し適用すが，本稿ではそのうち４つの証明図を対象とする．２節
ることにより得られる木の形をした図式である．証明図
では，自然演繹の体系 NK を小野 [1] を参考にして導入の一番下の論理式をこの結論という．
し，３節では，証明図を作成する手順の説明を行う．
証明図の途中で使われた (⊃ I)，(∨E)，(RAA)，(∀I)，(∃E) により，この証明図の仮定 (すなわち，証明図の一2 自然演繹の定義番うえにある論理式) はとり除いてよい．ここでどの推
この節では，自然演繹の体系 NK を，小野 [1] を参考に論規則の適用でとり除かれたのかを明らかにするために，して導入する．
その推論規則の適用が行われた場所ととり除かれた論理
述語論理の言語に次のものを使う．
式に同じ番号をつけて区別することでわかりやすい証明
1) 論理記号 ∧，∨，⊃，¬
図の作成ができる．(∨E) の場合には，上の二つの C の2) 量化記号 ∀，∃うちの左側の C を結論とする証明図に現れる仮定 A およ
3) 対象変数 x，y ，z ，· · ·び右側の C を結論とする証明図に現れる仮定 B はとり除
4) 述語記号 P ，Q，· · ·いてよい．
述語論理の論理式の定義については，以下にしたがう．
なお，(RAA) は背理法 (reductio ad absurdum) を表す．
定義１
1) P が n 変数の述語記号，x1 ，· · · ，xn が対象変数であ 3 証明図の作成とその手順るならば，P (x1 ，· · · ，xn ) は論理式である．
この節では，体系 NK の証明図の作成の手順について
2) A，B がともに論理式であるならば，(A∧B)，(A∨B)，
説明し，どの段階で何がおこなわれているかを明らかに(A ⊃ B)，(¬A) はいずれも論理式である．
する．以下に，４つの例を示す．各例は，証明図とその3) A が論理式で，x が対象変数ならば，(∀xA)，(∃xA) は作成の手順の説明とで構成する．
ともに論理式である．
(1)(A ∨ B) ∨ C ⊃ (C ∨ A) ∨ B
体系 NK の推論規則は ⊃，∧，∨，∀，∃ についての導入と除去の規則および (⊥)，(RAA) からなる．それらの[A]4(∨I)
推論規則を以下に導ける．
[B]5C ∨A(∨I)(∨I)[A ∨ B]2 (C ∨ A) ∨ B(C ∨ A) ∨ B[A](∨E)4 ,5(C ∨ A) ∨ B
Π=A A⊃BB
AB(⊃ I)
(⊃ E)
(∧I)
A⊃B
B
A∧B
[C]3(∨I)C ∨A
A ∧ B (∧E)
A ∧ B (∧E)(∨I)[(A ∨ B) ∨ C]1 Π (C ∨ A) ∨ B
AB(∨E)2 ,3[A] [B](C ∨ A) ∨ B
AiA∨
BCC(⊃ I)1(∨I)(∨E)(A ∨ B) ∨ C ⊃ (C ∨ A) ∨ B
A1 ∨ A2(i = 1,2)
C1) 一番外側の記号に注目し (⊃ I) を行う．すなわち，
A[z/x](A ∨ B) ∨ C を仮定して (C ∨ A) ∨ B を導くことを示す．
∀xA (∀E)⊥ (⊥)(∀I)
A∀xAA[t/x]2) 仮定を先に使うことで仮定から結論に向けて証明図を作成できるので，仮定 (A ∨ B) ∨ C の一番外側の記号[¬A][A[z/x]]に注目し，(∨E) を行う．すなわち，A ∨ B を仮定して
A[t/x]∃xAB (∃E)⊥ (RAA)(∃I)(C∨A)∨Bを導くことと，C を仮定して (C ∨ A) ∨ B∃xA
BAただし，(∀I) と (∃I) の t は任意の項である。また，(∀I) を導くことを示す．
において z は ∀xA および A[z/x] に到る証明の (とり除か 3) 2) の仮定 C に注目し，(∨I) を行い C ∨ A を導く．
れていない) どの仮定にも自由変数としては現れないよう 4) (∨I) を行い，C ∨ A から (C ∨ A) ∨ B を導く．
な対象変数とする．同じように (∃E) において z は，∃xA， 5) 2) の仮定 A ∨ B の一番外枠の記号に注目し，(∨E) を
B および B に到る証明のうち A[z/x] 以外の (とり除かれ 行う．すなわち，A を仮定して (C ∨ A) ∨ B を導くこと

1∀x(A ⊃ C) を仮定して (∃xA ⊃ C) を導くことを示す．と，B を仮定して (C ∨ A) ∨ B を導くことを示す．
2) ∃xA ⊃ C に注目し，1) と同様に，∃xA を仮定して C
6) 5) の仮定 A に注目し，(∨I) を行い C ∨ A を導く．
を導くことを示す．
7) (∨I) を行い，C ∨ A から (C ∨ A) ∨ B を導く．
8) 5) の仮定 B に注目し，(∨I) を行い (C ∨ A) ∨ B を導 3) 変数条件のある (∃E) を優先して用いると失敗が少ないので，2) の仮定 ∃xA に注目し，(∃E) を行う．すなわ
く．
5′ ) 6),7) と 8) より，A から (C ∨ A) ∨ B を導くことと， ち，任意に z を与え，さらに A[z/x] を仮定して C を導B から (C ∨ A) ∨ B を導くことができた．ここで，5) の くことを示す．
4) ∀x(A ⊃ C) に注目し，(∀E) を行い (A ⊃ C)[z/x] を導二つの仮定 A と B はおちる．
2′ ) 5)〜5′ ) と 3)〜4) より，A ∨ B から (C ∨ A) ∨ B を導 く．ここで，C の条件より (A ⊃ C)[z/x] = A[z/x] ⊃ C
くことと，C から (C ∨ A) ∨ B を導くことができた．こ だから，A[z/x] ⊃ C を導く．
5) 3) の仮定 A[z/x] と A[z/x] ⊃ C に注目し，(⊃ E) をこで，2) の二つの仮定 A ∨ B と C はおちる．
1′ ) 2)〜2′ ) より，(A ∨ B) ∨ C から (C ∨ A) ∨ B を導くこ 行い C を導く．とができた．ここで，1) の仮定 (A ∨ B) ∨ C がおちる． 3′ ) 4),5) より，A[z/x] から C を導くことができた．ここで，3) の仮定 A[z/x] がおちる．
(2)((A ∨ B) ⊃ C) ⊃ (A ⊃ C) ∧ (B ⊃ C)
2′ ) 3)〜5) より，∃xA から C を導くことができた．ここ[A]2[B]3で，2) の仮定 ∃xA がおちる．
(∨I)
(∨I)
A∨B
[A ∨ B ⊃ C]1 A ∨ B[A ∨ B ⊃ C]1 1′ ) 2)〜2′ ) より，∀x(A ⊃ C) から (∃xA ⊃ C) を導くこCCとができた．ここで，1) の仮定 ∀x(A ⊃ C) がおちる．
(⊃ I)2(⊃ I)3A⊃CB⊃C(∧I)(4)(A ⊃ B) ⊃ (¬B ⊃ ¬A)(A ⊃ C) ∧ (B ⊃ C)(⊃ I)1((A ∨ B) ⊃ C) ⊃ (A ⊃ C) ∧ (B ⊃ C)
[A]3 [A ⊃ B]1(⊃ E)
ただし，(⊃ E) の記述は省略している．
B[¬B]2(¬E)1) 一番外側の記号に注目し (⊃ I) を行う．すなわち，⊥ (¬I)
3(A ∨ B) ⊃ C を仮定して (A ⊃ C) ∧ (B ⊃ C) を導くこと¬A(⊃ I)2¬B ⊃ ¬Aを示す．
(⊃ I)1(A ⊃ B) ⊃ (¬B ⊃ ¬A)2) 仮定から情報が得られないので，(A ⊃ C) ∧ (B ⊃ C)に注目し，(∧I) を行い，A ⊃ C ，B ⊃ C をそれぞれ導 1) 一番外側の記号に注目し (⊃ I) を行う．すなわち，A ⊃B を仮定して ¬B ⊃ ¬A を導くことを示す．
けばよいとわかる．
3) A ⊃ C に注目し，(⊃ I) を行う．すなわち，A を仮定 2) 仮定から情報が得られないので，¬B ⊃ ¬A に注目し(⊃ I) を行う。すなわち，¬B を仮定して ¬A が導かれるして C を導くことを示す．
ことを示す．
4) 3) の仮定 A に注目し，(∨I) を行い A ∨ B を導く．
5) (⊃ E) を行い，A ∨ B と 1) の仮定 (A ∨ B) ⊃ C から 3) 仮定から情報が得られないので，(¬I) を行う．すなわ
ち，A を仮定して ¬A を導くことを示す．
C を導く．
′3 ) 4),5) より，A から C を導くことができた．ここで， 4) 3) の仮定 A と 1) の仮定 A ⊃ B に注目し，(⊃ E) を行い B を導く．
3) の仮定 A がおちる．
6) 3) と同様に B ⊃ C に注目し，(⊃ I) を行う．すなわ 5) (¬E) を行い，B と 2) の仮定 ¬B から ⊥ を導く．
3′ ) 4),5) より，A から ¬A を導くことができた．ここでち，B を仮定して C を導くことを示す．
3) の仮定 A がおちる．
7) 4) の仮定 B に注目し，(∨I) を行い A ∨ B を導く．
′2) 3)〜3′ ) より，¬B から ¬A を導くことができた．ここ
8) (⊃ E) を行い，A ∨ B と 1) の仮定 (A ∨ B) ⊃ C からで，2) の仮定 ¬B がおちる．
C を導く．
′′′4 ) 7),8) より，B から C を導くことができた．ここで， 1 ) 2)〜2 ) より，A ⊃ B から ¬B ⊃ ¬A を導くことができた．ここで，1) の仮定 A ⊃ B がおちる．
4) の仮定 B がおちる．
1′ ) 2)〜4′ ) より，(A ∨ B) ⊃ C から (A ⊃ C) ∧ (B ⊃ C)
4 おわりにを導くことができた．ここで，1) の仮定 (A ∨ B) ⊃ C が本研究で自然演繹の証明図を説明する手順について取おちる．
(3)∀x(A ⊃ C) ⊃ (∃xA ⊃ C)[ただし C に x が自由変数 り組み，結果として，様々な証明の手順があるなかで的確な手順をみつけ利用していくことができるようになっとしてあらわれないものとする．]
た．今回の研究ではシークエント計算との比較などを行[∀x(A ⊃ C)]1(∀E)
うことができなかったが，自然演繹についての研究を進[A[z/x]]3 A[z/x] ⊃ C(⊃ E)
めるにつれ興味をもつことができた．
C[∃xA]2(∃E)3C(⊃ I)2
参考文献∃xA ⊃ C(⊃ I)1[1] 小野寛晰：『情報科学における論理』．日本評論社, 東∀x(A ⊃ C) ⊃ (∃xA ⊃ C)
京,1994.
1) 一番外側の記号に注目し (⊃ I) を行う．すなわち，