数理解析研究所講究録976 巻 1997 年 13-26

13

NDK における自然な証明についての考察
八杉満利子 (Mariko Yasugi)
中田昌宏 (Masahiro Nakata)

京産大理学部
京産大理学研究科

本稿は、 [1] および [3] で提案された–階の古典論理の体系 NDK における自然な証明についての報告である。 体系 NDK のひとつの特徴は、 証明の短さにある。 その状況は [31 で述べている。

大芝は、 [2] において自動証明により得られた証明から、 人にとって自然な証明への変換を与えた。 これは、 cut-free proof から、 自然な場合分けによる証明を (元の証明の構造を保存するように) 生成するものである。
また NDK においては、 critical な推論と呼ばれる不自然な推論が行なわれることがある。 そこで、 大芝の着想にもとずく変換により、 この様な推論を持つ deduction を自然な deduction へ変換することを目的とする。

The system of NDK

1

構成的論理 NJ の古典論理への 1 っの拡張として NDK を定義する。 $A,$ $B,$
で formula を、 ,\Delta ,で formula 又は空なものを表凱 また、 deduction を$\cdots$$\Gamma$表す記号として、

1.1$P_{1},P_{2},$$\cdots$を用いる。

Disjunctive component

formula$A$の disjunctive component(d.c.) を次で定義する

1.

$A$

が atomic のとき、 $A$ の

2.

$A$

が $B\wedge C,$ $B\supset C,$ $\neg B,\forall xB,$

3.

$A$

が B\vee C のとき、 $A$ の

12$\mathrm{d}.\mathrm{c}$$\mathrm{d}.\mathrm{c}$

.は

$A$

$\exists XB$$\circ$自身のとき、 $A$ の. は Bの$\mathrm{d}.\mathrm{c}$$\mathrm{d}.\mathrm{c}$. 及び C の.は$\mathrm{d}.\mathrm{c}$

$A$

自身

. 及び A 自身

Inference rule

NDK の推論規則を、次で与える。 (I は introduction を、 $E$ は elimination
を表凱) NDK では前提となる formula の. の 1 つに推論規則を適用する$\mathrm{d}.\mathrm{c}$ことができる。

14

.
$-$

$.. \frac{\Gamma\vee\dot{A}\vee\Delta\Gamma \mathrm{v}\dot{B}\Delta}{\Gamma\vee(A\wedge B)\vee\Delta}..\wedge I$$\frac{\Gamma\vee(A_{1}\wedge A_{2})\mathrm{v}\Delta}{\Gamma A_{i}\mathrm{v}\Delta}\wedge E$$(i=1,2)$$\frac{\Gamma\bigvee_{A}\dot{4}_{i}\vee\Delta}{\Gamma\vee(A_{1}\vee A2)\vee\Delta}.\cdot.\vee I$$(i=1,2)$$[A : a]$.

$[B : b]$$. \cdot..\frac{\Gamma\vee(A\dot{\vee}B)\Delta\dot{c}^{:}\dot{c}}{\Gamma\vee c\mathrm{v}\Delta}.\cdot.\cdot..(a,b)-E$$[A : a]$$\frac{\Gamma\vee\dot{B}\vee\Delta}{\Gamma\vee(A\supset B)\mathrm{v}\Delta}..\cdot(a)-\supset I$$. \cdot.\frac{\Gamma\vee\dot{A}\mathrm{v}\Delta\Pi\vee(\dot{A}\supset B)\mathrm{v}\Lambda}{\Gamma\Pi\vee B\Delta\vee\Lambda}.\cdot.\cdot\supset E$$[A:a]$$\frac{\Gamma\dot{\vee}\Delta}{\Gamma\neg A\vee\Delta}.\cdot.(a)-\neg I$$. \cdot.\frac{\Gamma\vee\dot{A}\mathrm{v}\Delta\Pi\neg A\vee\Lambda}{\Gamma\Pi \mathrm{v}\Delta\vee\Lambda}..\cdot.\wedge\neg E$$\frac{\Gamma\vee\dot{A}\vee\Delta}{\Gamma\forall XA\Delta}.\cdot\cdot\forall I$$\frac{\Gamma\vee\forall xA\Delta}{\Gamma\vee A[t/x]\Delta}.\cdot.\cdot\forall E$(eigenvariable $\omega ndition$ )$[A:a]$$\frac{\Gamma\vee A[t]\mathrm{v}\Delta}{\Gamma\vee\exists xA\vee\Delta}.\cdot.\cdot\exists I$$\frac{\Gamma\vee\exists xA\mathrm{v}\triangle\dot{B}}{\Gamma\vee B\vee\Delta}.\cdot.\cdot.\cdot.(a)-\exists E$(eigenvariable condition)
特に r,, A の全てが空ではない推論を classical な推論と呼ぶ。 更に空な前提から任意の formula を導く contradiction rule を加える。
$\Delta,\Pi$$\overline{A}Con$

この空な前提は classical でない推論\neg E によってのみ得られる。

15

Eigenvariable

13は次の eigenvariable condition を満たすも, NK と同様に、 推論
において、において、 は assumption 及 vT, に自由に現れない。
のは $[A:a]$ 以外 B への deduction
assumption 及び に自由に現れない。
$\mathrm{N}\mathrm{J}$$\forall I,$$\forall I$$\exists E$$\exists E$$\Delta$

$x$

$x$

$B$

Comparing NDK with NK

2

本節では、 NDK と NK が論理的に同等となることを見る。 NK は NDKの部分体系であることは明らかである。 (排中律は rI を用いて演繹できる。)
以下で、 NDK が NK の部分体系となることを見る。

2.1$\mathrm{N}\mathrm{K}$Lemma
において A\vee B 及び\neg A がそれぞれ assumption の有限集合

ら演繹されるとき、 $B$ を$A_{1}\cup A_{2}$$A_{1},$ $A_{2}$より排中律を用いずに演繹することができる。

[証$A_{2}.$.

$\neg.\dot{A}$$[A:1]$$A_{1}$::$\frac{A\vee BB[B\cdot 2]}{B}.(1,2)$.

22

Theorem

NDK は$\mathrm{N}\mathrm{K}$の部分体系である。

[証明] NDK-deduction P の最後の推論に関する帰納法で示すもI が\wedge I のとき、 P は.
$. \cdot.\frac{\Gamma\vee\dot{A}\vee\Delta\Gamma \mathrm{v}\dot{B}\mathrm{v}\Delta}{\Gamma\vee(A\wedge B)\Delta}.\cdot$と表すことができ、 これは$\mathrm{N}\mathrm{K}$において次のようにできる。

:$\Gamma\vee\dot{A}.\vee\Delta$$[\Gamma\vee\Delta:1]$

:

か

:

$. \frac{\mathrm{r}\mathrm{v}\dot{\Delta}A\Gamma \mathrm{v}(A\wedge B)\mathrm{v}\Delta Q}{\Gamma\vee(A\wedge B)\Delta}.\cdot(1,3)$

16

ただし $Q$ は次の deduction である。

.
$. \frac{[A.3].[B\cdot 4]}{A\bigwedge_{\prime}B}$$\Gamma\vee\dot{B}..\cdot.\cdot\vee\Delta$$[\Gamma..\Delta:2]$$.. \frac{\Gamma\vee\dot{\Delta}\vee B\Gamma \mathrm{v}(A\wedge B)\Delta\Gamma\vee(A\wedge B)\Delta}{\Gamma\vee(A\wedge B)\Delta}.\cdot.(2,4)$

I が\wedge E のとき、 P は::$\frac{\Gamma\vee(A_{1}\wedge A_{2})\vee\Delta}{\Gamma A_{i}\vee\Delta}$と表すことができ、 これは$(i=1,2)$において次のようにできる。

$\mathrm{N}\mathrm{K}$.
$\Gamma\vee(A_{1}\wedge\cdot.\cdot.

A_{2})\vee\Delta$$\frac{[A_{1}\wedge A_{2}.2]}{A_{i}}$$[\Gamma\vee\Delta:1]$$. \cdot.\cdot\frac{\Gamma\vee\Delta \mathrm{v}(A_{1}\wedge A2)\Gamma \mathrm{v}\dot{A}i\Delta \mathrm{r}\dot{A}_{i^{}}\Delta}{\Gamma A_{i}\mathrm{v}\Delta}.\cdot..\cdot.(1,2)$

I が VE のとき、 P は$[A:1]$$[B.’ 21$$\frac{\Gamma\vee(A\mathrm{v}B)\vee\Delta C:\dot{C}}{\Gamma\vee C\Delta}.\cdot.\cdot.(1,2)$と表すことができ、 これは$\mathrm{N}\mathrm{K}$において次のようにできる。

.

$[A:1\iota$$\Gamma\vee(A_{1}\dot{\vee}..\cdot.A2)\vee\Delta$$[\Gamma\vee\Delta:3]$$\Gamma\vee\Delta\vee(.\cdot.A_{1}\mathrm{v}A_{2})$$\Gamma\vee\dot{C}.\cdot.\Delta$.

$[B:2]$$\dot{C.\cdot..}.\cdot\cdot$$\cdot\dot{C.\cdot..}.\cdot$$[AB:4]$$\Gamma\vee C\Delta$$\Gamma\vee C\vee\Delta$$\overline{\Gamma\vee C\Delta}(1,2)$$\overline{\Gamma\vee c_{\vee}\Delta}(3,4)$

17

I が以上の外で\supset I,, \forall I 以外のときも同様に行なう。

$\neg I$I が\urcorner I のとき、 P は$[A:1]$$\frac{\Gamma\vee\Delta}{\Gamma\vee\neg A\mathrm{v}\Delta}(1)$と表すことができ、 これは$\mathrm{N}\mathrm{K}$において排中律を用いることにより次のよう

にできる。
$[A$

:1

$]$

:
:

.

$\Gamma\vee\Delta$$[\urcorner A:2]$$\frac{A\vee\neg A\mathrm{r}\neg_{\dot{\lrcorner}}4\mathrm{v}\Delta \mathrm{r}\neg\acute{A}\vee\Delta}{\Gamma\vee\neg A\mathrm{v}\Delta}(1,2)$

I が\supset I のとき、 P は$[A:1.]$:$\frac{\Gamma\vee\dot{B}\vee\Delta}{\Gamma\vee(A\supset B)\mathrm{v}\Delta}.(1)$と表すことができ、 これは$\mathrm{N}\mathrm{K}$において Lemma 21 と排中律を用いること

により次のようにできる。
$[\Gamma$:2$[\Delta$:$\Delta\vee\neg\Delta$$\Gamma\vee(A\supset.

:4

$]$

:
:

$]$

$\Gamma\vee\neg\Gamma$$\Gamma\vee(A\supset B)\mathrm{v}\dot{\Delta}$$\Pi$$\overline{\Gamma\vee(A\supset B)\mathrm{v}\Delta}(4,5)$B)\mathrm{v}\Delta$$\overline{\Gamma\vee(A\supset B)\mathrm{v}\Delta}(2,3)$

ここで 兇麓， deduction である。
$[A$

: 1

$]$

$\Gamma\vee\dot{B}.\cdot.\vee\Delta$

:
$=$

..

$[\neg\Gamma:5]$..

.

$\cdot$$\cdot$$\cdot....B\dot{\vee}..\Delta\cdot.$$.[\neg\Delta :$\frac{\dot{B}}{A\supset B}.’.(1)$:$\vee\cdot$$\Gamma\vee(A\supset B)\mathrm{v}\Delta$

3]$

18

I が \forall I のときも同様に行なう。

23

RemarkTheorem 22 の証明において、 classical な\supset I, ,\forall I の場合にたいする排中律の使用は本質的である。 なぜなら、 これらからは、排中律 (又は排中律$\neg I$と同値な命題) を演繹することができる。 それ以外の場合には、 変形は$\mathrm{N}\mathrm{J}$の推論で行われる。

3

Critical inference

本節では、 5 節以降の為の準備として、 NDK-deduction に関するいくつかの定義を与える。

3.1

Predecessor$C(X)$ で $X$ を含む component を表す。推論 I に関して d.c.A と$\mathrm{d}.\mathrm{c}$.B が次の関係のいずれかを満たすとき、 $B$ は $A$ の predecessor であるという。

1. I が前提が 1 っの推論のとき、 すなわち、$\frac{\Gamma\vee C(X)\vee\Delta}{\mathrm{r}\mathrm{v}c(\mathrm{Y})\mathrm{v}\Delta}\mathcal{I}$のとき、(a) I が VI で、 B が I で新しく導入される component のとき、 B(は Pre
decessor を持たない(b) I が\urcorner I で、 B が新しく導入される component のとき、 B は$\cdot$$\mathrm{p}\mathrm{r}\text{\’{e}}\triangleright$

cessor を持たない(c) (a), (b) のいずれでもないとき、$\mathrm{i}$$\mathrm{i}\mathrm{i}$.

$A$

が $C(X)$ で B が.

$A$, B はそれぞれ前提、結論の r(又は\Delta ) の同じ位置にある com-

$C(\mathrm{Y})$ponent2. I が\wedge I のとき、すなわち、$\frac{\Gamma \mathrm{v}c(x)\mathrm{v}\Delta\Gamma \mathrm{v}C(\mathrm{Y})\mathrm{v}\Delta}{\Gamma c(x\wedge \mathrm{Y})\mathrm{v}\Delta}\mathcal{I}$

のとき、

19

で B が $C(X\wedge \mathrm{Y})$

(a)

$A$

が $C(X)$ 又は

(b)

$A$

, B はそれぞれ前提、結論の F(又は\Delta ) の同じ位置にある compo-$C(\mathrm{Y})$nent
3. I が\supset E のとき、すなわち、$\frac{\Gamma\vee x\Delta\Pi x\supset Y\Lambda}{\Gamma\vee\Pi\mathrm{Y}\mathrm{v}\Delta \mathrm{v}\Lambda}\mathcal{I}$

のとき、

(a)

$A$

(b)

$A$

が X\supset Y で B が $Y$, B はそれぞれ前提、結論の r,, A の同じ位置にある(但し、 B が\Gamma と に重なるとき、 は B の r に対する component 又は 兇紡个垢 component となる。 B が\Delta と A に重なると$\mathrm{c}\mathrm{o}\dot{\mathrm{m}}_{\mathrm{P}}x$$\Delta,\Pi$

$A$

$\Pi$

$\mathrm{n}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathrm{O}}$きも同様)

4. I が\urcorner E のとき、すなわち、$\frac{\Gamma\vee x\mathrm{v}\Delta\Pi^{}-\neg X\mathrm{v}\Lambda}{\Gamma\mathrm{I}\mathrm{I}\Delta\Lambda}.\mathcal{I}$のとき、 3(b) と同様に定義する。

. :5. I が VE のとき、すなわち、$\cdot$.

$\iota$$\cdot$$\sim$$r[X]$

.
$[Y]$

$-$

$\frac{\Gamma\vee(x\vee \mathrm{Y})\vee\Delta\dot{D}\dot{D}}{\Gamma\vee D\Delta}\mathcal{I}$

のとき、

(a)

$A$

, B はそれぞれ前提、 結論の r (又は\Delta ) の同じ位置にある com-$\mathrm{p}_{\mathrm{o}\mathrm{n}\mathrm{e}}\mathrm{n}\mathrm{t}\text{、}$

(b)

$A$

もしくはそれぞれ前提、結論の D である。

が主前提の X\vee Y の

assumption(c) B が r と $D$ との $X$ 。 $A$$\Delta$がB がこの推論 I で discharge されるのときも同様 R$X_{\text{、}}$$\mathrm{Y}$の 2 つ以上と重なるとき、 $A$ は 3(b) と同様に定義する。

6. I が \exists E のとき、 すなわち、
$[F]$

:

$\frac{\Gamma\exists XF\vee\Delta\dot{D}}{\Gamma\vee D\vee\Delta}.\mathcal{I}$

のとき、

20

(a)

$A$

, B はそれぞれ前提、結論の F (又は\Delta ) の同じ位置にある comもしくはそれぞれ前提、結論の D である。

$\mathrm{p}_{\mathrm{o}\mathrm{n}\mathrm{e}}\mathrm{n}\mathrm{t}\text{、}$

(b)

$A$

が主前提の

$\exists xF_{\text{、}}$

B がこの推論 I で discharge される assumptionの $F$(c) B が\Gamma と $D$ と$\Delta$の 2 つ以上と重なるとき、 $A$ は 3(b) と同様に定義する。

predecessor を持たない formula を、 initial という。

32

String and Path

formula から始まる predece$or の列を、 の string という。 最後のformula が initial である string を、 path という。 また deduction の path を、
その deduction の結論から始まる path と定める。
$A$

33

$A$

Ancestor and Desendant

C の string で $D$ を含むものがあるとき、 C は D の desendant. D は C のancestor であるという。

3.4

Irrelevant and Essential component.C が irrelevant であるとは、 この C の ancestor の中に vI で導入される
formula があるときをいう。 irrelevant でない d . を essential と呼ぶ。
$\mathrm{d}.\mathrm{c}$$.\mathrm{c}$35Critical inference

irrelevant component に作用する推論\supset L\forall I を critical という。

4:The system of NDKE
4.1

Negative dual pairnegative dual pair (1.

]$\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}}$$\mathrm{a}A$$\mathrm{n}.\mathrm{d}$に対して、.P.) を帰納的に定義する。 ([2] を参照。)$(A, \urcorner A)$

は n.d.p.

2. formulaA に対して、 $(\neg A, A)$ は n.d.p

3. $(E_{i}, F_{i})(i=1,2)$ が n.d.p. のとき、$(E_{1}\wedge E_{2}, F_{1}\vee F_{2})$は n.d.p.

4. $(E_{i}, F_{i})(i=1,2)$ が n.d.p. のとき、$(E_{1}\vee E_{2}, F_{1}\wedge F_{2})$は n.d.p.

21

5. $(E, F)$ が n.d.p. のとき、$(\forall xE, \exists xF)$

は6. $(E,F)$ が n.d.p. のとき、$(\exists xE,\forall xF)$は n.d.p.

$(E, F)$ が42$\mathrm{n}.\mathrm{d}$$\mathrm{n}.\mathrm{d}$.P.

.P. のとき、 $E$ , F はそれぞれ $F$,E の negative dual であるという。

Excluded middle type axiom$(E, F)$ が n.d.p. のとき、 E\vee F を排中律型公理という43([2] を参照。)。

NDKE and NKE

NDK,に排中律型公理を加えてできる体系をそれぞれ NDKE, NKEと呼ぶ。 NDKE, NKE に対しても 31 から 36 と同様の定義を与えることが$\mathrm{N}\mathrm{K}$

できる。

4.4

Ra 泳

NDKE-deduction$P$にたいして、 \beta を $P$ の path とするとき、$\gamma_{\beta}.\cdot$

で\beta に沿った critical な推論の数を表し、 P の rank を

rank$(P)= \beta:path\sum\gamma\beta$

で定める。

5

Natural reasoning
前節で定義した critical な推論が不自然な推論であり、 そのような推論はどのように解釈すれば正当化できるかを、 例をもって見ていく。
NDK-deduction.
$\frac{[A\cdot 1]}{\exists xA}$$\frac{[D]}{\exists xA\vee D}$$\overline{\exists xA\vee C}\vee I$.
$\frac{\overline\exists xA(C\wedge D)}{\exists xA(A\supset C\wedge D)}(1)-\supset I$

この deduction において、 $[A$

: 1 ?はを導く為の asとは無関係に VI で導入された formula C から演繹される $C\wedge D$ にたいして作用している。

$\text{について考える_{。}}$.

sumption であるが、$]$$\exists xA$

この deduction は次の様に考えることができる。

1.

$A$

が真ならば、$\exists xA$は真$\exists xA$

22

2.

$A$

が偽ならば、 $C,D$ の真偽に関係なく A\supset C\wedge D は真

この推論を deduction の形で表すと、$1_{\text{、}}2$$[A:3]-$$[\neg.\cdot A:4].$.

$\frac{\dot{A}\vee\neg A\frac{\frac{[A.2|}{\exists xA}}{\exists xA(A\supset C\wedge D)}\frac{\frac{C[D]}{\frac{CD}{A\supset C\wedge D}(}3)}{)\exists xA\dot{\vee}(A\supset C\wedge\dot{D}\}}}{\exists xA(A\supset c\wedge D}.(2,4)$となる。
こうしてみると、 classical な\supset I, \urcorner I,\forall I 以外の推論は自然であると考えることができる。
ここで、NDKE から classical な\supset I,$\neg I,\forall I$を除いて得られる体系を NDKE*-deduction
これなるべくもとの構造を変えない様に変換するアルゴリズムがあり、へ、を次節で与える。
とする。このとき、classical な推論をもつ (NDK-)deduction を

6$\mathrm{n}_{\mathrm{a}\mathrm{n}}\mathrm{S}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}$$\mathrm{N}\mathrm{D}\mathrm{K}\mathrm{E}^{*}$

towards natural reason-ing
本節では、 (5 節で考察した) NDK-deduction から不自然な推論 (classical) を除くアルゴリズムを与える。 (詳細は [3] の 7 節と 8 節参照。)
な\supset I,
critical でない\supset I, を除くには、 Theorem 22 の証明で用いた変換を行$\neg I,\forall I$$\forall I$

なえば良い。
残されたのは、 critical な\supset I, \forall I を除くことである。 それには次の 61 から 63 で与えられる変換を行なえば良い。

61$P$($G$ は irrelevant)を\Gamma V $GV\Delta$

1. まず P から$G$への NDKE-deduction とするとき、の path を取り除く。

に適用する critical な\supset I により discharge
2. これにより、 の ancestor.
.
$A$ とすると、 $A$ の元は open assumptionの集合をされる assumption
$G$

である。

3. 1 で得られる図から無駄を除いて、 deduction にする。

23

4. $A$ の元の conjunction $E\equiv\wedge\{A|A\in A\}$ の universal closure E’ を、 3で得られた deduction の open assumption $A\in A$ の上に次の様に結合させ、得られた deduction を $P’$ とする。
$\underline{\frac{E’}{E}}\forall E\wedge E$$\overline{A}.\cdot.\wedge E$

この P’ に対して、 rank $(P’)<rank(P)$ が成り立つ。

62$P$

を r V $G\vee\Delta$($G$ は irrelevant)

への NDKE-deduction とするとき、

1. 612 における $A\in A$ に対して、とする。
formula をが discharge される推論の前提の$A$$G_{A}$

2. $A\in A$ に対して、 次の deduction を$P_{A}$$[A:a]$とする。

$[\neg A]$$G_{A}$:.

$\dot{G}$3. 614 における$E$に対して、 $E$ の negative dual F を $F\equiv\vee\{\neg A|A\in A\}$とする。 よって F と$P_{A}$

を用いて、 F から $G$ への deduction$P_{G}^{F}$を作る

ことができる。

4. 次の deduction を $P”$ とする。 (但し、$F^{J}$は F の existential closure)

.

$F’.$

:

$P_{G}^{F}$$\overline{G}$

こうして得られた P/’ は、 critical な推論をもたず、結論の $G$ は irrelevant でない。

63( $G$ は irrelevant) の現れる、 formula $H$ への deduction
途中に\Gamma V$\Gamma\vee
GV$\Delta への subdeduction P で、 rank $(P)>0$ となるようを考える。
$G\vee\Delta$$P_{H}$

な–番大きいものをとる。 これを$P_{G}$

としよう。

24

1. 61 より、次の様な deduction P9 を得る$[E^{J}]$::$\Gamma\vee\Delta$$\ovalbox{\tt\small REJECT}$から$P_{H}$の–部をコピーして次の deduction$P_{H}^{1}$を得る。

$[E^{J}]$::$\frac{\Gamma\vee\Delta}{\Gamma\vee G\Delta}.\cdot\#$.
$\dot{H}$の# より下における $G$ の desendant には、の適用がない。ゆえに、 rank(PHl)<rank(PH)、よってはに変形できる。
deduction$\ovalbox{\tt\small REJECT}$の取り方から、上の$P_{H}^{1}$$P_{H}^{1}$$\supset I$$\mathrm{N}\mathrm{D}\mathrm{K}\mathrm{E}^{*}-$$P_{H}^{1*}$2. 61 より、 次の様な deduction PG” を得る$[F’]$.

$\dot{G}.\cdot$$\ovalbox{\tt\small REJECT}$より、 VI を用いて次の deduction$P_{H}^{2}$

を得る。

.

$[F^{J}..\cdot]$$\dot{G}$$.\Gamma\vee G..\vee\Delta$$\ovalbox{\tt\small REJECT}$

このとき、 rank $(P_{H}^{2})<rank(P_{H})$ となり、$\ovalbox{\tt\small REJECT}$$P_{H}^{2}$は NDKE*-deductionに変形できる。

3. 次の deduction を$P_{H}^{*}$とする。
$[E’]$.
.
$\cdot$$\cdot$$[F^{J}]$..
$\cdot$$P_{H}^{1*}$$P_{H}^{2*}$$\cdot$$\frac{E’\vee FJHH}{H}$

この$P_{H}^{*}$

は我々の求めるものであり、 critic 訓な推論をもたない。

25

64

Remarkessential component に適用された classical な\supset $-I,\forall-I$ については、
Theorem 22 の変形を適用する。

65

例

ここで 2 っの例をあげる。

(1) $P$ :$\frac{\frac{[A(b).1]}{A(b)\mathrm{v}A(C)}\vee I}{A(b)\vee(A(b)\supset A(c))}.(1)$$\overline{(A(a)\supset A(b))\mathrm{v}(A(b)\supset A(c))}$$\frac{\overline{(A(a)\supset A(b))\forall v(A(b)\supset A(y))}}{(A(a)\supset A(b))\exists X\forall y(A(x)\supset A(y))}$$\frac{\frac{\overline{\forall y(A(a)\supset A(y))\vee\exists X\forall y(A(x)\supset A(y))}}{\exists x\forall y(A(_{X)}\supset A(y))v\exists x\forall v(A(x)\supset A(y))}}{\exists x\forall y(A(x)\supset A(y))}$Contraction$P^{1}\equiv P^{1*}:$$P^{2}\equiv P^{2*}:$$[\neg A(b):2]$$[A(b):3]$.
$\frac{[\forall zA(Z).1]}{P(b)}$$\frac{A(c)}{A(b)\supset A(c)}(3)$$\overline{A(a)\supset.\cdot.A(b)}$.

$\exists x\forall y(A(x.\cdot.\cdot)\supset A(y))$$. \frac{[\exists z\neg A(Z).4]}{\exists x\forall y(A(x)\supset A(y))}(2)$$\exists x\forall y(A(x.)\supset A(y))$$P^{*}:$$[\forall zA(z):1]$:$P^{1*}$$[\exists z\neg A(Z) : 4]$.

$\cdot$$P^{2*}$$\frac{\forall zA(z)\exists z\neg A(z)\exists x\forall y(A(X)\supset A(y))\exists x\forall y(A(x)\supset A(y))}{\exists x\forall y(A(x)\supset A(y))}.\cdot(1,4)$

26(2) $P$ :$\frac{[\forall x(F(x)\mathrm{v}C.)]}{\frac{F(x)\vee c}{\forall xF(X)\vee C}}$$P^{*}:$$\frac{[\forall x(F(_{X)C})]}{F(x)\vee c}$$[\neg C:1]$$\frac{F(x)}{\forall xF(_{X)}}.\cdot.\cdot$$\frac{C\vee\neg C\forall x\frac{[C\cdot 2]}{\forall xF(X)\vee C}\overline{F(_{X})VC}}{\forall xF(X)VC}.,(2,1)$

参考文献[1] M. Yasugi and K. Ryu, $NDK,$ A New Classical System, The Bull. of
the Inst. of Computer Science of Kyoto Sangyo Univ., vol.11(1994),

1-25.
[2] 大芝猛, 自動証明における自然な証明生成への–つの近接, 情報処理学
会論文誌, 第 35 巻 (1994), 222-231.
[3] M. Yasugi and M.Nakata, $NDK$ and Natural Reasoning,

submitted.

$\mathrm{M}\mathrm{S}(1996)$,