Glivenko's theorems from an ecumenical perspective

技術的概要：エキュメニカルな視点からのグリーヴェンコ定理

問題提起
本論文は、古典論理（CL）と直観主義論理（IL）の基礎的な関係性、特にグリーヴェンコ定理の再検討に取り組んでいる。これらの定理は、ある式が古典的に証明可能であれば、その二重否定が直観主義的に証明可能であり、また否定された式が古典的に証明可能であれば、それは直観主義的にも証明可能であることを確立する。これらの結果は個別の論理体系の文脈ではよく理解されているが、本論文は、これらの関係性がエキュメニカルな体系内でどのように現れるかを調査する。エキュメニカルな体系とは、古典論理と直観主義論理が互いに消滅することなく平和的に共存する統合された枠組みであり、演算子を区別する（例えば、古典的対偶と直観主義的対偶）か、式の論理的性質を示すためにラベルを付与するかによって実現されることが多い。中心的な問題は、古典的推論と直観主義的推論が単一の演繹体系に統合された際に、グリーヴェンコ型の結果がどのように翻訳されるかを決定し、エキュメニカルズムへの 2 つの主要なアプローチ、すなわち演算子を区別する「推論主義的」アプローチと、ラベルを通じて式を区別する「一般主義的」アプローチとの間の差異を分析することである。

方法論
著者らは、自然演繹体系を用いた証明論的解析を採用する。彼らは 3 つの特定のエキュメニカルな枠組みを検討する。

1. NE（プラウイツの体系）： 推論主義的アプローチであり、古典論理者と直観主義論理者が中立な演算子（論理積、全称量化子、否定、矛盾）を共有するが、非中立な演算子（含意、論理和、存在量化子）については異なるバージョンを持つ。
2. ECI（バルロソ・ナシメントの体系）： 一般主義的アプローチであり、単一の演算子セットを使用するが、式に定数 $c$ を付与して（例：$A^c$）、古典的な振る舞いを示す。この体系は、ラベルに対する導入規則（$I_C$）と除去規則（$E_C$）を追加して拡張された直観主義自然演繹に基づいている。
3. NEK（クラウスに着想を得た体系）： プラウイツの体系の変種であり、クラウスの未発表の業績に基づいて、古典的論理積（$\land_c$）と古典的全称量化子（$\forall_c$）を含む。

方法論には以下が含まれる。

• これらの体系内で、古典的演算子/式とそれらの直観主義的対応物との関係を結びつける、内部的なグリーヴェンコ型定理を定義すること。
• これらの内部的な関係を証明するための導出を構築すること。
• 体系間で式をマッピングする翻訳関数（$t_{ECI}$ および $t_{NEK}$）を定義すること。
• 特に、命題部分と全称量化を含む一階部分における、これらの体系の演繹的同等性を調査すること。

主要な貢献と結果

1. NE における内部的グリーヴェンコ定理：
   著者らは、異なる演算子が存在するプラウイツの体系（NE）において、「グリーヴェンコ型」の関係が内部的に成立することを示す。主演算子が古典的である任意の式 $C$ に対して、$C \vdash_{NE} \neg\neg C^*$ が成り立つ。ここで $C^*$ は、古典的演算子をそれらの直観主義的対応物に置き換えた式である。これは古典的論理和（$\lor_c$）、含意（$\to_c$）、存在量化（$\exists_c$）に適用される。否定された式についても同様の結果が成り立つ。すなわち、$\neg C \vdash_{NE} \neg C^*$ である。

2. ECI におけるグリーヴェンコ結果の自明性：
   ECI 体系において、古典的式 $A^c$ とその直観主義的対応物の間の関係は構造的に自明である。この体系の規則は即座に $A^c \vdash_{ECI} \neg\neg A$ を導く。したがって、$A^c$ を $\neg\neg A$ にマッピングする翻訳 $t_{ECI}$ は、ECI における正規化の問題を直観主義論理のものに帰着させる。著者らは、この翻訳が命題論理では機能するものの、導出が導出された式の「古典的性質」を追跡するために慎重に再構成されない限り、導出における古典的推論の具体的な位置を曖昧にしてしまうことを示す。

3. 古典的論理積と NEK の場合：
   本論文は、プラウイツの体系に古典的論理積（$\land_c$）を追加した NEK を導入する。著者らは、$\land_c$ が内部的グリーヴェンコ定理（$B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$）を満たすことを証明する。また、命題部分（または全称量化子を含まない一階論理）において、NEK と ECI が演繹的に同等であることを示す。この同等性は、NEK 内の古典的演算子を ECI 内のラベル付き式にマッピングする翻訳 $t_{NEK}$ によって確立される。

4. 全称量化による分岐：
   重要な結果として、全称量化が導入されると、NEK と ECI の間の演繹的同等性が破綻することである。

   • NEK において、古典的全称量化子 $\forall_c$ は直観主義論理と調和する規則によって定義される。しかし、$\forall_c$ に対して内部的グリーヴェンコ定理は失敗する。すなわち、$\vdash_{NEK} \forall_c x A(x)$ は $\vdash_{NEK} \neg\neg \forall_i x A(x)$ を意味しない。
   • ECI において、ラベル付き式 $(\forall x A(x))^c$ は異なって振る舞う。体系の規則により、$(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$ が成り立つ。
   • 著者らはこの不一致を説明する。NEK において $\forall_c x A(x)$ は $\neg \exists x \neg A(x)$ として解釈されるのに対し、ECI において $(\forall x A(x))^c$ は実質的に $\neg\neg \forall x A(x)$ として解釈される。これらは直観主義的に同等ではない。本論文は、全称式に対する ECI におけるグリーヴェンコ結果の「自明性」は、ラベル $c$ が、推論主義的アプローチにおける古典的全称量化子の意味論的振る舞いと整合しない二重否定解釈を強制することに起因すると論じる。

意義と主張
本論文は、エキュメニカルな視点が古典的推論と直観主義的推論の相互作用をより深く理解する手助けをすると主張する。「推論主義的」（NE/NEK）アプローチと「一般主義的」（ECI）アプローチを比較することで、著者らは微妙だが重要な概念的差異を浮き彫りにする。

• 推論主義的体系（プラウイツ/クラウス）は、古典的演算子に対する独自の導入規則と除去規則を提供することで、結合子の意味を直接的に変化させる。
• 一般主義的体系（ECI）は、証明のレベルを変化させ、ラベル $c$ を通じて直観主義論理に古典的な証明手段を備えさせることで、間接的に演算子の意味を変化させる。

著者らは、これらのアプローチが命題論理では同等であるが、全称量化が存在する場合には分岐すると結論づける。この分岐は、エキュメニカルな枠組みの選択が単なる表記上の好みに留まらず、量化子の論理的振る舞いに影響を与えることを示唆している。本論文は、エキュメニカルな視点が、古典的推論がいつ必要とされるかを正確に特定する手助けとなり、体系がこれらの異なる推論原理に注意して構築される限り、古典的原理と直観主義的原理が互いに消滅することなく共存し得ることを明確にすると提言している。