古典論理の自然推論体系

{古森雄一 \atop 千葉大学理学部}

鹿島亮 (東工大) 氏が考案し古森が改変した古典論理の自然推論体系 (cf. [1]) は, その正規形が部分論理式特性をもつ最初の体系と思われる (Parigot の体系は部分論理式特性をもつ複数の結論を許す自然推論体系と考えられる。しかし, ここでは一つの結論を持つものだけを自然推論体系といっている)。

鹿島-古森の体系の正規化定理や Church-Rosser 性などを考察している最中に本講演で述べる体系を考えついた。その体系は鹿島-古森の体系の良い点をすべて継承し, 正規化定理の証明も易しくなっている。また, その体系から導出される型なしラムダ計算風体系の Church-Rosser 性の証明も容易である。

体系の推論規則 (→ E), (→ I) は直観主義論理 NJ と同じ。

Π α ; β −k(A),  Π α ; α −k(R)

ただし, 規則 (R) では Π に現れる −k で index された規則 (A) の上式のすべては α である。

証明図の例

\begin{matrix}{2 \atop (α → β) → α} & \begin{matrix}1 α ; β & −1(A) \\ α → β \end{matrix} ; 1(→ I) \\ α \end{matrix} ; → E ; α ; −1(R) ; ((α → β) → α) → α ; 2(→ I)

規則 (A) (R) の α, β を原子論理式に制限しても証明能力は同じである。その制限をした体系の正規形への変形手続は従来の β 変形だけで十分である。原子論理式に制限しない体系では β 変形に 2 つの変形規則を付け加える必要があるが, 正規化定理の証明は容易である。この体系は Parigot の体系と似ているように見えるが違うものである。

参考文献

[1] Yuichi Komori. A natural deduction for classical logic, in which there exists a proof with the subformula property. In Proc. 33rd MLG meeting, pp. 3–6, Echigo Yuzawa, 2000.

2