昨日と今日で、某学会に行こうかと思っていたのですが、体調が思わしくないので、急遽取り止めにしました。
その学会では以下の発表を取り分け拝聴させていただきたいと考えていました。
- 大西琢朗 「フレーゲの「論理」」
この大西先生の発表はとても興味深く感じられます。幸い、abstract が net から入手できますので、それを読むことで、大会参加の代わりにしました。
先生の発表の主眼は次のもののようです。Abstract から引用させていただきます。
本発表は，フレーゲの概念記法における関数抽象のメカニズムと，『算術の基本法則』における「有意味性証明」の関係について考察する．
続けて以下のように述べられています。
フレーゲの概念記法（という論理体系ないし形式言語）は，現代の（高階）述語論理の原型であるが，そのシンタクスは，現代の標準的な見方からすると，独特な特徴を備えている．そのひとつが，いわゆる「除去」の方法による表現形成である．すなわち，概念記法においては，規定された原初的表現を合成し，複合表現を形成できるだけでなく，形成された複合表現から，その一部を除去することで，新しい，空所を伴った表現（関数名ないし述語）が形成できるのである．この除去による表現形成は，ラムダ計算における関数抽象（ラムダ抽象）とよく似てはいるが，むしろ逆の考え方だとも言える．ラムダ計算では，自由変数とラムダ記号を用いて，合成的に関数表現（ラムダ項）を形成した後，それがどのような正規形へ簡約できるかを調べる．概念記法で問われるのは，いわば正規形と言える複合表現から出発したとき，そこからどのような簡約可能項が生成できるか，である．意味の観点から考えるなら，ラムダ項の意味は，一言で言えばその正規形であると考えられるのに対し，概念記法では逆に，正規形に当たる表現が，そこへ簡約される項すべての内容を，何らかの仕方で含んでいると考えられるのである．
(上の引用文に対し、comment を次に付しますが、この日記の以下の記述はすべて、私による勝手な思い付きを書き付けているだけです。Lambda Calculus について無知な私の話ですから、読まれる方は絶対に真に受けないで下さい。必ずご自分で確認しつつお読み下さい。そして必ず間違ったことを書いているでしょうから、前もってここでお詫びしておきます。見当違いなことを記していましたら大変申し訳ございません。)
Lambda Calculus の Lambda Abstraction と Grundgesetze の Ausschluss の方法は、先生によると nearly equal だとのことです。しかし先生によると、Lambda Abstraction と Ausschluss は、互いにいわば逆の関係にあるようです。つまり前者により「自由変数とラムダ記号を用いて，合成的に関数表現（ラムダ項）を形成した後，それがどのような正規形へ簡約できるかを調べる」ということで、例えば、自由変数を x とし、ラムダ記号 λ を用いて、ラムダ項 M に対し、x, λ, M を合成してラムダ項 λxM などを形成した後、β-Reduction を通して Normal Form を特定するという process を経るのに対し、後者の Ausschluss によると、「概念記法で問われるのは，いわば正規形と言える複合表現から出発したとき，そこからどのような簡約可能項が生成できるか，である」ということで、これは例えば、Normal Form M [N/x] から (λxM)N というような Lambda Term を得る β-Expansion に相当することを実行するということであろうと推測致します。
Abstract の残りを記します。
この独特の形成法と，それに付随する意味の描像は，これまでダメットをはじめ，多くの論者の議論の的となってきた．本発表は，この「除去」の方法の存在が，『算術の基本法則』の「有意味性証明」の失敗とどのように関わっているのかを明らかにしたい．『基本法則』における概念記法は，「概念の外延（関数の値域）」の観念を含んだ一種の素朴集合論であり，フレーゲは，その言語の任意の表現が一意的な意味をもつという旨の「有意味性証明」を行っている．残念なことに，『基本法則』の概念記法では，ラッセル・パラドクスが生じるため，その証明は間違っている．だが，フレーゲはともかくも証明を試みているのであり，その証明の誤りと，「除去」の方法が関わっているのではないかというのが，本発表の予想である．もちろん，「除去」の方法の廃棄ないし改良が，そのままパラドクスの解決となるわけではない．本発表が目指すのは，有意味性証明の誤りの原因の解明を通じて，パラドクスへの理解を深めることである．
先生はここで次のように述べておられます。
フレーゲは，その言語の任意の表現が一意的な意味をもつという旨の「有意味性証明」を行っている．残念なことに，『基本法則』の概念記法では，ラッセル・パラドクスが生じるため，その証明は間違っている．
先ほどからのお話、および Lambda Calculus の観点から、Frege の Proof of Referentiality について考えてみると、想像力をたくましくして少しばかり空想してみるならば、極度に大雑把ですが、次のような図式を描くことが可能でしょうか？
(PR) Proof of Referentiality: Grundgesetze の任意の表現は一意的な意味を持つ。⇔ Grundgesetze は無矛盾である。
⇔
(PCRT) Proof of Church-Rosser Theorem: Lambda Calculus では β-Reduction が Church-Rosser Property を持つ。⇔ Lambda Calculus は無矛盾である。
しかし、(PCRT) は成り立ちますが、(PR) は、Russell Paradox により、成り立ちません。したがって、(PR) と (PCRT) は同値になりません。
(PR) と (PCRT) が同値にならない原因として、どこに着眼すべきでしょうか？ (PR) と (PCRT) が対照的であることを考慮してでしょうか、先生は上の引用文中で次のように述べられています。
だが，フレーゲはともかくも証明を試みているのであり，その証明の誤りと，「除去」の方法が関わっているのではないかというのが，本発表の予想である．
本日の発表を拝聴できませんのでよくわからないのですが、大西先生は Frege's Proof of Referentiality の問題点を、上記の (PCRT) の観点から考察され、取り分け β-Expansion に Grundgesetze の不具合が見られると述べられるのではなかろうかと空想致します。ではそうだとした場合、もしも β-Expansion をどうにかする必要があるとするならば、それはどうしたらいいのだろうか？ 私には難しすぎてわかりません…。
以上はまったくの空想です。まるで見当違いのことを述べていると思います。加えて、私は Lambda Calculus に無知ですから、必ず間違えています。上述の話は絶対に鵜呑みにしないで下さい。そのまま受け取ることは非常に危険です。必ずしかるべき文献や人物に当たって確認をお取り下さい。そして上記で的外れなことを申しまして大西先生にお詫び致します。誠に済みません。いずれにしましても、先生の abstract を拝読させていただくことで、空想を楽しむことができました。大変ありがとうございました。今後とも、間違いを正して行くために、勉強して参ります。
最後に今回の記述で参考にしました文献を念のために記しておきます。順不同。
- J. Barkley Rosser “Highlights of the History of the Lambda-Calculus,” in: Annals of the History of Computing, vol. 6, no. 4, 1984
- J. Roger Hindley and Jonathan P. Seldin Lambda-Calculus and Combinators: An Introduction, 2nd Edition, Cambridge University Press, 2008
- 小野寛晰 『情報科学における論理』、情報数学セミナー、日本評論社、1994年
- 萩谷昌己 『論理と計算』、岩波講座応用数学 基礎 11、岩波書店、1993年
ここまで記したことに関しまして、きちんと見直すことも、ちゃんと推敲することもしておりませんので、誤解や無理解や誤字や脱字がございましたらお詫び致します。
