はじめに

グリベンコの定理¹でお馴染みのグリベンコの手紙をいくつか翻訳する。

テキストはA. S. Troestra, On the Early History of Intuitionisitc Logic, In Mathematical Logic, Springer, pp.3-17 (1990) を使用した。

以下でも読むことができる。

https://eprints.illc.uva.nl/1281/1/ML-1988-04.text.pdf

以下の文献も参照した。

Dennis E. Hesseling, Gnomes in the Fog: The Reception of Brower's Intuitionism in the 1920s, Birkhäuser Verlag, 2003.

翻訳

1928年7月4日

ハイティング様、

この夏はモスクワから離れたヴォルガ近くの村にいたので、あなたの手紙を受け取ったのが今日となってしまいました。

直観主義論理と直観主義数学の形式化についての問題に関する私たちの観点が完全に同じであることを嬉しく思っています。ブリュッセルでの私の論争的なノート²ではこの問題を完全にはっきりとは提示できていません。それはあのノートの特殊な目的によって直観主義の考えを十分深くは知っていないと私が思うような学者にも容易に理解できるような言葉(langage)が必要とされたからです。しかし私自身この主題については、既に受理されたこれから数週間であなたにお伝えできると思っている別の結果に関して、より本質的ないくつかの考察を行いました。それではあなたにお伝えする結果を私のブリュッセルでのノートで議論されている内容と私が最近発見した内容に直接に関係するもののみに限定するのをご了承ください。ノートの中で与えられている公理I-Xからなる公理系は古典論理(la logique mathématique classique)の完全な公理系ではまったくないということに注意すべきです³。そして完全な公理系を得るためには、この公理系を少し変更するだけで十分です。つまり含意と連言(multiplication)の間の形式的な対応⁴を明確化するという変更を行います。

$XI^*: (p\to(q\to r))\to (p\land q\to r)$ ,

$XII^*: (p\land q\to r)\to (p\to(q\to r))$ ,

さらに排中律を二重否定除去(ce de réciprocité des espéces complémentaire)に置き換えるという変更を行います。

$X^*: \neg(\neg p)\to p.$

公理I-IXと $XI^*$ - $XII^*$ は明らかに直観主義論理で許容可能(admissible)であるので、これらの公理から定理(principe, 原理) $X^*$ の二重否定

$\neg(\neg(\neg(\neg p)\to p)).$

が証明可能(demonstrable)であるかそうでないかを問うのは自然なことです。

その答えは否定的であることを示しました⁵。

直観主義論理の構成についてこの事実から何を引き出すべきでしょうか? 研究の間にこの主題についてのいくつかの特徴的な情報(indication)を得ました。ただ、まだ十分には明確ではありません。私が確かだと思えることは次のことだけです。直観主義の原理の精密化にはずっと多くの研究が必要であり、そのような研究は重要な論理的事実に関する知識にとってとても実り多いものとなるでしょう。そのような論理的事実は古典論理でさえ与えてくれないような情報なのです。

敬具

グリベンコより

例えば以下を参照。
http://web.sfc.keio.ac.jp/~mukai/modular/gentzen-NK.pdf ↩
V. Glivenko, Sur la logique de M. Brouwer, Bulletin Acad. Bruxelles, 14:5, 225–228 (1928)のこと。この論文ではBarzin and Errera, Sur la logique de M. Brower, Academie Royale de Belgique, Bulletins de la Classe des Sciences 5:13, pp.56-71, (1927)に対する反論を行なっている。Barzin and Erreraはブラウアーの論理を三値論理であるとみなして矛盾が生じると批判した。↩
以下の4.3を参照。
https://plato.stanford.edu/entries/intuitionistic-logic-development/#Gliv19281929 ↩
圏論的論理の言葉で言えば連言と含意の随伴(関係)である。以下では記号と表記法は現代風に書き直している。↩
この結果については以降の手紙も参照
https://incognito0.hatenablog.com/entry/2021/05/13/194028 ↩

Asinus's blog

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

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

はじめに

翻訳