지난 한 달 동안 일본어로 된 논리학 입문서를 하루에 한 절씩 읽으며, 각 장의 증명을 짧은 Haskell 코드로 옮기는 작업을 병행해 왔다. 2000년에 나온 명제논리·술어논리 교과서가 내 도구들이 왜 어떤 건 멈추고 어떤 건 안 멈추는지에 대한 생각을 바꿔놓을 줄은 몰랐다. 그런데 7장쯤에서 정확히 그런 일이 일어났다.

일본어와 코드를 걷어내고, 논증의 뼈대만 적어본다.

명제논리가 공짜로 주는 것

명제논리 — “그리고”, “또는”, “아니다”, “만약 ~라면”을, 더 이상 쪼갤 수 없는 원자적 문장에 적용하는 논리 — 는 처음엔 초능력처럼 보이는 무언가를 준다. 이 언어로 던질 수 있는 어떤 질문이든(“이 논리식은 항진명제인가”, “이 두 논리식은 동치인가”, “이 논증은 전제로부터 타당하게 도출되는가”) 무차별 대입으로 해결할 수 있다. 원자 명제들에 참/거짓을 배정하는 모든 조합을 나열하고 각 행을 확인하면 끝. 원자 명제가 n개면 행은 2ⁿ개다. 표는 유한하고, 절차는 반드시 끝나며, 언제나 명확한 예/아니오를 준다. 이것이 결정가능성이고, 명제논리는 이걸 공짜로 갖고 있다.

왜 이게 가능한지 잠깐 생각해볼 가치가 있다. 진리표가 주는 건 가능한 경우의 공간 전체를 훑는 전수 탐색이고, 그게 작동하는 이유는 오직 그 공간이 유한하기 때문이다. 모든 경우를 나열할 수 있는 순간, 테스트는 증명이 된다 — “테스트는 버그의 존재는 보여줄 수 있어도 부재는 보여줄 수 없다”는 데이크스트라의 유명한 말과, 이 교과서가 자신 있게 내미는 2ⁿ행짜리 표 사이의 긴장은, 둘이 같은 사실을 반대쪽에서 말하고 있다는 걸 깨닫는 순간 사라진다. 데이크스트라의 경고는 무한한 입력 공간에 관한 것이고, 거기서 테스트 스위트는 필연적으로 표본일 수밖에 없다. 진리표는 표본이 아니다. 전수조사다.

문제는, 결코 가볍지 않은 문제인데, 이 완전함이 야심의 부족에서 온다는 것이다. 명제논리는 개체에 대해, 개체의 속성에 대해, 개체들 사이의 관계에 대해 아무것도 말할 수 없다. “모두가 누군가를 사랑한다”도 “A에서 B로 가는 경로가 있다”도 표현할 수 없다. 그 의미론적 내용 전체가 유한한 진리값 집합에서 진리값으로 가는 함수 하나에 담겨 있다 — 즉 쓸 수 있는 논리식은 무한히 많아도, n개의 원자 명제가 표현할 수 있는 진짜로 서로 다른 의미는 2^(2ⁿ)개뿐이다. 구문은 무한하고, 의미는 유한하다. 이 간극이 바로 전수 검사를 가능하게 하는 여유분이다.

바닥이 꺼지는 지점

술어논리는 양화사(“모든”, “어떤”)와 개체들 사이의 관계를 더하는데, 여기서 공짜 점심이 끝난다. “모든 x에 대해 어떤 y가 존재하여 R(x,y)” — 그래프의 도달가능성이나 경로, 관계의 연쇄에 대한 주장들의 뿌리에 있는 이 형식 — 을 말할 수 있는 언어가 되는 순간, 명제논리의 유한한 의미론적 내용은 사라진다. 한 개체가 다른 개체들과 맺는 관계는, 진리값 배정처럼 유한한 표로 압축할 수 없다.

흥미로운 건 이게 단순히 정리의 진술로서만이 아니라 절차적으로 어떻게 드러나는가이다. 교과서는 타당성을 검증하는 증명 탐색 절차(타블로 방법)를 다루는데, 여기에는 구조적 비대칭이 내장되어 있다 — 존재양화사를 다루는 규칙은 논리식당 한 번만 발동되고 끝난다. 새로운 개체 하나를 도입하면 그걸로 끝. 전칭양화사를 다루는 규칙은, 증명 중에 등장하는 어떤 개체에 대해서도, 나중 단계에서 생성된 개체를 포함해서, 몇 번이고 다시 적용될 수 있다. 명제논리에서는 이 비대칭이 보이지 않는다 — “개체”란 그저 진리값이고 2ⁿ개뿐이라서, 탐색은 반드시 바닥을 친다. 완전한 술어논리에서는 “모든 x에 대해 어떤 y가 존재하여 R(x,y)” 같은 논리식이 연쇄를 일으킬 수 있다 — 존재 요구를 만족시키려 개체를 도입하고, 거기에 전칭 규칙을 적용하면 새로운 존재 요구가 나오고, 또 개체를 도입하고, 또 전칭 규칙을 적용하고 … 끝이 보장되지 않는다. 이것은 Prolog 질의가 재귀적 절을 만족시키려다 영원히 돌아오지 않는 것과 구조적으로 완전히 같은 모양이고, 이건 우연이 아니다 — 자동 정리 증명기는 바로 이런 종류의 탐색 위에 세워져 있다.

이건 특정 증명법의 결함이 아니다. 알론조 처치와 앨런 튜링이 1936년, 각자 완전히 다른 형식적 도구를 써서(처치는 람다계산, 튜링은 오늘날 튜링 기계라 부르는 것) 독립적으로 증명한 무언가의 증상이다 — “이 술어논리 논리식은 타당한가”라는 질문은, 모든 입력에 대해 반드시 정지하는 것이 보장된 알고리즘으로는 답할 수 없다. 이것이 힐베르트의 결정문제(Entscheidungsproblem)였고, 서로 다른 두 방향에서 도달한 답은 둘 다 ‘아니오’였다1. 이 결과를 다루는 장의 제목은 일부러 안심시키려는 듯 “논리학자들을 탓하지 말라”이다 — 요점은 이것이 영리함의 부족이 아니라는 것. 더 똑똑한 탐색 절차로도 이걸 고칠 수 없다. 이 한계는 알고리즘이라는 부류가 할 수 있는 것에 대한 이미 증명된 수학적 사실이지, 아직 시도되지 않은 틈이 아니기 때문이다.

살아남는 비대칭

결정가능성 대신 얻는 건 반결정가능성이다. 논리식이 타당하다면, 어떤 탐색 절차든 결국 그것을 확인하고 정지하는 것이 보장된다. 타당하지 않다면, 그걸 알려주는 것이 보장된 절차는 존재하지 않는다 — 영원히 돌 수도 있고, 오랫동안 증명을 찾지 못한 채 돌고 있는 탐색은 “이건 타당하지 않다”와 “증명이 아직 어딘가에 있다”를 구별할 방법을 주지 않는다. 괴델의 완전성 정리가 ‘예’ 쪽을 보장해준다 — 의미론적으로 타당한 논리식의 집합은 재귀적으로 열거가능하므로, 후보 증명들을 체계적으로 나열하고 검사해 나가면 존재한다면 언젠가는 반드시 드러난다2. ‘아니오’ 쪽을 구제해줄 비슷한 보장은 없고, 이건 놓친 게 아니다 — 정지 문제와 증명 가능하게 동치다. “이 프로그램이 정지하는가”를 “이 논리식이 타당한가”로 부호화할 수 있고, 그 형식은 일반적인 타당성 판별기가 있다면 정지성 판별도 가능해짐을 보여준다 — 그리고 그건 이미 불가능하다고 알려져 있다.

나는 이게 좌절스럽다기보다 납득이 갔다. 이름 없던 것에 이름이 붙었다. 충분히 표현력이 높은 타입 시스템(고차 다형성, 종속 타입)에서의 타입 추론은 멈춰버릴 수 있다. SMT 솔버는 멈춰버릴 수 있다. 충족가능성 문제로 환원되는 패키지 버전 해결기는 멈춰버릴 수 있다. 각 경우마다 그 아래엔 설계 선택이 숨어 있다 — 도구가 정지를 보장할 만큼 작은 논리의 부분집합 안에 머물러 표현력을 내주는가, 아니면 표현력을 취하고 실무에서는 답이 타임아웃이 될 수 있음을 받아들이는가. 타입 시스템 설계자들은 자동 추론이나 논리 프로그래밍 세계보다 전자를 선택하는 경향이 더 강해 보이는데, 왜 문화가 그렇게 갈렸는지, 분야 전체에 걸쳐 일관되지 않은지는 아직 자신 있게 말할 수 없다. “가끔 컴파일을 거부하는 타입 검사기”가 “가끔 빌드를 멈춰버리는 타입 검사기”보다 견딜 만하다는 것뿐일 수도 있다.

교과서가 시종일관 조심스럽게 다루는 또 한 가지가 있다 — 튜링 기계와 람다계산이 둘 다 “계산”이라는 비형식적이고 이론 이전의 개념을 올바르게 형식화한다는 처치-튜링 테제가, 왜 정리가 아니라 테제라 불리는지에는 진짜 이유가 있다. 독립적으로 발명된 두 형식 체계가 서로 동치라는 건 정리이고, 수학 안에서 증명할 수 있다. 이 공유된 개념이 “무엇이 계산 가능한가”라는 모호한 인간적 개념의 올바른 형식화라는 것은 수학으로 검증할 수 있는 게 아니다. 모호한 인간적 개념은 애초에 수학적 대상이었던 적이 없기 때문이다. 이건 세계에 관한 주장이고, 그 이후의 모든 계산 형식화 시도들 — 재귀 함수, 레지스터 기계, 세포 자동자 — 이 같은 동치류에 도달했다는 사실로 뒷받침되지만, 그럼에도 솔직히 말하면 증명이라기보다는 귀납적 주장으로 남아 있다. 교과서가 이 선을 흐리지 않고 굳이 긋는다는 점이 마음에 든다. 증명된 것과 그저 “아직 반증되지 않은” 것 사이의 경계는, 확인이 쌓일수록 미끄러지기 쉬워지는 바로 그런 종류의 구분이기 때문이다.

열린 질문

지금 내가 붙들고 있는 건 기술적이라기보다 실무적인 질문이다. 어떤 문제가 이런 벽 너머에 있다는 걸 알 때 — 그저 어려운 게 아니라 정말로 결정 불가능하다는 걸 — 취할 수 있는 수는 딱 두 가지로 보인다. 결정가능한 부분집합에 들어갈 때까지 언어를 줄이거나, 표현력을 유지한 채 휴리스틱·깊이 제한·타임아웃으로 비정지의 위험을 실무에서 관리하거나. 둘 다 정당한 엔지니어링 선택이고, 서로 다른 커뮤니티들이 내가 딱히 짚을 수 있는 논거 없이 관습적으로 반대되는 쪽에 걸어온 것처럼 보인다. 여기 유일한 정답이 있다고는 생각하지 않지만 — 왜 그 두 문화가 그렇게 갈렸는지, 분야가 우연히 그렇게 자라난 것 이상으로 누군가 실제로 형식화한 적이 있는지 궁금하다.

  1. Entscheidungsproblem. Wikipedia. Accessed 2026-08-11. ↩

  2. Gödel’s completeness theorem. Wikipedia. Accessed 2026-08-11. ↩