1. 맞는 것과 틀린 것을 가려내는 일
수학 속 명제는 결국 "이것이 맞는가, 틀린가"를 가려내는 행위이다. 2 + 2는 4이지 5가 아니다. 삼각형의 내각의 합은 180도이지 200도가 아니다. 이 구분이 있기 때문에 수학 속의 명제는 쓸모가 있다. 다리가 무너지지 않을 만큼 튼튼한지, 비행기 날개가 버틸 수 있는지, 비밀번호가 안전한지. 이 모든 판단은 "맞는 것과 틀린 것의 구분"에 기대고 있다. 과연 그렇다면 맞는 것은 선이고 틀린 것은 악인가?
논리 체계는 이 구분을 지키기 위한 약속이다. "이것이 참이면 저것도 참이다"라는 약속들의 모음이다. 약속을 지키는 한, 참에서 출발하면 참에 도달한다. 거짓이 참으로 둔갑하는 일은 일어나지 않는다.
2. 약속이 깨지는 순간
그런데 이 약속 체계 안에 모순이 하나 들어온다고 하자. "P이면서 동시에 P가 아니다"가 참으로 인정된다고 하자. 비가 오면서 동시에 비가 오지 않는 세계. 있을 수 없는 일이 "있다"고 인정된 세계. 선과 악의 경계가 모호한 세계
이 세계에서는 이상한 일이 일어난다.
P가 참이니까, "P 또는 Q"도 참이다. "또는"은 하나만 맞으면 전체가 맞기 때문이다. 그런데 P가 아니라고도 했으니까, "P 또는 Q"에서 P는 탈락한다. 남는 것은 Q이다. 그런데 Q에 아무거나 넣어도 이 추론은 성립한다.
선 또는 악은 선이다. (에엥? 이거 무슨 개 풀 뜯어먹는 소리?) 선이 선일 수도 있고 악은 악이지만 선 또는 악은 둘 중의 하나만 성립하면 되니까 선이다. 그런데 선이 아니라면 악이다. 악은 선이 된다. 이 무슨 말이 안되는 상황인가? 완전히 얽혀버린 매듭상황이 되어 버렸다. 선과 악의 경계가 무너져서 선이 악이 될수도 악이 선이 될 수도 있다. 그러므로 모순하나가 세상에 들어와서 세상을 어지럽히는 원리가 이상하리만큼 폭발원리와 일치한다.
Q에 "1 = 2"를 넣으면 1 = 2가 증명된다. "달은 치즈로 만들어졌다"를 넣으면 그것도 증명된다. 무엇이든 넣을 수 있고, 무엇이든 증명된다.
이것을 "폭발 원리"라고 부른다. 모순 하나가 들어오면 아무 명제나 증명 가능해진다는 원리이다. 라틴어로 "ex falso quodlibet", "거짓으로부터 무엇이든 따라 나온다"이다. 이름이 "폭발"인 이유는, 모순 하나가 체계 전체를 폭발시키듯 무너뜨리기 때문이다.
3. 폭발 이후의 세계
모순 하나에서 무엇이든 증명 가능해진다. 이것을 흔히 "모든 것이 참이 된다"라고 설명한다. 그런데 이 설명은 절반만 맞다.
모든 명제가 증명 가능해지면, P도 증명되고, P가 아니라는 것도 증명된다. 그러면 P는 참인가, 거짓인가?
둘 다 맞다.
동시에 참이면서 거짓이다.
이 상태에서 "이것은 참이다"라고 말해도 의미가 없다. "이것은 거짓이다"라고 말해도 의미가 없다. 둘 다 증명이 되니까, 어느 쪽을 믿어야 하는지 알 수 없다. 맞는 것과 틀린 것을 가려내는 기능이 사라진 것이다.
논리 체계가 존재하는 이유가 바로 그 가려내기였는데, 그것이 사라졌다. 체계는 여전히 존재하지만, 아무것도 판별하지 못한다. 저울이 있는데 어느 쪽으로도 기울지 않는 것과 같다. 저울로서의 기능이 죽은 것이다.
4. 그래서 모순은 절대로 들어와서는 안 된다
결론은 단순하다. 모순이 들어오면 모든 것이 무너진다. 그러니 모순이 들어오지 못하게 해야 한다.
수천 년 동안 이 일을 한 것은 사람의 눈이었다. 수학자가 증명을 쓰고, 다른 수학자가 읽고, 학술지의 심사위원이 확인한다. "이 증명에 빈틈이 없는가? 모순이 숨어 있지 않은가?"를 점검한다.
문제는 사람이 실수한다는 것이다.
논리가 비약되는 것을 놓칠 수 있다. 경우의 수를 빠뜨릴 수 있다. "이건 당연하니까 넘어가자"라고 했는데 사실은 당연하지 않을 수 있다. 이런 틈으로 모순이 슬며시 들어온다. 들어왔는데 아무도 모를 수 있다. 그 모순 위에 새로운 정리가 쌓이고, 그 정리 위에 또 정리가 쌓인다.
기초에 금이 간 건물이 올라가고 있는데 아무도 모르는 것이다.
5. 기계가 검사한다
Lean 4는 이 검사를 사람 대신 컴퓨터가 하도록 만든 도구이다.
증명의 매 줄을 쓸 때마다, Lean은 그 줄이 논리적으로 타당한지 즉시 확인한다. "P를 가정한다"라고 쓰면 그 가정이 현재 맥락에서 허용되는지 확인한다. "이것이 답이다"라고 쓰면 정말로 답이 맞는지 확인한다. 한 줄이라도 타당하지 않으면 빨간 줄을 긋고 거부한다.
핵심은 이것이다. Lean이 매 줄을 검사하기 때문에, 모순이 슬며시 끼어들 틈이 없다. 사람의 눈은 속일 수 있지만, 타입 검사기는 속일 수 없다. Lean을 통과한 증명은 "이 증명 안에 모순이 없다"는 보증을 받은 것이다.
폭발 원리 -- 모순이 들어오면 무엇이든 증명 가능해진다는 그 원리 -- 는 Lean 안에 여전히 존재한다. 그런데 위험하지 않다. 모순 자체가 들어올 수 없으니까. 불이 붙을 수 없는 곳에 소화기가 있는 셈이다. 소화기가 있어도 좋고, 어차피 쓸 일이 없다.
6. sorry라는 빈자리
Lean에는 sorry라는 명령이 있다. 증명의 빈자리를 표시하는 것이다.
sorry를 쓰면 Lean은 그 부분을 검사하지 않고 넘어간다. "이 부분은 아직 못 했습니다"라는 솔직한 고백이다. Lean은 이 고백을 받아들여서, 틀렸다고 거부하지도 않고 맞다고 승인하지도 않는다. 판단을 보류한다.
sorry가 있는 증명은 "아직 검증이 끝나지 않은 증명"이다. 문이 하나 열려 있는 건물과 같다. 그 문으로 모순이 들어올 수도 있고, 아닐 수도 있다. 아직 모른다.
sorry를 실제 증명으로 채우면, 그때 Lean이 그 부분도 검사한다. 모든 sorry가 사라져야 비로소 "모든 문이 닫혔다, 모순이 들어올 곳이 없다"고 말할 수 있다.
7. 하나의 증명으로 보는 전체 이야기
지금까지의 이야기를 하나의 Lean 증명에서 볼 수 있다.
"p이거나 q이다. 그런데 p가 아니다. 따라서 q이다." 논리합 삼단논법이라 불리는, 아주 단순한 추론이다.
example (p q : Prop) (hpq : p ∨ q) (hnp : ¬p) : q := by
cases hpq with
| inl hp => exact absurd hp hnp
| inr hq => exact hq
네 줄뿐이다. 그런데 이 네 줄 안에 오늘의 모든 이야기가 들어 있다.
cases hpq with는 경우를 나누는 것이다. p이거나 q인데 어느 쪽인지 모르니까, 둘 다 따져보겠다는 선언이다. Lean은 모든 경우를 빠짐없이 다루도록 강제한다. 하나라도 빠뜨리면 거부한다. 경우의 수를 빠뜨리는 실수, 사람이라면 할 수 있는 그 실수가 원천 차단된다.
inl hp는 p인 경우이다. 그런데 가정에 "p가 아니다"가 있다. p이면서 동시에 p가 아니다. 모순이다. absurd hp hnp는 "이 경우는 모순이니 있을 수 없다"는 선언이다.
여기서 폭발 원리 -- 모순에서는 무엇이든 증명 가능하다는 그 원리 -- 가 쓰인다. 모순이 발생했으니 목표가 q이든 뭐든 상관없이 이 경우는 끝난다. 그런데 이것은 위험하지 않다. 이 모순은 "만약 p라면"이라는 가상의 경우 안에서 생긴 것이기 때문이다. 실제 세계에서 p와 ¬p가 동시에 참인 것이 아니라, "이 경우는 실제로 일어나지 않는다"는 것을 확인한 것이다.
inr hq는 q인 경우이다. q가 바로 있고, 목표도 q이다. exact hq, "이것이 답이다"로 끝난다. 이 경우가 실제로 일어나는 유일한 경우이다.
Lean은 이 네 줄 전부를 검사한다. 모든 경우를 다루었는지, 모순 처리가 타당한지, 답의 타입이 목표와 일치하는지. 네 줄 모두 통과하면, "이 증명에 모순이 없다"가 보장된다.
8. 왜 이 모든 것이 필요한가
논리 체계는 맞는 것과 틀린 것을 가려내기 위해 존재한다.
모순이 들어오면 이 가려내기가 불가능해진다. 무엇이든 증명할 수 있게 되고, 무엇이든 증명할 수 있다는 것은 아무것도 가려낼 수 없다는 뜻이다.
따라서 모순은 절대로 들어와서는 안 된다.
사람은 실수한다. 모순을 실수로 들여올 수 있고, 들여왔는지 모를 수 있다.
Lean 4는 증명의 매 줄을 검사하여 모순이 들어오지 못하게 막는다. sorry는 아직 검사하지 못한 부분을 표시하여 판단을 보류한다. sorry가 없는 증명만이 "모순이 없다"는 보증을 받는다.
폭발 원리 -- 모순이 들어오면 무엇이든 증명 가능해진다는 원리 -- 는 체계 안에 존재하지만, 모순 자체가 들어올 수 없으므로 발동할 일이 없다.
이것이 Lean 4가 존재하는 이유이다. 수학 증명이 맞는지 사람 대신 기계가 검사하는 것. 모순이 슬며시 들어오는 것을 차단하는 것. 맞는 것과 틀린 것의 구분을 지키는 것.
나는 인공지능과 오케스트레이션중이다.