はじめに

前回の記事はこちら。前の手紙から約3ヶ月が経過している。

https://incognito0.hatenablog.com/entry/2021/04/02/183020

翻訳

モスクワ、1928年10月13日

ハイティング様、

まずはあなたの論文の抜粋をご教示いただいたことに感謝いたします。この夏は田舎で過ごしていたので、あなたの手紙しか受け取れておらず、モスクワで私を待っていた抜粋については何も知らずにおりました。私が前の手紙であなたに書き送った公理 $\neg(\neg p)\to p$ の二重否定についてはおそらく私の思い違いの結果に過ぎませんでした。モスクワの数学選集32巻でコルモゴロフ氏が、彼はロシアの最も独創的な数学者の一人なのですが、「排中律について」¹という標題の論文を(ロシア語で)発表していました²。

その論文で彼は直観主義命題論理の公理系を提示していました。そこで彼は二重否定除去則を拒否しているだけではなく、公理 $\neg p\to (p\to q)$ も拒否していました³ (しかし一方で公理 $p\to (q\to p)$ は認めています)。私の結論が正しくなるのがちょうどこの制限からなのです。つまり公理 $\neg(\neg p)\to p$ の二重否定が成り立たないのです。ですが今では、私はコルモゴロフ氏によってなされた制限が正当であるかに疑問を抱き始めています。つまり直観主義数学においては私がその必然性(nécessité)を証明することができないので、公理 $\neg p\to (p\to q)$ を拒否することが必要なのです。一方で、排中律を拒否することの必然性は何度か非常に明確にブラウアー氏によって証明されています。

この主題についてのあなたの意見を教えていただけるならば幸いです。

敬具

グリベンコより

原論文は以下で読むことができる。
http://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=sm&paperid=7425&option_lang=rus
この論文には以下の英訳がある。
“On the principle of the excluded middle” in Jean van Heijenoort (eds), A Source Book in Mathematical Logic 1879–1931, Harvard Univ. Press, pp. 414–37, 1967.↩
コルモゴロフの二重否定翻訳はロシア語で出版されたが故にほとんど知られていなかったが、この手紙によりハイティングは論文の存在は知っていた事になる。↩
この箇所は翻訳元テキストでは $\neg p\to (q\to p)$ となっている。コルモゴロフの論文と手紙の他の箇所から判断して $\neg p\to (p\to q)$ のタイプミスと判断し修正する。
なおこの公理はコルモゴロフの「排中律について」ではI- $\S 5$ の否定の公理 (2) 5. $A\to(\neg A\to B)$ に該当するものと思われる(否定の位置は記憶違いによるのか逆)。
コルモゴロフは含意の公理4つ(1)1-4と、否定の公理 (3)5. $(A\to B)\to ((A\to\neg B)\to \neg A)$ を合わせたものを(ブラウアーの)体系 Bとしている。
以下の4.1を参照。
https://plato.stanford.edu/entries/intuitionistic-logic-development/
コルモゴロフが拒否した公理は爆発則とも呼ばれ、シーケント計算ではweakening規則が関係する。そしてコルモゴロフの体系Bは今日でいう最小論理である。この問題の公理についてはコルモゴロフは1932年の論文には受け入れている。↩

Asinus's blog

西牟田祐樹のブログです。

グリベンコからハイティングへの手紙 (2)

はじめに

翻訳