二重否定翻訳

数理論理学の一分野である証明論において、二重否定変換（否定変換とも呼ばれる）は、古典論理を直観論理に組み込むための一般的なアプローチである。通常、これは式を古典的には同値だが直観的には同値でない式に変換することによって行われる。二重否定変換の具体的な例としては、命題論理に対するグリヴェンコ変換、一階述語論理に対するゲーデル・ゲンツェン変換および黒田変換などがある。

最も簡単な二重否定の変換は、1929 年にValery Glivenkoによって証明されたGlivenko の定理から来ています。これは、各古典的な式 φ をその二重否定 ¬¬φ にマッピングします。

グリベンコの定理は次のように述べています。

φ が命題式である場合、¬¬φ が直観主義トートロジーである場合に限り、 φ は古典的トートロジーです。

グリベンコの定理は、より一般的な次の命題を暗示しています。

T が命題式の集合であり、 φ が命題式である場合、古典論理でT ⊢ φ となるのは、直観主義論理でT ⊢ ¬¬φとなる場合のみです。

特に、命題式の集合は、それが古典的に満足可能である場合にのみ、直観的に一貫しています。

ゲーデル・ゲンツェン変換（クルト・ゲーデルとゲルハルト・ゲンツェンにちなんで名付けられた）は、第一階言語の各式 φ に、帰納的に定義される 別の式 φ ^{Nを関連付けます。}

• φが原子であれば、φ ^Nは¬¬φである。

上記と同様ですが、さらに

• (φ ∨ θ) ^Nは ¬(¬φ ^N ∧ ¬θ ^N )である。
• (∃ x φ) ^Nは ¬(∀ x ¬φ ^N )

その他

• (φ ∧ θ) ^Nは φ ^N ∧ θ ^{Nである。}
• (φ → θ) ^Nはφ ^N → θ ^Nである
• (¬φ) ^Nは¬φ ^Nである
• (∀ x φ) ^Nは、 ∀ x φ ^{Nである。}

^{この変換は、 φ N が}古典的には φ と同値であるという性質を持つ。TroelstraとVan Dalen (1988、第 2 章、第 3 節)は、Leivant に依拠して、直観主義第 1 階述語論理でもゲーデル-ゲンツェン変換を意味する式について説明している。そこでは、これはすべての式に当てはまるわけではない。(これは、追加の二重否定を含む命題が、より単純な変形よりも強力になる可能性があるという事実に関連している。たとえば、¬¬φ → θ は常に φ → θ を意味するが、逆方向のスキーマは二重否定の除去を意味する。)

構成的同値性のため、翻訳には複数の代替定義があります。たとえば、有効なド・モルガンの法則により、否定選言を書き直すことができます。したがって、1つの可能性は次のように簡潔に説明できます。すべての原子式の前に「¬¬」を接頭辞として付け、すべての選言と存在量化子にも接頭辞として付けます。

• (φ ∨ θ) ^Nは ¬¬(φ ^N ∨ θ ^N )
• (∃ x φ) ^{N は}¬¬∃ x φ ^Nである

黒田の翻訳として知られる別の手順は、式全体の前とすべての全称量指定子の後に「¬¬」を置くことによって翻訳された φ を構築することです。この手順は、 φ が命題である場合は常に、命題翻訳に正確に簡約されます。

第三に、コルモゴロフが行ったように、 φ のすべての部分式の前に「¬¬」を付けることもできます。このような変換は、証明とプログラムの間のカリー・ハワード対応に沿った関数型プログラミング言語の名前呼び出し 継続渡しスタイルの変換の論理的対応物です。

各 φ のゲーデル-ゲンツェン変換式と黒田変換式は互いに同等であることが証明されており、この結果は極小命題論理においてすでに成り立っています。さらに、直観主義命題論理では、黒田変換式とコルモゴロフ変換式も同等です。

φから¬¬φへの単なる命題的写像は、いわゆる二重否定シフトのように、一階述語論理の健全な翻訳には至らない。

∀ x ¬¬φ( x ) → ¬¬∀ x φ( x )

^{は直観主義述語論理の定理ではありません。したがって、φ N}の否定はより特別な方法で配置する必要があります。

T ^{N が}T内の式の二重否定変換で構成されるものとします。

基本的な健全性定理 (Avigad and Feferman 1998, p. 342; Buss 1998 p. 66) は次のように述べています。

T が公理の集合であり、 φ が式である場合、 T ^{N が}直観主義論理を使用してφ ^Nを証明する場合のみ、T は古典論理を使用して φ を証明します。

ゲーデル (1933) は、自然数 (「算術」) の古典理論と直観主義理論の関係を研究するために、二重否定変換を使用しました。彼は次の結果を得ました。

式 φ がペアノ算術の公理から証明可能であれば、 φ ^{N は}ハイティング算術の公理から証明可能です。

この結果は、ヘイティング算術が一貫しているなら、ペアノ算術も一貫していることを示しています。これは、矛盾する式θ ∧ ¬θ がθ ^N ∧ ¬θ ^Nと解釈されるためであり、それでも矛盾しています。さらに、関係の証明は完全に構成的であり、ペアノ算術のθ ∧ ¬θの証明をヘイティング算術のθ ^N ∧ ¬θ ^Nの証明に変換する方法を提供します。

二重否定変換とフリードマン変換を組み合わせることで、ペアノ算術がヘイティング算術に対してΠ ⁰ ₂ -保存的であることが実際に証明できます。

• 弁証法の解釈
• モーダルコンパニオン

• J. AvigadおよびS. Feferman (1998)、「ゲーデルの機能的 (「弁証法」) 解釈」、証明理論ハンドブック、S. Buss 編、Elsevier。ISBN 0-444-89840-9 
• S. Buss (1998)、「証明理論入門」、証明理論ハンドブック、S. Buss 編、Elsevier。ISBN 0-444-89840-9 
• G. Gentzen (1936)、「Die Widerspruchfreiheit der reinen Zahlentheorie」、Mathematische Annalen、v. 112、pp. 493–565 (ドイツ語)。ゲルハルト・ゲンツェンの論文集、ME・ザボ編に「算術の一貫性」として英訳で転載。
• V. Glivenko (1929)、Sur quelques point de la logique de M. Brouwer、Bull。社会数学。ベルク。 15、183-188
• K. Gödel (1933)、「Zur intuitionistischen Arithmetik und Zahlentheorie」、Ergebnisse eines mathematischen Kolloquiums、v. 4、pp. 34–38 (ドイツ語)。The Undecidable、M. Davis 編、75 ～ 81 ページに「On intuitionistic arithmetic and Number Theory」として英訳で転載されています。
• AN コルモゴロフ (1925)、「O principe tertium non datur」(ロシア語)。英訳では「排中原理について」として、ヴァン・ヘイエノールト編『フレーゲからゲーデルへ』414～447ページに掲載。
• AS Troelstra (1977)、「構成的数学の側面」、数学論理ハンドブック、J. Barwise編、North-Holland。ISBN 0-7204-2285 -X 
• AS TroelstraとD. van Dalen (1988)、「数学における構成主義。入門」 、論理学と数学の基礎研究の第 121 巻と 123 巻、北ホラント。

• 「直観主義論理」、スタンフォード哲学百科事典。
• ムート、リチャード; レトレ、クリスチャン (2016)。「古典論理と直観論理: 自然演繹における同等の定式化、ゲーデル-コルモゴロフ-グリヴェンコ訳」。arXiv : 1602.07608 [math.LO]。