はじめに

前回の記事はこちら。

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

翻訳

モスクワ、1928年10月18日

ハイティング様、

偶然にも10月13日に私の手紙で述べられていた質問への答えが書かれていた10月7日のあなたからの手紙を昨日受け取りました。

実を言うと公理 $\neg p\to(p\to q)$ の役割が私にはまた十分には明確ではありません。

しかしいずれにせよ、直観主義数学はこの公理を拒否する必要はないというあなたの見解を理解いたしました。なのでこの公理を拒否するすべての見解は我々が取り組んでいる主題の範囲からは越え出ているように思います。

問題となっている公理に基づいたあの命題[二重否定の命題]の証明については、よりずっと一般的な方法で証明することができるように思えます。より正確には、もし私の公理 I-IX, $XI^*$ - $XII^*$ と¹あなたの公理

(A) $p\to(q\to p)$ ,

(B) $\neg p\to(p\to q)$

を認めるならば、これらすべての公理自体の二重否定が証明できるだけではなく、さらに公理 $\neg p\lor p$ の二重否定をも証明することができます。

簡単に証明できる論理式 $(p\to q)\to(\neg\neg p \to \neg\neg q)$ を用いて、すべての論理式の二重否定が公理 I-IX, $XI^*$ - $XII^*$ , (A), (B), $\neg p\lor p$ から証明可能であることが従います。

ところが、これらの公理は確かに古典命題論理の完全な公理系を形成しています(公理 $XI^*$ - $XII^*$ を取り除いた時でさえそうです)。このことから論理式 $\neg\neg p\to p$ の二重否定が帰結するだけではなく、古典論理で真であると認められている全ての論理式の二重否定をも帰結するのです。

直観主義論理について、私の見解では、この肯定的な結果はこの夏にあなたにお伝えした否定的な結果よりもよりずっと好ましいものだと感じております²。

敬具

グリベンコより

前々回の記事を参照。
https://incognito0.hatenablog.com/entry/2021/04/02/183020 ↩
爆発則を取り除けば直観主義論理で二重否定除去則の二重否定は証明できなくなるが、それよりも(爆発則を含む)直観主義命題論理で古典論理で証明可能なすべての論理式の二重否定を証明できると言う結果(グリベンコの定理)の方が深い結果であるということ。↩

Asinus's blog

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

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

はじめに

翻訳