1+1=2를 천 페이지로 증명한 책이, 프로그래머에게 낯설지 않은 이유

『프린키피아 마테마티카』는 화이트헤드와 러셀이 1910년부터 펴낸 수학기초론 저작으로, 흔히 "1+1=2를 증명하는 데 천 페이지가 걸린 책"이라는 농담과 함께 회자된다. 이 방대함은 저자들의 미숙함이 아니라 의도된 설계다. 서문이 강조하듯, 증명은 어떤 전제도 말없이 몰래 쓰이는 일이 없도록 고통스러울 만큼 세밀하게 전개된다. 목표는 아주 기초적인 개념 몇 가지를 제시하고, 오직 그것들만으로 수학 전체를 떠받칠 수 있음을 보이는 것이었다. 오카사키(Oleg Kiselyov)가 정리한 1장 독해 노트는, 정작 중요한 것은 끝없는 증명이 아니라 서문과 1장에 담긴 기본 개념과 그 설정 방식이라고 짚는다.

오늘이라면 증명은 정리 증명기로 갔을 것

노트의 관찰 하나가 특히 실무자의 시선을 끈다. 만약 프린키피아가 오늘 출간된다면 그 방대한 증명들은 본문에서 빠져 별도의 부록으로, 혹은 정리 증명기(theorem prover)로 넘겨졌으리라는 것이다. 이는 단순한 상상이 아니라 현대 소프트웨어 검증의 실제 작업 방식과 정확히 겹친다. 사람은 기본 개념과 구조를 설계하고, 기계적으로 반복되는 세부 증명은 자동화 도구에 위임한다. 러셀과 화이트헤드가 손으로 감당하려 했던 "숨은 전제 제거"라는 과제가, 지금은 형식 검증 도구가 담당하는 바로 그 일이다.

프로그래밍 언어 이론이 이미 여기 있었다

노트는 프린키피아의 용어와 현대 개념 사이의 대응을 짚는데, 이 지점이 개발자에게 가장 직접적이다. 프린키피아가 '가현 변수(apparent variable)'라 부른 것은 오늘날의 속박 변수(bound variable)이고, '실 변수(real variable)'는 자유 변수(free variable)에 해당한다. 저자들은 정적분을 예로 들어 속박 변수와 알파 동치(alpha-equivalence)를 설명하는데, 노트는 이를 인상적이라 평한다. 적분 변수의 이름을 바꿔도 값이 변하지 않는다는 사실은, 람다 대수에서 변수 이름을 바꿔도 의미가 같다는 알파 변환과 정확히 같은 직관이기 때문이다. 노트가 "람다 대수의 계보는 길다"고 말하며 라이프니츠의 통찰을 언급하는 이유가 여기 있다. 변수 포획을 피하려 씨름해 본 개발자라면, 이 문제가 100년도 더 된 발상의 후예임을 알게 된다.

또 하나 눈여겨볼 대목은, 프린키피아의 '임의의(for any)'를 뜻하는 도식적 공식이 프린키피아 논리에서 대응하는 전칭 한정 공식과 동치임에도, 저자들이 둘을 굳이 구별하려 했다는 점이다. 이 논리는 훗날 정제되어 오늘의 1차 논리(First-Order Logic)가 되었다. 도식 규칙과 전칭 명제를 구별하려는 이 태도는, 메타 수준의 규칙과 대상 수준의 명제를 뒤섞지 않으려는 신중함으로, 형식 체계를 다뤄본 사람에게는 익숙한 감각이다.

함수 같지만 함수가 아닌 것

노트는 러셀이 1905년 논문 「지시에 관하여(On denoting)」에서 세운 기술 이론과의 연결도 언급한다. 프린키피아는 이항 관계로부터 유도되는 함수를 '기술적 함수(descriptive functions)', 곧 오늘날 말하는 확정 기술(definite description)이라 부른다. 자크 카레트(Jacques Carette)의 지적에 따르면, 프린키피아는 이미 1910년에 '확정 기술'과 '명시적 함수'의 차이를 예견하고 있었다. 그 예로 든 것이 해석적 연속(analytic continuation)이다. 이는 함수적이면서도 함수는 아닌 과정으로, 일정한 선택이 개입하기 때문이다. 결과가 유일하게 정해지지 않고 경로나 선택에 의존하는 연산을 어떻게 다룰지는, 참조 투명성과 결정성을 따지는 오늘의 프로그래밍 논의와도 통한다.

노트는 같은 시기 브라우어의 저작도 나왔음을 덧붙이지만, 당시 그의 글은 수학자에게도 난해했으며 직관주의 대 고전주의 논쟁이 본격화된 것은 헤르만 바일 이후라고 선을 긋는다. 그 구성주의의 일부는 다시 30년 앞선 크로네커까지 거슬러 올라간다고 카레트는 짚는다. 다만 이 대목들은 노트에서 스쳐 지나가는 배경일 뿐, 깊이 파고들지는 않는다.

이 노트는 프린키피아 전체의 해설도, 체계적 논문도 아니다. 1장을 읽으며 남긴 단상과 몇몇 전문가의 논평을 엮은 것에 가깝다. 그럼에도 실무자에게 주는 값은 분명하다. 우리가 매일 쓰는 속박 변수, 알파 동치, 1차 논리, 정리 증명기 같은 도구들이 어느 날 갑자기 발명된 게 아니라, 수학 기초를 향한 한 세기 전의 집요한 시도에 이미 그 골격이 담겨 있었다는 사실이다. 낡은 텍스트를 현대의 어휘로 다시 읽을 때, 오래된 문제와 지금의 문제가 같은 뿌리를 공유함을 확인하게 된다.