Glivenko's theorems from an ecumenical perspective

기술적 요약: 에큐메니컬 관점에서의 글리벤키 정리

문제 제기
본 논문은 고전 논리 (CL) 와 직관주의 논리 (IL) 간의 근본적 관계를 다루며, 특히 글리벤키 (Glivenko) 정리를 재검토합니다. 이러한 정리는 어떤 명제가 고전적으로 증명 가능하면 그 이중 부정은 직관주의적으로 증명 가능하며, 부정이 붙은 명제가 고전적으로 증명 가능하면 그것 역시 직관주의적으로 증명 가능함을 확립합니다. 이러한 결과들이 개별 논리 체계의 맥락에서는 잘 이해되고 있지만, 본 논문은 이러한 관계가 에큐메니컬 시스템 (ecumenical systems) 내에서 어떻게 나타나는지 조사합니다. 에큐메니컬 시스템은 고전 논리와 직관주의 논리가 서로를 붕괴시키지 않고 평화롭게 공존하는 통합된 체계로, 종종 연산자를 구분 (예: 고전적 vs 직관주의적 논리합) 하거나 명제의 논리적 성질을 나타내기 위해 라벨을 부여함으로써 구현됩니다. 핵심 문제는 고전적 추론과 직관주의적 추론이 단일 추론 체계로 통합될 때 글리벤키 유형의 결과가 어떻게 번역되는지 결정하고, 에큐메니컬리즘에 대한 두 가지 주요 접근법인 '연역적 (inferentialist)' 접근 (연산자 구분) 과 '일반적 (generalist)' 접근 (라벨을 통한 명제 구분) 간의 차이를 분석하는 것입니다.

방법론
저자들은 자연 연역 (Natural Deduction) 체계를 사용하여 증명론적 분석을 수행합니다. 구체적으로 세 가지 에큐메니컬 체계를 검토합니다:

1. NE (Prawitz 의 체계): 연역적 접근으로, 고전 논리학자와 직관주의 논리학자가 중립적 연산자 (논리곱, 전칭 한정자, 부정, 모순) 를 공유하지만, 비중립적 연산자 (함축, 논리합, 존재 한정자) 에 대해서는 서로 다른 버전을 갖습니다.
2. ECI (Barroso-Nascimento 의 체계): 일반적 접근으로, 단일 연산자 집합을 사용하지만 상수 $c$로 명제를 라벨링하여 (예: $A^c$) 고전적 행동을 나타냅니다. 이 체계는 라벨에 대한 도입 규칙 ($I_C$) 과 소거 규칙 ($E_C$) 을 추가하여 확장된 직관주의 자연 연역을 기반으로 구축됩니다.
3. NEK (Krauss 에서 영감을 받은 체계): Krauss 의 미공개 작업을 기반으로 Prawitz 의 체계에 고전적 논리곱 ($\land_c$) 과 고전적 전칭 한정자 ($\forall_c$) 를 포함하는 변형 체계입니다.

방법론에는 다음이 포함됩니다:

• 이러한 체계 내에서 내부적 글리벤키 유형 정의를 정의 (고전적 연산자/명제를 직관주의적 대응물과 관련시킴).
• 이러한 내부 관계를 증명하기 위한 유도 (derivations) 구성.
• 체계 간 명제를 매핑하는 번역 함수 ($t_{ECI}$ 및 $t_{NEK}$) 정의.
• 특히 전칭 한정자가 포함된 명제 단편과 1 차 단편 간의 이러한 체계들의 연역적 동등성 조사.

주요 기여 및 결과

1. NE 내의 내부적 글리벤키 정리:
   저자들은 서로 다른 연산자가 존재하는 Prawitz 의 체계 (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 의 사례:
   본 논문은 Prawitz 의 체계에 고전적 논리곱 ($\land_c$) 을 추가한 NEK 를 소개합니다. 저자들은 $\land_c$가 내부적 글리벤키 정리를 만족함을 증명합니다 ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$). 또한 명제 단편 (또는 전칭 한정자가 없는 1 차 논리) 에서 NEK 와 ECI 가 연역적으로 동등함을 보여줍니다. 이 동등성은 NEK 의 고전적 연산자를 ECI 의 라벨링된 명제로 매핑하는 번역 $t_{NEK}$를 통해 확립됩니다.

4. 전칭 한정성과의 불일치:
   중요한 결과는 전칭 한정자가 도입될 때 NEK 와 ECI 간의 연역적 동등성이 실패한다는 것입니다.

• NEK에서 고전적 전칭 한정자 $\forall_c$는 직관주의 논리와 조화 (harmonic) 되는 규칙을 통해 정의됩니다. 그러나 $\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$가 연역적 접근법에서 고전적 전칭 한정자의 의미론적 행동과 일치하지 않는 이중 부정 해석을 강제하기 때문에 발생한다고 주장합니다.

의의 및 주장
본 논문은 에큐메니컬 관점이 고전적 추론과 직관주의적 추론 간의 상호작용에 대한 더 깊은 이해를 제공한다고 주장합니다. "연역적 (inferentialist)"(NE/NEK) 접근과 "일반적 (generalist)"(ECI) 접근을 비교함으로써, 저자들은 미묘하지만 중요한 개념적 차이를 강조합니다:

• 연역적 시스템(Prawitz/Krauss) 은 고전적 연산자에 대한 별도의 도입 규칙과 소거 규칙을 제공함으로써 직접적으로 연결사의 의미를 변경합니다.
• 일반적 시스템(ECI) 은 증명 수준을 변경하여 (라벨 $c$를 통한) 직관주의 논리에 고전적 증명 수단을 제공함으로써 간접적으로 연산자의 의미를 변경합니다.

저자들은 이러한 접근 방식이 명제 논리에서는 동등하지만 전칭 한정자의 존재 하에서는 분기된다고 결론지었습니다. 이러한 분기는 에큐메니컬 체계의 선택이 단순한 표기법의 선호가 아니라 한정자의 논리적 행동에 영향을 미친다는 것을 시사합니다. 본 논문은 에큐메니컬 관점이 고전적 추론이 필요한 정확한 지점을 식별하는 데 도움이 되며, 체계가 이러한 서로 다른 연역적 원칙에 주의를 기울여 구성된다면 고전적 원칙과 직관주의적 원칙이 서로를 붕괴시키지 않고 공존할 수 있음을 명확히 한다고 제시합니다.