직관주의 논리와 고전 논리의 한계를 짚고, 구조 규칙을 제거해 얻은 선형 논리(MALL, LL, exponentials 등)의 아이디어와 의미론, 그리고 Par(⊥) 연산자의 역할을 소개한다.
2025년 2월 11일
이 글은 논리에 관한 연재의 두 번째 글이다. 여기서 다루는 아이디어들은 타입 이론과 람다 계산을 포함한 프로그래밍 언어 이론 논문들, 특히 중요한 논문들을 이해하는 데 매우 유용하다. 첫 번째 글에서는 논리를 다루는 하나의 체계로서 수열(sequent)과 수열 계산(sequent calculus)을 설명했으므로, 이제 그 개념들은 알고 있다고 가정하겠다. 이 글에서는 수열 계산을 공부한 가장 놀라운 성과인 선형 논리(linear logic)에 대해 파고들 것이다. 삼부작의 마지막 글은 다음 글에서 마무리할 예정인데, 거기서는 Par와 고전 논리의 계산적 해석에 대해 다룰 것이다.
(이 글에 나오는 모든 증명에서, 교환 규칙(Exchange rule)의 사용은 선형 논리에서 관례적으로 그러하듯 전부 암묵적으로 남겨 두겠다. 실제로는 여전히 사용되고 있지만, 그냥 쓰지 않을 뿐이라는 점을 알고 있으면 도움이 될 것이다.)
지난 글에서 우리는 수열 표기가 직관주의 논리를 꽤 우아하게 특징화할 수 있다는 사실을 보았다. 바로 턴스타일(⊢)의 오른쪽에 올 수 있는 식을 최대 하나로 제한하는 것이다. 보기에는 꽤 근사하지만, 이 제한은 동시에 수열 계산의 아름다움, 특히 턴스타일의 양쪽에 있는 식들의 대칭성을 상당히 희생시킨다. 고전 수열 계산에서는 다음과 같은 대칭이 있었다는 점을 기억하자.
⊢ A 는 ¬A ⊢ 와 동치이고,A, Γ ⊢ 는 Γ ⊢ ¬A 와도 동치이다.표기에 다시 익숙해지기 위한 워밍업으로, 왜 그런지 잠깐 복습해 보자.
좀 더 기본적인 논리 표기로는 첫 번째를 (비형식적으로) ⊢ A 를 ¬A → ⊥ 정도로 쓸 수 있다.
두 번째는 오른쪽이 비어 있다는 것은 왼쪽에 모순이 있어야 한다는 뜻이므로 Γ, A ⊢ 는 Γ ⊢ ¬A 와 같다. 추상대수나 모노이드를 알면, ⊥ 가 합(∨)에 대한 단위원(unit)이기 때문이기도 하다. 따라서 우리는 ¬A ∨ ⊥ 를 가지게 되고, 드 모르간 법칙을 적용해 ¬(A ∧ ⊤) 로 바꿀 수 있다. 고전 논리에서는 부정이 함의와 동치이므로, 이걸 다시 반대로 드 모르간 시켜 함의 꼴로 바꿀 수 있다: A → ⊥. 결국 ¬A ⊢ 와 ⊢ A 가 서로 바뀌는 것이다. 이 변환의 각 단계는 되돌릴 수 있으므로 두 형식이 동치라는 것을 안다.
세 번째 경우도 매우 비슷한 과정을 따르므로 더 자세한 설명은 생략하겠다. ⊤ 는 합(∧)에 대한 단위원이므로 A ⊢ 와 ⊢ ¬A 의 대응도 같은 식으로 따라갈 수 있다.
(범주론을 읽어본 적 있다면, 작은 이스터 에그를 하나 남겨 두겠다. 이렇게 함의 양변을 넘나들며 부정을 이동시키는 것은, 부정이 자기-부수(adjoint)인 함수라는 사실에서 온다. 이 성질은 continuation을 모델링할 때 쓰이는 이중 부정 모나드(double-negation monad)를 낳는다! 물론 이 모든 건 이 연재에서 기대하는 배경지식보다 훨씬 윗단계 이야기다 :)
이제 우리는 턴스타일의 양쪽을 오가며 식을 옮기는 방법을 볼 수 있는데, 꽤 멋지다. 실제로 지난 글에서 했던 일, 즉 한쪽만 있는(one-sided) 수열 계산을 만드는 과정이 바로 이것이다. 다만 기억하겠지만, 그 방식은 오직 고전 논리에만 통한다. 직관주의 논리는 턴스타일 오른쪽에 항상 최대 하나의 식만 있도록 요구하기 때문에, 이런 이동이 성립하지 않는다. 그리고 이것은 직관주의 논리에서의 부정이 다소 어색하고, 고전 논리에서 보이는 아름다운 쌍대성(duality)을 잃는다는 사실과 연결된다.
직관주의 논리에서 이런 근본적인 불편함을 마주하고 나면, 가장 자연스러운 질문은 “도대체 왜 직관주의 논리에 신경을 써야 하지? 그런 멋진 성질을 다 가진 고전 논리를 그냥 쓰면 안 되나?”일 것이다. 고전 논리의 큰 문제는 배중률(Law of Excluded Middle, LEM)에 있다. 이는 임의의 명제 P 에 대해 P ∨ ¬P 를 가정하게 해 주는 공리다. 또 동치인 이중 부정 제거(DNE) 법칙은 ¬¬P → P 를 허용해, “P 가 거짓일 수 없다”는 증거만으로 “P 가 참이다”라고 결론내릴 수 있게 한다. 이 둘은 직관적으로는 꽤 그럴듯하지만, P 가 참이라는 이유 를 전혀 주지 못한다. 단지 P 가 거짓이 아니라는 사실만 줄 뿐이다.
직관주의 논리에서는, 어떤 명제의 증명을 보면 그 명제가 왜 참인지 그 증명 자체에서 정확히 읽어낼 수 있다. 예를 들어 P 를 “이 튜링 기계는 이 입력에 대해 멈춘다”로 두자. 고전 논리학자는 “분명 그 기계는 입력에 대해 멈추거나 멈추지 않거나 둘 중 하나다. 셋째는 없으니 P ∨ ¬P 다”라고 말한다. 그러면 직관주의자는 지적한다. “당신은 분명 P 가 참이거나 ¬P 가 참이라고 믿는다. 그럼 도대체 어느 쪽이 참인지 말해 보라!” 당연히 일반적으로는 그럴 수 없다. 결국 그 기계를 입력에 대해 실제로 돌려 봐야 하고, 멈추는지 안 멈추는지 보려고 “영원히” 기다릴 수도 없기 때문이다.
직관주의 논리는 강화된 ∨ 를 가진다. 즉, P ∨ Q 를 증명하려면 둘 중 어느 쪽이 참인지 알아야만 하고, 따라서 P ∨ Q 가 주어지면 어느 쪽이 참인지 묻는 것이 항상 유효하다. 이런 성질 덕분에 직관주의 논리는 토포스(topos), 유계 격자(bounded lattice), 카르테시안 닫힌 범주(cartesian closed category), 그리고 람다 계산 같은 다양한 수학적 대상과 잘 대응한다.
결국 우리는 고전 논리와 직관주의 논리 모두에 근본적인 거슬림이 있다는 상황에 놓인다. 이 중 어느 것도 치명적인 문제는 아니며, 실제로 지금도 두 체계 모두에서 심도 깊은 연구가 진행된다. 하지만 만약 이런 문제들을 모두 해결하는 논리를 찾을 수 있다면, 그 논리는 어떤 의미에서 더 “근본적(fundamental)”이고 “자연스러운(natural)” 체계일 것이고, 그런 논리를 찾기 전에는 상상조차 하지 못했던 새로운 이점들을 줄 가능성이 크다.
프랑스의 논리학자 Jean-Yves Girard는 이런 생각을 모두 했고, 수열 계산이 도움이 될 수 있는지 보기로 했다. 턴스타일을 기준으로 한 멋진 대칭성을 원한다면, 애초에 시스템이 어떤 형태로든 수열 계산이어야 한다. 그래서 요령은, 부정을 사용해 턴스타일을 넘나드는 이동을 허용하면서도, 합(∨)과 존재(∃)가 여전히 “어느 쪽이 참인지 기억하는” 성질을 유지하는 수열 계산을 정의하는 것이다.
(이런 성질을 “구성적(constructive)”이라고 부른다. 아이디어는, 증명이 항상 더 작은 증명들로부터 “구성”되며, 고전 논리처럼 그것들을 지워 버리지 않는다는 것이다. 직관주의 논리는 보통 “주류(main)” 구성적 논리로 여겨지며, 그래서 둘이 종종 혼동된다. Girard도 아래에서 이야기할 논문의 4쪽에서 “직관주의 논리를 넘어서는 구성적 논리는 없다(There is no constructive logic beyond intuitionistic logic)”라고 말한다. 하지만 아이러니하게도 바로 그 논문이, 구성적 논리 영역에서 직관주의 논리에 대한 첫 진지한 경쟁자인 선형 논리를 소개한다!)
그렇다면, 정확히 왜 고전 수열 계산에서 턴스타일 오른쪽에 최대 하나의 식만 허용하는 것이 시스템을 구성적으로 만드는 걸까? Girard가 깨달은 바에 따르면, 그 이유는 이 제한이 오른쪽에서의 수축(contraction) 구조 규칙 사용을 막기 때문이다. 오른쪽에 A 에 대한 두 개의 증명을 둘 수 없다면, 그 중복을 없애기 위한 수축을 쓸 수 없다.
고전 논리에서는 Γ ⊢ A 가 있을 때, 오른쪽에 ∨-도입-우(-Intro-R)를 사용해(합이 왼쪽 항 때문에 참인 경우) Γ ⊢ A ∨ B 를, 또 ∨-도입-우를 다른 쪽에 적용해(합이 오른쪽 항 때문에 참인 경우) Γ ⊢ C ∨ A 를 만들 수 있고, 이어서 수축을 사용해 둘 중 하나를 버려 Γ ⊢ A ∨ A 에서 Γ ⊢ A 로 갈 수 있다. 우리가 버리는 합 공식은 어느 쪽이든 상관없고, 각각은 서로 다른 이유(왼쪽 또는 오른쪽 항)로 “참”이다. 따라서 고전적으로는 A ∨ A 가 참이라는 사실만 알 뿐, 그 참이라는 증거 (왼쪽 때문인지 오른쪽 때문인지에 대한 정보)는 완전히 잊혀져 버린다.
Girard의 제안은 이렇다. 만약 오른쪽에 최대 하나의 식만 둔다는 제한의 목적이, 구성성을 깨뜨리는 상황에서 수축을 금지하는 데 있다면, 아예 제한을 풀고 수축 자체를 완전히 없애면 된다. 그러면 다시 멋진 대칭성이 돌아오고, 실제로 Girard는 자신이 새로 만든 논리를 지난 글에서 언급했던 한쪽만 있는(one-sided) 수열 스타일로 제시한다!
하지만 구성성 관점에서 새로운 문제가 생긴다. 약화(weakening)을 사용해 그냥 Γ ⊢ A 에서 Γ ⊢ A, B ∨ C 같은 걸 도입해 버릴 수 있다는 점이다. 이 경우는 당연히 어느 쪽이 참인지 알 수 없다. 심지어 그 합이 참일 필요도 없다! 그래서 Girard는 약화도 함께 금지한다. (이전에는 오른쪽 약화가 오른쪽이 비어 있을 때만 가능했으므로, 그때는 이미 왼쪽에 모순이 있는 상황이라 문제가 되지 않았다.) Girard의 말을 그대로 옮기면 이렇다. “직관주의 논리의 구성적 성질이 수열에서 특정 위치의 구조 규칙들을 버리는 데서 온다는 점을 인정하고 나면, 우리는 이 관찰의 결과를 직시할 준비가 된 것이다. 즉, 그 제한은 다른 위치들에도 일반화되어야 하며, 그 결과 약화와 수축은 사라진다(Once we have recognized that the constructive features of intuitionistic logic come from the dumping of structural rules on a specific place in the sequents, we are ready to face the consequences of this remark: the limitation should be generalized to the other rooms, i.e., weakening and contraction disappear)” (Girard 1987, p. 4).
이 최종 시스템, 즉 고전 논리에서 약화와 수축을 뺀 완전히 구성적인 논리가 바로 선형 논리(Linear Logic)다. 이제 가장 큰 단점은, 말 그대로 약화도 수축도 없다는 것이다. 식은 복제할 수도 버릴 수도 없어서, 모든 식을 정확히 한 번씩만 사용해야 한다. Girard는 이것에 대한 해법도 제시하는데, 나중에 설명하겠다.
이상한 결과 중 하나는, 선형 논리에서 참/타당성 개념이 “단조적(monotonic)”이지 않다는 점이다. 일반 논리에서는 증명을 진행하면서 사용할 수 있는 정보량이 늘어나기만 한다. 그러나 선형 논리에서는 이미 한 번 증명된 명제가, 그것을 “사용하고 나면” 다시 미증명 상태가 되며, 다시 쓰고 싶다면 새 증명이 필요하다.
이제 첫 두 규칙을 소개하자.
안타깝게도, 약화와 수축을 그냥 “없애기만” 해서는 충분하지 않다. 이 둘이 사라지면, 지난 글에서의 한쪽 수열을 기준으로 했을 때, 도입/제거 규칙들을 해석하는 방식이 여러 개 생긴다. 예를 들어 ∧-도입을 보자.
고전 논리에서의 규칙을 그대로 가져오면, 선형 논리에서는 이 규칙이 Γ 와 Δ 가 정확히 그 식들의 집합일 때만 Γ, Δ ⊢ A ∧ B 를 만들 수 있다는 뜻이 된다. 약화와 수축이 없어진 지금, 이 두 집합을 맞추기 위해 식을 집어넣거나 뺄 수 없으므로, 이는 매우 강한 요구다! 그래서 아예 다음과 같은 다른 규칙이 더 마음에 들 수도 있다. 고전 논리에서는 두 규칙이 서로 동치지만, 선형 논리에서는 전혀 그렇지 않다.
이 두 번째 규칙은 보다 직관적으로 느껴질 수 있는데, 결론의 다른 식들은 전혀 신경 쓰지 않는다는 정합적인 의미를 갖기 때문이다. 하지만 이 규칙도 나름의 제약이 있다. 이 규칙에서는 만약 Γ 와 Δ 가 동일하다면, 결론에서 모든 식이 두 번씩 나타나게 된다! 중복을 제거할 수 없으니 심각한 문제가 될 수 있다. 예를 들어, A ⊢ A 즉 항등 공리(Identity)조차 증명할 수 없다.
직관적으로는 다음과 같은 모양이 되는 것이다 (기호 없이 말로만 설명하자). 위에서부터 증명을 내려올 때, 맨 아래에는 A ⊢ A, A 같이 오른쪽에 A 가 남아 돌며, 이를 없앨 방법이 없다. 동치로 말하면, ⊢ A ⊸ A ⊗ A 는 증명할 수 있지만 (아래에서 기호를 소개한다), ⊢ A ⊸ A 는 증명할 수 없다.
선형 논리는 이 둘을 그냥 모두 채택한다! 즉, 기존의 ∧("and") 를 없애고, 대신 &("with")와 ⊗("tensor") 두 개의 연산자로 쪼갠다.
A & B 는 정리(theorem)이지만 A ⊗ B 는 아니다.A ⊗ ⊤ ⊢ A 같은 식으로 ⊗ 는 남는 식을 “소모”할 수 있기 때문에, A ⊗ B ⊢ A 는 정리가 아니지만, A ⊗ 1 ⊢ A 는 정리이다. (여기서 1 은 뒤에서 소개할 단위원 중 하나다.)직관적으로 A ⊗ B 는 “A 하나와 B 하나를 모두 가지고 있다”는 뜻이다. 둘 다 사용할 수 있고, 반드시 둘 다 써야 한다. 반면 A & B 는 “한 번만 쓸 수 있는 어떤 자원을 가지고 있는데, 그걸 A로 쓸 수도 있고 B로 쓸 수도 있다” 정도의 의미다. 하지만 ∨ 는 아니다. 왜냐하면 어느 쪽으로 쓸지를 내가 선택한다는 점에서, 대립하는 두 명제 중 어느 하나가 참임을 말하는 것이 아니라, “둘 중 하나로 사용할 수 있는” 자원을 말하는 것이기 때문이다.
그래서 다음처럼 우리가 기대하는 정리 A ⊗ (B & C) ⊢ (A ⊗ B) & (A ⊗ C) 는 성립하지만, A & (B ⊗ C) ⊢ (A & B) ⊗ (A & C) 는 성립하지 않는다.
같은 이야기를 ∨ 에도 적용해야 한다. 고전 논리와 직관주의 논리에서의 도입 규칙을 옮기는 방식이 여러 개 있기 때문이다. 먼저 직접적인 번역을 보자.
Γ ⊢ A 로부터 Γ ⊢ A ∨ B.Γ ⊢ B 로부터 Γ ⊢ A ∨ B.이건 분명히 유용한 형태의 ∨ 이다. 하지만 한쪽 수열에서는 콤마(,) 자체가 오른쪽에서는 합(∨)을 의미한다는 것을 기억하자. 따라서 다음과 같은 규칙도 유효해야 한다.
Γ ⊢ A, B.문제는, 이 둘이 같은 ∨ 인가 하는 것이다. 답은 아니다. 이유는, 다시 한 번 콤마 기반의 경우 두 명제가 자원 Γ 를 “나누어 쓰는(share)” 반면, 첫 번째 경우는 각 명제마다 Γ 를 하나씩 따로 준다는 차이가 있기 때문이다. 식들을 마음대로 “주무를” 수 없는 이 세계에서는 이 구분이 매우 중요하다.
그래서 선형 논리는 이번에도 둘 다 채택한다! 기존의 ∨("or") 를 없애고, 대신 ⊕("plus")와 ⅋("par") 두 개의 연산자로 분리한다. 그렇다, 이 연재의 이름이기도 한 바로 그 par 다!
A ⊕ B 는 정리이지만 A⅋B 는 아니다.A⅋B 는 정리이지만 A ⊕ B 는 아니다.각각은 우리가 ∨ 에 대해 가지고 있던 직관의 서로 다른 측면을 포착한다.
여기서 정말 흥미로운 점은, ⅋ 가 고전적 합에서 온다는 것이다. (한쪽 수열에서 콤마가 바로 그것이다.) 반면 ⊕ 는 직관주의 합에서 오는데, 항상 왼쪽 또는 오른쪽 중 하나를 명시적으로 선택해서 도입하고, 그 선택을 잊어버리지 않는다.
따라서 선형 논리의 아주 흥미로운 정리 중 하나가 바로 A⅋A⊥ 이다. 즉, 배중률 A ∨ ¬A 가 선형 논리에서는 다음과 같이 나타난다.
한쪽 수열에서의 Axiom 규칙을 떠올려 보자.
⊢ A, A⊥.즉, 배중률은 단순히 A⅋A⊥ 이고, 이건 매우 구성적으로 타당하다. 왜냐하면 선형 논리에서는, 직관주의 논리와 달리, 함의가 독립된 연산자가 아니라, (한쪽 수열 스타일로) 단지 정의로서 A ⊸ B := A⊥⅋B 로 주어지기 때문이다.
함의가 정의일 뿐 고유의 연산자가 아니라는 점을 존중하기 위해, 우리는 기존의 → 대신 다른 기호 ⊸("lollipop") 를 사용한다. 물론 이 함의는 직관주의 함의와 조금 다르게 동작한다. 왜냐하면 그 증명에서는 수축과 약화를 사용할 수 없기 때문이다. 이제부터는 이 새 기호를 사용하겠다.
par와 고전적 합에 대해서는 다음이자 마지막 글에서 훨씬 더 많이 이야기할 것이므로, 여기서는 짧게만 언급한다. 그러나 두 가지는 미리 짚어둘 가치가 있다.
첫째, par는 악명 높게 이해하기 어려운 연산자다. 실제로 기존의 어떤 논리에서도 이에 해당하는 것이 없었기 때문에, 선형 논리가 “발견한” 유일한 새로운 논리 연산자라고 할 수 있다.
둘째, 나도 par를 제대로 이해하고 나서, 그 어떤 논리 연산자보다도 압도적으로 가장 아름다운 연산자라고 느끼게 되었다. 그래서 사실상 par를 세상에 소개하고 싶다는 이유 하나로 이 길고 긴 연재를 쓰고 있다 :)
이제 남은 것은 선형 논리에서의 부정(¬) 번역이다. 그런데 놀랍게도, 선형 논리는 부정도 다른 것들을 이용해 정의해 버린다! 부정은 다음과 같이 재귀적으로 정의되는 함수다 (처음 두 규칙은 원자 명제에 대한 것이다).
(p)⊥ = p⊥ (원자 명제의 이름에 ⊥를 더하는 식으로 생각할 수 있다.)(p⊥)⊥ = p.(A ⊗ B)⊥ = A⊥⅋B⊥.(A⅋B)⊥ = A⊥ ⊗ B⊥.(A & B)⊥ = A⊥ ⊕ B⊥.(A ⊕ B)⊥ = A⊥ & B⊥.여기서 매우 중요하고 멋진 성질은, 부정이 “쌍대적(involutive)”이라는 점이다. 즉, 부정을 두 번 적용하면 원래로 돌아간다: (A⊥)⊥ = A. 그래서 선형 논리는 이중 부정 제거를 지원한다!
그럼 이제 끝인가? 연산자를 다 얻었으니 된 것 아닌가? 반은 맞고 반은 아니다. 참(true)과 거짓(false) 그 자체도 마찬가지로 두 종류로 나눠야 한다! 고전 논리의 ⊤ 는 ⊤("top") 과 1("one") 으로, ⊥ 는 ⊥("bottom") 과 0("zero") 로 각각 분해된다.
⊤ 와 1 에는 서로 다른 도입/제거 규칙이 있다.⊥ 와 0 도 마찬가지다.0 에는 도입 규칙이 없다.)이 규칙들이 수열 규칙들과 어떻게 상호작용하는지 직접 살펴보며, 이 기호들이 실제로 무엇을 하는지 파악해 보라. 힌트 하나만 주겠다. 이 네 기호가 “아무 기여도 하지 않는” 상황은 어떤 경우인가? 이 시스템을 잠깐 종이에 적어가며 생각해 보는 것이 정말로 가치 있다. 막힌다면, 어느 플랫폼이든 좋으니 주저 말고 연락을 주면, 최대한 자세히 도와 보겠다 :)
이제 부정 정의를 이 새로운 기호들까지 확장해야 한다.
⊤⊥ = 00⊥ = ⊤1⊥ = ⊥⊥⊥ = 1드디어 어느 정도 완전한 선형 논리 체계를 갖추게 되었다. 특히, 이를 MALL이라고 부른다. “곱-덧 선형 논리(multiplicative-additive linear logic)”의 약자다. 여기서 ⊗, ⅋, 1, ⊥ 기호들을 선형 논리의 “곱(fragment)”이라 하고(이 자체만으로도 MLL이라는 완전한 논리), &, ⊕, ⊤, 0 기호들을 “덧(fragment)”이라 한다(우변 콤마가 본질적으로 곱적이기 때문에, 단독으로는 완전한 시스템이라 보긴 어렵다).
곱 fragment는 대체로 고전적인 성격을 띠는데, 특히 합(⅋)과 함의(⊸)를 다루는 방식이 그렇다. 반면 덧 fragment는 좀 더 직관주의적인 느낌이 강하다. 이 점은 뒤에서 의미론을 잠깐 논할 때 조금 더 다루겠다.
하지만 그 전에 추가해야 할 것이 하나 더 있다. 직관주의 논리나 고전 논리만큼의 표현력을 얻으려면, 우리는 (조심스럽게) 약화와 수축을 어느 정도 다시 도입할 수 있어야 한다. 그게 가능하다면 진정한 의미의 “양쪽 세계의 최선”을 얻게 될 것이다.
Girard의 해법은 두 개의 새로운 연산자, 즉 “지수(exponentials)”인 !("of course A") 와 ?("why not A") 이다.
!A : 자원 A 를 원하는 만큼 쓸 수 있다는 의미.?A : A 를 요구(요청)하는 자원의 형태.(수열 !Γ 는 Γ 에 있는 모든 명제에 ! 를 붙인 집합을 뜻한다. 예: !A, !B, !C.)
우리는 여기서 원 저자의 한쪽 수열 제시를 따르고 있으므로, ! 쪽에 초점을 맞춘다. 하지만 오늘날 볼 수 있는 대부분의 선형 논리 소개는 “직관주의 선형 논리(ILL)”이다. 이는 양쪽 수열이지만 오른쪽에는 최대 하나의 명제만 둘 수 있고, 수축과 약화는 없으며, par ⅋, ⊥, 0 도 사용하지 않는다. 이 연산자들은 보통 오른쪽에 여러 명제가 있을 때만 자연스러우며, 그런 상황이 없다면 함의와 부정을 독립적인 기본 연산자로 취급하는 것이 더 간단하기 때문이다.
ILL 은 선형 논리에 비해 여러 단점이 있지만, 직관적으로 이해하기에는 훨씬 쉽다. 그 까다로운 par(또는 그에 상응하는, 오른쪽에 여러 명제를 둘 수 있게 해 주는 모든 것)가 없기 때문이다. 이런 이유로 대부분의 선형 논리 소개에서는 ! 에 치중한다. ? 와 ⅋ 를 제거하고 수열의 왼편에서 대부분의 일을 처리하기 때문이다. 왼쪽에 있는 명제들은 오른쪽 기준으로 부정된 상태이므로, 부정의 정의에 따라 왼쪽의 ?A 가 위에서 !A 가 하던 일을 대신 수행한다. 우리가 쓰는 한쪽 수열에는 왼쪽이 없으므로, 이 글에서는 ? 의 활동을 많이 보지 못할 것이다.
이제 시스템 전체는 LL(완전한 선형 논리) 또는 MAELL이라고 부른다. 여기서 MELL(MLL + 지수)은 MALL 과 마찬가지로 완전한 시스템이고, MELL에 덧 fragment를 더하든, MALL에 지수를 더하든 둘 다 LL에 도달한다. 그래서 LL = MAELL 이다. 또 ILL 과 구분하기 위해 “고전 선형 논리(classical linear logic, CLL)”라고 부르기도 한다.
MAELL이 직관주의나 고전 논리만큼 표현력이 풍부하다는 것은 (지수 ! 덕분에) 분명하다. 하지만 지수는 수축과 약화의 사용을 추적(track) 하는 방법을 제공한다는 점이 진짜 핵심이다. 일반적으로 A 로부터 !A 로 가는 규칙은 없기 때문에, 지수를 전혀 언급하지 않는 명제에 대한 정리는, 지수를 사용하지 않는 증명을 반드시 갖는다!
문제가 되는 배중률 버전은 ¬¬P ⊸ P 인데, LL 에는 지수가 있더라도 이 명제의 증명이 여전히 존재하지 않는다. 하지만 다음처럼 지수를 사용한 !¬¬P ⊸ P 는 증명할 수 있다.
¬¬P ⊢ P 형태의 논리를 사용하기 위해, !¬¬P 에 기존 이상의 힘을 부여한 뒤,!¬¬P 를 여러 번 사용하고,!¬¬P 를 ¬¬P 처럼 다루어, 결국 P 를 얻는다.이 증명의 한 줄로 등장하는 수열을 보면 ⊢ (?P ⊕ ¬P), (¬P ⊕ ?P) 처럼, 선형 논리에서는 (A ⊕ B) 형태의, 각각 다른 이유(왼쪽 항 또는 오른쪽 항)로 참인 “덧적 합(additive disjunction)”을 두 개 갖는 정리도 있는 셈이다. 다시 말해, par(⅋, 곱적 합)은 고전적 합의 일부 행동을 구성적으로 구현하는 방식이다.
위 증명의 중간 어딘가에서 수축 규칙이 이 두 개의 ⊕ 중 하나를 지워 버리는데, 결국 최종적으로 남은 ⊕ 에서 어떤 쪽이 참이었는지에 대한 증거를 잊어버리게 된다. 그러니 놀랄 것도 없이, 지수를 사용하는 정리들은 일반적으로 구성적이지 않을 수 있다.
그러나 다시 강조하자면, 지수를 한 번 붙이고 나면 그것을 없애는 일반적인 규칙은 없기 때문에, 지수를 전혀 사용하지 않는 명제에 대한 정리는 항상 지수를 사용하지 않는 증명을 가져야 하며, 따라서 완전히 구성적이다. 이는 고전 논리보다 훨씬 나은 보장을 준다. 고전 논리에서는 어떤 정리의 증명이 구성적인지 보통 알 수 없지만, 선형 논리에서 비구성적인 추론을 사용하는 증명은, 최종 결론에 지수 기호를 남김으로써 “나 비구성적이었음”을 스스로 드러내야 하기 때문이다.
(그래서 지수 도입 규칙 이름이 !-Intro 가 아니라 Dereliction(유기, 포기)인 것이다. 이 규칙을 사용한다는 것은 구성성을 포기하는 행위다. 이 규칙을 쓰지 않으려는 태도가 구성성의 “정신”이며, 이 규칙을 사용함으로써, 증명은 최종 정리에서 !가 보존되기 때문에 구성성에 대한 모든 주장을 잃게 된다.)
(하나의 아름다운 기술적 디테일: Cut 규칙이 지수 사용을 숨기는 데 쓰일 수 있을 것처럼 보일 수도 있다. Cut 는 어떤 명제든 잠재적으로 제거할 수 있기 때문이다. 하지만 선형 논리에 대한 재미있는 결과로, “Cut 제거 정리(cut elimination theorem)”가 있다. 즉, Cut 를 사용하는 어떤 증명이든, Cut 를 사용하지 않는 다른 증명을 갖는 정리만을 증명한다는 것이다. 다시 말해, LL 에서 Cut 는 전혀 사용하지 않아도 증명 가능한 정리들의 집합이 변하지 않는다.
Cut 제거는 많은 논리에서 매우 아름다운 결과인데, 증명에서 Cut 를 제거해 가는 알고리즘이, 어떤 함수형 언어의 프로그램 실행에 정확히 대응하기 때문이다! 또 그 언어가 튜링 완전하지 않고 반드시 종료함을 보여주기도 한다. 이 경우도 단순형 람다 계산(STLC)이 그러하듯, 동일한 이유 때문이다.)
선형 논리는 꽤 낯설게 느껴질 수 있다. 특히 “정확히 한 번만 사용하는” 명제라는 생각은 우리가 평소에 논리를 다루는 방식과 꽤 거리가 있어 보인다. 이 논리를 이해하는 데 도움이 되는 해석(semantics) 몇 가지를 소개하겠다.
첫 번째는 가장 유명한 “자원 해석(resource interpretation)”이다. 이는 ILL과 가장 밀접하게 연결되어 있어서 이 연재의 방향성과는 약간 거리가 있지만, 그래도 반드시 알아 둘 필요가 있다.
고전적인 예시는 자판기다. 우리가 돈 5단위를 가지고 있다고 하자(유한한 자원). 이 사실은 명제 M5 같은 걸로 표현할 수 있다. 어떤 음료 D 는 2단위를 소모한다고 하자. 이는 !M2 ⊸ D 라는 명제로 나타낼 수 있다 (! 는 자판기에서 원하면 여러 번 살 수 있다는 뜻을 반영한다). 보통의 논리에서는 첫 번째 명제 M5 는 M2 ∧ M2 ∧ M1 과 동치이고, 두 번째 명제는 M2 → D 와 동치라고 보면, M5 와 M2 → D 로부터 D ∧ D ∧ D ∧ … 를 얼마든지 도출할 수 있고, 이건 D 를 무한히 살 수 있다는 말과 별 차이 없다.
하지만 현실 세계에서 이건 맞지 않는다. 우리가 실제로 살 수 있는 최대 개수는 두 잔이다(4단위 소모). 선형 논리는 이를 정확히 반영한다. M5 에서 M3 으로 가고, 다시 거기서 D 를 하나 사면 M1 이 남으며, 이 시점에서 M2 ⊸ D 를 더 이상 쓸 수 없으므로 음료는 최대 두 잔까지만 살 수 있다. 직관주의와 고전 논리는 “단조적”이어서 증명 도중 정보(명제)는 늘어나기만 하고 줄지 않으므로, “한때는 돈이 충분했지만 나중에는 더 이상 충분하지 않다”라는 사실을 표현할 수 없다.
자원 해석은 특히 ILL과 친하며, 그래서 Rust 언어의 메모리 모델에도 사용된다! 빌림 검사기(borrow checker)의 규칙은 문법 설탕(syntax sugar)과 선형 논리의 규칙들이 결합된 결과다. 이건 꽤 흥미로운 사실이다.
하지만 이 연재에서는 좀 더 매운(spicy) 것들을 사랑한다. 도대체 par(⅋) 는 뭐란 말인가? 물론 다음 글(전부 par 에만 집중할 글)에서 프로그램 제어 흐름을 기반으로 한 의미론을 자세히 다룰 예정이다. 그 전에 여기서는 선형 논리에 대한 의미론 세 가지를 아주 짧게만 소개하고 마치겠다.
첫 번째는 범주론에서의 -자율 범주(-autonomous category)다. 이름부터 이미 깊은 범주론 토끼굴이라, 이 글의 전제 지식을 범주론으로 오염시키고 싶지는 않아 자세한 설명은 생략한다. 다만, (아마도) 가장 널리 쓰이는 직관주의 논리와 람다 계산의 범주론적 기초가, 수축과 약화를 암묵적으로 두는 대신, 지수 ! 를 가진 직관주의 선형 논리라는 점은 언급해 둘 만하다. 또 모노이달 범주(monoidal category)(여기에는 *-자율 범주도 포함된다)는 수축과 약화가 없는 상황을 다루는 데 자주 사용된다.
조금 덜 무서운 의미론으로는 게임 이론적 의미론(game semantics)이 있다. 게임 의미론은 정말 아름다운 분야로, 언젠가 따로 글을 쓰고 싶다. 게임 이론에 익숙하지 않은 사람에게는 겁을 줄 수도 있지만, 실제 개념은 매우 단순하다. 여기서는 “Conway 게임”을 사용할 것이고, 규칙을 간단히 설명하겠다.
게임은 점(“position”)들의 모음과, 그 사이를 잇는 화살표(“move”)들로 이루어진 그래프다. 빨간 플레이어와 파란 플레이어가 있고, 각 화살표는 둘 중 하나의 색을 가진다. 게임은 어떤 “루트 위치”에서 시작한다. 빨간 플레이어는 현재 점에서 나가는 빨간 화살표 하나를 골라 그 화살표가 가리키는 점으로 게임을 진행시키고, 파란 플레이어는 그 점에서 나가는 파란 화살표를 하나 골라 또 다른 점으로 넘긴다. 이런 식으로 게임은 그래프 위를 돌아다닌다.
플레이어는 자기 차례에, 현재 점에서 자신의 색의 화살표가 하나도 없다면 진다. 너무나 간단하다.
Conway 게임은 여러 놀라운 곳에서 등장하는데, 이유는 “대화(dialogue)”—즉, “지금까지 대화가 어떻게 진행되었는가(현재 위치와 거기서 나가는 화살표들)”에 따라 양쪽이 할 수 있는 선택지가 달라지는 상호작용—를 멋지게 모델링해 주기 때문이다.
이제 “전략(strategy)”은 상대가 할 수 있는 모든 행동에 대해, 매번 어떻게 반응할지를 결정하는 결정적 계획이다. Conway 게임에서 패배 조건은 “더 이상 둘 수 있는 수가 없는 것”이기 때문에, 항상 이기게 해 주는 전략(“항상 상대가 무엇을 하든 이기는 전략”)은, 결코 자신을 수가 없는 위치로 몰아넣지 않는 전략이다. 즉, 상대의 가능한 모든 선택에 대한 응답을 전부 정의해 주므로, 프로그램 플로차트와 비슷하게 생각할 수 있다.
선형 논리와의 연결은, Conway 게임들을 다른, 관련된 Conway 게임들로 변환하는 연산자들을 정의할 수 있다는 데 있다. 이 연산자들은 LL 연산자들과 아주 비슷하게 생겼다. 가장 유명하고 철학적으로 통찰력 있는 예는, 부정이 단순히 모든 화살표의 색을 뒤바꾸는 것이라는 점이다.
이항 연산자는 서로 다른 방식으로 “두 게임을 동시에 플레이하는” 것으로 정의된다. 예를 들어 A ⊗ B 에서는 두 게임 모두에서 이겨야 하고, A⅋B 에서는 둘 중 하나에서만 이기면 된다. 나머지 두 연산자 &, ⊕ 는 부정이 색 바꾸기라는 사실을 이용해 유도할 수 있다. 이 글에서는 형식적인 정의를 하지는 않겠지만, 이 논문을 꽤 인상 깊게 읽었다. 이렇게 해서 A⊥⅋B 같은 Conway 게임이 생기고, LL 명제 A⊥⅋B 의 증명은 이 Conway 게임에 대한 승리 전략이라고 볼 수 있다.
게임 의미론은 “극성(polarity)”이라는 아름다운 아이디어를 준다. 증명은 세계(또는 “상대방(Opponent)”)이 던지는 모든 반례(공격)에 성공적으로 방어하는 전략이다. 여기에서 극성은 한 수의 “색”이다. 즉, 다음 수를 선택할 권한이 증명(Proponent)에 있는지, 아니면 증명을 반박하려는 적대적 Opponent 에 있는지의 문제다. 철학적 통찰은, 어떤 명제를 부정한다는 것은 Opponent 가 그 명제를 입증하려 하고, 우리의 증명이 그것을 반박하려 한다는 관점에서 이해할 수 있다는 점이다.
이 주제는 다음 글에서 더 자세히 다룰 예정이지만, 논리에 대한 철학으로서 개인적으로 매우 좋아하는 아이디어다. 더 아름다운 철학 이야기는 스탠퍼드 철학 백과사전의 이 항목을 참고하라.
게임 의미론과 그 철학은 이 글의 마지막이자, 아마 가장 악명 높은 LL 의미론인 “병렬성(parallelism)”을 이해하는 데도 기반을 제공한다.
이 설정에서는, 고도로 병렬적인 함수형 프로그래밍 언어의 프로그램들이 LL 명제의 증명 역할을 하고, 명제의 형태는 곧 그 프로그램들의 타입에 해당한다. 예를 들어 A⅋B 는 타입 A 를 가진 표현과 타입 B 를 가진 표현 두 개가 병렬로 실행되는 프로세스의 타입이다. 그래서 이름이 “par”다!
이 병렬 프로세스들은, 앞서 소개한 게임 의미론과 비슷한 방식으로 서로 상호작용한다. 한 프로세스에서 다른 프로세스로 값이 전달될 때, 보낸 쪽에서의 타입과 받은 쪽에서의 타입은 서로 부정 관계에 있다. 예를 들어, 한 프로세스가 타입 A 의 값을 요청하는 경우, 그 값은 당연히 그 프로세스 안에서는 타입 A 로 쓰인다. 하지만 외부 세계에서 보면 이 요청은 A 가 아니라 A⊥ 타입을 가진다. 실제 값이 아니라, 그런 값을 “집어넣을 수 있는 자리”이기 때문이다.
프로그램들은 Cut 를 사용해 통신한다. 요청 A⊥ 와 실제 값 A 를 갖고 있는 프로세스를 Cut 로 “붙여” A⊥⅋A 를 만들어, A 를 요청하던 코드가 실제 값으로 실행을 계속하게 만든다. Cut 규칙을 Γ ⊢ A 와 A⊥, Δ ⊢ 를 Γ, Δ ⊢ 로 합치는 것으로 보면, 이를 A⊥⅋A 로 보는 것도 가능하다. 그래서 Cut 는 modus ponens, 또는 함수 적용(function application)처럼 이해할 수 있다. 이 라인이 궁금하다면 이 논문을 정말 강력히 추천한다.
이렇게 선형 논리에 대한 초단기(crash course)를 마쳤다! 다음 글에서는 마지막으로, 곱적 합(par, ⅋) 의 의미론을 훨씬 더 깊게 파고들 것이다.
선형 논리의 아이디어와 연산자들을 빠르게 참고할 수 있는 위키 페이지를 여기에 만들어 두었다.
© 2025 Ryan Brewer.