직관주의 논리(Intuitionistic logic)

'$a^b$가 유리수⁠(rational number)⁠가 되는 무리수⁠(irrational number)⁠ a, b가 있다'는 짧게 증명됩니다. $\sqrt2^{\sqrt2}$를 봅시다. 이것이 유리수라면 $a = b = \sqrt2$로 끝입니다. 무리수라면 $a = \sqrt2^{\sqrt2}$, $b = \sqrt2$로 두면 $a^b = \sqrt2^{\,2} = 2$입니다. 어느 경우든 그런 a, b가 있습니다. 그런데 이 증명을 다 읽고 나도 a가 무엇인지는 모릅니다. '유리수이거나 무리수이다'라는 배중률에 기대 두 경우를 모두 처리했을 뿐, 어느 경우인지는 정하지 않았기 때문입니다. ($\sqrt2^{\sqrt2}$는 사실 무리수이지만, 이것은 1934년의 겔폰트–슈나이더 정리⁠(Gelfond–Schneider theorem)⁠가 필요한 훨씬 깊은 사실입니다.) 답을 손에 쥐여 주는 증명도 있습니다. $a = \sqrt2$, $b = \log_2 9$이면 $a^b = 2^{\frac12\log_2 9} = 2^{\log_2 3} = 3$입니다. $\log_2 9 = p/q$라면 $2^p = 9^q$인데 왼쪽은 짝수, 오른쪽은 홀수이니 $\log_2 9$는 무리수입니다. 직관주의 논리는 두 증명의 이 차이를 논리 안에서 구별합니다.

네덜란드 수학자 브라우어는 1908년 논문 「논리 원리의 신뢰할 수 없음」에서, 무한한 대상에 대해 배중률을 쓰는 것을 문제 삼았습니다. 그에게 수학적 참은 정신이 해낸 구성이었고, '참이다'는 '증명이 있다'였습니다. 그러면 'A 또는 ¬A'는 'A를 증명했거나 A를 반박했다'가 되는데, 아직 풀리지 않은 문제에 대해 이것을 주장할 근거는 없습니다. 그의 제자 아런트 헤이팅은 1930년 이 논리를 형식 체계⁠(formal system)⁠로 적었고, 이것이 직관주의 논리입니다. 이 흐름이 형식주의⁠(formalism)⁠·논리주의⁠(logicism)⁠와 부딪친 이야기는 수학 기초론 논쟁⁠(debate on the foundations of mathematics)⁠에 있습니다. 흔한 오해와 달리, 직관주의 논리는 배중률이 거짓이라고 말하지 않습니다. 모든 명제에 대해 늘 쓸 수 있는 원리로 받아들이지 않을 뿐이고, 뒤에서 보듯 배중률을 반박하는 것은 이 논리에서도 모순입니다.

'증명이 있다'가 무엇인지는 연결사마다 정해집니다. 헤이팅과 콜모고로프가 1930년대 초에 다듬어 브라우어–헤이팅–콜모고로프(BHK) 해석이라 부르는 설명입니다. A ∧ B의 증명은 A의 증명과 B의 증명의 쌍입니다. A ∨ B의 증명은 A의 증명이나 B의 증명 가운데 하나와, 그것이 어느 쪽인지의 표시입니다. A → B의 증명은 A의 증명을 B의 증명으로 바꾸는 방법입니다. ⊥(거짓)에는 증명이 없고, ¬A는 A → ⊥, 곧 'A의 증명이 오면 모순을 만들어 내는 방법'입니다. '모든 x에 대해 P(x)'의 증명은 x마다 P(x)의 증명을 주는 방법이고, 'P(x)인 x가 있다'의 증명은 그런 x 하나와 P(x)의 증명입니다. '방법'을 '프로그램'으로 바꿔 읽으면 커리–하워드 대응의 표와 한 줄씩 같습니다.

그러면 배중률에 프로그램이 없는 까닭이 보입니다. 모든 튜링 기계⁠(Turing machine)⁠ M에 대해 'M은 멈춘다 또는 M은 멈추지 않는다'의 증명이 있다면, 그 증명은 M을 받아 어느 쪽인지를 알려 주는 방법이어야 합니다. 그것은 정지 문제⁠(halting problem)⁠를 푸는 프로그램이고, 그런 프로그램은 없습니다. 이 논증은 1945년 미국 논리학자 스티븐 클리니가 증명을 프로그램으로 해석하는 방법(실현 가능성⁠, realizability⁠)으로 엄밀하게 만들었습니다. 정확히 말하면, 이것이 보여 주는 것은 '모든 M에 대해 한꺼번에' 배중률을 주는 프로그램이 없다는 것입니다. '7은 소수다'처럼 기계적으로 확인할 수 있는 명제에 대해서는 A ∨ ¬A가 직관주의⁠(intuitionism)⁠에서도 증명됩니다. 확인하는 프로그램을 돌리면 되니까요.

배중률 자체는 없어도, 배중률을 반박하는 것은 불가능합니다. $\lnot\lnot(A \lor \lnot A)$에는 프로그램이 있습니다. $\lambda k.\;k\,(\mathsf{inr}\,(\lambda a.\;k\,(\mathsf{inl}\,a)))$. 이야기로 읽으면 이렇습니다. 누군가 'A ∨ ¬A를 반박하는 방법' k를 가져왔습니다. 우리는 모순을 만들어야 합니다. 먼저 'A는 아니다'라고 답합니다(inr). 그 근거로 내미는 함수⁠(function)⁠는 'A의 증명 a가 오면 k(inl a)로 모순을 만든다'입니다. 상대가 정말 A의 증명 a를 가져오면, 우리는 말을 바꿔 'A이다'(inl a)를 k에 넘겨 모순을 얻습니다. 어느 쪽이든 k는 자기모순에 빠집니다. 커리–하워드 대응 페이지의 그림에서 이 유도를 한 단계씩 볼 수 있습니다.

'프로그램을 못 찾았다'는 것과 '증명이 없다'는 것은 다릅니다. 없다는 것을 보이는 도구가 미국 철학자 솔 크립키의 모형(1965)입니다. 세계는 '그때까지 알아낸 것'을 나타내고, 세계들은 '나중'이라는 순서로 이어져 있습니다. 앞으로 무엇을 알게 될지는 갈릴 수 있으므로, 한 세계 뒤에 여러 세계가 갈라져 나올 수도 있습니다. 한 번 확인된 사실은 뒤의 세계에서도 계속 참입니다. 연결사는 이렇게 읽습니다. A ∨ B는 지금 A나 B 가운데 하나가 확인되어 있어야 합니다. ¬A는 지금과 그 뒤의 어느 세계에서도 A가 확인되지 않는다는 뜻입니다. A → B는 지금과 그 뒤의 모든 세계에서, A가 확인되는 곳이면 B도 확인된다는 뜻입니다. 크립키는 직관주의 명제 논리⁠(propositional logic)⁠로 증명되는 식이 정확히 모든 모형의 모든 세계에서 성립하는 식임을 보였습니다. 그러니 식이 성립하지 않는 세계를 하나만 찾으면, 그 식은 증명할 수 없습니다.

처음 모형에서 A는 w₃에서만 확인됩니다. w₀에서는 A가 아직 없고, w₃에서 A가 나올 수 있으니 ¬A도 주장할 수 없어서 A ∨ ¬A가 성립하지 않습니다. 그러니 배중률은 직관주의 논리로 증명할 수 없습니다. w₁에서는 ¬¬A가 성립합니다. w₁과 그 뒤의 w₃ 어디에 서 있든 앞으로 A가 확인되는 w₃에 닿을 수 있으니, ¬A가 성립하는 곳이 없기 때문입니다. 그런데 w₁에서 A는 아직 없으니 ¬¬A → A는 w₁에서, 따라서 w₀에서도 무너집니다. 반면 맨 아래 줄 ¬¬(A ∨ ¬A)는 어떻게 칠해도 모든 세계에서 성립합니다. 위의 프로그램이 있으니 그래야 합니다.

직관주의 논리는 참·거짓 두 값 대신 셋이나 넷의 값을 쓰는 논리가 아닙니다. 괴델은 1932년, 값이 유한 개인 어떤 진리표⁠(truth table)⁠로도 직관주의 명제 논리를 정확히 잡아낼 수 없음을 보였습니다. 대신 위상수학⁠(topology)⁠이 좋은 모형을 줍니다. 명제마다 실수⁠(real number)⁠ 직선의 열린 집합⁠(open set)⁠을 대응시키고, ∧는 교집합⁠(intersection)⁠, ∨는 합집합⁠(union)⁠, ¬U는 여집합⁠(complement)⁠의 내부(여집합 안에 들어 있는 가장 큰 열린 집합)로 읽습니다. $U = (0, \infty)$이면 $\lnot U = (-\infty, 0)$이고 $U \cup \lnot U = \mathbb R \setminus \{0\}$이라 전체가 되지 못합니다. 경계인 점 0에서 배중률이 새는 것입니다. $U = \mathbb R \setminus \{0\}$이면 $\lnot U = \varnothing$, $\lnot\lnot U = \mathbb R$이라 $\lnot\lnot U \ne U$입니다. 이런 구조를 헤이팅 대수라 하고, 늘 $\lnot\lnot a = a$인 헤이팅 대수⁠(Heyting algebra)⁠가 바로 불 대수⁠(Boolean algebra)⁠입니다.

고전 논리는 직관주의 논리 안에 통째로 옮겨 넣을 수 있습니다. 소련 수학자 발레리 글리벤코는 1929년, 명제 논리의 식 A가 고전적으로 증명되는 것과 $\lnot\lnot A$가 직관주의적으로 증명되는 것이 같음을 보였습니다. 술어 논리⁠(predicate logic)⁠에서는 이 정리가 그대로 성립하지 않아서, 식 전체에 ¬¬를 붙이는 것만으로는 부족하고 안쪽까지 바꿔야 합니다. 1933년 괴델이, 같은 무렵 겐첸도 따로, 술어 논리와 산술에서 통하는 그런 변환을 찾았습니다. 원자 명제 P는 $\lnot\lnot P$로, $A \lor B$는 $\lnot(\lnot A \land \lnot B)$로, $\exists x\,A$는 $\lnot\forall x\,\lnot A$로 바꾸고 나머지는 그대로 두면, 고전적으로 증명되는 문장은 바뀐 모양으로 직관주의적으로 증명됩니다. 그래서 고전 산술(페아노 산술⁠, Peano arithmetic⁠)에 모순이 있다면 직관주의 산술(헤이팅 산술⁠, Heyting arithmetic⁠)에도 모순이 있습니다. 고전 논리가 직관주의 논리보다 더 위험하지 않다는 뜻입니다. 직관주의 논리는 고전 논리를 버리는 것이 아니라, 고전 논리가 한 덩어리로 보는 'A'와 '¬¬A', '있다'와 '없지는 않다'를 갈라 보는 더 촘촘한 눈입니다.

쓰임도 뚜렷합니다. 미국 수학자 에렛 비숍은 1967년 『구성적 해석학⁠(mathematical analysis)⁠의 기초⁠(basics)⁠』에서 해석학의 상당 부분을 구성적으로 다시 세웠고, 그렇게 얻은 정리의 증명에서는 계산 방법을 뽑아낼 수 있습니다. 증명 보조기⁠(proof assistant)⁠ Coq(Rocq)와 Agda는 기본 논리가 직관주의이고 배중률은 필요할 때 공리⁠(axiom)⁠로 더합니다. Lean은 선택공리⁠(axiom of choice)⁠에서 배중률을 이끌어 냅니다. 외연성 원리들과 함께라면 선택공리가 배중률을 함축한다는 이 논증은 1975년 루마니아 수학자 라두 디아코네스쿠가 찾은 것입니다.

이어지는 곳. 증명을 프로그램으로 읽는 표와 ¬¬(A ∨ ¬A)의 유도 그림은 커리–하워드 대응에 있습니다. 브라우어가 이 논리로 무엇을 지키려 했는지, 힐베르트가 왜 반대했는지는 수학 기초론 논쟁과 브라우어 페이지에서 볼 수 있습니다. 모든 x에 대해 증명을 주는 '방법'을 실제 프로그램으로 쓰려면 의존 타입⁠(dependent type)⁠이 필요하고, 거기서 수학적 귀납법⁠(mathematical induction)⁠은 되부름 함수가 됩니다. 크립키 모형⁠(Kripke model)⁠과 열린 집합 모형은 둘 다 '어디까지 알려졌는가'에 따라 달라지는 참을 다루는 방식이라, 위상수학과 범주론⁠(category theory)⁠으로 이어집니다. 배중률을 모든 경우에 한꺼번에 주는 프로그램이 없다는 사실은 정지 문제의 다른 얼굴입니다. 불 대수와 헤이팅 대수의 차이는 불 대수에서 출발해 비교해 보면 선명합니다. 모든 토포스⁠(topos)⁠의 내부 논리가 직관주의 논리이고, 헤이팅 대수의 '이면'은 '그리고'의 위쪽 짝, 곧 갈루아 연결⁠(Galois connection)⁠ 하나로 정의됩니다. 또 $A\to B$를 ${!A}\multimap B$로 옮기는 지라르의 번역으로 직관주의 논리는 선형 논리⁠(linear logic)⁠ 안에 통째로 들어갑니다.