2012年8月19日に記した当日記の項目 'Who Was the First to Formulate Comprehension Principles as an Axiom?' において、Comprehension Principle が最初に axiom として立てられたのは、いつ、どこでのことだったのか、そのことを調べた結果をそこで掲載しました。その暫定的な答えは、1910年の Principia Mathematica, vol. 1 における the axiom of reducibility であろう、というものでした*1。今日はそのことについて、2点、補足します。なお、以下では、本来、引用符を付すべきところで、読みやすさを考慮して、しばしば引用符を省いています。また、私は間違っていたり、無理解を示していることがよくありますので、下記の事柄について、初めから正しいものと思って読まないようにしてください。前もって存在するはずの間違いに対し、お詫び申し上げます。
(1)
まず、今述べた the axiom of reducibility が最初に現われたのは、1910年の Principia Mathematica, vol. 1 ではありませんでしたので、訂正します。この公理は既に1908年には世に現われています。次の1908年刊行の論文にこの公理が出てきます。
- Bertrand Russell ''Mathematical Logic as Based on the Theory of Types,'' in his Logic and Knowledge, Robert Charles Marsh ed., Routledge, 1956/1992, p. 87, and the same paper in Jean van Heijenoort ed., From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, 1967/1976, p. 171.
この論文よりも前に the axiom of reducibility が出てくる刊行文献があるかもしれませんが、そこまではまだ調べが付いていません。刊行文献とは別に、Russell の手稿のうちに、この公理がいつごろ出てくるのかも調べていません。とにかくこの公理が刊行された文献に出てくるのは1910年よりも前の1908年以前だということです。
(2)
Comprehension Principle に関連した注目すべき定理として、次の式が Principia に出てきます。この式について、以下で comment します。ただし、何か結論のようなものがあるのかというと、それはありません。何気なく脳裏に浮かんだ瑣事を記しただけです。私は論理学についても Russell についてもよく知りませんので、以下の話には間違いが含まれているはずです。充分ご注意ください。
*20･3. ⊢ : x ε (ψz) .≡. ψx
この定理は、以下の箇所で出てきます。
- Alfred North Whitehead and Bertrand Russell Principia Mathematica to *56, Cambridge University Press, Cambridge Mathematical Library, 1997, pp. 189, 193, 188.
また、次にも出てきます。
- Bertrand Russell ''Mathematical Logic as Based on the Theory of Types,'' in his Logic and Knowledge, Robert Charles Marsh ed., Routledge, 1956/1992, p. 90, and the same paper in Jean van Heijenoort ed., From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, 1967/1976, p. 173. This paper was first published in 1908.
さて、
*20･3. ⊢ : x ε (ψz) .≡. ψx
につきまして、この式と Comprehension Principle との関係を述べ、その後、この式と the axiom of reducibility との関係を述べます。
まずこの式を現代に近い記法で書き換えてみます。Turnstile は省きます。x は、一応は任意のものを表しているので、とりあえずそのまま普遍量化しておきます。
*20･3'. (∀x) ( ( x ∈ { z |ψz } ) ≡ ψx )
この定理は ( class に関する) Comprehension Principle にかなり近い形をしています。( class に関する) Comprehension Principle を掲げてみます。
Unrestricted / Impredicative Comprehension Principle Concerning Classes:
UCPC (∃C) (∀x) ( ( x ∈ C ) ≡ ψx )
C は class, ∈ は membership relation.
今述べた *20･3' と UCPC を比べると、*20･3' の { z |ψz } を C に代えて、それを存在汎化するだけで *20･3' は UCPC になることがわかります。
ただ、*20･3 と *20･3' の x は、先に「一応は任意」と言ったように、本当のところは、まったくの任意という訳ではありません。The theory of types の枠内に *20･3 と *20･3' はありますので、実際には、ある特定の type を持っている任意の x ということです。すべての type を通じた任意の x, あるいは、type の区別を一切無視したあらゆる x ということではありません。つまり、*20･3 と *20･3' はunrestricted / impredicative な式ではなく、restricted / predicative な式になっていて、UCPC のような unrestricted / impredicative な式ではありません。
また、*20･3 の (ψz) と *20･3' の { z |ψz } は、一応、class の名前であるかのように振る舞うものと見なされていますが、もちろん、実際には class の名前ではありません。と言うのも、Russell にとって class は存在しないとされているので*2、
(ψz) と { z |ψz } は何かの名前でも何でもなく、それらはいわゆる不完全記号 (incomplete symbols) として厳密には文脈的に定義されて削除、解消されてしまうものです。ですから、それらは何か個体のようなものの名前ではありません*3。ところで *20･3 も *20･3' も定理なので真です。そのため、*20･3 と *20･3' に名前が含まれていれば、それを存在汎化してよく、その結果も真になります。しかし、*20･3 と *20･3' に含まれている
(ψz) と { z |ψz } は、今述べたように、どちらも個体などの名前ではないので存在汎化できません。したがって、*20･3 と *20･3' を UCPC に書き換えることはできません。
このように、そのままでは *20･3 と *20･3' は、( class に関する) Unrestricted / Impredicative Comprehension Principle ではありません。しかし *20･3 と *20･3' の (ψz) と { z |ψz } を、class という個体を表す名前だと認めさえすれば、すぐさま *20･3 と *20･3' は ( class に関する) Unrestricted / Impredicative Comprehension Principle になります。
今、class を個体とし、 (ψz) と { z |ψz } が class の名前だとします。すると *20･3 と *20･3' の
(ψz) と { z |ψz } を存在汎化することができて、結局できあがった式は UCPC と同じ形になり、結果は真となります。しかも、*20･3 と *20･3' に含まれる ε と ∈ の後には、the theory of types では個体の名前は来てはならないのに、今の場合、
(ψz) と { z |ψz } を個体の名前として ε と ∈ の後に意図的に置くことになります。ということは意図的に type の区別は守らない、type の区別はないものとしていることになります。つまり個体としての class の名前とされた
(ψz) と { z |ψz } を ε と ∈ の後に置くことは、
(ψz) と { z |ψz } が正真正銘の名前であるとともに、the theory of types を放棄することをいみします。このように、*20･3 と *20･3' の
(ψz) と { z |ψz } を、class という個体を表す名前だと認めるだけで、それらの名前の存在汎化が可能となり、結果は unrestricted / impredicative な式になる、ということです*4。
ですから、*20･3 と *20･3' を ( class に関する) Unrestricted / Impredicative Comprehension Principle とするかどうかは、class を個体として存在すると認めるかどうかにかかっています。ただし、Russell は class を個体として存在するものとは認めていませんし、認めないでしょう。今も述べました通り、それを認めれば、the theory of types が無に帰しますし、それだと Russell Paradox が復活してしまいます。そもそも Russell が Russell Paradox から学んだ教訓とは、一つには、Russell Paradox を解決するためには type の区別を設けねばならない、つまり the theory of types に頼らねばならないということに思い至ったことと、class は一般に思われているように個体などではないはずだ、ということに思い至ったことでした。他にも Russell が得た教訓はあったと思いますが、少なくとも今の話の脈絡では、以上の二つが Russell の得ていた重要な教訓だと考えられます。これら二つの教訓のうち、前者についてはよく知られていると思いますが、後者はひょっとすると、それほど知られてはいないかもしれません。(あるいは知らなかったのは、私だけなのかもしれませんが…。) この後者に関して、次の文章をご覧ください。長い引用ですが、とても興味深いので (少なくとも個人的にはとても印象深かったので) one paragraph 全体を引いてみます。特にこの paragraph 後半に出てくる 'There is no advantage in assuming that … ' 以下にご注意ください。
If mathematics is to be possible, it is absolutely necessary […] that we should have some method of making statements which will usually be equivalent to what we have in mind when we (inaccurately) speak of ''all properties of x.'' (A ''property of x'' may be defined as a propositional function satisfied by x.) Hence we must find, if possible, some method of reducing the order of a propositional function without affecting the truth or falsehood of its values. This seems to be what common-sense effects by the admission of classes. Given any propositional function ψx, of whatever order, this is assumed to be equivalent, for all values of x, to a statement of the form ''x belongs to the class α.'' Now assuming that there is such an entity as the class α, this statement is of the first order, since it involves no allusion to a variable function. Indeed its only practical advantage over the original statement ψx is that it is of the first order. There is no advantage in assuming that there really are such things as classes, and the contradiction about the classes which are not members of themselves shows that, if there are classes, they must be something radically different from individuals. It would seem that the sole purpose which classes serve, and one main reason which makes them linguistically convenient, is that they provide a method of reducing the order of a propositional function. We shall, therefore, not assume anything of what may seem to be involved in the common-sense admission of classes, except this, that every propositional function is equivalent, for all its values, to some predicative function of the same argument or arguments.*5
'[T]he contradiction about the classes which are not members of themselves shows that, if there are classes, they must be something radically different from individuals.'*6
「Russell Paradox による矛盾が示していることは、次のことである。すなわち、class があるとすれば、それは個体とは何か根本的に異なるものであるに違いない、これである。」
大胆な見解だと感じます。それに率直な気持ちが伝わってきます。個人的には大変印象に残る文章です。
さて、the theory of types を後々まで死守し*7、ここでの引用文にあるように、class は個体ではなく、そもそも class など本当のところは存在しないのだ、と考えていた Russell なら、*20･3 と *20･3' の (ψz) と { z |ψz } を、class という個体を表す名前だとは認めないでしょう。その結果、*20･3 と *20･3' は、( class に関する) Unrestricted / Impredicative Comprehension Principle によく似ていますが、しかし似てはいても厳密には異なるものとして、あり続けることになると思います。
ここまでで、*20･3 と ( class に関する) Unrestricted / Impredicative Comprehension Principle との関係は、大よそのところ、わかりました。では、Comprehension Principle と関連のある the axiom of reducibility は *20･3 と、いかなる関係にあるのでしょうか。それは問題の定理 *20･3 の証明を、Principia から引いてみるとわかります。この証明に眼を通すならば、定理 *20･3 が、the axiom of reducibility から出てくることが見て取れます。その証明を引用してみましょう。
*20･3. ⊢ : x ε
(ψz) .≡. ψx
Dem.
⊢ . *20･1 .⊃
⊢ :: x ε
[(*20･02)] ≡∴ (∃φ) ∴ ψy .≡y . φ! y : φ! x ∴
[*10･43] ≡∴ (∃φ) ∴ ψy .≡y . φ! y : ψx ∴
[*10･35] ≡∴ (∃φ) : ψy .≡y . φ! y ∴ ψx ∴
[*12･1] ≡∴ ψx :: ⊃ ⊢ . PropThis proposition shows that x is a member of the class determined by ψ when, and only when, x satisfies ψ*8.
この証明を、簡単に説明してみます。
Dem. と書かれた上記証明中、上から一行目の '*20･1' とは、ある定理の名前で、次がそれです。(Dem. は 'demonstration' の略です。)
*20･1 ⊢ ∴ f { (ψz) } .≡ : (∃φ) : φ! x .≡x . ψx : f { φ!
} [*4･2. (*20･01)]
この式の終わりにある '[*4･2. (*20･01)]' とは、以下の式を表しています。
*4･2 ⊢ . p ≡ p
*20･01 f { (ψz) } .= : (∃φ) : φ! x .≡x . ψx : f { φ!
} Df
'[*4･2. (*20･01)]' において、*20･01 が丸カッコに入っているのは、*20･01 が定義式であることを表しています。(丸カッコに入っていない *4･2 は、それが定理であることを表しています。)
先の *20･1 の終わりにある '[*4･2. (*20･01)]' は、それによって *20･1 が得られることを示しています。
例えば、*4･2 の p に *20･01 の左辺を入れます。
(%) ⊢ . f { (ψz) } ≡ f {
(ψz) }
そして例えば、この式 (%) の右辺は、定義式 *20･01 の右辺と等しいので、(%) の右辺を *20･01 の右辺と交換すると、求めようとしていた *20･1 ができます。
次に、上記証明中、一行目の '*20･1 .⊃' とは、まず定理 *20･1 を条件法の前件として取ります。次に *20･1 の f を x ε で置き換え、φ! x と ψx を入れ替え、入れ換えた ψx と φ! x の x を y に付け替えます。こうしてできた *20･1 の新たな式を先の条件法の後件に取ります。このようにして作られた条件文を考えると、そこから *20･1 と Modus Ponens を使えば、その条件文の後件である上記証明二行目の式が得られることを示しています。
次の、上記証明中、三行目を見ると、その先頭に '[(*20･02)]' とありますが、これは定義式 *20･02 によって、上記証明二行目から、その三行目が得られることを示しています。*20･02 とは次の定義式です。
*20･02 x ε (φ! ) .=. φ! x Df
上記証明中、二行目右端の 'x ε (φ! )' は、この定義式 *20･02 の右辺と交換できるので、交換した結果が三行目になります。
四行目の *10･43 は、次の定理です。
*10･43 ⊢ : φz ≡z ψz . φx .≡. φz ≡z ψz . ψx
この定理がいわんとしていることは、φ と ψ が同値なら、φ が現れているところで、それと ψ を交換してよい、ということです。そこで三行目では ψ と φ! が同値だと言っているので、三行目右端の φ! を ψ と交換してやった結果が四行目となります。
五行目の *10･35 は、次の定理です。
*10･35 ⊢ ∴ (∃x) . p .φx .≡: p : (∃x) . φx
これは p に x が現れていないならば、p を量化の scope から外してもよい、ということを述べています。そこで四行目を見ますと、その右端の ψx を p と取れば、この p には、存在量化子が束縛している φ が現れていませんので、この p である ψx を存在量化子の scope から外してやってもよく、その結果は五行目になります。
六行目の *12･1 とは次の式で、
*12･1 ⊢ : (∃f) : φx .≡x . f ! x Pp
これは the axiom of reducibility です。(Pp は、'primitive proposition' の略です。) 任意の order の propositional function φx には、それと同値な predicative function f ! x がある、と述べています。この公理は五行目の、三つの三点 dot のうち、左二つの三点 dot の間に挟まる形で、その行の式に埋め込まれています。これは公理でいつでも成り立つとされていますから、いわば冗長である故、省いてよく、その結果は求めようとしていた Prop, すなわち
*20･3. ⊢ : x ε (ψz) .≡. ψx
となります。
以上のように、*20･3 の証明は、まず定理 *20･1 を立て、x ε (ψz) から始めて同値変形を繰り返し、the axiom of reducibility の助けを借りて出てくることがわかります。
今証明した *20･3 は、通常なら Comprehension Principle を実質的にいみしているものと解されるでしょうが、そのような class に関する最も基本的とも目される式が、Principia では the axiom of reducibility に依存していることが、上記の証明から理解できることと思います。
最後に。
上記 *20･3 に対する証明では、Principia の dot 記法がそのまま使われていました。この dot 記法になれていない方もおられると思いますので、カッコや通常の連言記号を使ってそれを書き換えたものを、以下に掲載しておきます。なお、普遍量化子の明示は、ややこしくなり過ぎるので、省いています。あまりに簡単で自明すぎる場合も、カッコを省いています。また、Principia の dot 記法の読み方については、当日記、2011年6月12日、項目 'How to Read Elementary Dot Notational Formulae in Principia Mathematica' をご覧ください。非常にくどく説明しています。
下記の証明では、一番内側のカッコは、今まで通り ( ) を使い、その外側では [ ] を、その外側では〈 〉を、さらに一番外側では【 】を使っています。
*20･3. ⊢ [ ( x ε
Dem.
⊢ . *20･1 .⊃
⊢【 x ε
[(*20･02)] ≡ 〈 (∃φ) [ ( ψy .≡y . φ! y ) ∧ ( φ! x ) ] 〉
[*10･43] ≡ 〈 (∃φ) [ ( ψy .≡y . φ! y ) ∧ ( ψx ) ] 〉
[*10･35] ≡ 〈 [ (∃φ) ( ψy .≡y . φ! y ) ] ∧ ( ψx ) 〉
[*12･1] ≡ ( ψx ) 】⊃ ⊢ . PropThis proposition shows that x is a member of the class determined by ψ when, and only when, x satisfies ψ.
*20･1 ⊢ 【 ( f {
*4･2 ⊢ . p ≡ p
*20･01 ( f {
*20･02 x ε (φ!
*10･43 ⊢ 〈 [ ( φz ≡z ψz ) ∧ ( φx ) ] ≡ [ ( φz ≡z ψz ) ∧ ( ψx ) ] 〉
*10･35 ⊢ 〈 (∃x) ( p ∧ φx ) ≡ [ ( p ) ∧ ( (∃x) . φx ) ] 〉
*12･1 ⊢ 〈 (∃f) [ ( φx ) ≡x ( f ! x ) ] 〉 Pp
以上の記述には誤りが含まれていると思います。絶対に鵜呑みにしないでください。私は論理学や Russell のことについて詳しい人間ではありません。本当に正しいことが書かれているかどうか、ご自分でお確かめください。含まれているはずの誤りに対し、および含まれているはずの誤字・脱字等に対し、お詫び申し上げます。
*1:この答えは、他の人々に先んじて、私が初めて明らかにしたことだ、というのでは、まったくありません。既にこの答えは他の人によって与えられており、私はそれをなぞっただけです。
*2:Russell は、class が存在するともしないとも主張せず、態度を保留する場合もあります。See Bertrand Russell, Introduction to Mathematical Philosophy, Routledge, 1993 (first published in 1919), p. 184, ラッセル、『數理哲學序説』、岩波文庫、岩波書店、1954年、241ページ。
*3:Russell にとって個体とは何か、という問題については、ここでは検討致しません。とりあえず、例えば、Principia の一部解説的な側面を持つ次の文献をご覧ください。ただし、そこでの Russell の個体に関する考察は、本人も認めている通り、充分なものではありません。See Russell, Introduction to Mathematical Philosophy, pp. 141-143, ラッセル、『數理哲學序説』、185-187ページ。
*4:Class を個体とし、 (ψz) と { z |ψz } が個体としての class の名前だとすることは、岡本賢吾先生が「素朴集合論の原理」、「NS の原理」と呼んでおられるものと、ちょうど同じです。次をご覧ください。岡本賢吾、「数学基礎論の展開とその哲学」、飯田隆編、『哲学の歴史 第11巻 論理・数学・言語 【20世紀】』、中央公論新社、2007年、294ページ、岡本賢吾、「編者解説」、岡本賢吾、金子洋之編、『フレーゲ哲学の最新像』、双書 現代哲学5、勁草書房、2007年、354ページ。次もぜひ参照のこと。岡本賢吾、「命題を集合と同一視すること 包括原理からカリー=ハワード対応へ」、『科学哲学』、第36巻、第2号、2003年、108-114ページ、特に108ページの「(1) クラス演算子」の箇所と111ページを参照。
*5:Whitehead and Russell, Principia Mathematica to *56, p. 166. なお、これと非常によく似た文章が、次にも出てきます。Russell, ''Mathematical Logic as Based on the Theory of Types,'' in his Logic and Knowledge, p. 81, and the same paper in From Frege to Gödel, p. 167. ''Mathematical Logic … '' 論文の方が Principia より前に書かれているだろうから、おそらく ''Mathematical Logic … '' 論文の文章を流用して Principia が書かれたのだと思われます。
*6:これと同じ見解が、次においても見ることができます。Russell, Introduction to Mathematical Philosophy, p. 183, ラッセル、『數理哲學序説』、239ページ。
*7:See Bertrand Russell, My Philosophical Development, Revised ed., Routledge, 1995 (first published in 1959), pp. 60-63, バートランド・ラッセル、『私の哲学の発展』、野田又夫訳、みすずライブラリー、みすず書房、1997年、101, 104-106ページ。
*8:Whitehead and Russell, Principia Mathematica to *56, p. 193. なお *20･3 の証明の概略が、次にも載っています。Russell, ''Mathematical Logic as Based on the Theory of Types,'' in his Logic and Knowledge, p. 90, and the same paper in From Frege to Gödel, p. 173. さらに、次にも載っています。大出晁、「Principia Mathematica における命題函数 I」、日本科学哲学会編、野本和幸責任編集、『分析哲学の誕生 フレーゲ・ラッセル』、科学哲学の展開 1、勁草書房、2008年 (初出 1958年)、204-205ページ。これは以下においても再録されています。『大出晁哲学論文集』、野本和幸編・解題、慶應義塾大学出版会、2010年、758(19)-759(18)ページ。ただし、大出先生の論文に見られる *20･3 の証明には、『分析哲学の誕生』においても、『大出晁哲学論文集』においても、誤植や脱落があるので注意が必要です。『分析哲学の誕生』では、証明内における (5) の行の真ん中にある同値記号 ≡ は、正しくは条件法 ⊃ でなければなりません。そのため、証明を一読しただけでは、証明がよくわかりません。私はもう一度読み直して誤植に気が付きました。加えて『大出晁哲学論文集』では、件の証明の第一行目が完全に脱落しています。そのため証明の出だしのところで、何のことかわからなくなっています。あと、『分析哲学の誕生』と『大出晁哲学論文集』の両方に載っている証明の (3), (5) 行目を導く際に、普遍汎化則 (ψ) を使用していると証明中に記されているように見えるのですが、実際に使用されているのは普遍汎化則ではなく存在汎化則 (∃ψ) のように思われます。その場合、証明中に普遍汎化則 (ψ) と書くのではなく、存在汎化則 (∃ψ) と書くべきですが、大出先生の論文の証明では、そのようになっていません。誤植でないかと思われるのですが…。間違っていましたらすみません。
