はじめに

前回の記事はこちら

今回の記事でグリベンコの手紙に関しては完結です。

翻訳

モスクワ 1933年10月24日

ハイティング様、

発音について教えていただきありがとうございました。私にとって全く十分な情報でした。なので今ためらわずに既に何人かのロシア人著者によって用いられている転写Стультьесを転載しておきます。

そのほかに、この機会を利用してコルモゴロフ氏の問題計算(le calcul des problemes)¹についてのいくつかの考えをあなたとやりとりしたいと思います。彼のアイデアは明らかに非常に興味深いものです。しかし、彼が定めた意味での操作(l'operation)²

$\neg a$

は彼の計算に論理のある不可避な要素を介在させてしまうように私には思われます³。例えば古典命題論理の要素がそれです。実際に、問題

$\neg a$

は彼にとっては次のような意味を持ちます。

「問題 a が解かれたという仮定のもとで、そこから矛盾を導き出す(tirer)」

これは以下のことに他ならないでしょう。

「次の命題を示すこと: 問題 a が解かれたという前提が矛盾を導くこと」

さて今や、完全に独立な問題計算を得ることができます。そのために、彼の公理 2.1, 2.11-15, 3.1, 3.11-3.12⁴とさらに以下の公理も認めましょう。

「任意の要素bに対して $0\to b$ が成り立つような要素0が存在する。」

形式的にはこの公理体系は我々のものと同値になります。ただし操作 $\neg a$ の代わりに、ここで操作 $a\to 0$ を取ります。この変更の帰結は明らかです。具体例のみ付け加えておきます。

算術の問題のなす領域を取ったとしましょう。つまり以下の形の問題です。

「方程式

$f(x_1,x_2, \dots, x_n)=0$

を満たすような整数 $x_1,x_2, \dots, x_n$ を見つけること。

ここで $f$ はwell-definedな関数である。」

問題0⁵に対しては、次の形の問題を取ることができます。

「方程式

$x+1=x$

を満たすような整数 $x$ を見つけること。」

実際に、もしこの問題が解かれたと仮定するならば、記号 $f$ のもとで任意の $x_1,x_2, \dots, x_n$ について次々と解を得ることができます。

$(x+1)f=xf$ ,

$f=0$ .⁶

形式的に同値であるにも関わらず、計算の意味と使用(le sens et l'emploi du calcul)はこのように変更されていることが分かります。そして計算自体も変更されており、第一にすべての論理的な要素から解放されていることも分かります⁷。

この主題に対するあなたの見解がとても知りたいです。

敬具

グリベンコより

次の論文で発表された。BHK解釈の"K"としてコルモゴロフが名を連ねたのはこの論文によってである。
Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift, 35, pp.58-65, 1932.
https://webspace.science.uu.nl/~ooste110/studsemIntMod/KolmogorovProblems.pdf
英訳もある。
On the Interpretation of Intuitionistic Logic, in P. Mancosu eds., From Brower to Hilbert: the debate on the foundations of mathematics in the 1920s, Oxford University Press, pp.328-334, 1998.↩
$\neg a$ は問題(Aufgabe)「aの解(Lösung, 答え)が与えられたと仮定して、矛盾を得ること。」(Kolmogorov, 1932, p.60).
また、コルモゴロフの論文には"operation"に類する表現はない。明示的にoperationとして言及しているのはグリベンコのオリジナルである。↩
ここでグリベンコは論理と計算を区別して捉えている。そして自分たち(ハイティングとグリベンコ)の否定の解釈の方が計算により適していると考えている。↩
Kolmogorov(1932)の論文p.61にある公理。↩
矛盾 $0=1$ を生み出す問題のこと。これが解かれたとして(矛盾よりfを用いて)任意の整数解を求めている。↩
i.e. f(0)=0, f(x+1)=f(x).↩
論理的な要素と呼ばれているのは $\bot$ のこと。0=1の方が計算にふさわしいとグリベンコは考えている。ただしコルモゴロフは矛盾としか言っていないのでグリベンコ達のような解釈も許容できる。↩

Asinus's blog

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

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

はじめに

翻訳