二重否定翻訳

数理論理学の分野での、証明論において、二重否定翻訳（にじゅうひていほんやく、Double-negation translation、ときに否定翻訳とも）は、古典論理を直観主義論理に埋め込む一般的なアプローチである。

典型的には二重否定翻訳は、論理式を、古典的には同値であるが直観主義的には同値でない論理式に変換することでなされる。特に、二重否定翻訳の実例として命題論理についてのグリベンコの定理と、一階論理のためのゲーデル=ゲンツェン翻訳およびKurodaの翻訳などが知られている。

命題論理

最も記述が単純な二重否定翻訳はグリベンコの定理に由来する。この定理は、Valey Glivenkoによって1929年に証明された。ここではそれぞれの古典的論理式 $\varphi$ をその二重否定 $\lnot \lnot \varphi$ に写される。

諸結果

グリベンコの定理の主張は次の通りである。

$\varphi$ が命題論理式であるとき、$\varphi$ が古典的トートロジーである必要十分条件は、 $\lnot \lnot \varphi$が直観主義的トートロジーであることである。

グリベンコの定理はいっそう一般的な主張も含んでいる。すなわち、

$T$ が命題論理式の集合であって $\varphi$ が命題論理式であるとき、 $T\vdash \varphi$ が古典論理で成立する必要十分条件は、直観主義論理で $T\vdash \lnot \lnot \varphi$ が成立することである。

特に、命題論理式の集合 $T$ が直観主義的に無矛盾である必要十分条件は、 $T$ が古典的に充足可能であることである。

一階論理

ゲーデル=ゲンツェン翻訳 (Kurt Gödel および Gerhard Gentzen にちなんで命名されている) は、ある一階言語内のそれぞれの論理式 $\varphi$ を、帰納的に定義される異なる論理式 ${\varphi }^{N}$ に結びつける。

• $\varphi$ が原子論理式であるとき、 ${\varphi }^{N}$ は論理式 $\lnot \lnot \varphi$ である。
• ${(\varphi \lor \psi )}^{N}\equiv \lnot (\lnot \varphi \land \lnot \psi )$
• ${(\exists x\varphi )}^{N}\equiv \lnot (\forall x\lnot {\varphi }^{N})$
• ${(\varphi \land \psi )}^{N}\equiv \varphi ^{N}\land \psi ^{N}$
• ${(\varphi \to \psi )}^{N}\equiv {\varphi }^{N}\to {\psi }^{N}$
• ${(\lnot \varphi )}^{N}\equiv \lnot {\varphi }^{N}$
• ${(\forall x\varphi )}^{N}\equiv \forall x{\varphi }^{N}$

この翻訳は、一階の論理式 ${\varphi }^{N}$ が $\varphi$ に古典的同値であるという性質を持っている。TroelstraとVan Dalen (1988, Ch. 2, Sec. 3) は、Leivantに依存した、自身の直観主義一階述語論理内にゲーデル=ゲンツェン翻訳を行う論理式に関する記述を与えている。そこでは、この翻訳が成立するのは全ての論理式についてというわけではない。 (このことは、次の事実に関連する。すなわち、付加的な二重否定を伴う命題がそのもっと単純な場合より強くなりうる、という事実である。例えば、$\lnot \lnot \varphi \to \psi$ は常に $\varphi \to \psi$ を常に含意するがしかし、逆方向でのスキーマは二重否定除去を伴うものである。)

Equivalent variants

構成的同値性のおかげで、翻訳の定義にいくつかの代替が存在する。例えば、ド・モルガンの法則により否定付きの選言を書き換えることができる。よって次のように簡潔に記述することができる。すなわち、すべての原子論理式に "$\lnot \lnot$" 前置し、同様にすべての選言文および存在量化子に前置する、という次第である。

• (φ ∨ θ)^N は ¬¬(φ^N ∨ θ^N)に翻訳され、
• (∃x φ)^N は ¬¬∃x φ^Nに翻訳される。

もう一つの手続きは、黒田の翻訳として知られ、翻訳後の $\varphi$ を構成するのに二重否定 "$\lnot \lnot$" をもとの式の全体の前と全ての全称量化子の後ろに挿入するというものである。この手続きは正確に、$\varphi$ が命題論理式であるかぎりでは、命題的な翻訳に還元される。

第三に、代わりに、論理式 $\varphi$ のすべての部分論理式に二重否定 "$\lnot \lnot$" を前置する仕方がある。これは Kolomogorov によってんされた。このような翻訳は、関数プログラミング言語のcall-by-name continuation-passing style 翻訳への、証明とプログラムの間の Curry–Howard correspondence に基づく論理的対応物である。

各 $\varphi$ がゲーデル=ゲンツェンおよび黒田の仕方によって翻訳された論理式は、もとの $\varphi$ に証明された仕方で同値であり、この結果は最小命題論理で成立する。さらには、直観主義命題論理においては、黒田およびKolmogorovの仕方によって翻訳された論理式が同値である。

単に命題論理的な写像 $\varphi \mapsto \lnot \lnot \varphi$ は、一階論理の健全な翻訳に拡大されることはない。というのも、いわゆる二重否定 shift は直観主義述語論理の定理ではないからである:

$\forall x\lnot \lnot \varphi (x)\to \lnot \lnot \forall x\varphi (x)$.

したがって、${\varphi }^{N}$ 内の否定の出現は、もっと限定的な仕方で表現されなければならない。

諸結果

$T^{N}$を 論理式の集合 $T$ に属する論理式の二重否定翻訳全体からなる集合とする。

The fundamental soundness theorem (Avigad and Feferman 1998, p. 342; Buss 1998 p. 66) が主張するのは、

$T$ が公理の集合であり、$\varphi$が論理式であるとするなら、$T$ が古典論理を用いて $\varphi$ を証明する必要十分条件は、$T^{N}$ が直観主義論理を用いて ${\varphi }^{N}$ を証明することである。

算術

二重否定翻訳はゲーデルによって、自然数に関する古典的理論と直観主義的理論の間の関係を研究するために用いられた (1933) 。なお、自然数に関する理論を算術という。ゲーデルは、次の結果を得ている:

論理式 $\varphi$ がペアノ算術の公理から証明可能であるとき、 ${\varphi }^{N}$ がHeyting arithmeticの公理から証明可能である。

この結果は、ハイティング算術が無矛盾であるならペアノ算術も無矛盾であることを示している。これは、矛盾する論理式 $\theta \land \lnot \theta$ は ${\theta }^{N}\land \lnot {\theta }^{N}$と解釈されてまた矛盾することに起因する。

さらに、この関係の証明は完全に構成的であり、ペアノ算術内の $\theta \land \lnot \theta$ をハイティング算術内の${\theta }^{N}\land \lnot {\theta }^{N}$に変形する方法を与えている。

二重否定翻訳をFriedman translationと組み合わせることにより、実際に次のことを証明できる。すなわち、ペアノ算術はハイティング算術上 Π⁰₂-conservative であるということである。　

関連項目

• Dialectica interpretation
• Modal companion

出典

• J. Avigad and S. Feferman (1998), "Gödel's Functional ("Dialectica") Interpretation", Handbook of Proof Theory, S. Buss, ed., Elsevier. ISBN 0-444-89840-9
• S. Buss (1998), "Introduction to Proof Theory", Handbook of Proof Theory, S. Buss, ed., Elsevier. ISBN 0-444-89840-9ISBN 0-444-89840-9
• G. Gentzen (1936), "Die Widerspruchfreiheit der reinen Zahlentheorie", Mathematische Annalen, v. 112, pp. 493–565 (German). Reprinted in English translation as "The consistency of arithmetic" in The collected papers of Gerhard Gentzen, M. E. Szabo, ed.
• V. Glivenko (1929), Sur quelques points de la logique de M. Brouwer, Bull. Soc. Math. Belg. 15, 183-188
• K. Gödel (1933), "Zur intuitionistischen Arithmetik und Zahlentheorie", Ergebnisse eines mathematischen Kolloquiums, v. 4, pp. 34–38 (German). Reprinted in English translation as "On intuitionistic arithmetic and number theory" in The Undecidable, M. Davis, ed., pp. 75–81.
• A. N. Kolmogorov (1925), "O principe tertium non datur" (Russian). Reprinted in English translation as "On the principle of the excluded middle" in From Frege to Gödel, van Heijenoort, ed., pp. 414–447.
• A. S. Troelstra (1977), "Aspects of Constructive Mathematics", Handbook of Mathematical Logic, J. Barwise, ed., North-Holland. ISBN 0-7204-2285-XISBN 0-7204-2285-X
• A. S. Troelstra and D. van Dalen (1988), Constructivism in Mathematics. An Introduction, volumes 121, 123 of Studies in Logic and the Foundations of Mathematics, North–Holland.

外侮リンク

• "Intuitionistic logic", Stanford Encyclopedia of Philosophy.
• Moot, Richard; Retoré, Christian (2016). "Classical logic and intuitionistic logic: Equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation". arXiv:1602.07608 [math.LO]。