二重否定翻訳

ウィキペディア

二重否定翻訳

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/12/22 06:08 UTC 版)

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

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

命題論理

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