Generalized Decidability via Brouwer Trees

당신이 미스터리를 풀기 위해 노력하는 탐정이라고 상상해 보세요. 컴퓨터 과학의 세계에서 우리는 보통 미스터리를 세 가지 바구니로 분류합니다: 결정 가능(Decidable) (우리가 빠르게 답을 찾을 수 있음), 반결정 가능(Semidecidable) (답이 "예"라면 찾을 수 있지만, "아니오"라면 영원히 기다려야 할 수도 있음), 그리고 결정 불가능(Undecidable) (우리는 전혀 해결할 수 없음).

하지만 어떤 미스터리는 다른 것보다 "더 많이" 반결정 가능한 것이라면 어떨까요? 어떤 "예"라는 답은 찾는 데 시간이 조금 더 걸리겠지만, 여전히 영원히 걸리지는 않는다면요?

이것이 바로 톰 데 용(Tom de Jong), 니콜라이 크라우스(Nicolai Kraus), 아레프 모하마드자데(Aref Mohammadzadeh), 그리고 프레드릭 노드발 포스베르그(Fredrik Nordvall Forsberg)가 새로운 논문에서 탐구하고 있는 내용입니다. 그들은 **브라우어 트리 서수(Brouwer tree ordinals)**라고 불리는 특별한 숫자 체계를 사용하여, "예"라는 답을 찾는 데 정확히 얼마나 오래 걸리는지를 측정하는 방법을 제안합니다. 이것을 일반적인 숫자 1, 2, 3이 아니라, 무한함을 훨씬 뛰어넘는 마법 같은 시간 단계의 사다리로 생각해보세요.

시간의 마법 사다리

그들의 프레임워크에서, 그들은 단순히 "풀 수 있다"라고 말하지 않습니다. 대신, "그것은 $\alpha$-결정 가능하다"라고 말하며, 여기서 $\alpha$는 그들의 마법 사다리의 특정 칸을 의미합니다.

• 레벨 1 (결정 가능): 어떤 문제가 1-결정 가능하다는 것은, 유한한 단계 내에 답을 찾거나(또는 그것이 불가능함을 증명하거나) 할 수 있음을 의미합니다. 이는 어떤 숫자가 소수인지 확인하는 것과 같습니다. 그냥 숫자를 세어 올라가면 결국 확실히 알게 됩니다.
• 레벨 $\omega + 1$ (반결정 가능): 어떤 문제가 $(\omega + 1)$-결정 가능하다는 것은, 만약 답이 "예"라면 $\omega$ 단계 내에 답을 찾을 것이라는 뜻입니다. 하지만 $\omega$는 일반적인 숫자가 아닙니다. 그것은 "영원히 세는 것"을 나타냅니다. 따라서 답이 "예"라면 당신은 결국 그것을 찾겠지만, 답이 "아니오"라면 당신은 멈추지 않고 영원히 숫자를 세고 있을지도 모릅니다. 이것이 고전적인 "반결정 가능"의 정의입니다.

저자들은 이 새로운 시스템이 기존의 것과 완벽하게 부합한다는 것을 증명합니다. 만약 문제가 "결정 가능"하다면, 그것은 칸 1에 들어맞습니다. 만약 "반결정 가능"하다면, 그것은 칸 $\omega + 1$에 들어맞습니다. 하지만 마법은 그 사이 혹은 그 훨씬 높은 곳에 있는 칸들에 대해서도 이제 이야기할 수 있다는 점입니다.

쌍둥이 소수의 미스터리

이것이 어떻게 작동하는지 보여주기 위해, 그들은 유명한 수학 퍼즐인 **쌍둥이 소수 추측(Twin Prime Conjecture)**을 사용합니다. 이 문제는 다음과 같이 묻습니다: "숫자를 아무리 높이 세더라도, 항상 두 숫자 차이가 나는 소수 쌍(예: 3과 5, 또는 11과 13)이 존재하는가?"

• 특정한 하나의 쌍이 존재하는지 확인하는 것은 쉽습니다 (결정 가능).
• 특정 숫자 이상의 어떤 쌍이라도 존재하는지 확인하는 것은 반결정 가능합니다 (계속 찾아보면 됩니다. 만약 하나를 발견하면 멈춥니다).
• 하지만 큰 질문은 이것이 모든 숫자에 대해 참인지 묻는 것입니다.

저자들은 이 특정한 질문이 $\omega^2$-결정 가능하다는 것을 보여줍니다. $\omega$를 하나의 무한한 선이라고 상상해 보세요. $\omega^2$는 그런 무한한 선들이 층층이 쌓여 있는 것과 같습니다. 이는 만약 쌍둥이 소수 추측에 대한 반례가 존재한다면, 당신은 그것을 찾을 수 있겠지만, 그 시간은 무한한 선들이 쌓인 무한한 스택을 통과해 걷는 것과 맞먹는 시간만큼 걸릴 수도 있다는 것을 의미합니다.

그들은 또한 이러한 문제들을 결합했을 때 어떤 일이 일어나는지도 살펴보았습니다:

• AND (그리고): 두 문제가 $\alpha$-결정 가능하다면, 그들의 "AND"(둘 다 참이어야 함) 역시 $\alpha$-결정 가능합니다. 이는 두 개의 상자를 체크하는 것과 같습니다. 만약 동일한 시간 제한 내에 둘 다 체크할 수 있다면 성공입니다.
• OR (또는): 이것은 더 까다롭습니다. 두 문제가 있을 때, 그들의 "OR"(둘 중 하나가 참임)은 시간 제한이 충분히 작을 때만(구체적으로 레벨이 $\omega \cdot k + n$ 같은 경우) 결정 가능함이 보장됩니다. 만약 시간 제한이 너무 커지면, "OR"는 그들의 규칙을 깨뜨릴 수도 있습니다.

"선택" 문제

여기서부터 정말 흥게로워집니다. 저자들은 만약 무한한 수의 "반결정 가능"한 문제들(예를 들어, 모든 시작 숫자에 대해 쌍둥이 소수 추측을 확인하는 것)을 결합하고 싶다면, 벽에 부딪히게 된다는 것을 발견했습니다. **가산 선택 공리(Countable Choice)**라는 특별한 수학적 규칙 없이는, 그 결합된 결과가 반결정 가능하다고 증명할 수 없습니다.

사실, 만약 그 규칙 없이도 그것을 증명할 수 있다면, 그것은 다른 근본적인 논리 법칙들을 깨뜨릴 것이라고 그들은 증명했습니다. 그래서 그들은 무한한 조합에 대해 수학을 매끄럽게 작동시키려면, 가산 선택을 가정해야 한다고 제안합니다.

하지만 그들은 또 다른 해결책을 찾아냈습니다! 그들은 **시에르핀스키-반결정 가능(Sierpiński-semidecidable)**이라는 다른 종류의 "반결정 가능"을 살펴보았습니다. 이것은 원래의 것보다 약간 더 약한 버전이지만, 가산 선택 규칙 없이도 무한한 리스트를 결합할 수 있는 방식입니다. 이는 마치 빛이 아주 밝지는 않지만, 가산 선택이라는 배터리 없이도 켤 수 있는 다른 종류의 손전등과 같습니다.

해결하지 못한 것들

이 논문이 무엇을 하지 않는지 아는 것도 중요합니다. 저자들은 자신들이 쌍둥이 소수 추측을 해결한 것이 아니라는 점을 명확히 하고 있습니다. 그들은 단지 이 새로운 측정 도구가 어떻게 작동하는지 보여주기 위한 장난감 예시로 이 문제를 사용했을 뿐입니다.

그들은 또한 자신들의 사다리가 아직 전체적인 모양을 갖추지 못했다는 점도 인정합니다. 그들은 만약 어떤 문제가 칸 $\alpha$에 있고 다른 문제가 칸 $\beta$에 있으며, $\alpha$가 $\beta$보다 낮다면, $\alpha$에 있는 문제도 $\beta$에서도 풀 수 있어야 한다고 추측합니다. 하지만 그들은 아직 이 사다리의 모든 칸에 대해 이것을 증명하지 못했습니다. 이것은 확정된 사실이 아니라 "추측"입니다.

결론

이 논문은 수학과 컴퓨팅에서 "예"라는 답을 찾는 것이 얼마나 어려운지를 이야기하는 새로운 방법을 제시합니다. 단순히 "찾을 수 있다" 또는 "찾을 수 없다"라고 말하는 대신, 그들은 무한한 단계로 이루어진 정밀한 자를 제공합니다. 그들은 이 자가 우리가 이미 알고 있는 것들(결정 가능 및 반결정 가능)에 어떻게 적용되는지 증명했으며, 쌍둥이 소수 추측과 같은 복잡한 문제를 측정하여 그것이 $\omega^2$라는 특정하고 측정 가능한 높이에 위치함을 찾아냈습니다.

또한 그들은 이 자가 강력하지만 한계가 있다는 점도 보여주었습니다: 무한한 문제의 리스트를 결합하려면 (시에르핀스키-반결정 가능성을 사용하는 대신에는) 가산 선택이라는 특정 가정이 필요합니다.

이 모든 과정은 **큐비컬 아가다(Cubical Agda)**라는 컴퓨터 프로그램 안에서 구축되고 검증되었습니다. 이 프로그램은 그들의 논리 단계 하나하나가 완벽하도록 보장하는 매우 엄격한 심판 역할을 합니다. 따라서 아이디어는 새롭고 흥미롭지만, 그 수학적 토대는 매우 견고합니다.