직관주의 논리와 고전 논리의 한계를 동시에 보완하는 선형 논리를, 시퀀트 계산을 바탕으로 개념·규칙·연산자·의미론까지 차근차근 해설한다.
2025년 2월 11일
이 글은 논리에 관한 연재의 두 번째 글이다. 여기서 다루는 아이디어들은 프로그래밍 언어 이론, 특히 타입 이론과 람다 계산에 관한 중요한 논문들을 이해하는 데 매우 유용하다. 첫 번째 글에서는 논리를 전개하는 하나의 체계로서 시퀀트와 시퀀트 계산(Sequent Calculus)을 설명했고, 이제 그 개념들을 알고 있다고 가정하겠다. 이번 글에서는 시퀀트 계산을 공부한 결과로 얻어지는 가장 놀라운 결실인 **선형 논리(linear logic)**에 들어가 보겠다. 그리고 다음 글에서 Par와 고전 논리의 계산 해석을 이야기하며 이 3부작을 마무리할 예정이다.
(이 글에 나오는 모든 증명에서 교환 규칙(Exchange rule)의 사용은 전부 묵시적으로 처리할 것이다. 선형 논리에서는 원래 그렇게 쓰는 것이 관례다. 실제로는 여전히 교환이 일어나고 있다는 것만 알고 있으면 된다.)
지난 글에서 우리는 시퀀트 표기가 직관주의 논리를 꽤 우아하게 특성화할 수 있음을 보았다. 바로 턴스타일(⊢) 오른쪽에 있는 식의 개수를 최대 하나로 제한하는 것이다. 꽤 그럴듯한 제약이지만, 이 제약은 시퀀트 계산의 아름다움, 특히 턴스타일 양변의 대칭성을 상당 부분 잃게 만든다. 고전 시퀀트 계산에서는 다음과 같은 동치들이 있었다는 것을 기억하자:
Γ ⊢ 는 Γ ⊢ ⊥ 와 동치이고,⊢ Δ 는 ⊤ ⊢ Δ 와 동치이다.표기법에 다시 익숙해지기 위한 워밍업 삼아, 왜 그런지 잠깐 복습해 보자.
보다 기본적인 논리 표기법으로 첫 번째를 (비공식적으로) 쓰면 Γ → ⊥ 라고 할 수 있다.
두 번째는 ⊤ → Δ 가 된다. 오른쪽이 비어 있다는 것은 왼쪽에 모순이 있어야 함을 의미한다. 추상대수나 모노이드에 익숙하다면, ⊥ 가 합(논리합)(∨)의 단위元(unit)이라는 점 때문에 그렇다는 것도 알 수 있을 것이다. 그래서 Γ ⊢ 는 Γ ⊢ ⊥ 로, 다시 Γ → ⊥ 로 볼 수 있고, 이를 드모르간 법칙으로 옮기면 ¬Γ ∨ ⊥ 꼴을 생각할 수 있다. 고전 논리에서 A → B 는 ¬A ∨ B 와 동치이므로, 약간의 역-드모르간을 통해 적절한 함의 형태로 옮길 수 있고, 결국 양쪽 표현이 서로 완전히 되돌릴 수 있는 변환을 통해 동치임을 알 수 있다.
세 번째 경우도 유사한 과정을 거치므로 자세한 전개는 생략하겠다. ⊤ 이 곱(논리곱)(∧)의 단위이므로 ⊤ ∧ Γ ≃ Γ 를 이용하면 되고, 나머지는 비슷하게 따라가면 된다.
(범주론을 미리 읽어둔 사람에게 소소한 이스터에그를 남겨두겠다. 이런 식으로 부정을 함의의 양쪽으로 옮길 수 있는 것은 부정이 자기 수반(adjunct)이기 때문이다. 이 성질이 바로 continuations를 모델링할 때 쓰이는 double-negation 모나드를 낳는다! 물론 이 시리즈에서 기대하는 배경지식 수준은 한참 넘어간 이야기다 :)
이제 우리는 턴스타일 양변 사이에서 부정을 이용해 식들을 이리저리 옮길 수 있게 되었다. 꽤 멋진 일이다. 지난 글에서 본 one-sided sequent calculus 도 이 과정을 이용해 만들었다. 하지만 기억하겠지만, 그것은 고전 논리에서만 동작했다. 직관주의 논리는 오른쪽에 항상 최대 한 개의 식만 올 수 있어야 하므로 이러한 변환이 통하지 않는다. 그리고 이것은 직관주의 논리에서의 부정이 좀 이상하고, 고전 논리의 아름다운 쌍대성(duality)을 잃는다는 사실과 관련이 있다.
직관주의 논리에서 근본적인 불편함을 마주하게 되면, 자연스럽게 이런 질문이 떠오른다. “애초에 왜 직관주의 논리를 신경 써야 하지? 그냥 좋은 성질들 다 가진 고전 논리를 쓰면 되잖아?” 고전 논리의 큰 문제는 배중률(Law of Excluded Middle, LEM) 에 있다. 이는 임의의 명제 P 에 대해 P ∨ ¬P 를 가정해도 좋다는 공준이다. 혹은 동치인 이중 부정 제거 법칙(Double-Negation Elimination, DNE) 으로 볼 수도 있는데, ¬¬P 가 주어지면 P 를 결론낼 수 있다는 것이다 (¬¬P → P). 둘 다 충분히 직관적으로 참처럼 느껴지긴 하지만, 이 법칙들은 P 가 왜 참인지에 대한 이유를 전혀 주지 않는다. 그저 거짓이 아니다 라는 점만 알려줄 뿐이다.
반면 직관주의 논리에서는, 어떤 명제의 증명을 보면 그 명제가 왜 참인지, 그 근거를 증명 자체에서 정확히 읽어낼 수 있다. 예를 들어, P 를 “이 튜링 기계가 이 입력에 대해 멈춘다” 라는 명제로 보자. 고전 논리주의자는 “기계는 입력에 대해 멈추거나, 아니면 안 멈추거나, 셋 중에 하나겠지. 그러니 P ∨ ¬P 가 참이다”라고 말한다. 직관주의자는 이렇게 되묻는다. “당신은 분명 P 이거나 ¬P 둘 중 하나가 참이라고 믿고 있으니, 어느 쪽인지 말할 수 있어야겠죠?” 하지만 일반적으로 그렇게 할 수 있는 방법은 없다. 결국 실제로는 기계를 돌려 보는 수밖에 없는데, 멈출지 안 멈출지 영원히 기다릴 수는 없기 때문이다.
직관주의 논리에서의 논리합(또는) ∨ 는 이렇게 강화된(disjunctive) 의미를 갖는다. P ∨ Q 를 참이라고 증명하려면, 실제로 어느 쪽이 참인지 알고 있어야 한다. 그래서 누군가 P ∨ Q 를 주면 “그럼 둘 중 어느 쪽이 참이냐?” 라고 되묻는 것이 항상 타당하다. 이 멋진 성질 덕분에 직관주의 논리는 토포스(topos), 유계 격자(bounded lattice), 카르테시안 닫힌 범주(cartesian closed category), 그리고 물론 람다 계산과도 자연스럽게 대응된다.
결국 우리는 고전 논리와 직관주의 논리 모두에 근본적인 거슬림이 있음을 보게 된다. 둘 다 치명적이라 할 정도의 문제는 아니고, 실제로 지금도 많은 사람들이 두 체계 모두에서 진지한 연구를 한다. 하지만 만약 이 모든 문제를 한꺼번에 해결하는 어떤 논리를 찾을 수 있다면, 그 논리는 더 “근본적(fundamental)”이고 “자연스러운(natural)” 체계일 것이며, 아직 예측하지 못한 여러 장점을 품고 있으리라는 기대를 가질 수 있다.
프랑스의 논리학자 Jean-Yves Girard(장이브 지라르)는 이런 생각들을 품고, 시퀀트 계산이 도움이 되지 않을지 탐구해 보았다. 턴스타일 양변의 아름다운 대칭성을 유지하고 싶다면, 애초에 그 체계가 시퀀트 계산 이어야 한다. 따라서 요령은, 부정을 이용해 턴스타일 양변을 오갈 수 있으면서도, 논리합(또는 존재 양화사)이 여전히 “어느 쪽이 참인지 기억하는” 성질을 유지하는 새로운 시퀀트 계산을 정의하는 것이다.
(이런 성질을 보통 “구성적(constructive)”이라고 부른다. 증명은 더 작은 증명들로부터 구성되어야 하며, 고전 논리처럼 증명을 지워 버리면 안 된다는 뜻이다. 직관주의 논리는 흔히 대표적인 구성적 논리로 여겨져서, 둘이 종종 혼동되기도 한다. Girard는 심지어 자신이 이 글에서 다루려는 논문의 4페이지에서 “직관주의 논리 너머에는 어떤 구성적 논리도 없다(There is no constructive logic beyond intuitionistic logic)” 라고 말하기까지 한다. 하지만 아이러니하게도, 바로 그 논문에서 직관주의 논리에 처음으로 진지하게 맞붙을 만한 새로운 구성적 논리 체계가 소개된다!)
그렇다면, 왜 고전 시퀀트 계산에서 오른쪽 식의 수를 하나로 제한하면 그 체계가 구성적이 되는 걸까? Girard의 통찰은, 이것이 오른쪽에서의 축약(contraction) 구조 규칙 사용을 막기 때문이라는 데 있다. 오른쪽에 A 가 두 번 있을 수 없다면, A, A 를 A 로 줄이는 contraction을 적용할 수 없는 것이다.
고전 논리에서는 다음과 같은 일이 가능하다. Γ ⊢ A, A 에서 시작해, 오른쪽에서 ∨-도입 규칙을 두 번 적용해 (A 로부터 왼쪽 분지, 오른쪽 분지에서 각각) Γ ⊢ A ∨ B, A ∨ B 를 만들고, 거기에 contraction을 적용해 Γ ⊢ A ∨ B 를 얻는다. 이때 우리는 어느 쪽 분지에서 얻은 A ∨ B 를 버릴지 마음대로 선택할 수 있다. 두 분지에서 얻은 A ∨ B 는 서로 다른 이유로 참인데, contraction을 통해 어느 쪽이든 버릴 수 있고, 결국 남은 A ∨ B 가 어떤 근거로 참이 되었는지에 대한 증거가 완전히 잊혀진다.
Girard의 제안은 다음과 같다. 오른쪽 식의 개수를 제한하는 이유가, 구성성을 깨뜨리는 방식의 contraction 사용을 막기 위한 것이라면, 그런 제약 없이 그냥 contraction 자체를 금지하면 되지 않는가? 오른쪽에 식을 여러 개 둘 수 있게 하고, 대신 contraction을 아예 제거하는 것이다. 그러면 턴스타일의 대칭성을 다시 얻을 수 있고, 실제로 Girard는 자기의 새로운 논리를 지난 글에서 언급한 one-sided sequent 스타일로 제시한다!
하지만 구성성을 지키려 할 때 새로운 문제가 생긴다. 바로 약화(weakening) 규칙을 통해 Γ ⊢ Δ 에서 Γ ⊢ Δ, A ∨ B 같은 걸 마음대로 추가할 수 있다는 점이다. 이렇게 얻은 A ∨ B 는 당연히 ‘어느 쪽이 참인지 모르는’ 논리합이다(사실 참일 필요도 없다!). 그래서 Girard는 weakening도 아예 금지한다. (직전까지는 오른쪽 weakening이 오른쪽이 비었을 때(Γ ⊢)만 가능했기 때문에, 이미 왼쪽에 모순이 있다는 뜻이 되어 문제가 되지 않았다.) Girard의 말로 직접 옮기면 다음과 같다.
“직관주의 논리의 구성적 성질이 시퀀트의 특정 위치에서 구조 규칙들을 버린 데서 나온다는 걸 깨달은 이상, 우리는 이 관찰의 귀결을 기꺼이 받아들여야 한다. 즉 이런 제한은 다른 ‘방들(rooms)’로도 일반화되어야 하고, 그 결과 weakening과 contraction은 사라진다.” — (Girard 1987, p. 4)
이렇게 얻은 최종 체계, 즉 고전 논리에서 weakening과 contraction을 제거한 완전히 구성적인 체계를 선형 논리(Linear Logic) 라 부른다.
이제 주요 단점은 뻔하다. weakening도 없고 contraction도 없다. 식을 복제하거나 버릴 수 없으므로, 모든 식은 정확히 한 번만 사용되어야 한다. 이에 대한 Girard의 해결책은 나중에 다루겠다.
이상한 귀결 중 하나는, 선형 논리에서 ‘참/타당성’ 개념이 더 이상 단조(monotonic) 하지 않다는 점이다. 직관주의/고전 논리에서는, 증명이 진행되는 동안 사용할 수 있는 정보의 양이 줄어들지 않는다. 하지만 선형 논리에서는 어떤 명제를 한 번 사용하고 나면 더 이상 그 명제를 가지고 있지 않으므로, 다시 쓰기 위해서는 새 증명이 필요하다. 증명 도중에 사실이 더 이상 사실이 아니게 될 수 있는 셈이다.
이제 첫 두 규칙부터 살펴보자.
불행히도, weakening과 contraction을 제거하는 일은 그렇게 간단하지 않다. 이들을 없애고 나면, 지난 글에서 소개했던 one-sided sequent의 도입·소거 규칙들을 선형 논리에 어떻게 옮길지에 여러 해석이 생긴다.
예를 들어, (고전/직관주의) 논리곱 도입 규칙 ∧-Intro를 생각해 보자. (이 글에서는 실제 규칙 도식 그림 대신 말로 설명하겠다.)
Γ ⊢ A 와 Δ ⊢ B 로부터 Γ, Δ ⊢ A ∧ B 를 얻는 규칙을 가지고 있었다고 하자.이를 선형 논리로 그대로 들고 오면, 이 규칙은 A 와 B 가 정확히 Γ, Δ 라는 동일한 식 모음 속에 있어야만 A ∧ B 를 만들 수 있다는 식으로 읽힌다. 하지만 이제는 weakening도 contraction도 없으므로, 두 모음을 서로 맞추기 위해 식을 넣거나 뺄 수 없다는 점에서 이는 매우 강한 요구다.
그래서 이렇게 바꾼 규칙을 선호할 수도 있다:
Γ ⊢ A 와 Γ ⊢ B 로부터 Γ ⊢ A ∧ B 를 얻는 식.이 규칙은 고전 논리에서는 첫 번째와 동치지만, 선형 논리에서는 그렇지 않다. 이 버전은 직관적으로 더 자연스러워 보일 수 있다. 논리곱은 나머지 식들에는 전혀 신경 쓰지 않는다 라는 느낌을 주기 때문이다. 하지만 이쪽 역시 다른 방식으로 제약을 건다. 만약 우연히 두 전제의 왼쪽이 완전히 같은 Γ 라면, 결론의 A ∧ B 는 Γ 안의 모든 식을 중복해서 가지고 있는 셈이 된다. contraction 없이 이 중복들을 제거할 수 없으므로, 매우 곤란한 상황이 벌어진다.
예를 들어, 기본적인 정리인 A ⊢ A (혹은 one-sided로 쓰면 ⊢ A ⊸ A, ⊸ 는 곧 소개할 선형 함의라고 생각하자) 조차도 위 버전만으로는 증명하지 못하는 상황이 생긴다.
실제로 해 보면, 마지막에 쓸데없이 남는 A 를 제거할 수 없어서 ⊢ A, A 같은 꼴로밖에 안 끝난다. 다시 말해, A ⊢ A 가 아니라 A ⊢ A, A 를 증명하게 되는 셈이다.
선형 논리는 아주 과감하게 둘 다 유지하기로 한다. 즉 기존의 ∧ 는 사라지고, 대신 두 개의 다른 ‘그리고’가 등장한다. 바로 with를 뜻하는 & 와, tensor(또는 곱)를 뜻하는 ⊗ 이다.
& 는 두 번째 버전 규칙(왼쪽 맥락이 동일한)을 반영하고,⊗ 는 첫 번째 버전 규칙(맥락을 합치는)을 반영한다.그래서 ⊢ A ⊗ B ⊸ A 는 정리지만, ⊢ A & B ⊸ A 는 정리가 아니다(식의 정확한 형태는 부정/함의 정의까지 본 뒤에 조금 다듬어야 하지만, 직관만 잡으면 된다).
반대로, ⊢ A & B ⊸ A ⊗ B 는 정리가 아니지만, ⊢ A ⊗ B ⊸ A & B 는 정리이다. 왜냐하면 ⊗ 는 실제로 A 와 B 둘 다를 ‘가지고’ 있는 상황이므로, 그로부터 “둘 다 가능하지만 그중 하나처럼 쓰는” & 를 만드는 건 문제가 없지만, 반대로 & 는 “한 번만, 그리고 둘 중 하나로만” 사용할 수 있는 자원처럼 동작하기 때문이다.
직관적으로 요약하면:
A ⊗ B 는 실제로 A 와 B 둘 다를 가지고 있다는 뜻이다. 둘 다 (그리고 각각 정확히 한 번씩) 사용해야 한다.A & B 는 한 번만 사용할 수 있는 어떤 것인데, 그걸 A 로 쓸 수도 있고 B 로 쓸 수도 있다는 뜻이다. 하지만 이것은 보통의 논리합 ∨ 와는 다르다. 왜냐하면 어느 쪽으로 사용할지 우리가 선택하기 때문이다. (논리합은 보통 누군가가 어느 쪽이 참인지 알려주는 구조다.)그래서 선형 논리에서는 기대하던 정리 ⊢ A ⊗ B ⊸ A & B 는 있지만, ⊢ A & B ⊸ A ⊗ B 는 없다.
같은 현상이 논리합에도 나타난다. 고전/직관주의 논리에서의 ∨-도입 규칙을 선형 논리로 옮기려 하면, 둘 다 가능한 두 가지 번역이 생긴다.
Γ ⊢ A 로부터 Γ ⊢ A ∨ B 를, 그리고 Γ ⊢ B 로부터 Γ ⊢ A ∨ B 를 얻는 규칙.Γ ⊢ A, B 를 Γ ⊢ A ∨ B 로 보는 식.두 경우 모두 고전 논리에서는 동치지만, 선형 논리에서는 그렇지 않다. 두 번째(쉼표 기반) 경우는 A 와 B 가 한 ‘자원 풀’을 공유하는 꼴이고, 첫 번째는 각각에 A ∨ B 를 따로 주는 꼴이기 때문이다. weakening·contraction이 없으면 이런 차이가 무시할 수 없을 정도로 중요해진다.
그래서 선형 논리는 여기서도 둘 다 취한다. 고전 논리의 ∨ 는 사라지고, 대신 두 개의 다른 ‘또는’이 등장한다. 바로 plus를 뜻하는 ⊕ 와, 시리즈의 제목이기도 한 par를 뜻하는 ⅋ 이다.
⊕ 는 additive disjunction (더하기식 논리합)이고,⅋ 는 multiplicative disjunction (곱하기식 논리합, 즉 par)이다.선형 논리에서는 다음과 같은 현상이 생긴다.
⊢ A ⊕ B ⊸ A⅋B 는 정리지만, ⊢ A⅋B ⊸ A ⊕ B 는 정리가 아니다.⊢ A⅋B ⊸ (A ⊕ B) 의 어떤 다른 조합은 정리일 수 있지만, ⊢ A ⊕ B ⊸ A⅋B 의 다른 조합은 안 될 수 있다.각각이 우리가 직관적으로 생각하는 논리합의 서로 다른 측면을 포착해 내는 것이다.
여기서 흥미로운 점은 다음과 같다.
⅋ 는 고전 논리의 논리합에서 온 것이다. one-sided sequent에서 쉼표가 곧 multiplicative disjunction이기 때문이다.⊕ 는 직관주의의 논리합에서 온 것이다. 언제나 왼쪽/오른쪽 분지 중 하나로부터 도입되고, 어떤 분지에서 왔는지를 잊지 않는다.그래서 선형 논리에서 나오는 멋진 정리 중 하나는 바로 배중률이다:
⊢ A⅋¬A보다 정확히 말하면, one-sided sequent에서는 ⊢ A, A⊥ 와 같은 형태를 Ax(공리) 규칙으로 허용한다. 이것이 바로 배중률의 선형 논리 버전이다.
다시 말해, 배중률은 ⊢ A⅋A⊥ 라고 쓸 수 있고, 이는 매우 구성적인 방식으로 타당하다. 왜냐하면 선형 논리에서의 함의는 독립된 연산자가 아니라 one-sided 스타일에서 A⊥⅋B 로 정의되기 때문이다.
이 사실을 존중하기 위해, 즉 함의가 별도의 원시 기호가 아니라 정의된 연산자라는 점을 드러내기 위해, 선형 논리에서는 함의에 ⊸ (막대사탕, "lollipop") 기호를 쓴다. A ⊸ B 는 A⊥⅋B 로 정의된다. 이런 정의 때문에 ⊸ 는 직관주의의 함의와 조금 다른 식으로 동작한다. A ⊸ B 의 증명 역시 contraction·weakening을 사용할 수 없기 때문이다. 이 글의 나머지 부분에서는 함의를 모두 ⊸ 로 쓰겠다.
par와 고전 논리의 논리합에 대해서는 다음(final) 글에서 훨씬 더 자세히 다룰 것이다. 여기서는 짧게만 짚고 넘어가자.
먼저, par는 이해하기 매우 어렵기로 악명 높다. 실제로 선형 논리가 “발견한” 유일한 연산자이기도 하다. 그 전까지 어떤 논리 체계에도 par와 비슷한 것이 없었다. 둘째로, 나 역시 한참을 고생한 끝에 par를 이해하고 나서는, par가 내가 본 어떤 논리 연산자보다도 가장 아름다운 연산자라고 느꼈다. 그래서 사실상 par를 세상에 소개하고 싶어서 이 거대한 연재를 만들었다고 해도 과언이 아니다 :)
이제 남은 것은 선형 논리에서의 부정(negation) 이다. 놀랍게도, 선형 논리에서는 부정도 별도의 원시 연산자가 아니라, 다른 것들에 대한 재귀적 정의로 주어진다. (처음 두 규칙은 원자식(atomic formula)에 대한 정의다.)
(A⊗B)⊥ ≔ A⊥ & B⊥(A & B)⊥ ≔ A⊥ ⊗ B⊥(A⅋B)⊥ ≔ A⊥ ⊕ B⊥(A ⊕ B)⊥ ≔ A⊥⅋B⊥A⊥⊥ ≔ A (원자식에 대해)여기서 핵심이자 멋진 성질은, 부정이 “이중 부정이 사라지는(involutive)” 연산이라는 점이다. 즉 A⊥⊥ 가 다시 A 로 돌아온다. 따라서 선형 논리는 이중 부정 제거를 지원한다.
이제 모든 연산자를 다 얻은 것처럼 보인다. 하지만 아직 끝나지 않았다. 참(true)과 거짓(false) 그 자체도 각각 두 가지 버전으로 나뉘어야 한다.
⊤ 은 ⊤(top) 과 1(one) 으로 나뉘고,⊥ 은 0(zero) 와 ⊥(bottom) 으로 나뉜다.(여기서는 0 에 대한 도입 규칙이 없다.)
각각의 단위 기호들이 시퀀트 규칙에서 어떻게 등장하고 사라지는지 살펴보고, 이들이 어떤 역할을 하는지 스스로 파악해 보라. 힌트를 약간 주자면: 어떤 상황에서 이 네 기호가 ‘아무것도 기여하지 않는’ 것처럼 보이는가?
이 체계를 종이에 직접 써 보고, 몇 가지 간단한 정리를 증명해 보는 것을 정말로 추천한다. 막히면 어떤 플랫폼이든 좋으니 나에게 연락해 주면, 최대한 자세히 도와 보겠다 :)
이제 부정의 정의를 이 네 기호에 대해서도 확장해야 한다.
⊤⊥ ≔ 01⊥ ≔ ⊥0⊥ ≔ ⊤⊥⊥ ≔ 1드디어 선형 논리의 어느 정도 완전한 시스템을 얻었다. 특히 지금까지 소개한 체계를 MALL(Multiplicative-Additive Linear Logic) 이라고 부른다. 여기서
⊗,⅋,1,⊥ 들이 곱셈적 조각(multiplicative fragment) 을 이루고 (이 네 개만으로도 완전한 논리 체계가 되며, 이를 MLL이라 부른다),&,⊕,⊤,0 들이 덧셈적 조각(additive fragment) 을 이룬다. (오른쪽 쉼표 자체가 곱셈적 의미를 갖기 때문에, additive fragment 단독으로는 완전한 시스템이 되기는 어렵다.)곱셈적 조각은 전반적으로 고전 논리 쪽에 가깝고, 특히 논리합과 함의를 다루는 방식이 그렇다. 반면 덧셈적 조각은 보다 직관주의 논리와 닮아 있다. 이것이 의미론을 잠시 논할 때 다시 등장할 것이다.
이제 한 가지를 더 추가해야 한다. 직관주의나 고전 논리와 비슷한 표현력을 얻으려면, 조심스럽게라도 weakening과 contraction을 다시 도입하는 방법이 필요하다. 정말로 세상 모든 장점을 다 가져오고 싶은 것이다.
Girard의 해결책은 두 개의 새로운 연산자, 즉 지수(exponentials) 다. 보통
!A (of course A),?A (why not A)라고 쓴다.
여기서 !Γ 는 Γ 안의 모든 식에 ! 를 붙인 집합, 예를 들어 !A, !B, !C 와 같은 꼴을 의미한다.
원 논문과 이 글에서 모두 one-sided sequent calculus 표현을 따르고 있으므로, 여기서는 주로 ! 쪽 규칙에 초점을 맞추겠다. 다만 현대의 대부분 선형 논리 교재/논문은 intuitionistic linear logic (ILL) 관점에서 서술된다는 점을 언급할 가치가 있다.
ILL은 다음과 같은 특징을 가진다.
⅋), Ⅵ, 0 같은 연산자들은 거의 사용하지 않는다.
→)와 부정(¬)은 원시 연산자로 다시 도입한다.ILL은 선형 논리보다 여러 결함을 갖지만, 직관적으로 이해하기에는 훨씬 쉽다. par 같은 미스터리한 연산자도 없고, 오른쪽에 여러 식을 두는 다중 결론 구조도 없기 때문이다.
대부분의 현대적인 선형 논리 소개 글에서 ! 에 초점을 맞추는 이유는 다음과 같다.
?A 는 오른쪽의 !A 와 동치이므로,? 로 표현되는 꼴을 따른다.하지만 이 글에서 쓰는 one-sided sequent 표현은 왼쪽이 아예 없다. 그래서 ? 를 쓸 일이 거의 없고, ! 규칙만 보면 된다.
이제 ! 까지 더한 전체 체계는 보통 LL(Linear Logic)이라고 부른다. 더 구체적으로는 MAELL(Multiplicative-Additive-Exponential Linear Logic)이라고도 한다. 왜냐하면
그래서
지금까지 본 것만으로도 MAELL은 직관주의나 고전 논리만큼이나 표현력이 강하다는 점은 분명하다. (지수를 이용하면 weakening·contraction을 ‘안전하게’ 모방할 수 있다.)
하지만 exponentials의 참맛은, weakening·contraction 사용을 추적할 수 있다 는 데 있다.
A ⊢ !A 로 가는 규칙은 없으므로,P 가 exponentials를 전혀 포함하지 않는다면,P 의 어떤 정리도 exponentials를 전혀 사용하지 않는 완전히 구성적 증명 을 가지고 있어야 한다.문제가 되는 배중률 버전은 ⊢ A ⊕ ¬A 같은 식이다. LL에는 이런 형태의 정리에 대한 증명이 여전히 없다. 하지만 다음과 같이 지수를 붙인 버전, 예를 들어 ⊢ !(A ⊕ ¬A) 같은 것은 증명할 수 있다. (정확한 모양은 규칙에 따라 조금 다르지만 요지는 같다.)
앞에서 언급했던 요령을 사용하면 ⊢ !(A ⊕ ¬A) 류의 명제를 증명할 수 있다. 이때 증명 내부에서는 다음과 같은 일이 벌어진다.
⊢ A ⊕ ¬A, A ⊕ ¬A 를 얻는 줄이 등장한다.⊕ 는 왼쪽 분지(예: A) 덕분에 참이고,¬A) 덕분에 참이다.그리고 어느 순간 contraction을 써서 둘 중 하나를 지운다. 하지만 지운 것이 왼쪽-근거인지 오른쪽-근거인지는 알 수 없다. 그래서 최종적으로 남은 A ⊕ ¬A 가 어느 쪽 이유로 참이 되었는지에 대한 증거가 사라진다.
이처럼 exponentials를 사용하는 정리는 반드시 구성적일 필요는 없다. 하지만 중요한 점은, 지수 ! 는 한 번 생기면 다시 제거할 수 없다는 것이다. 즉 어떤 명제 P 가 지수를 전혀 포함하지 않는다면, 그 정리의 증명에서 지수를 썼다가 없애는 일은 불가능하다. 따라서 그런 정리들은 언제나 완전히 구성적인 방식으로 증명 가능하다.
고전 논리와 비교하면 훨씬 더 나은 보장을 준다. 고전 논리에서는 어떤 정리가 구성적인지 아닌지 전체적으로 파악하기 어렵지만, 선형 논리에서는 구성적이지 않은 추론을 쓴 증명은 결론에 반드시 ! 같은 지수 기호를 남겨야만 한다. 다시 말해, 증명 자체가 ‘비구성적 추론을 했노라’고 실토해야 하는 셈이다.
(그래서 !-도입 규칙을 !-Intro 대신 Dereliction(유기, 포기) 라고 부른다. 이 규칙을 사용하는 순간, 구성성을 버리는(derelict) 것이다! 이 규칙을 쓰지 않는 것이 바로 구성성의 ‘정신’이며, 이 규칙을 적용한 순간, 최종 정리에 대한 어떤 구성성 주장도 할 수 없게 된다.)
(아름다운 기술적 세부사항 하나. 혹시 Cut 규칙을 이용해 exponentials 사용을 몰래 숨길 수 있는 것이 아니냐고 생각할 수 있다. Cut은 잠재적으로 어떤 식이든 없애 버릴 수 있기 때문이다. 하지만 선형 논리에 대해 중요한 결과 중 하나가 바로 Cut 제거 정리(Cut elimination) 이다. 즉 Cut을 사용하는 어떤 증명이든, Cut을 전혀 쓰지 않는 증명으로 변환할 수 있다. 다시 말해, Cut을 논리에서 완전히 제거해도, 증명 가능한 정리 집합은 변하지 않는다. 이러한 Cut 제거 알고리즘은 종종 어떤 함수형 언어에서의 프로그램 실행과 정확히 대응되며, 그 언어가 반드시 종료(terminating)함을 보이는 수단이 되기도 한다. (STLC를 알고 있다면 같은 이유다.) )
선형 논리는 처음 보면 꽤 낯설게 느껴진다. 각 식을 정확히 한 번만 쓴다는 조건은 우리가 평소에 논리를 다루는 방식과 거리가 있어 보인다. 하지만 이 체계를 이해하는 데 도움을 주는 여러 의미론(semantics, 해석)이 있다.
가장 널리 알려진 해석은 자원 해석이다. ILL과 가장 밀접하게 연결되어 있어, 이 시리즈의 방향성에는 살짝 맞지 않지만, 그래도 반드시 언급해야 할 해석이다.
고전적인 교육용 예시는 자판기다.
M5 같은 명제로 표현하자.D)가 2 단위의 돈이 든다고 하자. 이를 !M2 ⊸ D 정도의 명제로 쓸 수 있다. (여기서 ! 는 자판기를 원하는 만큼 쓸 수 있다는 뜻으로 생각하면 된다.)일반적인(고전/직관주의) 논리에서는,
M5 를 (M1 ∧ M1 ∧ M1 ∧ M1 ∧ M1) 정도로,!M2 ⊸ D 를 (M2 → D) ∧ (M2 ∧ M2 → D) ∧ ... 처럼 무한히 반복 가능한 것으로 간주하곤 한다.그러면 이 둘로부터 D ∧ D ∧ D ∧ ... 같은 것을 끌어내는 게 가능해 보이는데, 실제 현실 세계에서는 불가능하다. 우리가 가진 돈은 제한되어 있고, 최대 두 잔까지밖에 살 수 없기 때문이다.
선형 논리는 이를 정확히 반영한다.
M5 로부터 한 번 M2 ⊸ D 를 적용하면 D 와 M3 정도가 남는다.M3 에 M2 ⊸ D 를 적용하면 또 하나의 D 와 M1 이 남는다.M1 로는 더 이상 M2 ⊸ D 를 사용할 수 없다.고전/직관주의 논리는 단조(monotonic) 해서, 증명이 진행되는 동안 참인 것으로 간주되는 정보가 줄어들지 않는다. “한때 돈이 충분했다” 라는 사실이 나중에 더 이상 사실이 아니게 되었다고 말할 방법이 없다.
반면 선형 논리는 자원을 한 번 쓰면 소모되는 것으로 본다. 자원 해석은 그래서 자원 관리, 특히 메모리 관리에 매우 잘 맞는다. 실제로 Rust 언어의 borrow checker 규칙은 선형 논리 + 문법 설탕 으로 이해할 수 있다. 선형 논리가 러스트의 메모리 안전성을 수학적으로 떠받치고 있는 셈이다.
조금 더 이론적인 해석으로, 범주론에서의 *-autonomous(스타-자율) 카테고리가 있다. 이는 깊은 범주론적 주제라 이 글의 전제 지식을 어지럽히고 싶지는 않아서 자세히 다루지는 않겠다. 다만 다음 정도는 언급할 가치가 있다.
! 연산자로 명시된다.)조금 덜 무서운 해석은 게임 이론적 의미론이다. 게임 의미론은 정말 아름다운 분야이고, 언젠가 따로 글을 쓸 계획이다. 이름 때문에 겁먹을 수 있지만, 실제로는 꽤 단순하다. 여기서는 Conway games 라는 간단한 게임 모델을 사용해 보겠다.
규칙은 다음과 같다.
이게 전부다.
Conway games는 “대화(dialogue)”를 모델링하는 데 탁월하다. 어떤 상호작용에서, 한 참여자가 다음에 할 수 있는 행동은 지금까지의 대화 흐름에 따라 제한되는 법이다. 게임 이론에서는 이를 “현재 위치와 그 위치에서 나가는 화살표들”로 표현한다.
이제 **전략(strategy)**를 “상대가 무엇을 하든 간에, 자신이 어떤 수를 둘지 미리 정해 놓은 계획”이라고 정의한다. 그리고 승리 전략(winning strategy) 는 상대가 어떤 수를 두더라도 결코 막다른 길(자기 색의 화살표가 없는 위치)에 도달하지 않도록 하는 전략이다. 승리 전략은 프로그램의 제어 흐름도(flowchart) 처럼 생각하기에 매우 좋다.
선형 논리와의 연결고리는 다음과 같다.
⊗, &, ⊕, ⅋, (·)⊥ 등과 매우 흡사한 구조를 갖도록 정의할 수 있다.예를 들어:
G⊥ 는 게임에서 모든 화살표의 색을 뒤바꾸는 것으로 정의할 수 있다.G ⊗ H 에서는 두 게임 모두에서 이겨야 승리.G⅋H 와 G ⊕ H, G & H 등은 색을 뒤집는 부정과 결합해 정의될 수 있다.이렇게 해서 예컨대 A⊗(B⅋C⊥) 같은 논리식을 하나의 거대한 Conway game 으로 볼 수 있다. 그리고 “A⊗(B⅋C⊥) 가 선형 논리에서 증명 가능하다”는 말은 곧 “그에 해당하는 Conway game에서 빨간 플레이어(증명) 가 항상 이길 수 있는 승리 전략이 존재한다”는 뜻이 된다.
이 해석의 아름다운 철학적 아이디어는 극성(polarity) 이다.
이 관점은 논리를 “대화(dialogue)”로 보는 매우 아름다운 철학을 제시한다. 더 알고 싶다면 스탠퍼드 철학 백과의 이 항목을 추천한다.
게임 의미론과 그 철학은, 이 글에서 마지막으로 소개할, 그리고 가장 악명 높은 선형 논리 의미론인 병렬성(parallelism) 으로 자연스럽게 이어진다.
이 해석에서, 고도로 병렬적인 함수형 언어의 프로그램 들이 선형 논리의 증명 으로 작용하고, 각 프로그램의 타입은 해당 증명이 표현하는 논리식 에 대응된다.
A⅋B 는 타입 A 인 식과 타입 B 인 식이 병렬로 실행되는 표현식의 타입 으로 읽을 수 있다. 그래서 이름이 par다.예를 들어:
A 인 값을 요청하고 싶다면, 외부 세계에서 보기에 그 요청은 A⊥ 타입이다.
A 로 쓰고 싶지만,A 값을 넣을 수 있는 자리”이므로 A 의 부정으로 보는 것이다.프로그램들 사이의 통신은 Cut 규칙 으로 모델링된다.
A⊥ 타입의 요청이 있고,A 타입의 값이 있을 때,Cut 규칙을 A⅋A⊥ 관점에서 보면, 사실상 Modus Ponens(함수 적용) 으로 해석할 수 있다. 그래서 Cut 제거는 프로그램의 통신 단계를 없애면서도 의미를 보존하는 최적화/정규화 과정 과 대응된다.
이 라인(선형 논리를 병렬 프로그래밍 언어의 타입 시스템·의미론으로 쓰는 접근)이 궁금하다면, 이 논문을 강력히 추천한다. 매우 아름답고 통찰이 가득한 작업이다.
이렇게 선형 논리에 대한 속성 강좌를 마쳤다. 다음 글에서는 이 시리즈의 하이라이트라 할 수 있는 곱셈적 논리합, 즉 par(⅋) 의 의미론을 훨씬 더 깊이 파고들 예정이다.
선형 논리의 아이디어와 연산자들을 간단히 참고할 수 있는 위키 요약본도 준비해 두었다. 여기에서 확인할 수 있다.
© 2025 Ryan Brewer.