フレーゲ以後の演繹体系について

フレーゲ以後 の演繹体系 について

哲学教室 田 §0。 はじめに

Sl.フ

レーゲ

&ヒ

ルベル ト流体系 §

2.自

然演繹 §

3.連

式計算 とタブロー・ メソッド §0。 は じ

bに

ア リス トテレス以来

,論

理学 は

,妥

当な推論 をそうでない推論か らどのようにして区別するのか, ということを中心的研究課題 として きた。今 日

,妥

当な推論 はい くつかの論理的な演繹体系 として 整備 されてお り

,そ

れ らの特徴づ けも種々の観点か ら行われている。本論文 の目的 は

,フ

レーゲ以 後の代表的な論理的演繹体系 を概観 し

,そ

れ らの相互関係

,論

理体系 としての役割

,そ

れの持つ哲 学的合意等 を簡潔 に要約す ることである。以下で は

,四

つの演繹体系

,す

なわち① フレーゲ

&ヒ

ル ベル ト流体系

,②

自然演繹

,③

運式計算

,お

よび④ タブロー・ メソッドを取 り上 げる。 フレーゲ

&

ヒルベル ト流体系 は

,フ

レーゲに由来 し

,ラ

ッセル

,ヒ

ルベル ト等 によって継承 された公理体系 と いう形での演繹体系であ り

,真

理 としての論理法則 を組織的 に導出す ることで特徴づけられ る。 自

然演繹体系 (natural deduction system)は ゲ ンツェンに由来 し

,主

として数学 にインフォーマル

な形で現れ る推論形式 をそのまま「自然 な形で

J採

集す ることを意図 して作 られた体系である。連 式計算 (Sequent calculus)も ゲ ンツェンに由来 し,「主定理」 と呼 ばれ るメタ定理 により

,多

くの 数学 (または数学基礎論

)に

応用 され る体系である。ダブロー・ メソッドは連式計算 と解釈上の密 接な関連 をもつ直観的に見通 しの良い体系である。 これ らの体系 はそれぞれの特徴 と目的に応 じて 一長一短があ り

,一

概 に優劣 をつけることはで きない(1ち _以下

_,本

_{論文で は歴史的考察 は必要最小限} に抑 え

,

もっぱら体系的 に (主として構文論的観点か ら

)こ

れ らの演繹体系の考察 に焦点 を絞 る。 演繹体系 とい う論理学の最 も基本的部分が持つ主要なアイディア と目的を検討す ることによって, 情報科学・ 言語学・ 数学基礎論 との交流 により急速 な変貌 を遂 げつつある現代 の論理学の根幹 をそ の故郷である哲学 の立場か ら捉 えること

,そ

れが本論文の目的である。 敏 博 畑

§

1.フ

レー ゲ

&ヒ

ル ベ ル ト流 体 系

1.1

公理体系 現代論理学の創始者 の一人であるフレーゲに始 ま りK21,ヒ_{ルベル トによ り整備 された}0フ _レーゲ

&

ヒルベル ト流体系の中心概念 は「証明可能性 (prOvability)」 (または「導出可能性」「定理性」

)の

概念である。 フレーゲが論理 を真理の公理体系 として捉 えた ことと

,算

術 の真理 は論理的真理であ るという彼 の論理主義 の主張 とは密接 に関連 している。 この体系 は

,ま

ず

,い

くつかの整式 (文法

的に整 った式 :well‐formed fOrmula)を_{公理 として定 め}

_,定

_{理 を}

_,公

_{理 を含 み一定 の証明規則}141の

下で閉 じている整式 の最小集合 とす ることによ り

,定

式化 され る。証明規則 は前提か ら結論へ移行

する推論パター ンとい う形式 を取 るが

,前

提が仮定 に依存す るとい うことはない。

古典命題計算 CPC(Classical Propositional Calculus)の 公理系の一つ は次の公理図式 (a

Om

schemata)に

よ り与 えられ る:

(Al)

φ⊃ (ψ⊃φ)

(A2) (φ

⊃ (ψ⊃θ))⊃((φ⊃ψ

)⊃

(φ⊃θ))

(A3) (￢

′⊃￢φ

)⊃

(φ⊃ψ) ここで,φ,ψ自体が整式であるか ら

,二

つの公理があるので はな く三種類 の無限 に多 くの公理があ ることになる。証明規則 はモ ドゥス・ポネンス

(MP):「

φ⊃′およびφが定理 な らば″も定理であ る」である。 この とき

,定

理の明示的定義 はこうなる: 1。 すべての公理 は定理である。

2.φ

⊃″とφが ともに定理ならば

,ψ

も定理である。 上で与 えられた公理系 を

FCPCと

呼ぶ(`F'は Fregeに由来)。 メタ変項 φ

,ψ

,θ の代わ りに文

変項

pO,pl,p2,…

に対 して

(Al)― (A3)の

公理 を書 けば二つの公理 を定 めた ことになるが,

次の代入規則が付力日されねばな らない。 代入規則 :定 理中の文変項への整式の代入の結果 は定理である。 `卜_φ'を_「φは

FCPCの

_{定理である」 と読む と}

,MP(モ

_{ドゥス・ ポネンス}

_)は

卜φ⊃′

卜φ

(MP)

卜 ψ と表せ る。

FCPCで

の「証明」は

,根

に証明 され る式 (つま り定理

),枝

(出発点

)に

公理 を持 ち

MPに

統御 された樹形図 となる0。 _フレーゲ

_&ヒ

_{ルベル ト流体系 の欠点 の一つ は} ,証明 を遂行す るこ とが一般 に煩雑 だ とい うことである。 もし枝 (出発点

)に

任意 の整式 を仮定す ることが許 され るな らば

,証

明 は容易 になる。い ま

,Dが

,出

発点 にφl,φ2,…・

,ぬ

を持 ち

MPに

よって統御 され終式 としてφを持つ整式 の有限樹形図の とき

,Dは

,「仮定φl,φ2,…・

,φ

kからのφの証明」と言われ, φl, φ2, …ちφkl―φ と書 き表す。

1.2

演繹定理 仮定か らの証明の概念 は,仮定 の集合(無限集合で もよい)「と整式 との間の帰結関係 (COnsequence relation)と _{して拡張 され}

_,次

_{のように表現 され る}: 「 卜φ ⇔ ある(φl, ・・・, φ

k}⊆

Fに 対 して, φl, ・・・, φkttφ● この概念 について

,演

繹定理 と呼 ばれ るメタ定理が成 り立つ。

鳥取大学教育学部研究報告 人文・社会科学 第 47巻 第

1号

(1996) 演繹定理

(deduCtiOn theorem):「 ,φ

卜ψな らば

F卜

φ⊃ψ. この定理の証明 (正確 にはメタ証明

)は ,仮

定 「

,φ

(正確 にはF∪ {φ

)で

あるが

,

このように略 記す る。以下同様。)からの″の証明

Dに

`φ⊃'変<sub>形 を施 した</sub>`φ⊃D'と い う擬証明樹が

,公

理

(Al),

(A2),MPに

よって,仮定 「 か らのφ⊃″の証明に常 に改変で きることを示す ことによ り実行 され る0。 このような証明が一般的 に行 われ得 るのは

,フ

レーゲ

&ヒ

ルベル ト流体系の「証明

Jに

おけ る式変形が

MPた

だ一つに統一 されているか らである。すなわち

,演

繹定理が成 り立つのは,「仮定 の集合か らの帰結関係」が「仮定か らの証明」 により導入 され

,か

つ,

(1)(Al)と (A2)が

公理図式であ り,

(2)MPが

唯― の証明規則である, という条件が成 り立つ ような

,

このタイプの任意 の体系である。 この第二の条件が重要であることを確認す るために

,演

繹定理が成 り立 たないか

,ま

たは成 り立 つ として も

FCPCの

ように直接的な仮定か らの証明 によっては

,任

意の集合か らの帰結関係が導 入で きない場合 を考察 しよう。証明樹が仮定か らの証明樹へ と拡張 されるときに生 じているのは,

MPが

「証明規則」か ら「推論規則」へ と事実上変換 されているとい うことである。 というのは, 「 卜φ⊃θと,△卜φか ら

,F,△

卜θが許 されるか らである。

そこで

,様

相命題論理

S4を

考 える。これ は

,FCPCに

文演算子`□ 'と <sub>(`&'をφ</sub>

&ψ

_=def.￢ (φ

⊃￢ψ

)と

して定義

)以

下 の公理図式・ 証明規則 を追加 して得 られ る:

(A4)

□φ⊃φ

(A5)

□ (φ⊃ψ

)⊃

(□φ⊃□″)

(A6)

□φ⊃□□φ 必然化

(Nec)

卜φ 卜□φ もし仮定か らの証明を

MPと

Necに_{より統御 された証明樹であるとすると,先}の

MPの

場合 と同様 に, 証明規則Necを, 「 卜S4 φ 「 卜

S4

□φ という推論規則 に変換す ることになる。 しか し

,こ

の規則 は

,演

繹定理 を認 める とす ると

,S4の

通常の意味論 に対 して健全で はな くなる。 というのは,

φ卜

S4

φ

(Nec) φ卜

S4

□φ (演繹定理) 卜

S4

φ⊃□φ として,φ⊃□φという

S4で

の非定理が導かれるか らである。そこで,このような難点を避けるた め

,い

まの場合

,仮

定か らの帰結の関係 はぅ 「 卜

S4

ψ

C)Fに

おけるい くつかのφl,…・

,φ

kに対 して, 卜

S4

φ

l&

…

&φ

k⊃φ という形で定義 し直 される。 このや り方で仮定からの帰結の関係 を導入すると

, FCPCで

仮定か らの証明を導入する以前の欠点が残 る。なぜなら

,S4で

の仮定か らの帰結の関係 は,「証明可能性」 によって定義されているか ら

,そ

れに伴 う欠点をすべて持ち越 しているか らである。しかし,`卜'に

対する演繹定理 は成 り立つ。というのは

,FCPCで

φ&φ

l&…

&φk⊃ψが証明可能であるのは,φ

l&

1.3

述語論理

次に

,等

号つ き古典述語論理 (量化計算

)CQC=(Classical Quantification Calculus with

identity)で_{演繹定理が成 り立つ場合 を考察する。 ここで}

_,普

_遍量化子`V'を_{原始記号 とする。整式} ψがφの一般化(generalization)であるのは

,い

くつかの変項Xl,…・

_,Xkに

_{対 してψがV Xl…V Xttφ} となるとき

,か

つその時に限る

(k=0も

含む)。 公理 シェーマは次の

8個

である。

(Ql)―

(Q3)=def.(Al)― (A3)の

事例の一般化

(Q4) VXφ

⊃φXt。)・……ここで tは φの

Xに

代入可能なω)項

(Q5) VX(φ

⊃ψ

)⊃

(VXφ ⊃

VXψ

)

(Q6)

φ⊃Vxφ ……

Xが

_{φで自由には出現 していない場合}

(Q7) X=X

(Q8) X=y⊃

(φ⊃φ′

)…

…φが原子文で

,φ

′がφ中の

0個

以上の

Xを yで

置 き換え てφから得 られる式である場合

MPは

唯―の証明規則 この公理体系を

FCQC=と

すると

,こ

れに対 して次のメタ定理が成 り立つ。 メタ定理 (一般化

):Xが

「 のいかなる整式にも出現 していないならば, 「 卜φ ⇒

F卜

Vxφ

. 証明は

,公

理の一般化がぶたたび公理であることと

,(Q6)(Q5)を

不U用することにより行われ る。ち このメタ定理 は派生推論規則である。

MPの

みを証明規則 とする

,CQC_に

対するこのタイ プの体系(10に_{対 して}

_,

_{これ と同値な多 くの体系がある}(11ち ここで

,次

節以後の自然演繹

,連

式計算の体系 との関連 をつける意味で

,フ

レーゲ

&ヒ

ルベル ト 流体系のゲンツェン寄 りのバージョンを考 える。まず個体変項 として

,

もっぱら自由変項 としての み現れる「パラメータ」

(a, b, C,一

)と 束縛変項 としてのみ用いる「変項」

(X, y, Z,一

)

を明確に区別 して

,個

体項 (indi dual terms)を改めて定義 し直すり 。論理記号 として

,&,V,D9

上

,V,ヨ

をすべて用いるが

,否

定のみ ￢φ=def.φ⊃上 として`⊃ 'と `上'で_{定義する。整式 は通常} の仕方で定義されるが

,量

化子については次の定義文 を用いる。

(*)φ

が整式

, bが

パラメータ

,Xが

ψに出現 していない変頂であるとき

, Vxφ

′

,ヨ

xφアは ともに整式である。(ここで,ψ′はφ中のすべての`b'の<sub>出現を</sub>`X'で_{置 き換 えてφから得} られる表現である。) ①パラメータの導入 と

,②

束縛変項を含む整式を再び同じ変項で東縛することの禁止

,

という二つ の変化 は

,同

一の変項が自由変項 としても束縛変項 としても現れることがないこと

,お

よびいかな る変項 も同一の整式中で三度束縛されることがないこと

,

という結果 をもたらす。 これ自体 はフレ ーゲ

&ヒ

_{ルベル ト流体系にとって重要ではないが連式計算にとっては本質的である。 また}

_,こ

れに より言語の表現力が弱まった訳ではない。例えば

,ヨ

X(Px&VXQX)は

禁 じられるが

,同

じ意味を 持つ ヨ

y(Py&VxQx)は

_{認められるか らである。}

_{(`Py&VXQX'の}

_{ようにパラメータではな く変} 項が自由変項 として現れる表現 を

,以

後

,擬

整式 と呼ぶ。)

1.4

直観主義論理 と古典論理 ゲンツェン流の体系に一層接近するために

,以

下のような等号つ き直観主義述語論理のバージョ ン

FIQC=(`I'は

Intuitionisticに _{由来)を 考える。命題論理の部分の公理図式 は以下のものであ} る:

(A⊃

1)

φ⊃

(ψ

⊃φ

)

鳥取大学教育学部研究報告 人文・ 社会科学 第 47巻 第

1号 (1996) 53

(A⊃

2) (φ

⊃ (ψ⊃θ))⊃((φ⊃″

)⊃

(φ⊃θ))

(A&I)

φ⊃ (ψ⊃ (φ

&ψ

))

(A&El)

φ。&φ

l⊃

φ

I(i=0, 1)

(A∨

11)

φ

l⊃

φ。∨φ

l(i=0, 1)

(A∨

E) (φ

⊃θ

_)⊃

_((ψ⊃θ

)⊃

(φ∨ψ⊃θ))

ここまでの公理図式で最小論理 (Minimal 10gic)が 与 えられ

,次

の公理図式

(A上

)を

追加 す るこ

とにより, 直観主義論理 (Intuitionistic logic)が得 られ る。

(A上

)

上⊃φ

MP(モ

ドゥス・ ポネンス

)は

(命題論理 の部分 の

)唯

―の証明規則である。 よって (この部分 に おいて

),演

繹定理が成 り立つ。 これ に量化 と等号 に関す る公理 を付 け加 える:

(AVE) Vxφ

⊃φXt (Aヨ

I)

φXt⊃ヨXφ

(A=I) a=a

(A=E) a=b⊃

(φXa⊃φ

Xb)

…… ここでφは原子文である。

さらに量化 に関す る証明規則 を二つ加 える: は

VD

… ここ

"メ

ータ 中 硼 現 し

9ま

な られ 、 は ヨ動 … … ここでパ ラメー タ

aは

_{″に出現 して はな らない。} (これ らのパラメータは固有パ ラメータ と呼 ばれ ることがある。) 最後の二つの証明規則 に付加 されている条件 は

,

これ らの規則が健全であるために必要である。

卜Pa⊃ Paで_ぁるが

_,Pa⊃

V xPxは論理的 に妥当で はないか らである。(例えば

,個

体領域 を「人間J,

`P'を_{「将棋 の七冠王」}

_,`a'を

_{「羽生名人」 と解釈す ると反例モデルが作れる。}

_)ま

_た

_,(RVI)が

証明規則であることが重要であ り

,対

応す る推論規則 にはそれ以上の制限条件が必要である。 とい うのは

,公

理

(A⊃

1)と

MPに

より,

Pa tt VyQy⊃ Pa

が成 り立つが

,こ

れか ら

Pa tt VyQy⊃ vXPX

を導 くことは許 されないか らである。(この場合 も上 と同様 の反例 モデルが作れ る。

)そ

こで

,仮

定 か らの証明 において

(RVI)を

適用す るとき必要 な制限 はこうである: いま

,Dを

,公

理でない式φl,・・・

,仇

を出発点 とする,φ ⊃ψを導 く仮定か らの証明樹 とし

,パ

ラメ ータ

aが

_{φにおいて出現 していない とき},

D

φ⊃ψ φ⊃V X ψax が

,仮

定 φl,一 ,φkからのφ⊃V Xψaxの証明であるのは

,パ

ラメータ

aが

φl,―・,φ上の どの式にも 出現 しない場合である。(Rヨ

E)を

仮定か らの証明 において適用す るときも同様 の制限が必要であ る。 これ らの制限 を伴 う

FIQCの

体系で は,`φ⊃'変_形

_{(1. 2節}

_{お よび註}

6参

照

)を

用いて演繹定

理 が成 り立 つ ことが示 され る(13比

(RVI)は

仮 定 の帰結関係 に関す る条件 として も書 くことがで きる。 すなわ ち

,固

有 パ ラメー タ

aが

「 お よび θに出現 していない とき, 「 卜 θ⊃ψ

ならば 「 卜 θ⊃V X ψ ax. (Rヨ

E)に

ついて も同様である。 以上 の直観主義述語論理 に

,次

のいずれか一方 を加 えると古典述語論理が得 られ る:

(DN)

￢￢φ⊃φ (排中律

)

φ

V￢

φ (`DN'は二重否定dOuble negationに 由来) 否定記号 を原始記号 とす る場合

,直

観主義論理 を特徴づける公理

(A上

)の

代わ りに次の公理 を採 る:

(A￢

I) (φ

⊃ψ

)⊃

((φ ⊃￢ψ

)⊃

￢φ)

(A￢

E)

φ⊃ (￢φ⊃ψ) 本節で考察 したフレーゲ

&ヒ

ルベル ト流体系 は

,

これを外か ら特徴づ ける際にある種 の単純 さを 持 っている。例 えば,「整式」や「証明」が帰納的 に定義 され るとい う単純 な構造 を持 ってい るため, 超数学 の算術化 に適 しているといった長所がある。 §

2.自

然 演 繹

2.1

推論規則の体系 フレーゲ

&ヒ

ルベル ト流体系での仮定か らの証明 と演繹定理 は

,証

明の構成 に際 して この体系 に 伴 う過度の負担 を軽減 しようとす る工夫であった。 これを

,全

く異 なるタイプの体系 を作 ることで 一層徹底 したのがゲ ンツェンの自然演繹 の体系である(14ち _{ゲ ンツェンは「数学の証明 に含 まれ る実} 際の論理的推論 をで きるかざり正確 に反映 した記号体系 を作 りたい」と書いている(19。 _{自然演繹 の} 特徴 は次の二点 に集約で きる。第一 に

,す

べての規則 は基本的 には証明規則で はな く推論規則であ り

,仮

定か ら何が論理的 に推論 されるかに関心 の焦点があって

,証

明可能性 (定理性

)は

仮定か ら の導出の極端 な場合 と見 られ る。つ まり

,フ

レーゲ

&ヒ

ルベル ト流体系が証明可能性 を中心 とした 論理的真理の公理体系であったのに対 して

,自

然演繹 は推論規則 の体系である。第二 に

,結

合子や 量化子等の論理的オペ レータは

,そ

れ らに対す る対称的な二種類 の規則一―すなわち

,当

該 オペ レ ータを主要オペ レータ として含む文 を結論 として どう導 くか を述べ る「導入」規則 と

,当

該 オペ レ ータか ら何が導かれ るかを述べ る「消去」規則一― により統御 されている。

まず

,直

観主義述語論理の自然演繹体系

NIQC(`N'は

natural deductionに 由来)から考察 を始

める。 この体系 は

,以

下の12個 (正確 には12種類

)の

推論規則 を持つゲ ンツェンのオ リジナルの

N

」のヴァリエーシ ョンである(10。

仮定の規則 (A)

&の

導入規則

(&I)

φ ψ

&の

消去規則

(&E)

φ

&ψ

φ

&ψ

φ

&ψ

∨の導入規則 (∨

I)

φ

ψ φ

ψ [φ

] [ψ

] ● ● ● θ ● ● ● θ ψ ∨ φ φ∨ψ φ∨ψ ∨ の消去規則 (∨

E)

鳥取大学教育学部研究報告 人文 。社会科学 第47巻 第

1号 (1996) 55

⊃の導入規則 (⊃ I) [φ]

φ⊃ψ

上

⊃の消去規則

(⊃

E)

φ⊃ψ

上 の規則

(上

) φ

Vの

導入規則

(VI)

φ

Vの

消去規則

(VE)

VXφ

'ァ ただし

,固

有パラメータ

aは

φが依存するいかなる仮定にも 出現 していない。 VXφ ヨの導入規則 (ヨ

I)

φアι

ヨの消去規則 (ヨ

E)

ヨXφ _ヨXφ θ ただ し

,固

有 パ ラメー タ a は,θが依存 す るφXa以外 の 仮 定 に もθに もヨXφに も出 現 してい ない。

NICQで

は

,整

式 の「仮定への依存」の関係が重要である。規則 (⊃

I)(∨ E)(ヨ

E)に

お

いて

,結

論 は

,直

前の導出が依存 していた仮定の総和 の うちの

,い

くつかの仮定 に もはや依存 しな くなる。結論が依存 しな くなる仮定 は「解除 された」 (diSCharged)仮 定 と呼ばれ るが,「解除」が生 じたことを明示す るために

,解

除 され る式 を鉤括弧

[ ]で

囲んで番号 を付 け

,そ

の同 じ番号 を解除 が生 じた推論線の横 にも付 ける。解除 されていない仮定 は開いた仮定 と呼 ばれ る。すべての仮定が 解除された ときの結論 は「証明 された」整式である。証明 を作 るために解除 は権利であるが義務で はない。例 えば

,導

出: ψ φ/ι ゲ ・ ・_♭ 1

[p]

2

[p]

齢 )(⊃

(&I)

I)1

p⊃ (p⊃

(p&p))

(⊃

I)2

で

,二

度出現 した仮定

pは ,異

なる推論 において別々 に解除 されている。一般 に,φ⊃ψを結論 とす る (⊃

I)の

適用 において

,φ

の形の仮定がすべて解除 され るには及 ばない。導出:

φ⊃

(ψ

⊃φ

) i) (⊃ I)1 における最初 の (⊃

I)に

おいては

,い

かなる解除 も生 じていない。 この寛大 さによって

,自

然演 繹 は適切論理 (releVant logic)に は適 していない(1つ。同 じ形 のすべての仮定が同一の場所で解除 さ れる必要 はないゆえに

,同

じ形 をした仮定のうち

,同

一推論 において解除 され る仮定 の出現 のみが 同 じ仮定のクラスに属す る

,と

しなければならない(10。

(VI)と

(ヨ

E)の

固有パ ラメータヘの制限条件 は

, 1.3節

での

(RVI),(Rヨ

E)の

場

1

器

合 と同様 に

,健

全 さを維持す るために必要である。

2. 2

二つの体系の演繹的同値性 自然演繹 とフレーゲ

&ヒ

ルベル ト流体系 とは体系のスタイルの点で大いに異なっているが

,演

繹 の効力 と言 う点で は同値である。直観主義述語論理 においてその ことを確認 しよう。まず

,仮

定φl, 一

,仇

か ら

,あ

るい は仮定 の集合 「 か ら

,整

式φが導出可能であることを φl,…・

,φ

k卜

Nφ

あ るい は 「 ￨ Nφ

と書 く。フレーゲ

&ヒ

ルベル ト流体系 として

, 1. 4節

で扱った

FIQCを

採 る。

FIQCの

公理

がすべて

NIQCで

証明されることは容易に確かめ得 る(19ち _そこで

, FIQCで

_{仮定から証明され} た整式が

NIQCで

同 じ仮定か ら導出されることを示すには

,自

然演繹の体系である

NIQCが

F

IQCの

証明規則に関 して閉 じていることを示せばよい。これ も容易に確かめ得る90ち _よって

_,以

下の (メタ

)定

理が成 り立つ。 定理

:「

卜

Fφ

⇒

F卜

Nφ

. この定理の逆 も証明される。その証明を行 うには,「卜Nφであるとして,φが12個のどの推論規則 によって仮定 「 か ら導出されていても

,FIQCで

同じ仮定か らの証明が作れることを示せばよい。 それは

,FIQCの

公理 と演繹定理をうまく使 うことによってなされる。1ち _こうして

_,次

_の定理が 成 り立つ。 定理

:「

卜

Nφ

⇒

F卜

Fφ.

2.3

標準化定理

NIQCで

は

(A)と

(上

)を

除 く10個の推論規則が導入 と消去に分類され

,

これ らが対をなし て互いに逆の関係にある。 これらの規則において

,同

一のオペ レータに対する導入 と消去の規則を 連続 して使 うと

,あ

る種の回 り道 をすることになる。例えば

,(&I)と

(&E)を

連続 して使 うと, ψ

(&I)

φ

&″

φ2

(&E)

となる。φlと φ2は出現 を異 にす る同一の整式であるが,φ2を導 くために必要な φ

&ψ

が既 にφl を前提 している。

(&I)を

使用 した直後 に

(&E)を

使 うことは回 り道 (ない しは無駄

)と

なる。 このように

,同

じオペ レータに関す る規則 の導入 と消去 を連続 して使用す るときの中央の整式 (導

入の結論

,ま

たは消去の大前提

)は

最大式 (ma

mum fOrmula)と

_{呼ばれ る。 しか しこのような回}

り道 は他の導出に置 き換 えることで取 り除かれ る。 これ は還元 (reduction)と 呼 ばれ る。例 えば, 上の回 り道 は, i φl により還元 され る。

&以

外 の他 のオペ レータについて も同様である。例 えば

,⊃

については, φユ 1 [φ] 岩 万 (⊃

I)l

φ ⋮ φ ⋮ ″ は に還元 され る。

Vの

場 合, (⊃

E)

鳥取大学教育学部研究報告 人文・社会科学 第47巻 第

1号

(1996) 57

(φの導 出 のすべ て の場所 :子 で

,パ

ラメー タaを tで は

φ'ι 置 き換 え る。) へ と還元 され る。 こうして

,す

べ ての最大 式 は還元 に よ り除去 され

,回

り道 のない標準 的 な証 明 に 書 き換 え る こ とが で きそ うで あ る。 ところが

,最

大 式 を取 り除 くことによ り新 たな最大式 が生 じる こ とが あ る。例 えば,

藤 膊

】

1 [φ] 岩 万 (⊃ I)1 (φ⊃ψ)&θ θ

(&I)

φ⊃ψ

(&E)

″ であるが

,

これ を除去す るために, ● ● ● φ (⊃

E)

で最大式 は (φ⊃ψ)&θ 1 [φ] 岩 万 (⊃ 上 の導出 を

I)1

(⊃

E)

へ と還元す ると

,新

しい回 り道が出来

,新

しい最大式 φ⊃″が生 じる。しか し,これ ら二つの最大 式 (φ ⊃ψ)&θ と φ⊃ψ の複雑 さを比べ ると明 らかに前者が より複雑である。還元 を行 うと, た とえ新 しい最大式が生 じて も

,そ

れの複雑度が元 の最大式のそれ よ り小 さ くなることが帰納法 に より証明で きる。 よって

,次

の標準化定理が成 り立つ。 標準化定理 (nOrmahZation theorem): すべての導出は

,一

連 の還元 により最大式 を含 まない標準的導出に変換す ることがで き る(2り_。 還元 と標準化 は

,タ

ルスキー流の真理概念 に基づ く意味論 に代わる

,い

わゆる「証明論的意味論J において重要な役割 を演 じる。 ここで

,証

明論的意味論 について論 じる余裕 はないが

,

これ はウィ トゲンシュタインの

,あ

る文脈 中での「使用」 としての意味の観点 に通 じる興味深 い洞察 を含んで いる(2覧

2.4

自然演繹の連式ヴァージ ョン 自然演繹 と連式計算 (Sequent calculus)と の異同 を検討す るために

,こ

こで自然演繹 の連式ヴァ ージョンを考察す る。すでに述べたように

(2. 1節

参照

),自

然演繹 の体系で は導出 され る整式が いかなる仮定 に依存 しているか

,

とい う「仮定への依存

Jの

関係が重要であった。 この関係 を明示 する形で推論規則 を表現するのが

,自

然演繹 の連式 ヴァージ ョンである。 「 を整式 の有限集合,φ を 整式 とす るとき

,連

式 は “ 「 卜φ

"の

形で定義で きる。 この とき

,例

えば

,(&I)規

則 は次のよう に表現 され る。 「 卜φ かつ △卜ψ な らば

, F,△

卜φ

&ψ

. 他の規則 について も同様である・ 0。 _ここで

_,仮

_{定 を増力日す ることを認 めるとす る}

_,つ

_{ま り}

「 卜φ ならば

, F,△

卜φ ……・ (※) (1三

0,1)

φ,「卜θ

ψ

,F卜

θ を認 めると

,(&I)規

則 は

,一

般 に, 「 卜φ

「

卜ψ

(&I)

「 卜φ

&″

として

,上

の多種 の仮定か ら一元化 された仮定 に依存す る形 に表現で きる。とい うの は,「卜φか ら 「仮定 の増加」(※

)に

より,「

,△

卜φ;他方

,△

卜φと(※

)に

より

,F,△

卜″。新 しい規則

(&

I)に より,「 ,△卜φ

&ψ

;こ うして

,上

の元 の規則 は新 しい規則 によって模倣で きるか らである。 他 の規則 について も同様 である。さらに

,仮

定 の規則 を φ,「 卜φ とい う形 に一般化 し

,こ

れ を フレーゲ

&ヒ

ルベル ト流体系 になぞ らえて「公理」 と呼ぶ と

,以

下のような自然演繹 の連式 ヴァー ジ ョンがで きる。 公理

:

φ,「卜φ 仮定の増加

:

「 卜φ 「 ,△ 卜φ 「 卜φ

O&φ

l

(&I)

(VI)

(⊃ I) (上)

(VI)

(ヨ I) 「 卜φ

F卜

ψ 「 卜φ

&ψ

「 卜φi

(&E)

(∨

E)

(DE)

(VE)

(ヨ

E)

「 卜φi 「 卜φ∨ψ 「 卜φ。∨φ

l(1=0, 1)

φ,「 卜ψ 「 卜φ⊃ψ 「 卜上 「 卜φ 「 十一φ 「 卜VXφ αχ 「 卜φχι 「 トヨXφ 「 卜φ 「 卜θ 「 卜φ⊃ψ 「 卜ψ 「 ￨―VXφ 「 卜φ ア_ι 「 卜φ α / 「 トヨXφ

(こ こで

,(VI)と

(ヨ

E)に

おいて固有パ ラメータ

aは

制限条件 を満た している とす る。)

この連式 ヴ ァージ ョンにおいて も

,&,∨

,⊃

,V,ヨ

の各オペ レータに関する規則 は

,導

入 と消 去の対称的な形 になっている。(これに対 して

,連

式計算 の規則 は

,次

節でみるように

,導

入規則 だ けか ら成 る。) §

3.連

式 計 算 と タブ ロー・ メ ソ ッ ド

3.1

連式計算 自然演繹 の連式 ヴァージ ョンで は

,消

去規則 がなお存在 して`卜'の_{右 に位置 してい る。消去規則} に対す る全 く異なるアプローチを採 ることでゲ ンツェンの連式計算が導かれ る。導出可能 な連式 φ

,φ

l,…・

,φ

k卜θ を考 え

,こ

の導出可能性 を

,仮

定φ,φl,―・,φにか らθへ到 る導出樹が構成で きることと解釈す る。 そして

,そ

の導出樹 を

鳥取大学教育学部研究報告 人文・社会科学 第47巻 第

1号 (1996) 59

φ

,φ

l,‥ ち φk

D

θ とす る。 ここで

,φ

は未 だ解 除 されていない (すなわ ち開 いて い る)。 これ の導 出図 を

(&E)を

使 って,

撃 ⑪ …

仇

D

θ に書 き換 える(ここでφは仮定からは消える)。 すると

,連

式 φ

&ψ

,φl,…・,φk卜θ が導出可能 となり

,上

の解釈に従 うと

,規

則: φ,「 卜θ φ

&サ

,「 卜θ が健全な証明規則 となる。 これは

(&E)に

より正当化される。よって

,(&E)を

新 しい形で構成 し直 したことに外 ならない。同様 に

,規

貝

J(⊃

E)を

「 卜φ

ψ

,F卜

θ φ⊃″,「 卜θ という健全な規則 として構成 し直すことができる。なぜなら, 「 φ

および という導出樹が与 えられているならば, 「

lDEl r

θ

が(⊃

E)に

より正当化 されるか らである。規則

(VE),(VE),(ヨ

E)とこついて も同様 である￠働。

こうして

,消

去規則 を`卜'の<sub>左辺への導入規則 と見 ることがで きる。ゲ ンツェンのオ リジナルの</sub> 連式計算 の記号 `→'に な らって

_,以

_後

_,連

_{式 を} 「 → θ と書 くこ とにす る(こ こで,「は整 式 の有限集合,θは整式 で あ る)。 この とき

,ゲ

ンツェンの連 式計 算の公理 と規則 は次のもの として与 えられる。 (公理

)φ

,「 →φ (→

&)「

→φ

F→

″ 「 →φ

&ψ

(増

)

「 →φ △,「→φ Ｆ ， ・ ・ ・  ｎ ν ψ (→

V)「

→φ

F→

ψ

(&→

)

φ,「 →θ

ψ

,F→

θ

φ&″

,「

→θ

φ&″

,F→

θ

(∨

→)φ

,「

→θ

″

,F→

θ

φ∨ψメ

_「

→θ

「

→φVψ

F→

φ

V′

(→

⊃)φ ,「→ψ

「

→φ⊃ψ

(→

V)「

→φ

「→

VXφ

後

缶

弱し

そ∴

矮

背

(→ヨ)「→ φXt r→ョxφ (上

)「

→上 「 → θ

この体系がカッ トな しの直観主義連式計算 (これ を

ISで

表す:IntuitiOnistic Sequent)で ある。

連式:「→φが

ISで

_{証明可能であるのは,出発点がすべて公理であ り}

_,上

の規則 により統御 された 証明樹が構成 され るとき

,か

つその ときにか ぎる。連式 「 →φが

ISで

証明可能であることを 卜

Is「

→φ で表す。

3.2

主定理 さて

,連

式計算 と

2.4節

での自然演繹の連式 ヴァージ ョンとの関係 を考 えよう。 まず, 卜IsP→ψな らば

,自

然演繹 の連式ヴァージ ョンで 「 卜φが導出可能である… (*) (証明 は,「→φの

ISに

おける証明の長 さに関す る数学的帰納法 による。) この

(*)の

逆 も成 り立つ。い ま

,ゲ

ンツェンが導入 した次の規則

(CUT)を

考 える。 (⊃→)「 →φ

″

,F→

θ φ⊃ψ,「 →θ

(V→

)

φXt,「→θ

VXφ

,「 →θ (ヨ

→

)百

三

井

ギ

圭

零

た

_露

_境

_t鳥

_債

_教

_ャ

_篭

∝

Uり

これは自然演繹での消去規則をある意味で模倣する規則である。

6ち

_ャ

ゝま

, Is十三

_IS十

_(CUT)

とす る と, 「 卜 φが 自然演繹 の連式 ヴ ァー ジ ョンで導 出可能 な らば

,卜

Is+F→φ. が証 明で きる。 そ こで

,ゲ

ンツェ ンの主定理 : 「

CUTは

消去 可能 で あ る」 が成 り立 つな らば

,卜

Is.「 → φ な らば卜IsF→ φ とな るか ら

,上

の

(*)の

逆 が成 り立 つ こ とに な る。 ところで

_,自

然 演 繹 に とってカ ッ ト

(CUT)は

どの よ うな意味 を持 つか。 カ ッ トは,「卜 φ お よび φ,「r―′ か ら

,F卜

ψへ の移行 を許 す。 この移 行 は(⊃

I)と

(⊃

E)を

連続 して行 うこ と に よ り実現す る: φ,「 卜ψ (⊃ I) (⊃

E)

「 卜φ⊃ψ 「 卜φ 「 卜ψ ここに,新 しい最大式 φ⊃ψ が生 じている。また,導 出樹 の構成 とい う観点か らカッ トを見 ると, φ,「 φ

および ψ か ら,

鳥取大学教育学部研究報告 人文・社会科学 第 47巻 第

1号 (1996) 61

ψ を作 ることを許す もの と解す ることがで きる。この とき,φは新 しい最大式 となっている可能性があ る。 こうして

,カ

ッ トのない連式計算 の導出は

,最

大式のない標準的導出のみか ら成 る自然演繹 の 導出に対応する。 自然演繹 の導出が標準的な らば

,(*)の

逆 によ り

,そ

の導出 はカ ッ トのない連式 計算

ISで

証明 され ることになる。す ると

,主

定理 を証明することが

,自

然演繹 と連式計算の同等 性 を示すのに好都合であることが分か る。 ゲンツェンの主定理の証明 は

,よ

り複雑 なカッ トをよ り単純 なカ ッ トヘ と還元す る一連 の手続 き を示す ことか ら成 る。例 えば, Ｆ Ｆ ・ ︰ ぁ ァ 「 →φ 「 →ψ φ,「 →θ 卜式φが よ り単純 にものになっている。実際 うな洞察が基本 となっている9n。 を, (→

&)

「 →φ

&ψ

φ

&ψ

,「 →θ

(&→

)

(CUT)

「 →φ 「 → θ φ,「 →θ

(CUT)

「 → θ へ と置 き換 える。上 のカ ッ ト式 :φ

&ψ

_{よ り下 のカ ッ} の状況 は これ ほ ど簡単 な ものばか りで はないが

,

この よ 3。

3

古典論理の連式計算 さて

,古

典論理 に対する連式計算 を考察す るために

,連

式 を

T→

△'と_{い う形で表現す る。ここで}, 先件 「 は後件△とともに整式の有限集合であるが,△は空でない とす る。△が空の とき

,`F→

'と 書 く。 また,「→ (φ

)の

代わ りにF→φと略記する。 ところで

,こ

れ まで

IS(直

観主義連式計算

)で

は`上 'を_{原始記号 としたが}

_,こ

_{れ を落 として}`￢' (否定

)を

原始記号 とすることがで きる。 そして

,規

則 (上

)の

代 わ りに, 「 → 「 → θ を採用 し,`￢'に_{関す る規則 として,}

的 牝

い 〕 翠 お よび を追加す る。 この新 しい定式化 をIS′ とす る。 新 しい形式での連式:「→△の解釈 について考 える。Fの すべての要素が真であれば△の少な くとも 一つの要素が真であるとき,「→△は妥当であると呼ばれ

,Fの

すべての要素 を真 とし,△のすべての 要素 を偽 とす ることがで きるとき,「→△は反証可含ヒであると呼ばれる。これに対応 して

,規

則 につ いて も二つの解釈 を考 えることがで きる。規則 :

SI S2

S

において,「もし連式Slと S2がともに妥 当であるな らば

,連

式 Sも 妥当である」とい う解釈が可能で あるとともに,「もし連式

Sが

反証可能であるな らば

,連

式SlまたはS2の少 な くとも一方が反証可能

である」とい う解釈 も可能である。 この第二の解釈が成 り立つ ことを上のISアの (￢→)と (→￢) について確認 しよう。 まず(￢→

)で

ある。結論(下の運式

):￢

φ,「→が反証可能 な らば

,￢

φと 「 をすべて真 とす ることがで きる。よって

,Fの

要素 をすべて真,φ を偽 にし得 る。よって

,前

提(上 の連式):「→ φが反証可能 となる。次 に(→￢)である。結論

:F→

￢φが反証可能 とする。すると, 「 をすべて真

,￢

φを偽 とすることがで きる。 よって

,φ

とFを すべて真 とす ることがで きる。 よっ て

,前

提:φ,「→ が反証可能 となる。 ここで

,古

典論理 に対応 させ るため, ISアでの`￢ 'に_{ついての規則 (→}￢

_)(￢

→

_)を

_{各々一般化} して, φ,「 →△ 「 →△

,￢

φ 「 →△

,φ

￢φ,「→△ φ

&ψ

,「 →△ (∨→

)φ

,「 →△

ψ

,F→

△ φ∨ψ,「 →△ (⊃→)「 →△

,φ

ψ

,F→

△ φ⊃ψ,「 →△ (￢→

)「

→△

,φ

￢φ,「 →△

(V→

)φXt, VXφ,「 →△

VXφ

,「 →△ (ヨ→)φ ,「→△ ヨX _φax,「→△ ただし

,aは

「

,△

に出現 していない。 とする。する と

,各

規則 の結論 (下の運式

)の

反証可能性 の必要十分条件が

,少

な くとも一つの前 提 (上の連式

)の

反証可能性であるような

,運

式体系 を構成することがで きる。 この とき

,公

理 は 反証可能ではあ り得ない。 また一般 に

,規

則 の前提 の複雑 さの度合いはその規則 の結論 より (量化 子 に関す る規則 を除いて

)低

くなる。 よって

,結

論 の反証可含p14は

,よ

り複雑 さの低 い反証可台2性 の条件 によって表現 され得 る。 このような連式体系 を

CS(古

典論理連式計算

:`C'は

dassicalに 由来

)と

呼ぶ。

CSは

以下の公理 と推論規則か ら成 る: 公理 φ,「 →△, φ (→

&)「

→△,φ

F→

△

,ψ

(&→

)φ

,ψ

,「 →△ r→ △,φ

&ψ

(→∨)「 →△,φ

,ψ

「 →△,φ

Vψ

(→⊃

)φ

,「 →△

,ψ

「 →△,φ ⊃ψ (→￢

)

φ,「 →△ 「 →△

,￢

φ (→

V)「

→△, φ 「 →△, V Xφ ax (→ヨ)「 →△, ヨXφ, φXt 「 →△

,ヨ

xφ た だ し

, aは

「

,△

に出現 していない。

3.4

タブ ロー・ メソッ ド 最後に,カットなし連式計算の完全性証明の研究から1950年代に,Beth,Hintikka,Kanger,Schutte によって独立 に発見 されたタブロー・ メソッド (または意味論 タブロー

)を

考察す る90。 まず

,次

の定義か ら始 める。 定義 :φが整式の とき

,Tφ

, Fφはともに記号づ けられた整式である。 ここで意図 されている解釈 は

,Tφ

が「ψは真である

J,Fφ

が「φは偽である」とい うことであ り,

CSで

の反証可能性 を徹底することである。 こうして

,連

式(φl,一

,φ

k)→ (ψl,いちVlll}は記 号づけられた整式の有限列

:T

φl,…・

,T

φ

k,Fぬ

,一

,F VIllへ と変換 され る。

CSで

の規則 は上 下が逆転 した形で再解釈 され

,新

たな導出 は反証可能性解釈 の体系的探索 とな り

,枝

分かれす る規

鳥取大学教育学部研究報告 人文・ 社会科学 第 47巻 第

1号 (1996) 63

則は解釈の複数の選択肢 ということになる99ち 探索 は樹状の形 に表現 され

,探

索に成功 した場合, 連式の妥当性に対する反証が得 られたことにな りにの

,探

索樹が閉 じられて反証可能性が存在 しない ことが判明する場合

,元

の連式の妥当性が示 される°1ち タブロー・メソッドの体系

Tの

規則 は以下のものである (`S'は記号づけられた整式の有限集合で ある)。

S, Fφ &ψ

S, Fφ

lS, Fψ

S,Fφ

∨ψ

S, Fφ , Fψ

S,Fφ

⊃ψ

S,Tφ

, Fψ

S,F￢

φ

S, Tφ

S,FVXφ

S, F

φXa ただ し

, aは Sに

出現 していない。 Fヨ

: S, Fヨ

Xφ

S, Fヨ

Xφ , F φXt

_{S, T}

φXa ただ し

,aは

Sに

出現 していない。 枝分かれす る規則

(F&)(T∨

)(T⊃

)は ,反

証条件 の可能 な選択肢 の存在 を示 してお り

,探

索 においてはそのすべての選択肢が調べ られねばな らない。整式φのタブローによる証明 は,樹 の頂点 が(Fφ)であ り

,す

べての枝が閉 じている形での

,記

号づ けられた式の有限集合か ら成 る有限樹で ある。 より簡便 なタプロー は

,樹

の節 を記号づ けられた整式 の集合で はな く

,整

式 そのもの とす ること によって得 られ る。 まず

,頂

点の節

:(T

φl,…。

,T

φ

k, Fぬ

,…

,F Plrl}を縦方向に, T φl T φk

Fぬ

: F Fnl と書 き

,以

下の規則 を使 う: Tφ

&ψ

Tφ

Tψ

Tφ

Vψ

/

＼ Tφ

Tψ

Tφ ⊃ψ /// ＼＼ Fφ

Tψ

F&

FV

T&: S,Tφ

&ψ

S,Tφ ,Tψ

T∨

: S,Tφ

∨ψ

S,Tφ

IS,Tψ

T⊃

: S,Tφ

⊃ψ

S, Fφ

_IS,Tψ

T￢

I S,T￢

φ

S, Fφ

TVi S,TVXφ

S,TVXφ

,T

φXt

Tヨ

: S,Tヨ

Xφ

F⊃

F￢

FV

F/

｀ψ

Fφ∨ψ Fφ Fψ Fφ⊃ψ Tφ Fψ

T￢

φ

Fφ

T VXφ

Tφ

≒

Tヨ

Xひ

ただし

_,aは

枝

―

で新しいパラメ

Tφ

X. ―夕である。

これにより

,簡

潔な探索樹が得 られる

(鬱

_ち

さらに簡潔なタプローを得るには

,Tφ

'を`￢

_φ

'に

_,`Tφ

'を`φ'に

_{変換することで}

_,記

_{号づけられ}

た整式に替えて通常の整式の分解規則 とすることである。すると上の規則は次のようになる。

︼

、 ＼

＼ ″

 

 

 

代

″

φ

/

φ ／ た φ ﹁

Vxφ

￨

φ≒

.

ヨ

Xψ ￨ φ

tt aは

枝で新 しい パ ラメータ

例 として

,vx(φ

⊃の ⊃φ

Vvxψ

(こ

こでφにXは 出現していない

)を

_{,こ の最後の方式での}

タブロー

,メ

_ソンドで

_1分

_{析 しよう。}

F￢ φ

Tφ

FVxφ

矢

デ

ン

生

多

悠

哲

憲

訂

し

い

Fヨ 文φ

F

φ

Xt

￢

_評

φ

_ヽ″

司

_(φ

_Vψ

) ￨

￢φ

￨

￢ψ

￢

(φ

⊃ψ

) ￨

φ

￨

￢ψ

￢￢φ

￨

φ

￢

_VXφ

￨

コφ

tta aは

枝で新しい

パラメータ ￢ヨXφ ￨

￢φ

lt

φ&″

￨

φ

￨

ψ

鳥取大学教育学部研究報告 人文 。社会科学 第47巻 第

1号

(1996) 65

￢

_(VX(φ

_Vψ

_)⊃

_φ∨

_VXψ

) ￨

VX(φ

∨ψ

) ￨

￢

(φ

∨

VXψ

) ￨

￢φ

￨

￢

_VXψ

￨

￢ψ

Xa l

φ∨ψ

Xa /// ＼ ＼＼ ＼ φ

ψXa 二つの可能 な枝が ともに矛盾 を含 んで閉 じているので

,反

証 は不可能である。よって

,VX(φ

∨ψ) ⊃φ∨

VXψ

は妥当であることが証明 された。 こうして

,連

式計算か ら示唆 を得 て発展 したタブロー・ メソッドは

,反

証可能性 による整式の妥 当性

,非

妥当性 の判定方法 を提供す る。

註

サンドホルムによ/bば (G6ran SundhOlm,“ Systerns of Deduction"in D Gabbay and F Guenthner(edS), Handbook of Philosophical Logic,vOI I,Reidel,1983,pp 133 188),論理学的研究における演繹体系の役割 と

して,以下の事例 を挙げうる。① フレーゲの場合のような数学 (フ レーゲにおいては算術)の確実な基礎 を与 え ること

,②

様相論理のい くつかの分野 に見 られるような,すでに与 えられた意味論的帰結関係 を構文論的に生成 すること,③カットなしのゲンツェン連式による無限論理の初期の展開に見 られるような発見の道具 となること, ④ ヒルベル トの無矛盾性証明の計画に関する伝統的仕事のような,メ タ数学の研究対象 となること

,⑤

推論の本 性 についての哲学的洞察 を定式化するときの一つのモデルケースとなること,等において演繹体系が用いられて いるという。尚,本論文 を準備する過程で,このサンドホルムの論文か ら多 くの貴重な示唆を得た。 フレーゲの体系は『概念記法』に史上最初の論理の公理体系 として現れた。Gottiob Frege:Begnffsschnft,Nebert, 1879

ヒルベル トはこの体系を例えば次の書物で採用している。D Hilbert and P BernayЫ Grundiagen der Mathemauk V01 1/H,Sprilager,1934/39,2nd ed 1968/79.邦 訳

:D.ヒ

ルベル ト

/P.ベ

ルナイス (吉田夏彦・ 測野昌 訳)『数学の基礎』シュプリンガー・ フェアラーク東京 1993は,第2版 か らの抄訳である。 通常 この体系においても「推論規則Jと いう名称が使われるが,Sundholmに従い「証明規則Jと いう名称 を採用 する。 これは,推論の前提が「定理」であ り,単なる「仮定」であってはならない ということを暗示するのに都 合がよヤゝ。 証明 (正確には証明図式)の例 として,φ ⊃φの証明を描 く: (φ⊃((φ⊃φ)⊃φ))⊃((φ⊃ (φ⊃φ))⊃ (φ⊃φ

))

φ⊃((φ⊃φ)⊃φ) φ⊃ (φ⊃φ) (φ⊃ (φDφ))D(φDφ) φDφ (1) これ は,

という形 をしている。(→と② は各々公理

(A2)(Al)で

あ り,偲)はこれ らを前提 としての

MPに

よる結論であ る。(4)は再び公理

(Al)で

あ り,13),(4)か ら

MPに

より(働が導かれる。証明が唯一つの移行パターンである

M

Pに より形成 されるという単純 さにより,この体系の証明に関するメタ定理 (証明の特徴 を述べる命題)の発見 とその証明 (メタ証明)が容易になる。 しか し反面

,上

の最 も簡単な例か らも分かるように, この体系の証明を 遂行するのは頗 る煩雑である。出発点が三種類の公理に限 られていて(大抵 は長大なものになる),しか も一つの パターンでしか移行できないから先の見通 しが限られるか らである。 この欠点は,しか し,以下で述べる演繹定 理により,相当程度 は解消される。 脩

)証

明は概略以下のようになる。定理の仮定 により,出発点 としてφl,―。,ぬ(「の要素)とφという仮定 と公理9/1, …_{,7mを取 る′の証明}Dが存在する: φ

,

φl,¨。

,仇

.,

狛,一,9/n θ⊃δ

θ (A/1P) Dに`φ⊃'変<sub>形,す</sub>なわちDの各 φD(θ⊃δ) φ⊃θ `φ⊃

MP'

φ⊃δ φ⊃ψ この`φ⊃D'を<sub>改良 して,「</sub>だけか らのφ⊃ψの証明を作 ることができることを示す。<sub>(言</sub>い換 えると<sub>,`φ</sub>DD'を構 成 しているすべての式2に 対 して,「 卜αであることを示す。)ま ず擬証明樹`φ⊃D'の出発点である三種の式の場 合である。 (a)φ⊃φの場合。註5よ り証明可能。ゆえに,「 卜φ⊃φ.

(b)φ⊃φi(φiC「)の場合。仮定φiと 公理

(Al)φ

i D(φ⊃φl)を_{挿入 して},

φi φi⊃ _(φ⊃φi)

(A/1P)

φ⊃φi

を作 ることで,「卜φ⊃φiが示せ る。

(C)φ⊃γi(γiは公理9/1,…,9/111の一つ)の場合。公理 γiと公理

(Al)γ

i D(φ⊃γi)を挿入 して,

γl γi D(φ Dγi

(Mp)

φ⊃γi を作 ることで 「 卜φ⊃γiが示せる。公理

(Al)の

存在理由はこの

(b)(C)が

可能 となる点にある。残 るは, (d)擬

MP,す

なわす φ

DMP'に

よって移行 している途中の段階を正 しい

MPに

復元することである。そのた めに公理

(A2)を

使って,φ ⊃(θ⊃δ)と φ⊃θからφ⊃δへの

MPに

よる移行 を次のように作 る(公理

(A2)

の存在理由はここにある): (φ⊃ (θ⊃δ))D((φDθ

)D(φ

Dδ)) φ⊃ (θ⊃δ)(MP) φDθ (φ⊃θ)⊃ (φ⊃δ)

(MP)

φ⊃δ 明   ， 証 て     ・ ⋮ ︰

δ

⋮

ψ

拗

_祉

先

噺

榊

沖

”

獅

_¨

と り

腕

靴

Ｄ

φ

_，

て   の   φ さ 式 い   Ｄ

視

界

φ

⊃

に                 Ｄ め               ⊃

級

を

作

る

_。

﹁

_︲

︲

牌

︱

ユ

帰納 のイ反定 よ り_「 卜φ⊃ (θ⊃δ

), F卜

φ⊃θであるか ら,F卜φ⊃δ. ずれかのパ ター ンに当て はまるか ら,「卜φ⊃ψ

.Q.E.D.

`φXt'と_{い う表現 は,変項}Xが_{φ中で 自由変頂 として現れてい るとき},Xを る。 これ は次のように帰納的 に定義 され る。 こうして,φ ⊃″も,(a)― (d)のい tで置 き換えてφか ら得 られる表現であ (0)φ が原子文 の とき,φXtはφ中のXを tで置 き換 えて得 られ る表現である。

鳥取大学教育学部研究報告 人文・ 社会科学 第 47巻 第

1号 (1996) 67

(1)(￢φ)Xt=def￢ (φXt)

(2)(φ⊃′)Xt=def φXt⊃ψXt

?lV ypl神

工 骰ガ班絲摩

で

あ

る

と

試

こ う し て,(X=y)yxは X=X で あ り, VX(X=X)Xtは VX(X=X)で あ る 。

い ま,φを￢

Vy(x=y)と

す る。す ると,`t'を yとす る とφXt=def￢

vy(y=y),(VXφ

Dφ )Xt=def (VXφ)Xt⊃φ

Xt=VX￢

Vy(x=y)⊃

￢

Vy(y=y)で

あ る。 ところが この最後 の式 は論理的に妥当で は ない。 なぜな ら,二つ以上 の個体 を持つ任意 の個体領域 において,先件 は真であるが後件 は常 に偽 だか ら,反例 モデル を作 ることがで きるか らである。 これが

(Q4)に

制 限条件 が必要 な理 由である。すなわち, Xの自由出 現がφ中 において,tが持つ 自由変項 を束縛す ることにな るような変項 の作用域 に存在 しない とき,tはXに対 し て「代入可能」 と言われ る (または「Xに対 して代入可能」の代 わ りに「Xに対 して自由」 とも言われ る)。 これ は次のように帰納的 に定義 され る。 (1)φが原子文 の とき, tはXに_{対 してφで代入可能 であ る。}

(1)tが

Xに_{対 してφにおいて代入可能であるとき, tは}Xに対 して (￢φ)において代入可能である。 (

)tが

Xに対 してφと′において代入可能である とき, tはXに対 して(φ⊃の￨こおいて代入可能 であ る。 (

)Xが

Vyφにおいて 自由に現れない ときか,また はyが tにおいて出現せずtが Xに対 してφにおい て代入可能である とき, tは Xに対 してVyφにおいて代入可能である。 証明 は以下の ようになる。_「 か らのφの証明樹 をDとす る と

,Dは

次の形 をしてい る: 耳

公響

￨ ￨ ￨ ￨

φl, …

_,

_ぬ

_,

_拗

_,

…。, 9/111 (MP) そ こで

,D中

で出現 している各整式 δに対 して,「卜VXδ を示す。 まず,δがDの出発点である場合: (i)δが公理9/1,… ,9/ntの一つで あるとき。公理 の一般化 はすべて再 び公理であるか ら

,VXδ

は公理で ある。ゆ えに,「卜VXδ。 (1)δが 「 の要素であるとき。定理 の仮定 によ り,F中のいか なる式 において もXは自由変項 として は出現 してい ないか ら,当然δにも出現 していない。 しか るに

,公

理

(Q6)よ

り,卜δDV Xδ.δは 「 の要素 だったか ら,

MPに

よ り_「 卜VXδ。(公理

(Q6)の

存在理 由 はこの ことが可曾ヒとなる ことにある。) 残 るはモ ドゥス・ポネ ンスを適用す る場合である。帰納法 の仮定 よ り,「卜

VX(θ

⊃の およびF卜VXθ。とこ ろが

(Q5)よ

り,卜 VX(θ⊃ψ

)D(VX'⊃

VXψ

),よって

MPを

2回適用 して,「卜

VXψ

。(公理

(Q5)

の存在理 由はここにある。

)Qo E,D。

このタイプの体系 は,タルスキー,カ リシュ&モンタギ ュー,モンク等の以下 の一連 の論文で取 り上 げ られてい る。 A Tarskit“A sirnphfied formulation of predicate logic with identity",Archiv fiir mathematische Logik

und Grundiagenforschung(以 下Archと略記)7,1965,pp 61-79 D Kalsh and R A/1ontague:“On Tarski's

fOrmalization of predicate logic with identity",Arch 7,1965,pp 81-101 D Monk:“ Substitutionless predicate

logic Mrith identity",Arch 7,1965,pp■o2-121

例 えば,以下 のチ ャーチやメンデル ソンが採用 してい る体系 は

,(Al)―

(A3),(Q4)(同

じ制限 を伴 う)は 共通であ るが,次の公理 を加 える: (Q′

5)VX(φ

⊃ψ

)D(φ DVXψ

)… … Xはφ中に自由には出現 しない。 この体系 (F′

CQCと

す る)では,公理が公理図式 の事例 のみで あ り,それ らの一般化 は公理 に含 まれない。 た だ し,次の二 つの証 明規則 によってその効力 を確保す る 。 R′ 1. A/1P

R′

2(一

般化). 卜φ ⇒ 卜VXφ

先 の体系

FCQCで

は一般化 は派生推論規則であつたが,こ のF′

CQCで

は原始証 明規則である。Cf A Claurch

:introduction to Mathematical Logic,x01 1,PricetOn U P 1956,E A/1endelson:introduction to Mathematical

Logic,、/an Nostrand, 1964

個体項 の定義 はこうなる: (i)個体定項 は項である。 (it)パラメータ は項 である。 (iit)f'が ,項関数記号であ り, tl,…・_{, tjがすべて項 な らば,} f'(tl,…, ti)は項 である。 ポイ ン トは量化 に関す る証明規則 であるか ら

,(RVI)の

場合 のみ考 える。い ま

,Dを

,仮定 φ,φl,…

,仇

か らのθ⊃V X ψaxの証明 とす る: φ

,

φl, ・, 'Dψ θ⊃

VX″

ax

(RVI)に

対 す る制限が満 たされているか ら,固有パ ラメータaはθに も,仮定 …

,ぬ

のいずれにも出 して,仮 定φl,―,,仇 だ 現 していない。帰納法の仮定 によ り,`φ⊃'変<sub>形 によって得 られ る擬証 明樹</sub>`φ⊃

D

けか らのφ⊃ (θ⊃の の証明Dアが存在する。 このD′に続 けて以下の証明樹が作 (φD(θ⊃ψ))⊃ (φ&θ⊃ψ

)*

φl, ―, φk φ⊃ (θ⊃ψ)

(φ&θ⊃V X ψax)⊃ (φ⊃ (θ⊃V X ψax))**

φ&θ⊃ψ φ&θ⊃V X ψax (h/1P) φD(θD V X _ψax) ここで,`*'のついた式 は公理(A&Ei)と命題論理部分 の演繹定理 によって証明可能 であ り,φ&θ お よび仮定 φl, …

_,仇

のいずれ に も固有パ ラメータaが出現 していないか ら

,(RVI)の

適用 は正 し く,`*・'のついた式 は公理

(A&I)と

命題論理の部分 の演繹定理 によ り証明可能である。

ゲ ンツェンのオ リジナルの論文 は次のものである。G Gentzen:“Untersuchungen dber das iogische Schliessen", Mathematische Zeitschrift 39, 1934,SS 176-210, 405-431

M Szabo:The Co‖ected Papers of Gerhard Gentzen,North‐ Holland, 1969,p.74 本文中の規則 の表現 は略式 の ものである。 ここで

,煩

を厭わず詳 し く正確 に表現す る。

(A) :任

意 の整式φに対 して,φただ一つか ら成 る木がφ自身 に依存す る(つま りφ自身 を仮定 とす る)φの

導出 となる。

Do Dl

(&I):

φ。 と

VrO

が,それぞれ,仮定φl,…

,ぬ

と仮定 沈,…,Flllに依存す るφOとVrOの導出で あ る とき,

Do

φl

望生

_型

_k&I)

は

,仮

定 φl,―。

,仇

,ψl,―・

,ち

に依存す る φ。&Tr。 の導出である。

D

(&Ei):i=0,1に

応 じて二つある。あ&φlがЙ,…,rnIに依存 す る φ。&φlの導出である とき,

D

撃 鰻

ED

は,同じ仮定 に依存す る φiの導出である。 司 Ｉ Ｆ 封 Ｖ ぬ 。   似

︲ φ．，確

律

 

ヴ

 

Ｄ

Ｅ φ ，

_湾

鵬

﹁ 卜

︲Ｊ

餌

(RVI)

鳥取大学教育学部研究報告 人文 。社会科学 第 47巻 第

1号 (1996) 69

D

(V11):三

=o,1に

応 じて二つ ある。 φl力ゞ仮定 仇,…

,あ

に依存す るφiの導 出で あるとき,

D

φ

i(V11)

は同 じ仮定に依存す る φoVφlの導出である。

D

φ

Dl D2

ψ

(VE):φ

Vサ が仮定ぬ,…,pltに依存するφV′の導出であり,θ

と θ が,そ れぞれ,仮定 φ

,4,

・・_{・デ仇 と仮定ψ}

_,a,i,吼

_{に依存するθの導出であるとき}, [φ

] [ψ

]

D Dl D彦

φVψ

θ

θ_{^_、} 戸三 生

_二

cvE)

は,仮定φl,・・・

,ぬ,ぬ

,■

,仇

,乳―,中●,■に依存す るθの導出であ る。

D

(DI):

サ が仮定仇

,…

,益

に依存す る′の導 出である とき,

D

濤

(DI)

は

,仮

定 仇半,...,弗*に依存 す るφ⊃サの導 出であ―る。ただ し,仇半j.,,φm・はφl,…Ⅲ あ か らい く つかの (0個 やすべての場合 も含む)φの出現を取 り除いて得 られるリス トである。取 り除かれたψの 出現 は「解除された」 と言われる。

DO Dl

(DE):φ

⊃ψ と

,

が,それぞれ,仮定φl,―・

,ぬ

と仮定ぬ,…

,ち

に依存す るφ⊃ψ と φ の導出 であるとき, つ。

Dl

∵ ω め は

,仮

定仇,｀・_{・ ぬ}

,ぬ

,中i VInに依存するサの導出であ―る。

D

(■

) :

上 が仮定φl,…・

,ぬ

に依存する上の導出であるとき,

D

■ (・) は,同じ仮定 に依存するφの導出である。

D

(VI):

φ が仮定携,…

,ぬ

に依存するφの導出であり,φ 中の固有パラメータaがこれ らの どの仮定にも 出現 していない とき,

D

器 “

D

は,同じ仮定に依存する V Xφ4そ _{の導出である。}

D

(VE),VXψ

が

,仮

定 仇,1・・

,ぬ

に依 存 す るVXφの導 出で あ る とき,

D

響 付ゆ

は,同じ仮定に依存するφ工1の導出である。

D

(ヨ

I):

φXt が仮定 ぬ,…

,ぬ

に依存す るφXtの導出である とき,

D

勢 徊

D

は,同じ仮定 に依存 す るヨ Xφ の導出である。 φXa

D Dl

(ヨ

E):ヨ

Xφ が仮定 φl,―・

,ぬ

に依存す るヨ Xφ の導出であ り,θ が仮定φXa,島,…

,ら

に依存 す るθの 導出であ り,固有パ ラメータaがョ Xφ に もθに も,φXa以外 のθが依存す るどの仮定 に も出現 していな い とき, [φXa] Dl θ (ヨE) は,仮定φl,¨・,φ

k,a,… ,ら

に依存するθの導出である。 例 えば,次の二つの導出においては

(DI)は

いずれ も「解除」を伴 う。

D

ヨ Xφ 3 [P] ― 一 ― ―

(VI)1

P∨ (Q⊃

P) [P]

2 1

[Q] [Q⊃

P]

(DP)

PIV E)ユ

話

￨三

￨￨:

しか し, これ らは回 り道 のある

,標

準的 (nOrmal)でない導出になっている点で

,適

切 とは言い難 い。 自然演繹 の体系 の中で「適切性Jを確保 す るためにはい くつかの条件 が必要 となる。それ について は,D Prawitz:Natural Deducjon,Almqvist&Wiksells,1965,pp 81-87参 照。

(lo Cf D Leivant : “Assumption classes in natural deduction", Zeitschrift fur mathematische Logik und

Grundiagen der Mathematik 25,1979,SS l-4

10 (ADl)に

ついて はすでに扱 った。(A⊃2)について は以下のように証明で きる。 1 3 [φ

] [φ

D(ψ

Dθ)] ψ⊃θ 1 2 [φ

] [φ

⊃ψ]

(DE)

(DE)

竺(DE)

浩 (DI )1 (φ⊃ψ)⊃ (φDθ) (DI)2 (φ⊃ (″Dθ))⊃((φ⊃ψ

)D(φ

⊃θ))

(DI)3

FIQCの

他の公理

:(A&I),(A&Ei),(AV Ii),(A∨

E),(A■

),(AVE),(Aヨ

E)に

ついても同 様である。

90 FIQCの

証明規則は

(RVI)と

(Rヨ

E)の

二つである。これらをいま推論規則とみて

,仮

定からの証明を

D

考 える。

(RVI)の

場合。仮定 ぬ,…

,ぬ

か らのφ⊃″の導出をφ⊃ψと表 す。

(RVI)に

よ り,φ⊃V X ψaxの 導出が許 されるが,(固有パ ラメー タaに関す る制限条件 によ り)aはφに出現 してお らず,(自然演繹 での推論規 則 としての条件 に合致す る意味で)仮定 Й,…

,ぬ

に も出現 していない とみな して よい。 この とき,以下 の導出

鳥取大学教育学部研究報告 人文 。社会科学 第 47巻 第

1号 (1996) 71

D l

φ⊃′

[φ

]

(DE)

廟 粗

1 (Rヨ

E)も

同様￨

l D

[φ

Xa]

φXaD′

2 (DE)

[ヨXφ

]

ψ r司ぃ、.

″一ニァ、

FE)1

競

OD2

ここで,固有 オペ レー タaは,ψにも,仮定 ψl,…・

,ぬ

に も出現 していないか ら,(ヨE)適用 に伴 う制 限条件 は 守 られている。

90「

卜Nφを確立 す る最終推論規則が

(&I)と

(ヨ

E)の

場合 を考 える。他 の場合 は類比的 に実行 で きる。

(i)(&I)の

場合。 φl,…・

,仇

卜F φOおよび ψl,…・,Vln卜Fぬ と仮定す る。1, 4節の

FIQCの

公理

(A&1)に

よ り,卜Fあ ⊃(Vro D(φ

O&ぬ

))。 仮定 φl,…。

,仇

,Vrl,…,PIllの下で

MPを

三度使 って,φl,

…

_{,仇 ,仇}

_,…,Vnl卜あ

&ぬ

.

規則

(&E)の

場合 は公理(A&El)を,規則

(VI)の

場合 は公理 (A∨Iりを,規則

(VE)の

場合 は公理

(AV

E)を

,規則

(DI)の

場合 は演繹定理 を,規則 (■)の場合 は公理 (A上 )を使 って同様 に証明で き

,規

則 (D

E)は

MPそ

の ものであるか ら トリブィアルに成 り立 つ。

(1)(ヨ E)の

場合。 「 卜FヨXφ を示す

,仮

定か らの証 明Dと ,△ ,φ ax卜_{Fθ を示す仮定か らの証 明Diがあ} る とす る。 ただ し,固有パ ラメータaは,ヨXφ に も△に もθに も出現 していない とす る。 この とき, [φ

aX]

△ Dl θ 一―― (演繹定理) 「

φ axDθ

D

二二一―― (Rヨ

E)

―パラメータaの 制限条件 は ヨXφ

ヨXφ⊃θ

_{守 られ} rい_る ^

(MP)

守 られている。 θ によって,「 ,△ 卜Fθ が示される。

同様 に

,規

則 (ヨ

I)の

場合 は公理 (AヨI)を ,規則

(VE)の

場合 は公理

(AVE)を

,規則

(VI)の

場

合 は証明規則

(RVI)を

それぞれ使 って示す ことがで きる。

9か この定理の証明はD Prawit2の 前掲書 (Natural Deducjon)で 与えられている。

120 Cf G,Sundholin:“Proof「Γheory and Meaning",Handbook of Ph‖Osophical Logic v01 HI,Reidel,1986,pp 471-506

90規

則 は次のように表現 される。 (0)φ卜φ …仮定の規則

(i)F卜

φならば

,F,△

卜φ …「仮定を増やしてよい」という規只J。 これは暗黙のうちに認められていたもの を明示的に表 したものである。 (1)「卜φかつ△卜ψならば

,F,△

卜φ&ψ …

(&I)

( )「 卜φ。&φ lな らば, F卜φi(i=0,1)…

(&E)

( )「 卜φiな らば, F卜φo Vφ

l(1=0, 1)

―

(VI)

(v)「卜φVψかつ φ,△ I卜 θかつ ψ,△ 2卜 θならば

,F,△

1,△2卜 θ `¨ (VE) ( )φ ,「 卜ψならば,F卜φDψ …

(Dl)

( )「 卜φ かつ△卜φDψ ならば

,F,△

卜ψ …

(DE)

(v )「 卜上ならば,F卜φ … (■) ( )「 卜φ かつ

aが

F中 に出現していないならば,F卜V X φax …

(VI)