보완
사실 검토 — 작은 수정 후 가능
2026-10-07 에 이 글에 적힌 사실(인용한 정리·결과·추측·장벽 서술)을 원 논문·서베이와 대조한 검토입니다. 아이디어가 옳은지가 아니라 사실이 정확한지와, 알려진 결과와 이 글의 제안·판단이 문장에서 갈려 있는지를 봤습니다.
판정: 작은 수정 후 가능
유계 산술 이론 이름(PV₁·S¹₂·T¹₂·APC₁), Buss 위계, Razborov·Krajíček·Pich–Santhanam·Aaronson 인용은 맞다. 고칠 것은 ① Ben-David–Halevi 정리의 서술이 두 군데 틀림 — 전제는 「PA 또는…」이 아니라 반드시 PA + 참인 Π₁ 문장 전부(PA+Π₁) 로부터의 독립이고, 귀결은 「준다항 시간」이 아니라 n^{α(n)} 크기 회로(α 는 역 아커만급으로 아주 느리게 자라는 함수), 균일 알고리즘으로는 「무한히 많은 긴 구간의 n 에서 n^{α(n)} 시간」이다 ② 요약·개요가 「약한 이론에서 P≠NP 형식화의 증명 불가능성을 보인 기존 결과」라고 써서, P≠NP 자체가 PV₁ 에서 증명 불가능하다고 알려진 것처럼 읽힌다 — 알려진 것은 조건부 결과(암호 가정)이거나 강한 형태의 하한 명제(준지수·근사 불가·공비결정 회로)에 대한 무조건 결과다.
확인한 사실
| 주장 | 사실 여부 | 근거 링크 |
|---|---|---|
| 유계 산술의 약한 이론 PV₁, S¹₂, T¹₂, APC₁ | 맞음 (PV: Cook 1975, S^i_2·T^i_2: Buss 1986, APC₁ = PV₁ + 다항 시간 함수에 대한 이중 약한 비둘기집 원리: Jeřábek) | https://www.scottaaronson.com/papers/indep.pdf (참고문헌 [9]~[11]) · https://arxiv.org/abs/2305.15235 |
| Buss 위계 — 각 이론이 다항시간 함수·다항 위계 각 층에 대응 | 맞음 (S^i_2 의 Σ^b_i-정의 가능 함수 = FP^{Σ^p_{i-1}}) | https://arxiv.org/abs/2305.15235 (서론) |
| 「약한 이론들에서 회로 하한이나 P≠NP 형식화의 증명 불가능성을 보인 기존 결과」 | 과장된 요약 — Razborov(1995)·Krajíček(1997)의 결과는 강한 의사난수 생성기·암호 가정 아래의 조건부. 무조건 결과는 Pich–Santhanam(STOC 2021: PV 는 NP 언어가 준지수 크기 공비결정 회로로 근사 불가능함을 증명 못함 — APC₁ 일부에도 성립), Li–Oliveira(STOC 2023) 등 강한 형태의 하한 명제에 대한 것. P≠NP 자체(표준 형식화)가 PV₁ 에서 증명 불가능한지는 미해결 | https://ora.ox.ac.uk/objects/uuid:4bb0ed7a-1983-4d95-8296-ab973094292e · https://arxiv.org/abs/2305.15235 |
| Razborov 의 자연 증명–유계 산술 연결 | 맞음 (「Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic」, Izvestiya Math. 59, 1995) | https://arxiv.org/abs/2305.15235 (관련 연구) |
| Krajíček 의 실행 가능 보간(feasible interpolation) | 맞음 (「Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic」, J. Symbolic Logic 62(2), 1997) | 같은 곳 |
| 「강한 의사난수 생성기가 존재하면 특정 유계 산술 이론은 초다항 회로 하한을 증명할 수 없다」 | 맞음 (Razborov 1995 의 유형 — 조건부로 정확히 표시돼 있음) | 같은 곳 |
| Ben-David–Halevi: 「P≠NP 가 PA(또는 참인 Π₁ 문장을 더한 체계)로부터 독립이라면 SAT 에 사실상 준다항 시간에 가까운 알고리즘적 귀결」 | 두 군데 틀림 — (1) 전제는 PA+Π₁(PA 에 참인 Π₁ 문장 전부를 더한 체계)로부터의 독립이다. PA 만으로부터의 독립은 이 귀결을 주지 않는다(Kreisel 보조정리로 두 체계의 증명 가능 재귀 함수가 같다는 점을 쓰는 논증). 「또는」이 아니다. (2) 귀결은 NP 가 크기 n^{α(n)} 회로를 가진다는 것(α 는 PA 에서 증명 가능 재귀인 임의의 무한 증가 함수의 역 — 예: 역 아커만)이고, 균일 판은 「무한히 많은 긴 구간의 n 에서 n^{α(n)} 시간」. 준다항(n^{polylog n})보다 훨씬 다항에 가깝다. 원 문헌: Ben-David–Halevi, Technion 기술 보고서(1991/92), Kurtz–O'Donnell–Royer 가 독립적으로 같은 관찰 | https://www.scottaaronson.com/papers/indep.pdf (5절) |
| Aaronson 의 독립성 서베이 | 맞음 (「Is P versus NP formally independent?」, Bulletin of the EATCS 81, 2003) | https://www.scottaaronson.com/papers/indep.pdf |
| 「유계 산술에서의 증명 불가능성은 증명 복잡도 하한과 동전의 양면」 | 대체로 맞음 — 보편 유계 문장(∀Π^b_1)에 대해 PV ↔ Extended Frege(Cook 1975), 유계 깊이 이론 ↔ 유계 깊이 Frege(Paris–Wilkie) 대응. 엄밀한 동치가 아니라 한 방향 번역이 기본이라 「밀접히 대응」 정도가 정확 | https://www.scottaaronson.com/papers/indep.pdf (참고문헌 [10]) |
| 「PV₁/S¹₂ 수준에서 확립된 증명 불가능성을 더 강한 유계 산술 이론, 나아가 PA의 단편으로」 | 표현 부정확 — 유계 산술 이론도 이미 PA 의 단편이다. 「유계가 아닌 귀납을 가진 단편(IΣ₁ 등)」으로 쓰는 것이 정확 | 정의 |
| 「직접 증명 경로가 상대화·자연 증명·대수화 장벽에 모두 막혀 있는 상황」 | 과장 — 세 장벽은 특정 성질의 기법을 막을 뿐이고, 세 장벽을 모두 넘은 결과(Williams 의 NEXP ⊄ ACC0)도 있다 | https://scottaaronson.blog/?p=472 |
| 글 안 순서 대조 — 그림 설명 「6단계는 그 경계를 더 강한 이론 쪽으로 올리는 공격 계획」 | 맞음 (6 = 경계 상승 시도 설계) | 본문 |
고칠 곳
- 원문(개요 2문단): 「"P≠NP가 PA(또는 참인 Π₁ 문장을 더한 체계)로부터 독립이라면 SAT에 대해 사실상 준다항 시간에 가까운 알고리즘적 귀결이 따른다"는 Ben-David–Halevi 류의 정리」
→ 제안: 「"P≠NP 가 PA+Π₁(PA 에 참인 Π₁ 문장을 모두 더한 체계)로부터 독립이라면 NP 는 크기 n^{α(n)}(α 는 역 아커만 함수처럼 아주 느리게 자라는 함수)인 회로를 가지며, 균일하게도 무한히 많은 긴 구간의 n 에서 SAT 를 n^{α(n)} 시간에 푸는 알고리즘이 있다"는 Ben-David–Halevi(와 Kurtz–O'Donnell–Royer)의 정리 — 알려진 독립성 증명 기법은 모두 PA+Π₁ 로부터의 독립을 보이므로, 그 기법으로 독립을 보이면 이 귀결이 따른다」 - 원문(핵심 정리 4): 「Ben-David–Halevi 류 정리(독립이라면 SAT 에 사실상 준다항 시간에 가까운 알고리즘적 귀결)」
→ 제안: 「Ben-David–Halevi 류 정리(PA+Π₁ 로부터 독립이라면 NP 에 n^{α(n)} 크기 회로 — 다항에 거의 붙은 알고리즘적 귀결)」 - 원문(핵심 정리 2·개요 1문단): 「유계 산술의 약한 이론들(PV₁, S¹₂, T¹₂, APC₁ 등)에서 회로 하한이나 P≠NP 형식화의 증명 불가능성을 보인 기존 결과」
→ 제안: 「유계 산술의 약한 이론들(PV₁, S¹₂, T¹₂, APC₁ 등)에서 회로 하한 명제의 증명 불가능성을 보인 기존 결과 — 암호 가정 아래의 조건부 결과(Razborov 1995, Krajíček 1997)와, 준지수·근사 불가·공비결정 회로 같은 강한 형태의 하한 명제에 대한 무조건 결과(Pich–Santhanam 2021 등). P≠NP 의 표준 형식화가 PV₁ 에서 증명 불가능한지는 아직 모른다」 - 원문(진행 방법 6): 「더 강한 유계 산술 이론, 나아가 PA의 단편으로 끌어올리기 위한」
→ 제안: 「더 강한 유계 산술 이론, 나아가 유계가 아닌 귀납을 가진 PA 단편(IΣ₁ 등)으로 끌어올리기 위한」 - 원문(가치 1): 「직접 증명 경로가 상대화·자연 증명·대수화 장벽에 모두 막혀 있는 상황에서」
→ 제안: 「알려진 직접 증명 기법 대부분이 상대화·자연 증명·대수화 장벽에 걸리는 상황에서」 - 원문(가치 3): 「"독립이라면 실제 세계에서는 P=NP에 준하는 귀결이 따른다"는 유형의 결과」
→ 제안: 「"PA+Π₁ 로부터 독립이라면 NP 가 다항에 거의 붙은 n^{α(n)} 크기 회로를 가진다"는 유형의 결과」
넣을 수 있는 문헌 목록 (제안)
- S. Buss, Bounded Arithmetic, Bibliopolis, 1986.
- S. Cook, Feasibly constructive proofs and the propositional calculus, STOC 1975.
- A. Razborov, Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic, Izvestiya Math. 59, 1995.
- J. Krajíček, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic 62(2), 1997.
- E. Jeřábek, Approximate counting in bounded arithmetic, J. Symbolic Logic 72(3), 2007.
- J. Pich, R. Santhanam, Strong co-nondeterministic lower bounds for NP cannot be proved feasibly, STOC 2021.
- J. Li, I. Oliveira, Unprovability of strong complexity lower bounds in bounded arithmetic, STOC 2023 (arXiv 2305.15235).
- S. Ben-David, S. Halevi, On the independence of P versus NP, Technion 기술 보고서, 1991/1992.
- S. Aaronson, Is P versus NP formally independent?, Bulletin of the EATCS 81, 2003.
고칠 곳을 반영하고 글 아래에 참고 문헌(위 표의 근거)을 붙이면 「검토 완료」로 바꿀 수 있습니다.
이 글에 단 답 0
아직 없습니다.