A proof complexity conjecture and the Incompleteness theorem

논문 개요

이 논문은 증명 복잡성 (Proof Complexity) 이론의 오래된 추측인 **"모든 증명 시스템에 대해 어려운 (hard) 생성기가 존재한다"**는 가설을 연구합니다. 저자 Jan Krajíček 은 일차 논리 (first-order logic) 의 구문 (syntax) 을 형식화할 수 있는 공리계 (sound first-order p-time theory) $T$를 기반으로 특정 함수 $g_T$를 구성하고, 이를 통해 괴델의 불완전성 정리를 유도합니다. 또한, 이 구성을 명제 논리 (propositional logic) 수준으로 축소하여 증명 복잡성, 계산 복잡성, 그리고 난해성 (hardness) 간의 관계를 규명하는 새로운 삼분법 (trichotomy) 결과를 제시합니다.

---

1. 연구 문제 (Problem)

• 핵심 추측: 모든 입력을 1 비트 늘리는 다항 시간 (p-time) 함수 $g: \{0, 1\}^* \to \{0, 1\}^*$가 존재하며, 그 치역 (range) 이 모든 무한한 NP 집합과 교차한다는 것입니다. 즉, $g$의 치역은 모든 증명 시스템에 대해 "어렵다 (hard)"는 의미입니다.
• 연구 목표:
  1. 일차 논리 이론 $T$를 사용하여 위와 같은 함수 $g_T$를 구성하고, 이것이 괴델의 불완전성 정리를 어떻게 증명하는지 보여주는 것.
  2. 이 구성을 명제 논리 버전으로 변환하여, 위 추측이 성립하지 않을 경우 어떤 복잡성 이론적 결론이 도출되는지 분석하는 것.

---

2. 방법론 (Methodology)

2.1 일차 논리 이론 기반 구성 (Section 2)

• 기반 이론: Buss 의 $S^1_2$ 이론을 기반으로 하며, 이를 포함하는 공리계 $T$ ($T \supseteq S^1_2$) 를 가정합니다. $T$는 공리계가 유한하며, $N$ (자연수) 에서 참인 (sound) p-time 이론입니다.
• 함수 $g_T$의 정의:
  • 입력 $u$ (길이 $n$) 에 대해, $u$의 접두사 (prefix) 인 논리식 $\Phi$ (자유 변수 $x$ 하나, 길이 $\le \log n$) 를 찾습니다.
  • $\Phi$가 없으면 $0$을 출력합니다.
  • $\Phi$가 있으면, $w \in \{0, 1\}^{c+1}$ ($c=|\Phi|+1$) 에 대해 다음 문장 $\Phi_w$의 $T$-증명 (크기 $\le \log n$) 을 탐색합니다:
    $$\exists y \forall x > y (\Phi(x) \to \neg(w \subseteq_e x))$$
    (즉, $\Phi$로 정의된 집합이 $w$로 시작하는 문자열을 무한히 많이 포함하지 않는다는 명제)
  • 모든 $w$에 대해 증명이 발견되면 $0$을 출력하고, 그렇지 않으면 첫 번째로 증명이 발견되지 않는$w_0$를 찾아$w_0 u_0$를 출력합니다 ($u = \Phi u_0$).
• 논리 구조: $T$가 완전 (complete) 하고 정합 (sound) 하다면, $g_T$의 치역은 $\{0, 1\}^*$의 모든 무한한 정의 가능한 부분집합과 교차해야 합니다. 그러나 $g_T$의 치역의 여집합은 무한하고 정의 가능하므로, 이는 모순입니다. 따라서 $T$는 불완전해야 합니다.

2.2 명제 논리 버전 구성 (Section 3)

• 접근: 일차 논리의 증명 대신 명제 논리의 증명 길이 하한 (lower bounds) 을 사용합니다.
• 전환 (Translation): $\Sigma^b_1$-공식 $\Phi$와 $w$에 대해, $\Phi_w$에 해당하는 명제 논리 공식 $\varphi_{n,w}$를 구성합니다.
• 가정:
  1. p-최적 명제 증명 시스템 (p-optimal propositional proof system) 이 존재하지 않는다.
  2. $E \subseteq P/poly$ (즉, $E$가 다항 회로 크기를 가진 회로로 계산 가능).
• 함수 $h_P$의 구성:
  • 위 두 가정이 성립한다고 가정하고, $E \subseteq P/poly$를 이용해 증명 시스템 $P$의 증명을 회로 (circuit) 의 진리표 (truth-table) 로 근사합니다.
  • $g_T$와 유사하게, $\varphi_{n,w}$에 대한 $P$-증명을 회로의 진리표 탐색을 통해 찾습니다.
  • 증명이 발견되지 않는 $w_0$를 찾아 출력을 생성합니다.

---

3. 주요 기여 및 결과 (Key Contributions & Results)

3.1 괴델의 제 1 불완전성 정리의 새로운 증명

• 정리 2.2 및 Corollary 2.3: 정합적이고 p-time 인 이론 $T \supseteq S^1_2$는 완전할 수 없습니다.
• 의미: 함수 $g_T$의 치역이 모든 무한한 정의 가능 집합과 교차한다는 가정은 모순을 야기하므로, $T$는 $g_T$의 치역 여집합에 대한 어떤 진리 명제도 증명할 수 없습니다. 이는 괴델의 불완전성 정리를 증명 복잡성 관점에서 재해석한 것입니다.

3.2 삼분법 정리 (The Trichotomy Theorem)

정리 3.1: 다음 세 명제 중 적어도 하나는 참이어야 합니다.

1. p-최적 명제 증명 시스템이 존재하지 않는다. (이는 시간 최적의 증명 탐색 알고리즘이 존재하지 않음을 의미함)
2. $E \not\subseteq P/poly$: 지수 시간 계층 $E$가 다항 회로 크기 클래스에 포함되지 않는다.
3. 하위 지수 시간 함수 $h$의 존재: 모든 입력을 1 비트 늘리는 함수 $h$가 존재하며, 이는 하위 지수 시간 ($2^{O((\log n)^{\log \log n})}$) 에 계산 가능하고, 그 치역이 모든 무한한 NP 집합과 교차한다.

• 해석: 만약 1 번과 2 번이 모두 거짓이라면 (즉, 최적 증명 시스템이 있고 $E \subseteq P/poly$라면), 3 번이 성립해야 합니다. 이는 NP 집합을 피하는 (avoiding) 매우 효율적인 함수가 존재하지 않음을 시사합니다.

---

4. 의의 및 중요성 (Significance)

1. 증명 복잡성과 불완전성 이론의 연결: 괴델의 불완전성 정리를 증명 복잡성 (proof complexity) 의 언어, 즉 "증명 시스템의 효율성"과 "함수 생성기의 난해성"으로 재해석하여 두 분야 간의 깊은 연관성을 보여줍니다.
2. NP vs coNP 및 증명 시스템의 한계: 만약 3 번의 조건이 성립한다면 (모든 NP 집합과 교차하는 함수 존재), 이는 NP $\neq$ coNP 를 암시할 수 있습니다. 또한, p-최적 증명 시스템의 부재는 증명 탐색 알고리즘의 근본적인 한계를 나타냅니다.
3. 개방 문제 (Open Problem): 저자는 특정 이론 $T$에 대해 $g_T$가 실제로 모든 무한 NP 집합과 교차하는지 (즉, 모든 증명 시스템에 대해 어려운지) 는 여부는 여전히 미해결 문제 (Problem 2.4) 로 남겼습니다. 이 문제가 해결된다면 NP 와 coNP 의 관계에 대한 결정적인 통찰을 제공할 수 있습니다.
4. 복잡성 계층의 교차점: 이 논문은 $P/poly$, $E$, 증명 시스템의 최적성, 그리고 NP 집합의 구조가 서로 어떻게 얽혀 있는지를 보여주는 강력한 연결 고리를 제시합니다.

결론

Jan Krajíček 의 이 논문은 증명 복잡성 생성기 (proof complexity generator) 에 대한 추측을 일차 논리 이론을 통해 형식화하고, 이를 통해 괴델 불완전성 정리를 유도한 후, 이를 명제 논리로 축소하여 복잡성 이론의 핵심 미해결 문제들 (최적 증명 시스템 존재 여부, $E$와 $P/poly$의 관계 등) 과의 논리적 필연성을 규명했습니다. 이는 계산 복잡성 이론의 여러 핵심 가설들이 서로 긴밀하게 연결되어 있음을 보여주는 중요한 연구입니다.