古典論理

古典論理 ^∗ の理解の観点に関する一考察

角田健太郎 2019 年 3 月 22 日

概 要

数学における証明で用いられる論理である古典論理(すなわち各論理式の意味は真か偽のどちらかに定まって いるという理解が一般的である論理)は、論理式という構文論的単位に意味内容を与えることでその意味理解を図 るような(論理の理解に当たって標準的な観点である)モデル論的意味論では捉えることのできないような意味の 差異を、証明図という構文論的単位において持っているということを論じ、古典論理の理解にあたって求められ る観点とはどのようなものであるのかを検討する。

この検討のために本論文では次のような流れで議論を行う。まず出発点として、証明可能な論理式に意味内容 を与えるモデル論的意味論による論理理解の方法が、古典論理に対しては有効に機能していないと考えられるこ とを論じる。そしてモデル論的意味論と古典論理の間のこのような事情はどのような理由により引き起こされる のか、という形で問題を提起する。そしてこの問題に対し、その非有効性を引き起こしている原因は、近年の論 理学領野の研究において示された古典論理の特徴である「論理的推論の冗長さを含む証明図をその冗長さを含ま ない証明図(正規な証明図)へと変形する計算論的手続きが非決定的な計算であり、その変形手続きによって得ら れる正規な証明図は一意には定まらない」という特徴に求めることができる、ということを論じることによって 答えることを試みる。

∗本論文では論理ということでその範囲を命題論理に限って議論を行う。

0.1 はじめに

ある論理についてその意味論が果たす役割の一つということで、次のことは哲学と論理学において広く受け入 れられていることだと言えよう。それは、ある論理の意味論は、その論理の構文論で証明可能な論理式を構成する 文字列の文法上の各部分が、論証活動においてどのような操作的手続き (これは機能や振る舞いや使い方等々と一 般的には呼ぶことができよう) を果たしているかということを、数学的概念と論理式との間の対応関係を定めるこ とで論理式という形式的表現にその内容の解釈を与えることによって明らかにしている、ということである。特 にその数学的概念と論理式との間の対応関係ということで、モデルと呼ばれる集合や写像などの概念を用いて論 理式の真理条件を定めることを考える意味論を、ここではモデル論的意味論と呼ぶことにする。基本的に論理学 において意味論と言えば、このモデル論的意味論を指すと言えよう。

0.2 問題提起および本論文の目的

さてしかし、モデル論的意味論は古典論理に対しては、上で述べたような意味論の役割すなわちその構文論で 証明可能な論理式の操作的意味内容の解明という役割を果たしていると言えるだろうか？これが本論文の第一の 問いである。そして、この問いに対する否定的回答に一定の正当性が存するならば、では古典論理とモデル論的 意味論の間のそうした事情はどのような原因によって生じていると考えられるのだろうか？これが本論文の第二 の問いである。

本論文の目的は二つである。まず一つ目は、その第一の問いの確立およびこれに対する否定的回答を与えるこ との正当化を試みることである。すなわち、古典論理で証明可能な論理式の操作的意味内容を既存のモデル論的 意味論が解明しているということに対する疑義の正当化を試みることである。そして二つ目は、古典論理の意味 論としてモデル論的意味論が有効に働かないということが認められることのそもそもの原因の究明を試みること である。この究明のために本論文では、古典論理とモデル論的意味論の間でそのような事態が起こる原因を解明 していると見なし得るある論理学的事実を紹介し、この事実がどのような点で先の第二の問いに対する答えを与 えているのかということの考察を行う。なお、ここで紹介することになる論理学的事実とは具体的には、Gerhard

Gentzen の論文 [5] によって考案された古典論理の形式体系の一つである sequent 計算においては、その強正規的

な cut 除去を考えた際に正規形が一意に定まらない、という事実である。

0.3 本論文の構成

本論文の構成は次の通りである。まず、本論文の主要部分は全部で 3 つの章から成る。先の本論文の目的のう ちの一つ目が第 1 章に、二つ目が第 2 章に対応する。第 3 章ではまとめを行い、そして今後の展望を述べる。

第 1 章は問題提起を試みる章である。ここでは、まず古典論理で証明可能な論理式の操作的意味内容を既存の モデル論的意味論が解明しているということに対する疑義の正当化を試み、そして古典論理とモデル論的意味論 の間で認められるこうした事情はそもそもどのような原因によって起こるのか、という形で問題提起を行う。第 1 章は 4 つの節から成る。まず第 1 節では、モデル論的意味論がある論理で証明可能な論理式の操作的意味内容を 解明するということが具体的にどのようなことであるのかを、直観主義論理の意味論のひとつとして知られる S4 フレームの Kripke モデルによる意味論を例にとり説明する。より具体的には、直観主義論理で証明可能な論理式 の真理条件と、その論理式の部分論理式の真理条件を比較することによって、この意味論がどのようにしてその 論理式の部分表現に対して論証における操作的振る舞いを与えているかということを説明する。そして続いて第 2 節では、今度は古典論理と真理値モデルによる意味論を取り上げ、先の直観主義論理 -S4 フレームの Kripke モ デルによる意味論の場合と対照的に、真理値モデルによる意味論が論理式に操作的意味内容を与えていないとい うことを、部分論理式の意味内容を孤立的に考えることができるという点から説明する。さらに続く第 3 節では、

ここまでの議論に対して想定され得る反論である、古典論理で証明可能な論理式に操作的意味内容を与えること

ができないのは、真理値モデルに固有の問題なのではないか、という反論に対しその再反論として、古典論理の

S5 フレームの Kripke モデルによる意味論を考える。そしてここでも真理値モデルによる意味論の場合と本質的

に同様の事態が起こることを指摘する。最後の第 4 節では、以上の議論から古典論理で証明可能な論理式の操作

的意味内容のモデル論的意味論による解明に一定の困難が認められるということを確認し、そしてこれを踏まえ

て本論文第二の問いすなわち「古典論理の意味論としてモデル論的意味論が有効に働かないという傾向性が認め られることのそもそもの原因は何か？」という問題の提起を行う。

第 2 章は問題解決を試みる章である。ここでは、古典論理で証明可能な論理式にうまく操作的意味内容を与える ことができないことのそもそもの原因を解明していると見なし得るような先行研究があることを紹介する。それ は具体的には、 Gentzen により考案された形式体系におけるいわゆる証明の回り道の解消に関わる計算論的研究 である。より具体的には Gentzen により考案された形式体系である sequent 計算の cut と呼ばれる推論規則の強 正規的な除去についての研究であり、そしてその中でも 1990 年代ごろから [1] などを発端として行われるように なった、正規形に一意性の制限を課さないような cut 除去の研究である。ここではこの研究の系譜にある Christian

Urban の論文 [11] を取り上げ、そこでの議論を説明する。具体的には Urban の論文では、古典論理の sequent 計

算の強正規的な cut 除去がどのようにして非決定的な計算だと特徴づけられるのかということについての議論が 行われている。本章ではこの Urban の論文の紹介ののち、この研究が古典論理で証明可能な論理式の操作的意味 内容がうまく与えられないということの原因の理解にどのように貢献するか、ということを論じる。第 2 章は 2 つの節に分かれている。第 1 節では、準備として Gentzen の形式体系とそこで考えられる証明の回り道とその解 消という概念の説明をし、そしてさらに計算論的議論の準備としてラムダ計算と Curry ＝ Howard 対応の説明を 行う。そして第 2 節では、その証明の回り道とその解消に関わる研究の歴史的経緯の中で生じた古典論理に関わ る問題と、この問題に対する Barbanera らをはじめとする研究者の観点と Urban の議論の紹介を行う。第 4 節で

は、この Urban の議論が、本論文の問題意識である古典論理で証明可能な論理式のその操作的意味内容理解の困

難という事情にどのように結びつくのかということを論じる。

第 3 章では、まず本論文の全体の議論のまとめを行ったのち、本考察の意義と今後の展望を述べ、結びとする。

目 次

0.1 はじめに . . . . 2

0.2 問題提起および本論文の目的 . . . . 2

0.3 本論文の構成 . . . . 2

1

5 1.1 モデル論的意味論による論理式の操作的意味内容の解明 . . . . 5

1.2 古典論理の真理値モデルによる意味論 . . . . 7

1.3 古典論理の S5 フレームの Kripke モデルによる意味論 . . . . 8

1.4 古典論理とモデル論的意味論の間の事情 . . . . 8

2

10 2.1 Gentzen の形式体系と証明の回り道の解消、および計算論的議論の方法 . . . . 10

2.1.1 Gentzen の形式体系 N J ・N K 、LK・LJ . . . . 10

2.1.2 証明の回り道とその解消 . . . . 14

2.1.3 Gentzen の cut 除去定理 . . . . 16

2.1.4 型付きラムダ計算と Curry=Howard 対応 . . . . 18

2.2 LK の強正規化が非決定的計算であるとする観点と古典論理で証明可能な論理式の意味内容の問題 26 2.2.1 歴史的議論 . . . . 26

2.2.2 Urban による Danos の批判と強正規化手続きの定義 . . . . 27

2.2.3 Urban の強正規化が古典論理で証明可能な論理式の意味内容の問題にもたらす知見 . . . . . 34

3

36 3.1 まとめ . . . . 36

3.2 本考察の意義および今後の展望 . . . . 36

4

A：Hauptsatz

38

1 問題提起：古典論理とモデル論的意味論

本章では古典論理で証明可能な論理式の操作的意味内容を既存のモデル論的意味論が解明しているということ に対する疑義の正当化を試みる。

1.1 モデル論的意味論による論理式の操作的意味内容の解明

まず、ある論理で証明可能な論理式の操作的意味内容をモデル論的意味論が解明するということはどういうこ とであるかを説明する。直観主義論理の意味論として知られる S4 フレームの Kripke モデルによる意味論を具体 例にとり説明する。

まず準備として、我々の議論の前提となる言語と論理式の定義を行う。言語および論理式に関する定義は次の通 りである。 ( なお次の定義には第 2 章ではじめて用いることとなる記号や概念の定義が含まれている。 )

• 言語および論理式に関する定義：

– 言語の定義：

∗ 命題記号：

· 命題定数記号： ⋎ 、 ⋏

· 命題変数記号：

A、B、…、およびそれらに添え字を付けたもの

∗ 論理記号： ∧ 、 ∨ 、 ⊃ 、 ¬

∗ 補助記号： ) 、 ( 、 → 、 ,

– 論理式および terminal symbol の定義：

1. ちょうど 1 個の命題記号のみからなる文字列は論理式である。この論理式は terminal symbol を持 たない。

2. A と B が論理式のとき、A ∧ B と A ∨ B と A ⊃ B と ¬ A は論理式であり、それらの terminal symbol はそれぞれ、 ∧ 、 ∨ 、 ⊃ 、 ¬ である。

3. 以上の操作を有限回繰り返して得られる文字列のみが論理式である。

∗ なお、以降では任意の論理式を大文字のドイツ文字で表す。

さて直観主義論理の S4 フレームの Kripke モデルによる意味論の定義は次の通りである。(なお以下で「 ∧ b 」、

「b ∨ 」、「 ⊃ b 」、「 ¬ b 」、「b ∀ 」、「b ∃ 」はそれぞれメタ理論の命題間の論理的結合関係を表している。)

• S4 フレームの Kripke モデルによる意味論の定義：

– S4 フレーム F

、 2 元集合 T 、付値関数 V の組 M = 〈 F

, T , V 〉をモデルとし、これを S4 フレーム

の Kripke モデルと呼ぶ。ただし、

∗ F

とは、集合 W 、到達可能関係 R の組〈 W , R 〉である。

· W = { w

, w

, ... }

· R とは、反射性と推移性を満たす W 上の 2 項関係である。

∗ T = { true, f alse }

∗ V = W × P −→ T

· ただし P は命題記号全体の集合を表している。

· なお、b ∀ w

( V (w

, ⋎ ) = true)b ∧ b ∀ w

( V (w

, ⋏ ) = f alse)

– ある S4 フレームの Kripke モデル M

の集合 W のある元 w

について論理式 D が成り立つこと M

, w

| =

D の定義：

∗ Dが命題記号のとき、

M^′, wa|=D⇔b∀wx(waRwx⊃Vb (wx,D) =true)

∗ DがA∧Bという形のとき、

M^′, wa|=D⇔ M^′, wa|=Ab∧M^′, wa|=B

∗ DがA∨Bという形のとき、

M^′, wa|=D⇔ M^′, wa|=Ab∨M^′, wa|=B

∗ D^がA⊃B^{という形のとき、}

M^′, wa|=D⇔b∀wx(waRwx⊃b(¬Mb ^′, wx|=Ab∨M^′, wx|=B))

∗ Dが¬Aという形のとき、

M^′, wa|=D⇔b∀wx(waRwx⊃bb¬M^′, wx|=A)

– 真理条件の定義：

直観主義論理で論理式 D が証明可能

⇔ 任意の M について、b ∀ w

( M , w

| = D)

では、この S4 フレームの Kripke モデルによる意味論により、直観主義論理で証明可能な論理式は具体的には どのように解釈されるであろうか。例として直観主義論理で証明可能な論理式 A ⊃ A をとろう。定義により次の ことがわかる。

  直観主義論理で論理式A⊃Aが証明可能

⇔ 任意のMについて、b∀w_x(M, w_x|=A⊃A)

⇔ 任意のMについて、b∀w_x(b∀w_y(w_xRw_y⊃b(b¬M, w_y|=Ab∨M, w_y|=A)))

⇔ 任意のMについて、b∀w_x(b∀w_y(w_xRw_y⊃b(b¬b∀w_z(w_yRw_z⊃Vb (w_z, A) =true)b∨b∀w_v(w_yRw_v⊃Vb (w_v, A) =true))))

なるほど直観主義論理で証明可能な論理式 A ⊃ A の意味内容とは、「どのような S4 フレームの Kripke モデル M を考えようとも、その M の集合 W のどの元 w

についても、w

から到達可能なすべての元 w

において、w

から到達可能なすべての元で必ずしも A の付値が true でないか、または、w

から到達可能なすべての元で A の 付値が true であるか、のいずれかである」というものだとわかる。

ここでさらに部分論理式の概念を導入する。部分論理式の定義は次の通りである。

• 部分論理式の定義：

論理式 D が論理式 C の部分論理式であるという関係を C の構成に関する帰納法により次のように定義する。

1. C が命題記号のとき、D は C 自身。

2. C が A ∧ B または A ∨ B または A ⊃ B という形のとき、 D は C 自身、または、 A の部分論理式のひ とつ、または、B の部分論理式のひとつ。

3. C が ¬ A という形のとき、 D は C 自身、または、 A の部分論理式のひとつ。

ここで先に確認した論理式 A ⊃ A の意味内容を見ると、注目できる事実がある。それは、A ⊃ A の部分論理式 のうち条件節の A の意味内容および帰結節の A の意味内容はどちらも、A ⊃ A が成り立つ点としての W の元が まず考えられ、そしてその元からの到達可能な元というものを考えることができて初めて与えられる、というこ とである。つまり、A ⊃ A を構成する構文論的部分 (すなわち部分論理式) の意味内容は、S4 フレームの Kripke モデルによる意味論によっては孤立的には考えることができない ( すなわち当の部分論理式を取り巻く周囲の構文 的組成の在り方を考慮しないことには考えることができない) と言うことができよう。

ここまででは具体的な論理式 A ⊃ A を例として考えたが、上の S4 フレームの Kripke モデルによる意味論の定 義からして、直観主義論理で証明可能なある論理式を考えたとき、その部分論理式の意味内容は一般的に孤立的に 与えることができない、ということがわかる。そしてこのことは同時に、次のことを意味するであろう。それは、

直観主義論理で証明可能な論理式は、その文法的構成の過程 ( いわゆる文形成史 ) に現れる論理式たちがどのよう

な構成手続きの依存関係についての意味内容、すなわち操作的意味内容を持っているのかということを S4 フレー

ムの Kripke モデルによる意味論は明らかにしている、ということである。

「ある論理で証明可能な論理式の操作的意味内容をモデル論的意味論が解明する」ということで本論が想定し ているのは、以上で見た直観主義論理に対する S4 フレームのクリプキモデルによる意味論に認められるような、

論理式の構成手続きの依存関係についての意味内容がモデル論的意味論のモデルという集合と写像から成る道具 立てによって明らかとなる、ということである。

1.2 古典論理の真理値モデルによる意味論

さて以上を踏まえた上で、古典論理の意味論のひとつとして知られる真理値モデルによる意味論が、直観主義 論理に対しての S4 フレームの Kripke モデルによる意味論の関係とは対照的に、論理式の操作的意味内容の解明 を果たしていない、という議論を以下で試みる。

まず古典論理の真理値モデルによる意味論とはどのようなものかを確認する。定義は次の通りである。

• 真理値モデルによる意味論の定義：

– 2 元集合 T 、付値関数 V の組 M = 〈 T , V 〉をモデルとし、これを真理値モデルと呼ぶ。ただし、

∗ T = { true, f alse }

∗ V = P −→ T

· ただし P は命題記号全体の集合を表している。

· なお、 V ( ⋎ ) = trueb ∧V ( ⋏ ) = f alse

– ある真理値モデル M

について論理式 D が成り立つこと M

| = D の定義：

∗ D が命題記号のとき、

M

| = D ⇔ V (D) = true

∗ D が A ∧ B という形のとき、

M

| = D ⇔ M

| = Ab ∧M

| = B

∗ D が A ∨ B という形のとき、

M

| = D ⇔ M

| = Ab ∨M

| = B

∗ D が A ⊃ B という形のとき、

M

| = D ⇔ b ¬M

| = Ab ∨M

| = B

∗ D が ¬ A という形のとき、

M

| = D ⇔ b ¬M

| = A – 真理条件の定義：

古典論理で論理式 D が証明可能 ⇔ 任意の M について、 M | = D

では先ほどと同様にして、この真理値モデルによる意味論により古典論理で証明可能な論理式は具体的にはどの ように解釈されるかを見てみる。比較のために同じ論理式の例 A ⊃ A を考えよう。定義により次のことがわかる。

  古典論理で論理式 A ⊃ A が証明可能

⇔ 任意の M について、 M | = A ⊃ A

⇔ 任意の M について、 ¬M | b = Ab ∨M | = A

⇔ 任意の M について、 ¬V b (A) = trueb ∨V (A) = true

なるほど古典論理で証明可能な論理式 A ⊃ A の意味内容とは、「どのような真理値モデル M を考えようとも、A の付値が true でないか、または、A の付値が true であるか、のいずれかである」というものだとわかる。

さて S4 フレームの Kripke モデルによる意味論での直観主義論理で証明可能な論理式 A ⊃ A の解釈のときと

今回を比較すると、次のことがわかる。それは、直観主義論理の解釈の際に考慮しなければならなかったような、

A ⊃ A の諸部分論理式間の文法的構成上の依存関係を示すような意味内容すなわち操作的意味内容が認められな いということである。具体的には、A ⊃ A の部分論理式のうち条件節の A と帰結節の A の意味内容は、先の直 観主義論理の場合には A ⊃ A が成り立つ W の元が与えられることを待たねば考えることができなかった一方で、

しかしこの古典論理の場合には A ⊃ A の成立の仕方に関わるような情報 (すなわち命題の成立に伴う様相概念

) が与えられることを待たずとも孤立的に考えることができる、ということである。そしてこのことは上の真理値 モデルによる意味論の定義からして、古典論理で証明可能な論理式の解釈一般に成り立つことであるとわかる。

つまり古典論理で証明可能な論理式に意味内容を与える真理値モデルによる意味論は、ある論理式の諸部分論 理式に対してそれらの間の構成手続き上の連関や依存関係という操作的意味内容を与える道具立てを持っていな いと考えられるのである。

さてしかし、こうした真理値モデルによる意味論が帯びている特徴である言わば「命題の成立に伴う様相概念・

操作的意味内容の欠落」という事情は、真理値モデルによる意味論に固有の問題なのではないだろうか。結論か ら先に言えば、実はそうではないのである。次節ではこのことを論じる。

1.3 古典論理の S5 フレームの Kripke モデルによる意味論

古典論理の意味論として、真理値モデルによる意味論の他に、S5 フレームの Kripke モデルによる意味論が知 られている。名前からも類推できるように、この意味論は、先の S4 フレームの Kripke モデルの F

を F

で置 き換えて得られる意味論である。ただし、 F

とは集合 W 、到達可能関係 R の組〈 W , R 〉であり、特にこの R は反射性と推移性とさらに対称性という 3 つの条件を満たす W 上の 2 項関係である。 M

, w

| = D の定義および 真理条件の定義の仕方は、S4 フレームの Kripke モデルによる直観主義論理の意味論と全く同じである。

さてこれまでと同様にして、この S5 フレームの Kripke モデルによる意味論により古典論理で証明可能な論理 式は具体的にはどのように解釈されるかを見てみる。再び A ⊃ A を取り上げよう。定義により次のことがわかる。

  古典論理で論理式A⊃Aが証明可能

⇔ 任意のMについて、b∀wx(M, wx|=A⊃A)

⇔ 任意のMについて、b∀wx(b∀wy(wxRwy⊃b(b¬M, wy|=Ab∨M, wy|=A)))

⇔ 任意のMについて、b∀w_x(b∀w_y(w_xRw_y⊃b(b¬b∀w_z(w_yRw_z⊃Vb (w_z, A) =true)b∨b∀w_v(w_yRw_v⊃Vb (w_v, A) =true))))

さて一見するとこの結果からは、真理値モデルによる意味論と比べて古典論理の論理式 A ⊃ A の意味内容は、

この意味論のもとでは豊かな操作的意味内容が与えられているかのように思われる。しかし、注意しなければな らないのは、S4 フレームの Kripke モデルの R の条件にはなく、S5 フレームの Kripke モデルの R の条件におい て新たに加わった、対称性という条件である。 W 上の関係 R は反射性・推移性・対称性を満たすので、同値関係 である。このことは次のことを意味することに注意されたい。それは、 W を R により分割して得られる各同値類 ごとの各命題記号の付値は同値類の元の間ですべて同一になってしまうということである。そしてこれはすなわ ち、上の S5 フレームの Kripke モデルによる意味論によって論理式 A ⊃ A に与えられた意味内容に現れる R が、

諸部分論理式間の文法的構成過程上の依存関係を表す機能を実質的には担っていないということを意味する。つ まり、w

と w

と w

と w

はすべて同じ W の元だと考えることが許されてしまうのだ。そうするとこの状況は 先の真理値モデルによる意味論の状況と区別がなくなってしまう。

古典論理の真理値モデルによる意味論が「命題の成立に伴う様相概念・操作的意味内容の欠落」という特徴を 帯びるのは、真理値モデルによる意味論に固有の事情ではないのだ。

1.4 古典論理とモデル論的意味論の間の事情

さて以上の議論から言えることは、古典論理は直観主義論理に比して証明可能な論理式に操作的意味内容を与 えるようなモデル論的意味論を考えにくいという傾向性を持っているということであって、当然ながらこのこと

1)この様相概念とは何なのかという問い、すなわちより具体的にはS4フレームのKripkeモデルの集合Wやその集合上の到達関係Rと は何なのかという問いも考察されねばならない問題である。しかしここでは古典論理の意味論である真理値モデルによる意味論には、この概念 が現れないということだけが問題であるので、本論文ではこの概念についてはこのような問題がある、ということを付言するだけにとどめる。

は古典論理で証明可能な論理式に操作的意味内容を与えるようなモデル論的意味論は考えられないということを 意味しない。しかしながら前節で見た、様相的・操作的概念を論理式に隠伏的に同伴させる Kripke モデルの道具 立てが古典論理の意味論を考えるとなると、その機能が実質的に失われてしまうという事実は、モデル論的意味 論による操作的意味内容の解明という企てに対して古典論理が一定程度の受け付け難さを持っているということ を示唆している、と考えることは正当であろう。

では、果たしてなぜ古典論理は、モデル論的意味論によって証明可能な論理式の操作的意味内容をうまく解明 することができないという特徴・傾向性を持っているのか？これが本論文の主たる問いである。以降ではこの問 いに答えることを目指す。

この問いに答えるために、まず論理の理解のための視点の一つとして知られる計算論と呼ばれる立場から古典

論理を特異的に特徴づけることができるある論理学的事実を紹介し、そしてまさにこの論理学的事実が上述の古

典論理とモデル論的意味論の間の事情を引き起こしていると考えることができる、ということを論じる。ここで

の計算論とは、 Gentzen により考案されたある構文論の形式化の方法を前提とし、そこで考えられる形式表現上

の論理的冗長さ (「証明の回り道」と呼ばれる) を含むような証明について、その冗長さの当の証明からの解消と

いうことを考えた際に様々に問題となる (その解消手続きの仕方等々の) 構文論的構造を研究する論理学の一領域

のことである。以降ではこの計算論の立場から、古典論理の意味論としてモデル論的意味論が有効に働かないと

いう傾向性が認められることの原因究明を試みる。先を急げば、古典論理を特異的に特徴づけることができるあ

る計算論的・論理学的事実とは、証明の回り道を含む導出過程を持つ論理式については、その回り道を解消する

手続きが非決定的な計算と考えることができる、という事実である。次章ではこのことを、順を追った諸概念の

準備的説明と歴史的経緯の説明を踏まえて詳しく解説し、最後にこの事実が本論文の主たる問いに対してどのよ

うにして結びつき、そして答えを提供するものであるかということを論じる。

2 問題解決：古典論理と計算論

本章では、古典論理の意味論としてモデル論的意味論が有効に働かないという傾向性が認められることの原因 を、近年の計算論の研究において示された古典論理を特徴づけるある論理学的事実が解明している、という考察 を行うことを試みる。

2.1 Gentzen の形式体系と証明の回り道の解消、および計算論的議論の方法

まず、ある論理についての計算論的興味やその議論というものが具体的にはどのようなものであるのかというこ とを本節にて説明する。すでに第 1 章の最後で触れたように、計算論は Gentzen による構文論の形式化の仕方を 前提とした構文論的議論である。ちなみに構文論の形式化の方法は様々な手法が考案されているが、何故 Gentzen による形式体系が特に計算論という領域で前提となるかと言えば、それは Gentzen の形式体系が次のような特徴 を備えているからである。その特徴とは、ある論理の構文論ということで主として考えられる証明可能性の判定 法の形式化等の基本的性質のみならず、論理式導出の過程における論理的冗長さすなわち「証明の回り道」のあ り方や有無についての表現能力を備えており、さらにはその「証明の回り道」の解消に関する手続きの適用方法 等に関する数学的議論を成り立たせるような表現上の道具立てを備えている、という特徴である。以下本節では、

まずこの Gentzen の形式体系がどのようなものであるのかということを確認し、次いでこの形式体系において表

現される「証明の回り道」とはどのようなものであるのか、そしてこの「証明の回り道」が解消されるとはどの ようなことであるのか、さらにこの「証明の回り道」の解消に関わる計算論的議論とはどのようなものであるの かを解説する。

2.1.1 Gentzen

N J・N K、LK・LJ

Gentzen の論文 [5] において、構文論の形式化の手法として 2 つの方法が考案された。ひとつは自然演繹と呼ば

れ、もうひとつは sequent 計算と呼ばれる。そして [5] では、直観主義一階述語論理の形式体系と古典一階述語論 理の形式体系が、それら手法によりそれぞれ 2 つずつ定義された。自然演繹による直観主義一階述語論理の形式 体系は N J 、自然演繹による古典一階述語論理の形式体系は N K、sequent 計算による古典一階述語論理の形式体

系は LK 、 sequent 計算による直観主義一階述語論理の形式体系は LJ と呼ばれ、この順で定義された。命題論理

の範囲での N J・N K 、LK・LJ の定義は次の通りである。

1. N J ・N K の定義：

• 準備：

– 自然演繹の推論規則は

A

… A

B (if)

という形の図式で表わされる。 A

, ..., A

は仮定となる論理式を、 B は推論規則 if によって仮定か ら導かれた結論となる論理式を表している。

– 開いた仮定 D

, ..., D

から結論 E に至る自然演繹の証明図を次で定義する。

(a) ちょうど 1 個の論理式 E のみからなる図式は、開いた仮定 E から結論 E に至る自然演繹の証 明図である。

(b) π

が開いた仮定 D

, ..., D

から結論 E

に至る自然演繹の証明図であり、…、π

が開いた 仮定 D

, ..., D

から結論 E

に至る自然演繹の証明図であり、

E

… E

E (if) が仮定が n 個の推論規則であるとき、次の図式

π

… π

E (if)

は開いた仮定 D

, ..., D

から結論 E に至る自然演繹の証明図である。

(c) 以上の操作を有限回繰り返して得られる図式のみが開いた仮定 D

, ..., D

から結論 E に至る自 然演繹の証明図である。

• N J の定義：

– 推論規則：

A ∧ B

A ( ∧ -E) A ∧ B

B ( ∧ -E) A B A ∧ B ( ∧ -I)

A

A ∨ B ( ∨ -I) B

A ∨ B ( ∨ -I) A ∨ B [A] ..

..

C [B] ..

..

C C ( ∨ -E)

A ⊃ B A B ( ⊃ -E)

[A] ..

..

B

A ⊃ B ( ⊃ -I) [A] ..

⋏ ..

¬ A ( ¬ -I) ¬ A A

⋏ ( ¬ -E) ⋏ D ( ⋏ ) ここで、

∗ 各図式の右側に、その推論規則の名前が括弧書きで示されている。

∗ 図式中に現れる

D ..

..

E

という形の表現は、開いた仮定 D から結論 E に至る自然演繹の証明図を表している。

∗ ( ∨ -E) および ( ⊃ -I) および ( ¬ -I) について、 「[」 「]」という形の記号によって括られた論理式は、

その規則の結論を導く開いた仮定からその形の論理式を任意有限個除外して考えてよい、とい うことを表している。ただし ( ∨ -E) における仮定 A の除外は、開いた仮定 A から結論 C に至 る自然演繹の証明図の範囲に限定して考慮するものとする。 ( ∨ -E) の B についても同様。

∗ ( ⊃ -I) について、A で表された論理式は、結論 B に至る自然演繹の証明図の開いた仮定に現れ ない論理式であってもよい。

• N J - 証明図の定義：出現する推論規則がどれも N J の推論規則であるような、 0 個の開いた仮定から結 論 A に至る自然演繹の証明図のことを、A に至る N J-証明図と呼ぶ。

• 直観主義論理で証明可能な論理式の定義：ある論理式 A について、

A が直観主義論理で証明可能な論理式である。 ⇔ A に至る N J -証明図が存在する。

• N K の定義：

– 推論規則：

N J の推論規則にさらに次の推論規則

¬¬ A

A ( ¬¬ -E) を加えて得られるものである。

• N K -証明図の定義：出現する推論規則がどれも N K の推論規則であるような、0 個の開いた仮定から

結論 A に至る自然演繹の証明図のことを、 A に至る N K- 証明図と呼ぶ。

• 古典論理で証明可能な論理式の定義：ある論理式 A について、

A が古典で証明可能な論理式である。 ⇔ A に至る N K-証明図が存在する。

2. LK・LJ の定義：

• 準備：

– sequent の定義：

「A

, ..., A

」と「B

, ..., B

」がそれぞれ論理式をカンマ「,」で」区切った列 (空列含む) である とき、文字列「A

, ..., A

→ B

, ..., B

」(ただし m ≥ 0, n ≥ 0) を sequent と呼ぶ。

なお、 sequent A

, ..., A

→ B

, ..., B

において、補助記号 → よりも左側にある論理式の列 A

, ..., A

をその sequent の前件と呼び、また補助記号 → よりも左側にある論理式の列 B

, ..., B

をその sequent の後件と呼ぶ。

– sequent 計算の推論規則は S

S (if)

または

S

S

S (if

)

という形の図式で表わされる。 S

と S

は前提となる sequent を、 S は推論規則 if(または if

) に よって前提から導かれた帰結となる sequent を表している。なお、推論規則を表す図式の横棒の上

にある sequent のことをその推論規則の上式と呼び、その横棒の下にある sequent のことをその推

論規則の下式と呼ぶ。また、上式が 2 個ある推論規則について、左側の上式のことを左上式、右側 の上式のことを右上式と呼ぶ。

– 始式 S

, ..., S

から終式 S に至る sequent 計算の証明図を次で定義する。

(a) ちょうど 1 個の sequent S のみからなる図式は、始式 S から終式 S に至る sequent 計算の証明 図である。

(b) π

が始式 S

, ..., S

から終式 S

に至る sequent 計算の証明図であり、

S

S (if

) が上式が 1 個の推論規則であるとき、次の図式

π

S (if

)

は始式 S

, ..., S

から終式 S に至る sequent 計算の証明図である。

(c) π

が始式 S

, ..., S

から終式 S

に至る sequent 計算の証明図であり、 π

が始式 S

, ..., S

から終式 S

に至る sequent 計算の証明図であり、

S

S

S (if

) が上式が 2 個の推論規則であるとき、次の図式

π

π

S (if

)

は始式 S

, ..., S

から終式 S に至る sequent 計算の証明図である。

(d) 以上の操作を有限回繰り返して得られる図式のみが始式 S

, ..., S

から終式 S に至る sequent 計算の証明図である。

– D-sequent の定義：

sequent を、始式 S

, ..., S

から終式 S に至る sequent 計算の証明図において現れる位置により区 別するとき、その sequent を D-sequent と呼ぶ。

2)sequentA1, ...,Am→B1, ...,Bnは、論理式たちA1, ...,Amのすべてが仮定されたとき、論理式たちB1, ...,Bnのうち少なくとも1 つの論理式が結論として導かれるということを表している。

– path の定義：

始式 S

, ..., S

から終式 S に至る sequent 計算の証明図 π の D-sequent の列 Γ

→ Θ

, ..., Γ

→ Θ

において、各 n(ただし 1 ≤ n < m) に対し、Γ

→ Θ

が Γ

→ Θ

を下式とする推論規則 の上式のひとつであり、かつ Γ

→ Θ

が始式であり、また Γ

→ Θ

が終式であるとき、その D-sequent の列 Γ

→ Θ

, ..., Γ

→ Θ

は π における path であるという。

– 部分証明図の定義：

始式 S

, ..., S

から終式 S

に至る sequent 計算の証明図 π

が始式 S

, ..., S

から終式 S に至る

sequent 計算の証明図の部分証明図であるという関係を π の構成に関する帰納法により次のように

定義する。

(a) π がちょうど 1 個の sequent の出現のみからなるとき、 π

は π 自身。

(b) π が

π

S (if

)

という形のとき、π

は π 自身、または、π

の部分証明図のひとつ。

(c) π が

π

π

S (if

)

という形のとき、 π

は π 自身、または、 π

の部分証明図のひとつ、または、 π

の部分証明図 のひとつ。

• LK の定義：

– 公理：

A → A – 推論規則：

∗ 構造に関する推論規則：

Γ → Θ

D, Γ → Θ (w → ) Γ → Θ

Γ → Θ, D ( → w)

∆, D, E, Γ → Θ

∆, E, D, Γ → Θ (ex → ) Γ → Θ, E, D, Λ

Γ → Θ, D, E, Λ ( → ex) D, D, Γ → Θ

D, Γ → Θ (c → ) Γ → Θ, D, D Γ → Θ, D ( → c) Γ → Θ ∆ → Λ

Γ, ∆

→ Θ

, Λ (cut： D)

∗ 論理記号に関する推論規則：

A, Γ → Θ

A ∧ B, Γ → Θ ( ∧ → ) Γ → Θ, B

Γ → Θ, A ∨ B ( → ∨ )

B, Γ → Θ

A ∧ B, Γ → Θ ( ∧ → ) Γ → Θ, A

Γ → Θ, A ∨ B ( → ∨ ) A, Γ → Θ B, Γ → Θ

A ∨ B, Γ → Θ ( ∨ → ) Γ → Θ, A Γ → Θ, B Γ → Θ, A ∧ B ( → ∧ ) Γ → Θ, A

¬ A, Γ → Θ ( ¬ → ) A, Γ → Θ

Γ → Θ, ¬ A ( → ¬ )

Γ → Θ, A B, ∆ → Λ

A ⊃ B, Γ, ∆ → Θ, Λ ( ⊃→ ) A, Γ → Θ, B

Γ → Θ, A ⊃ B ( →⊃ ) ここで、

· 各図式の右側に、その推論規則の名前が括弧書きで示されている。

· 大文字のギリシア文字は、それぞれ 0 個を含む任意有限個の論理式の列を表している。

· cut について、Θ は論理式 D が 1 個以上出現する論理式の列であり、Θ

は Θ から D の出現 をすべて除いて得られる論理式の列である。 Λ と Λ

についても同様。また、 Θ および Λ か ら除かれる論理式 D を cut formula と呼ぶ。cut のあるインスタンスの cut formula をその cut の名前の隣に示す。

· 論理記号に関する推論規則の適用において、下式で新たに出現する論理式のことを principal formula と呼ぶ。

• LK- 証明図の定義：始式のどれもが LK の公理であり、かつ出現する推論規則がどれも LK の推論規 則であるような、始式 S

, ..., S

から終式 S に至る sequent 計算の証明図のことを、 S を終式とする LK-証明図と呼ぶ。

• 古典論理で証明可能な論理式の定義：ある論理式 A について、

A が古典論理で証明可能な論理式である。 ⇔→ A を終式とする LK-証明図が存在する。

• LJ の定義：LK の定義について、そこで sequent に関する定義を後件に現れる論理式の個数を高々1 個に制限して得られるものである。

• LJ -証明図の定義：始式のどれもが LJ の公理であり、かつ出現する推論規則がどれも LJ の推論規則

であるような、始式 S

, ..., S

から終式 S に至る sequent 計算の証明図のことを、 S を終式とする

LJ -証明図と呼ぶ。

• 直観主義論理で証明可能な論理式の定義：ある論理式 A について、

A が直観主義論理で証明可能な論理式である。 ⇔→ A を終式とする LJ -証明図が存在する。

2.1.2

ではこれらの体系で表現される証明の回り道とはどのようなものなのであるのかを説明する。

しかし一旦その前に、何故 2 通りの形式化が行われているのかの説明を行う。その経緯は次のとおりである。

Gentzen ははじめ自然演繹によって直観主義論理と古典論理の形式体系を与えた。しかし、証明の回り道の解消と

いう問題を考えたとき、自然演繹はそこで現れる証明の回り道がその解消手続きを与えるのに都合の悪い形式体系 だということに Gentzen は気が付き、証明の回り道の解消のためにより都合の良いような形式体系として sequent 計算を考案したのである。[5] の Page 177 では次のように述べられている。なお以下の Hauptsatz とは、証明の回 り道の解消を意味する定理のことのことを指している。

3)なお[5]では、cutの定義ははじめ、

Γ→Θ,D D,∆→Λ

Γ,∆→Θ,Λ (cut：D)

の形で与えられた。そしてそのすぐ後にcut除去定理の証明のために、mixと呼ばれる本論文のcutをした推論規則が定義され、そして、

.. .. Π→Σ,D

.. .. D,Ψ→Ω

Π,Ψ→Σ,Ω (cut:D) という形に対する

.. .. Π→Σ,D

.. .. D,Ψ→Ω

Π,Ψ^∗→Σ^∗,Ω (mix:D)

Π,Ψ→Σ,Ω (w→)s/(ex→)s/(→w)s/(→ex)s

という置き換え操作を施したのち、このmixを除去する手続きを定義することによってcut除去定理が証明された。本論文では説明の便宜 上、はじめからLKのcutの定義を[5]のmixの形で与えている。

Um ihn(=Hauptsatz) in bequemer Form aussprechen und beweisen zu k¨ onnen, mußte ich einen besonders daf¨ ur passenden logischen Kalk¨ ul zugrunde legen. Hierzu erwies sich der nat¨ urliche Kalk¨ ul nicht als geeignet.

Hauptsatz を適切な形で表現しかつ証明できるようにするためには、私は特にこの目的に見合ったあ

る形式体系を考えなければならなかった。この目的のためには自然演繹は適切ではなかった。 ( 拙訳 )

• 原文中の表現「(=Hauptsatz)」は訳者が補ったものである。

ともあれ、ひとまず自然演繹体系において証明の回り道とその解消とは具体的にどのようなものであるのかを 見てみよう。例えば、論理式 A ⊃ A を終式とする N J- 証明図として次のものを考えよう。

[A…☆]

A ⊃ A ( ⊃ -I) [A]

A…★ ( ⊃ -E)

A ⊃ A ( ⊃ -I)

このとき、上の N J-証明図において☆以上の証明図と★以上の証明図はともに仮定 A から結論 A に至る証明図で あることがわかる。すなわち、推論規則の適用の仕方に冗長性があることが認められる。証明の回り道とは、自 然演繹体系では、こうした証明図が含み得る推論規則の適用の仕方の冗長さのことを指す。ここで、★以上の証 明図を☆以上の証明図で置き換えることにより、冗長性のない次のような N J - 証明図を得ることができる。

[A]

A ⊃ A ( ⊃ -I)

こうした推論規則の適用の冗長さを解消する手続きが自然演繹体系における証明の回り道の解消である。なお、証 明の回り道を 1 個以上含む自然演繹の証明図に対し、上のような解消手続きを有限回繰り返すことによって最終 的に回り道のない証明図を得る操作のことを、証明図の正規化と呼ぶ。そして証明図の正規化によって得られる 回り道のない証明図のことを正規な証明図と呼ぶ。上の例では証明の回り道は 1 箇所だけであり、そして 1 回の 解消手続きによって正規な証明図が得られたが、2 個以上の証明の回り道を含む証明図を考えることもできるし、

さらには回り道の解消手続きのやり方次第では回り道の数がその解消手続きを行う前よりもさらに増えてしまう ことさえありうる。そしてさらに、上の例では同じ論理記号 ⊃ の導入則と除去則が隙間なく連続的に出現したこ とで回り道がどこに生じているのかがすぐに判明したが、実は自然演繹の回り道のすべてがこの形によって現れ るとは限らない。たとえば、

[( ¬ A ∨ B) ∧ A]

¬ A ∨ B ( ∧ -E)

[ ¬ A] [A]

⋏ ( ¬ -E) B ( ⋏ )

A ⊃ B ( ⊃ -I) [B]

A ⊃ B ( ⊃ -I)

A ⊃ B ( ∨ -E) [( ¬ A ∨ B) ∧ A]

A ( ∧ -E)

B ( ⊃ -E)

(( ¬ A ∨ B) ∧ A) ⊃ B ( ⊃ -I)

という形の N J-証明図 (以下 π

と呼ぶ) は同じ論理記号についての導入則と除去則が隙間なく連続的に出現する 箇所が見当たらないために一見すると正規な証明図であるかのように思われるが、実は回り道を含んでいる。次 のような正規な証明図 π

が存在する。

[( ¬ A ∨ B) ∧ A]

¬ A ∨ B ( ∧ -E) [ ¬ A]

[( ¬ A ∨ B) ∧ A]

A ( ∧ -E)

⋏ ( ¬ -E) B ( ⋏ )

[B]

B ( ∨ -E)

(( ¬ A ∨ B) ∧ A) ⊃ B ( ⊃ -I)

詳しく見てみると、π

で出現する論理式は ( ⋏ を除いて) そのすべてが終式の部分論理式であるのに対して、π

で

は ( ⋏ 以外に ) 終式の部分論理式ではない論理式 A ⊃ B が出現していることがわかる。この π

が満たすような、

「ある証明図で出現する論理式のうち ⋏ を除くすべての論理式が終式の部分論理式である」という証明図が持ち得 る性質は、部分論理式特性と呼ばれる。回り道のない自然演繹の証明図を得るためには、同じ論理記号について の導入則と除去則が隙間なく連続的に出現する箇所をすべてなくすだけでは不足で、さらに証明図が部分論理式 特性を満たすようにして証明図を変形しなければならない。このように自然演繹の回り道の解消は一筋縄ではい かないのだ。なお本論文以降では、ある自然演繹の証明図について「論理記号 ＊ についての導入則と除去則が隙 間なく連続的に出現する箇所を 1 箇所なくすこと」を ＊ に関する簡約と呼び (ただし ＊ は任意の論理記号を表し ている ) 、簡約可能な箇所を持たない自然演繹の証明図のことを正規な証明図、簡約可能な箇所を持たずかつ部分 論理式特性を満たす自然演繹の証明図のことを完全に正規な証明図と呼ぶことにする。π

は正規な証明図ではあ るが、完全に正規な証明図ではない。また本論文では、簡約可能な箇所を持つ証明図から正規な証明図を得る操 作のことを証明図の正規化と呼び、部分論理式特性を満たさない証明図から完全に正規な証明図を得る操作のこ とを証明図の完全正規化と呼ぶことにする。

このような自然演繹体系の事情を踏まえた上で、 sequent 計算での証明の回り道とその解消手続きを見てみよう。

実は sequent 計算では、(自然演繹においてそもそも回り道がどこに発生しているのかを特定することが難しいの

と対照的に) 証明の回り道を含む証明とはただ推論規則 cut を含む証明図に他ならない。そして sequent 計算にお いて証明の回り道の解消とは、cut を含む証明図から同じ終式で cut を用いない証明図を得る操作にあたる。なお 本論文では、cut を含む sequent 計算の証明図から同じ終式で cut を用いない sequent 計算の証明図を得る操作の

ことを sequent 計算の証明図の正規化と呼ぶ。そして sequent 計算の証明図の正規化によって得られる cut を含ま

ない証明図のことを正規な sequent 計算の証明図と呼ぶ。例えば sequent → A ⊃ A を終式とする LJ -証明図とし て次のものを考えよう。

A → A

A, A → A (w → )

A → A ⊃ A ( →⊃ ) A → A A → A A ⊃ A, A → A ( ⊃→ )

A, A → A (cut：A ⊃ A)

A → A (c → )

→ A ⊃ A ( →⊃ )

さてこの証明図の終式を下式とする推論規則 ( →⊃ ) の上式は、公理の形をしていることがわかる。したがって、次 の LJ - 証明図を考えれば cut のない証明図が得られる。

A → A

→ A ⊃ A ( →⊃ )

しかしながらこの回り道の解消方法は、与えられた証明図が特定の推論規則の下式に公理の形の sequent がたまた ま出現するようなものであったために上手くいったに過ぎない。一般的に、cut を 1 個以上含む任意の証明図が与 えられた時に、同じ終式で cut を含まないような証明図を得ることはできるだろうか？この問いに対する肯定的解 答が [5] の cut 除去定理により与えられた。cut 除去定理とは、推論規則 cut を除いても体系で証明可能な式の範 囲は変わらないということを示す定理である。同論文においてこの定理は、cut を含む任意の LK(または LJ )-証 明図が与えられたとき、同じ終式で cut を含まないような LK( または LJ )- 証明図を構成する手続きを具体的に定 義することによって証明された。次でこの証明の概要を説明する。

2.1.3 Gentzen

cut

[5] での cut 除去定理の証明の概要を説明する。

cut を 1 個以上含むような任意の LK(または LJ )-証明図 π が与えられた時、その π から cut を含まない証明図 を具体的に構成する操作は、次の手順によって行われる。

1. π の部分証明図のうち、cut の下式を終式とし、かつ cut がちょうど 1 個しか出現しないような部分証明図 のひとつ π

に注目する。

2. 次の定理 (ここでは Hauptsatz の補題と呼ぶこととする) により、π

に対して (π

)

を得る。

3. π の π

を (π

)

で置き換える。